|
|
- {-# LANGUAGE PatternSynonyms #-}
- {-# LANGUAGE DeriveDataTypeable #-}
- module Syntax where
-
- import qualified Data.Map.Strict as Map
- import qualified Data.Sequence as Seq
- import qualified Data.Set as Set
- import qualified Data.Text as T
- import Data.Map.Strict (Map)
- import Data.Sequence (Seq)
- import Data.Function (on)
- import Data.IORef (IORef)
- import Data.Text (Text)
- import Data.Set (Set)
- import Data.Data
-
- import Presyntax.Presyntax (Plicity(..))
-
- data WiredIn
- = WiType
- | WiPretype
- | WiInterval
- | WiI0
- | WiI1
- | WiIAnd
- | WiIOr
- | WiINot
- | WiPathP
-
- | WiIsOne -- Proposition associated with an element of the interval
- | WiItIsOne -- 1 = 1
- | WiIsOne1 -- i j -> [i] -> [ior i j]
- | WiIsOne2 -- i j -> [j] -> [ior i j]
-
- | WiPartial -- (φ : I) -> Type -> Typeω
- | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
-
- | WiSub -- (A : Type) (φ : I) -> Partial φ A -> Typeω
- | WiInS -- {A : Type} {φ : I} (u : A) -> Sub A φ (λ x -> u)
- | WiOutS -- {A : Type} {φ : I} {u : Partial φ A} -> Sub A φ u -> A
-
- | WiComp -- {A : I -> Type} {phi : I}
- -- -> ((i : I) -> Partial phi (A i)
- -- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
-
- | WiGlue -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
- | WiGlueElem -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
- | WiUnglue -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
-
- | WiBool
- | WiTrue
- | WiFalse
- | WiIf
- deriving (Eq, Show, Ord)
-
- data Term
- = Ref Name
- | App Plicity Term Term
- | Lam Plicity Name Term
- | Pi Plicity Name Term Term
- | Let [(Name, Term, Term)] Term
- | Meta MV
- | Type
- | Typeω
-
- | Sigma Name Term Term
- | Pair Term Term
- | Proj1 Term
- | Proj2 Term
-
- | I
- | I0 | I1
- | IAnd Term Term
- | IOr Term Term
- | INot Term
-
- | PathP Term Term Term
- -- ^ PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
- | IElim Term Term Term Term Term
- -- ^ IElim : {A : I -> Type} {x : A i0} {y : A i1} (p : PathP A x y) (i : I) -> A i
- | PathIntro Term Term Term Term
- -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
- -- ~~~~~~~~~ not printed at all
-
- | IsOne Term
- | IsOne1 Term
- | IsOne2 Term
- | ItIsOne
-
- | Partial Term Term
- | PartialP Term Term
-
- | System (Map Term Term)
-
- | Sub Term Term Term
- | Inc Term Term Term
- | Ouc Term Term Term Term
-
- | Comp Term Term Term Term
-
- | GlueTy Term Term Term Term
- | Glue Term Term Term Term Term Term
- | Unglue Term Term Term Term Term
-
- -- ugly. TODO: proper inductive types
- | Bool | Tt | Ff | If Term Term Term Term
- deriving (Eq, Show, Ord, Data)
-
- data MV =
- MV { mvName :: Text
- , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
- }
-
- instance Eq MV where
- (==) = (==) `on` mvName
- instance Ord MV where
- (<=) = (<=) `on` mvName
- instance Show MV where
- show = ('?':) . T.unpack . mvName
-
- instance Data MV where
- toConstr _ = error "toConstr"
- gunfold _ _ = error "gunfold"
- dataTypeOf _ = mkNoRepType "MV"
-
-
- data Name
- = Bound {getNameText :: Text, getNameNum :: !Int}
- | Defined {getNameText :: Text, getNameNum :: !Int}
- deriving (Eq, Show, Ord, Data)
-
- type NFType = Value
- type NFEndp = Value
- type NFLine = Value
- type NFSort = Value
- type NFPartial = Value
-
- data Value
- = VNe Head (Seq Projection)
- | VLam Plicity Closure
- | VPi Plicity Value Closure
- | VSigma Value Closure
- | VPair Value Value
-
- | VType | VTypeω
-
- | VI
- | VI0 | VI1
- | VIAnd NFEndp NFEndp
- | VIOr NFEndp NFEndp
- | VINot NFEndp
-
- | VPath NFLine Value Value
- | VLine NFLine Value Value Value
-
- | VIsOne NFEndp
- | VItIsOne
- | VIsOne1 NFEndp
- | VIsOne2 NFEndp
-
- | VPartial NFEndp Value
- | VPartialP NFEndp Value
- | VSystem (Map Value Value)
-
- | VSub NFSort NFEndp Value
- | VInc NFSort NFEndp Value
-
- | VComp NFSort NFEndp Value Value
-
- | VGlueTy NFSort NFEndp NFPartial NFPartial
- | VGlue NFSort NFEndp NFPartial NFPartial NFPartial Value
- | VUnglue NFSort NFEndp NFPartial NFPartial Value
-
- | VBool
- | VTt
- | VFf
- | VIf Value Value Value Value
- deriving (Eq, Show, Ord)
-
- pattern VVar :: Name -> Value
- pattern VVar x = VNe (HVar x) Seq.Empty
-
- quoteWith :: Set Name -> Value -> Term
- quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
- goHead (HVar v) = Ref v
- goHead (HMeta m) = Meta m
-
- goSpine t (PApp p v) = App p t (quoteWith names v)
- goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i)
- goSpine t PProj1 = Proj1 t
- goSpine t PProj2 = Proj2 t
- goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t
-
- quoteWith names (VLam p (Closure n k)) =
- let n' = refresh Nothing names n
- in Lam p n' (quoteWith (Set.insert n' names) (k (VVar n')))
-
- quoteWith names (VPi p d (Closure n k)) =
- let n' = refresh (Just d) names n
- in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
-
- quoteWith names (VSigma d (Closure n k)) =
- let n' = refresh (Just d) names n
- in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
-
- quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
- quoteWith _ VType = Type
- quoteWith _ VTypeω = Typeω
-
- quoteWith _ VI = I
- quoteWith _ VI0 = I0
- quoteWith _ VI1 = I1
- quoteWith names (VIAnd x y) = IAnd (quoteWith names x) (quoteWith names y)
- quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
- quoteWith names (VINot x) = INot (quoteWith names x)
-
- quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
- quoteWith names (VLine p x y f) = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
-
- quoteWith names (VIsOne v) = IsOne (quoteWith names v)
- quoteWith names (VIsOne1 v) = IsOne1 (quoteWith names v)
- quoteWith names (VIsOne2 v) = IsOne2 (quoteWith names v)
- quoteWith _ VItIsOne = ItIsOne
-
- quoteWith names (VPartial x y) = Partial (quoteWith names x) (quoteWith names y)
- quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
- quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))
- quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quoteWith names c)
- quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c)
- quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
-
- quoteWith names (VGlueTy a phi t e) = GlueTy (quoteWith names a) (quoteWith names phi) (quoteWith names t) (quoteWith names e)
- quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x)
- quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x)
-
- quoteWith _ames VBool = Bool
- quoteWith _ames VTt = Tt
- quoteWith _ames VFf = Ff
- quoteWith names (VIf a b c d) = If (quoteWith names a) (quoteWith names b) (quoteWith names c) (quoteWith names d)
-
- refresh :: Maybe Value -> Set Name -> Name -> Name
- refresh (Just VI) n _ = refresh Nothing n (Bound (T.pack "phi") 0)
- refresh x s n
- | T.singleton '_' == getNameText n = n
- | n `Set.notMember` s = n
- | otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0)
-
- quote :: Value -> Term
- quote = quoteWith mempty
-
- data Closure
- = Closure
- { clArgName :: Name
- , clCont :: Value -> Value
- }
-
- instance Show Closure where
- show (Closure n c) = "Closure \\" ++ show n ++ " -> " ++ show (c (VVar n))
-
- instance Eq Closure where
- Closure _ k == Closure _ k' =
- k (VVar (Bound (T.pack "_") 0)) == k' (VVar (Bound (T.pack "_") 0))
-
- instance Ord Closure where
- Closure _ k <= Closure _ k' =
- k (VVar (Bound (T.pack "_") 0)) <= k' (VVar (Bound (T.pack "_") 0))
-
- data Head
- = HVar Name
- | HMeta MV
- deriving (Eq, Show, Ord)
-
- data Projection
- = PApp Plicity Value
- | PIElim Value Value Value NFEndp
- | PProj1
- | PProj2
- | POuc NFSort NFEndp Value
- deriving (Eq, Show, Ord)
|