-- Labelled sum: c (x1 : A1) .. (xn : An)
type LblSum = [(Binder,Tele)]
+-- Declarations: x : A = e
type Decl = (Binder,(Ter,Ter))
-
--- Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en
type Decls = [Decl]
declBinders :: Decls -> [Binder]
| Path Name Ter
| AppFormula Ter Formula
-- Kan Composition
- | Comp Name Ter Ter (System Ter)
+ | Comp Ter Ter (System Ter)
+ | Trans Ter Ter
deriving Eq
-- For an expression t, returns (u,ts) where u is no application and t = u ts
-- Id values
| VIdP Val Val Val
| VPath Name Val
- | VComp Name Val Val (System Val)
+ | VComp Val Val (System Val)
+ | VTrans Val Val
-- Neutral values:
| VVar String Val
data Env = Empty
| Pair Env (Binder,Val)
- | PDef Decls Env
+ | Def Decls Env
+ | Sub Env (Name,Formula)
deriving Eq
pairs :: Env -> [(Binder,Val)] -> Env
lookupIdent :: Ident -> [(Binder,a)] -> Maybe a
lookupIdent x defs = listToMaybe [ t | ((y,l),t) <- defs, x == y ]
-mapEnv :: (Val -> Val) -> Env -> Env
-mapEnv _ Empty = Empty
-mapEnv f (Pair e (x,v)) = Pair (mapEnv f e) (x,f v)
-mapEnv f (PDef ts e) = PDef ts (mapEnv f e)
+mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
+mapEnv f g e = case e of
+ Empty -> Empty
+ Pair e (x,v) -> Pair (mapEnv f g e) (x,f v)
+ Def ts e -> Def ts (mapEnv f g e)
+ Sub e (i,phi) -> Sub (mapEnv f g e) (i,g phi)
valOfEnv :: Env -> [Val]
valOfEnv Empty = []
valOfEnv (Pair env (_,v)) = v : valOfEnv env
-valOfEnv (PDef _ env) = valOfEnv env
+valOfEnv (Def _ env) = valOfEnv env
+valOfEnv (Sub env _) = valOfEnv env
+
+formulaOfEnv :: Env -> [Formula]
+formulaOfEnv e = case e of
+ Empty -> []
+ Pair rho _ -> formulaOfEnv rho
+ Def _ rho -> formulaOfEnv rho
+ Sub rho (_,phi) -> phi : formulaOfEnv rho
+
+domainEnv :: Env -> [Name]
+domainEnv rho = case rho of
+ Empty -> []
+ Pair e (x,v) -> domainEnv e
+ Def ts e -> domainEnv e
+ Sub e (i,_) -> i : domainEnv e
--------------------------------------------------------------------------------
-- | Pretty printing
instance Show Env where
show = render . showEnv
-showEnv :: Env -> Doc
+showEnv, showEnv1 :: Env -> Doc
showEnv e = case e of
- Empty -> PP.empty
- PDef _ env -> showEnv env
- Pair env (x,u) -> parens (showEnv1 env <> showVal u)
- where
- showEnv1 (Pair env (x,u)) = showEnv1 env <> showVal u <> text ", "
- showEnv1 e = showEnv e
+ Empty -> PP.empty
+ Def _ env -> showEnv env
+ Pair env (x,u) -> parens (showEnv1 env <> showVal u)
+ Sub env (i,phi) -> parens (showEnv1 env <> text (show phi))
+showEnv1 (Pair env (x,u)) = showEnv1 env <> showVal u <> text ", "
+showEnv1 e = showEnv e
instance Show Loc where
show = render . showLoc
IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2]
Path i e -> char '<' <> text (show i) <> char '>' <+> showTer e
AppFormula e phi -> showTer1 e <> char '@' <> text (show phi)
- Comp i e0 e1 es -> text "comp" <+> text (show i) <+> showTers [e0,e1] <+>
- text (showSystem es)
+ Comp e0 e1 es -> text "comp" <+> showTers [e0,e1] <+> text (showSystem es)
+ Trans e0 e1 -> text "trans" <+> showTers [e0,e1]
showTers :: [Ter] -> Doc
showTers = hsep . map showTer1
VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2]
VPath i v -> char '<' <> text (show i) <> char '>' <+> showVal v
VAppFormula v phi -> showVal1 v <> char '@' <> text (show phi)
- VComp i v0 v1 vs -> text "comp" <+> text (show i) <+> showVals [v0,v1] <+>
- text (showSystem vs)
+ VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
+ VTrans v0 v1 -> text "trans" <+> showVals [v0,v1]
showVal1 v = case v of
VU -> char 'U'
VCon c [] -> text c
| k == j = i
| otherwise = k
-
-- | Directions
data Dir = Zero | One
deriving (Eq,Ord)
swapFace :: Face -> (Name,Name) -> Face
swapFace alpha ij = Map.mapKeys (`swapName` ij) alpha
--- i,j,k,l :: Name
--- i = Name 0
--- j = Name 1
--- k = Name 2
--- l = Name 3
-
--- f1,f2 :: Face
--- f1 = Map.fromList [(i,0),(j,1),(k,0)]
--- f2 = Map.fromList [(i,0),(j,1),(l,1)]
-
-- Check if two faces are compatible
compatible :: Face -> Face -> Bool
compatible xs ys = and (Map.elems (Map.intersectionWith (==) xs ys))
meets :: [Face] -> [Face] -> [Face]
meets xs ys = nub [ meet x y | x <- xs, y <- ys, compatible x y ]
--- instance Ord Face where
-
leq :: Face -> Face -> Bool
alpha `leq` beta = meetMaybe alpha beta == Just alpha
-- leqW :: Face -> Face -> Face
-- leqW = undefined
--- data Faces = Faces (Set Face)
-
--- instance Nominal Faces where
--- support (Faces f) =
--- act (Faces f) (i, phi) = Faces f
-
-- | Formulas
data Formula = Dir Dir
| Atom Name
orFormula phi (Dir Zero) = phi
orFormula phi psi = phi :\/: psi
-evalFormula :: Formula -> Face -> Formula
-evalFormula phi alpha =
- Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha
+-- evalFormula :: Formula -> Face -> Formula
+-- evalFormula phi alpha =
+-- Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha
-- (Dir b) alpha = Dir b
-- evalFormula (Atom i) alpha = case Map.lookup i alpha of
invFormula :: Formula -> Dir -> [Face]
invFormula (Dir b') b = [ eps | b == b' ]
invFormula (Atom i) b = [ Map.singleton i b ]
-invFormula (NegAtom i) b = [ Map.singleton i (- b) ]
+invFormula (NegAtom i) b = [ Map.singleton i (- b) ]
invFormula (phi :/\: psi) Zero = invFormula phi 0 `union` invFormula psi 0
-invFormula (phi :/\: psi) One =
- meets (invFormula phi 1) (invFormula psi 1)
+invFormula (phi :/\: psi) One = meets (invFormula phi 1) (invFormula psi 1)
invFormula (phi :\/: psi) b = invFormula (negFormula phi :/\: negFormula psi) (- b)
--- primeImplicants :: Formula -> Dir -> System ()
--- primeImplicants phi Zero = primeImplicants (NegAtom phi) One
--- primeImplicants phi One = undefined
-
propInvFormulaIncomp :: Formula -> Dir -> Bool
propInvFormulaIncomp phi b = incomparables (invFormula phi b)
-prop_invFormula :: Formula -> Dir -> Bool
-prop_invFormula phi b =
- all (\alpha -> phi `evalFormula` alpha == Dir b) (invFormula phi b)
+-- prop_invFormula :: Formula -> Dir -> Bool
+-- prop_invFormula phi b =
+-- all (\alpha -> phi `evalFormula` alpha == Dir b) (invFormula phi b)
testInvFormula :: [Face]
testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1
class Nominal a where
support :: a -> [Name]
--- act u (i,phi) should have u # (phi - i) ??
act :: a -> (Name,Formula) -> a
-
- swap :: a -> (Name,Name) -> a
- -- swap u (i,j) =
- -- where k = fresh (u,i,j)
+ swap :: a -> (Name,Name) -> a
fresh :: Nominal a => a -> Name
fresh = gensym . support
| (alpha,u) <- Map.toList ts ]
insertSystem :: Face -> a -> System a -> System a
-insertSystem alpha v ts =
- case find (comparable alpha) (Map.keys ts) of
- Just beta | alpha `leq` beta -> ts
- | otherwise -> Map.insert alpha v (Map.delete beta ts)
- Nothing -> Map.insert alpha v ts
+insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of
+ Just beta | alpha `leq` beta -> ts
+ | otherwise -> Map.insert alpha v (Map.delete beta ts)
+ Nothing -> Map.insert alpha v ts
insertsSystem :: [(Face, a)] -> System a -> System a
insertsSystem faces us =
mkSystem :: [(Face, a)] -> System a
mkSystem = flip insertsSystem Map.empty
-unionSystem :: System a -> System a -> System a
+unionSystem :: System a -> System a -> System a
unionSystem us vs = insertsSystem (Map.assocs us) vs
-- could something like that work??
transposeSystemAndList tss (u:us) =
(Map.map head tss,u):transposeSystemAndList (Map.map tail tss) us
--- transposeSystem :: System [a] -> [System a]
--- transposeSystem ts =
--- Map.map (\as -> head a) ts : transposeSystem (Map.map (\as -> tail as) ts)
-
-- Quickcheck this:
-- (i = phi) * beta = (beta - i) * (i = phi beta)
rename :: Nominal a => a -> (Name, Name) -> a
rename a (i, j) = a `act` (i, Atom j)
-connect :: Nominal a => a -> (Name, Name) -> a
-connect a (i, j) = a `act` (i, Atom i :/\: Atom j)
+conj, disj :: Nominal a => a -> (Name, Name) -> a
+conj a (i, j) = a `act` (i, Atom i :/\: Atom j)
+disj a (i, j) = a `act` (i, Atom i :\/: Atom j)
leqSystem :: Face -> System a -> Bool
alpha `leqSystem` us =
error $ "proj: eps not in " ++ show usalpha ++ "\nwhich is the "
++ show alpha ++ "\nface of " ++ show us
where usalpha = us `face` alpha
-
--- actSystemCom :: Formula -> Name -> Formula -> Bool
--- actSystemCom psi i phi = border phi
import Data.List
import Data.Maybe (fromMaybe)
+import Data.Map (Map,(!))
+import qualified Data.Map as Map
+-- import Data.Set (Set)
+-- import qualified Data.Set as Set
import Connections
import CTT
look :: String -> Env -> Val
look x (Pair rho ((y,_),u)) | x == y = u
| otherwise = look x rho
-look x r@(PDef es r1) = case lookupIdent x es of
+look x r@(Def rho r1) = case lookupIdent x rho of
Just (_,t) -> eval r t
- Nothing -> look x r1
+ Nothing -> look x r1
+look x (Sub rho _) = look x rho
lookType :: String -> Env -> Val
lookType x (Pair rho ((y,_),VVar _ a)) | x == y = a
| otherwise = lookType x rho
-lookType x r@(PDef es r1) = case lookupIdent x es of
+lookType x r@(Def rho r1) = case lookupIdent x rho of
Just (a,_) -> eval r a
Nothing -> lookType x r1
+lookType x (Sub rho _) = lookType x rho
+lookName :: Name -> Env -> Formula
+lookName i (Pair rho _) = lookName i rho
+lookName i (Def _ rho) = lookName i rho
+lookName i (Sub rho (j,phi)) | i == j = phi
+ | otherwise = lookName i rho
+
+-----------------------------------------------------------------------
+-- Nominal instances
+
+instance Nominal Env where
+ support = support . formulaOfEnv
+ act e iphi = mapEnv (`act` iphi) (`act` iphi) e
+ swap e ij = mapEnv (`swap` ij) (`swap` ij) e
+
+instance Nominal Val where
+ support VU = []
+ support (Ter _ e) = support e
+ support (VPi v1 v2) = support [v1,v2]
+ support (VComp a u ts) = support (a,u,ts)
+ support (VIdP a v0 v1) = support [a,v0,v1]
+ support (VPath i v) = i `delete` support v
+ support (VSigma u v) = support (u,v)
+ support (VSPair u v) = support (u,v)
+ support (VFst u) = support u
+ support (VSnd u) = support u
+ support (VCon _ vs) = support vs
+ support (VVar _ v) = support v
+ support (VApp u v) = support (u, v)
+ support (VAppFormula u phi) = support (u, phi)
+ support (VSplit u v) = support (u, v)
+
+ act u (i, phi) =
+ let acti :: Nominal a => a -> a
+ acti u = act u (i, phi)
+ sphi = support phi
+ in case u of
+ VU -> VU
+ Ter t e -> Ter t (acti e)
+ VPi a f -> VPi (acti a) (acti f)
+ VComp a v ts -> comp (acti a) (acti v) (acti ts)
+ VIdP a u v -> VIdP (acti a) (acti u) (acti v)
+ VPath j v | j `notElem` sphi -> VPath j (acti v)
+ | otherwise -> VPath k (v `swap` (j,k))
+ where k = fresh (v, Atom i, phi)
+ VSigma a f -> VSigma (acti a) (acti f)
+ VSPair u v -> VSPair (acti u) (acti v)
+ VFst u -> VFst (acti u)
+ VSnd u -> VSnd (acti u)
+ VCon c vs -> VCon c (acti vs)
+ VVar x v -> VVar x (acti v)
+ VAppFormula u psi -> acti u @@ acti psi
+ VApp u v -> app (acti u) (acti v)
+ VSplit u v -> app (acti u) (acti v)
+
+ -- This increases efficiency as it won't trigger computation.
+ swap u ij@ (i,j) =
+ let sw :: Nominal a => a -> a
+ sw u = swap u ij
+ in case u of
+ VU -> VU
+ Ter t e -> Ter t (sw e)
+ VPi a f -> VPi (sw a) (sw f)
+ VComp a v ts -> VComp (sw a) (sw v) (sw ts)
+ VIdP a u v -> VIdP (sw a) (sw u) (sw v)
+ VPath k v -> VPath (swapName k ij) (sw v)
+ VSigma a f -> VSigma (sw a) (sw f)
+ VSPair u v -> VSPair (sw u) (sw v)
+ VFst u -> VFst (sw u)
+ VSnd u -> VSnd (sw u)
+ VCon c vs -> VCon c (sw vs)
+ VVar x v -> VVar x (sw v)
+ VAppFormula u psi -> VAppFormula (sw u) (sw psi)
+ VApp u v -> VApp (sw u) (sw v)
+ VSplit u v -> VSplit (sw u) (sw v)
+
+-----------------------------------------------------------------------
+-- The evaluator
+
eval :: Env -> Ter -> Val
eval rho v = case v of
U -> VU
SPair a b -> VSPair (eval rho a) (eval rho b)
Fst a -> fstVal (eval rho a)
Snd a -> sndVal (eval rho a)
- Where t decls -> eval (PDef decls rho) t
+ Where t decls -> eval (Def decls rho) t
Con name ts -> VCon name (map (eval rho) ts)
Split l t brcs -> Ter (Split l t brcs) rho
Sum pr lbls -> Ter (Sum pr lbls) rho
Undef l -> error $ "eval: undefined at " ++ show l
IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1)
- Path i t -> Ter (Path i t) rho
- -- let j = fresh (t,rho)
- -- in VPath j (eval rho (t `swap` (i,j)))
+ Path i t ->
+ let j = fresh rho
+ in VPath j (eval (Sub rho (i,Atom j)) t)
+ Trans u v -> case eval rho u of
+ VPath i u0 -> trans i u0 (eval rho v)
+ u0 -> VTrans u0 (eval rho v)
+ AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi)
+-- Comp
+evalFormula :: Env -> Formula -> Formula
+evalFormula rho phi = case phi of
+ Atom i -> lookName i rho
+ NegAtom i -> negFormula (lookName i rho)
+ phi1 :/\: phi2 -> evalFormula rho phi1 `andFormula` evalFormula rho phi2
+ phi1 :\/: phi2 -> evalFormula rho phi1 `orFormula` evalFormula rho phi2
+ _ -> phi
evals :: Env -> [(Binder,Ter)] -> [(Binder,Val)]
evals env bts = [ (b,eval env t) | (b,t) <- bts ]
sndVal (VSPair a b) = b
sndVal u | isNeutral u = VSnd u
+(@@) :: ToFormula a => Val -> a -> Val
+(VPath i u) @@ phi = u `act` (i, toFormula phi)
+-- (KanUElem _ u) @@ phi = u @@ phi
+v @@ phi = VAppFormula v (toFormula phi)
+
+-----------------------------------------------------------
+-- Transport
+
+trans :: Name -> Val -> Val -> Val
+trans i v0 v1 = case (v0,v1) of
+ (VIdP a u v,w) ->
+ let j = fresh (Atom i, v0, w)
+ ts' = mkSystem [(j ~> 0,u),(j ~> 1,v)]
+ in VPath j $ genComp i (a @@ j) (w @@ j) ts'
+ (VSigma a f,u) ->
+ let (u1,u2) = (fstVal u,sndVal u)
+ fill_u1 = transFill i a u1
+ ui1 = trans i a u1
+ comp_u2 = trans i (app f fill_u1) u2
+ in VSPair ui1 comp_u2
+ (VPi{},_) -> VTrans (VPath i v0) v1
+ (Ter (Sum _ nass) env,VCon n us) -> case lookupIdent n nass of
+ Just as -> VCon n $ transps i as env us
+ Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+ _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
+ | otherwise -> error "trans not implemented"
+
+transFill, transFillNeg :: Name -> Val -> Val -> Val
+transFill i a u = trans j (a `conj` (i,j)) u
+ where j = fresh (Atom i,a,u)
+transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i
+
+transps :: Name -> [(Binder,Ter)] -> Env -> [Val] -> [Val]
+transps i [] _ [] = []
+transps i ((x,a):as) e (u:us) =
+ let v = transFill i (eval e a) u
+ vi1 = trans i (eval e a) u
+ vs = transps i as (Pair e (x,v)) us
+ in vi1 : vs
+transps _ _ _ _ = error "transps: different lengths of types and values"
+
+-----------------------------------------------------------
+-- Composition
+
+comp :: Val -> Val -> System Val -> Val
+comp a u ts = error "comp"
+-- compNeg a u ts = comp a u (ts `sym` i)
+
+genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val
+genComp i a u ts | Map.null ts = trans i a u
+genComp i a u ts = comp ai1 (trans i a u) ts'
+ where ai1 = a `face` (i ~> 1)
+ j = fresh (a,Atom i,ts,u)
+ comp' alpha u = VPath i (trans j ((a `face` alpha) `disj` (i,j)) u)
+ ts' = Map.mapWithKey comp' ts
+genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i)
+
+genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val
+genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j))
+ where j = fresh (Atom i,a,u,ts)
+genFillNeg i a u ts = (genFill i (a `sym` i) u (ts `sym` i)) `sym` i
+
+comps :: Name -> [(Binder,Ter)] -> Env -> [(System Val,Val)] -> [Val]
+comps i [] _ [] = []
+comps i ((x,a):as) e ((ts,u):tsus) =
+ let v = genFill i (eval e a) u ts
+ vi1 = genComp i (eval e a) u ts
+ vs = comps i as (Pair e (x,v)) tsus
+ in vi1 : vs
+comps _ _ _ _ = error "comps: different lengths of types and values"
+
+
+-- fills :: Name -> [(Binder,Ter)] -> Env -> [(System Val,Val)] -> [Val]
+-- fills i [] _ [] = []
+-- fills i ((x,a):as) e ((ts,u):tsus) =
+-- let v = genFill i (eval e a) ts u
+-- vs = fills i as (Pair e (x,v)) tsus
+-- in v : vs
+-- fills _ _ _ _ = error "fills: different lengths of types and values"
+
+
-------------------------------------------------------------------------------
-- | Conversion
conv :: Int -> Val -> Val -> Bool
conv k u v | u == v = True
- | otherwise = case (u,v) of
+ | otherwise = let j = fresh (u,v) in case (u,v) of
(Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
let v = mkVar k (eval e a)
in conv (k+1) (eval (Pair e (x,v)) u) (eval (Pair e' (x',v)) u')
(VApp u v,VApp u' v') -> conv k u u' && conv k v v'
(VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
(VVar x _, VVar x' _) -> x == x'
+ (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c'
+ (VPath i a,VPath i' a') -> conv k (a `swap` (i,j)) (a' `swap` (i',j))
+ (VPath i a,p') -> conv k (a `swap` (i,j)) (p' @@ j)
+ (p,VPath i' a') -> conv k (p @@ j) (a' `swap` (i',j))
+ -- VAppformula
+ -- VTrans
+ -- VComp
_ -> False
convEnv :: Int -> Env -> Env -> Bool
Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ;
NoWhere. ExpWhere ::= Exp ;
-Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ;
-Lam. Exp ::= "\\" [PTele] "->" Exp ;
-Fun. Exp1 ::= Exp2 "->" Exp1 ;
-Pi. Exp1 ::= [PTele] "->" Exp1 ;
-Sigma. Exp1 ::= [PTele] "*" Exp1 ;
-App. Exp2 ::= Exp2 Exp3 ;
-Var. Exp3 ::= AIdent ;
-U. Exp3 ::= "U" ;
-Fst. Exp3 ::= Exp3 ".1" ;
-Snd. Exp3 ::= Exp3 ".2" ;
-Pair. Exp3 ::= "(" Exp "," Exp ")" ;
+Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ;
+Lam. Exp ::= "\\" [PTele] "->" Exp ;
+Path. Exp ::= "<" Name ">" Exp ;
+Fun. Exp1 ::= Exp2 "->" Exp1 ;
+Pi. Exp1 ::= [PTele] "->" Exp1 ;
+Sigma. Exp1 ::= [PTele] "*" Exp1 ;
+App. Exp2 ::= Exp2 Exp3 ;
+Var. Exp3 ::= AIdent ;
+AppFormula. Exp3 ::= Exp3 "@" Name ;
+U. Exp3 ::= "U" ;
+Fst. Exp3 ::= Exp3 ".1" ;
+Snd. Exp3 ::= Exp3 ".2" ;
+IdP. Exp3 ::= "IdP" ;
+Trans. Exp3 ::= "transport" ;
+Pair. Exp3 ::= "(" Exp "," Exp ")" ;
coercions Exp 3 ;
-- Branches
terminator nonempty PTele "" ;
position token AIdent ((letter|'\''|'_')(letter|digit|'\''|'_')*) ;
-terminator AIdent "" ;
\ No newline at end of file
+terminator AIdent "" ;
+
+position token Name (('?')(digit)*);
+terminator Name "" ;
\ No newline at end of file
import Exp.Abs
import qualified CTT
+import qualified Connections as C
import Control.Applicative
import Control.Monad.Trans
resolveAIdent :: AIdent -> Resolver CTT.Binder
resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l
-
+
+resolveName :: Name -> Resolver C.Name
+resolveName (Name (_,n)) = return $ C.Name $ read $ tail n
+
resolveVar :: AIdent -> Resolver Ter
resolveVar (AIdent (l,x))
| (x == "_") || (x == "undefined") = CTT.Undef <$> getLoc l
binds :: (Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter
binds f = flip $ foldr $ bind f
+resolveApps :: Exp -> [Exp] -> Resolver Ter
+resolveApps Trans (x:y:xs) = do
+ let c = CTT.Trans <$> resolveExp x <*> resolveExp y
+ CTT.mkApps <$> c <*> mapM resolveExp xs
+resolveApps IdP (x:y:z:xs) = do
+ let c = CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
+ CTT.mkApps <$> c <*> mapM resolveExp xs
+resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
+
resolveExp :: Exp -> Resolver Ter
resolveExp e = case e of
U -> return CTT.U
Var x -> resolveVar x
- App t s -> CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
+ App t s -> resolveApps x xs
where (x,xs) = unApps t [s]
Sigma ptele b -> do
tele <- flattenPTele ptele
Let decls e -> do
(rdecls,names) <- resolveDecls decls
CTT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e)
-
+ Path i e -> CTT.Path <$> resolveName i <*> resolveExp e
+ AppFormula e n -> CTT.AppFormula <$> resolveExp e <*> (C.Atom <$> resolveName n)
+
resolveWhere :: ExpWhere -> Resolver Ter
resolveWhere = resolveExp . unWhere
import Control.Monad.Error (throwError)\r
import Control.Applicative\r
\r
+import Connections\r
import CTT\r
import Eval\r
\r
addTypeVal (x,a) (TEnv k rho v) =\r
TEnv (k+1) (Pair rho (x,mkVar k a)) v\r
\r
+addSub :: (Name,Formula) -> TEnv -> TEnv\r
+addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v\r
+\r
addType :: (Binder,Ter) -> TEnv -> Typing TEnv\r
addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv\r
\r
TEnv (k + length nvs) (pairs rho nvs) v\r
\r
addDecls :: Decls -> TEnv -> TEnv\r
-addDecls d (TEnv k rho v) = TEnv k (PDef d rho) v\r
+addDecls d (TEnv k rho v) = TEnv k (Def d rho) v\r
\r
addTele :: Tele -> TEnv -> Typing TEnv\r
addTele xas lenv = foldM (flip addType) lenv xas\r
checkDecls d\r
local (addDecls d) $ check a e\r
(_,Undef _) -> return ()\r
+ (VU,IdP a e0 e1) -> case a of\r
+ Path i b -> do\r
+ rho <- asks env\r
+ when (i `elem` support rho) (throwError (show i ++ " is already declared"))\r
+ local (addSub (i,Atom i)) $ check VU b\r
+ check (eval (Sub rho (i,Dir 0)) b) e0\r
+ check (eval (Sub rho (i,Dir 1)) b) e1\r
+ _ -> do\r
+ b <- infer a\r
+ case b of\r
+ VIdP (VPath _ VU) b0 b1 -> do\r
+ check b0 e0\r
+ check b1 e1\r
+ _ -> throwError ("IdP expects a path but got " ++ show a)\r
+ (VIdP p a b,Path i e) -> do\r
+ rho <- asks env\r
+ when (i `elem` support rho) (throwError (show i ++ " is already declared"))\r
+ local (addSub (i,Atom i)) $ check (p @@ i) e\r
_ -> do\r
v <- infer t\r
k <- index <$> ask\r
let w = mkVar k (eval nu a)\r
in w : mkVars (k+1) xas (Pair nu (x,w))\r
\r
--- inferNeutral :: Val -> Val\r
--- inferNeutral (VN (VVar _ a)) = a\r
--- inferNeutral _ = error "not done yet"\r
+checkFormula :: Formula -> Typing ()\r
+checkFormula phi = do\r
+ rho <- asks env\r
+ let dom = domainEnv rho\r
+ if all (\x -> x `elem` dom) (support phi)\r
+ then return ()\r
+ else throwError ("checkFormula: " ++ show phi)\r
\r
-- infer the type of e\r
infer :: Ter -> Typing Val\r
Where t d -> do\r
checkDecls d\r
local (addDecls d) $ infer t\r
+ AppFormula e phi -> do\r
+ checkFormula phi\r
+ t <- infer e\r
+ case t of\r
+ VIdP a _ _ -> return $ a @@ phi\r
+ _ -> throwError (show e ++ " is not a path") \r
_ -> throwError ("infer " ++ show e)\r
\r
checks :: (Tele,Env) -> [Ter] -> Typing ()\r
id (A : U) (a : A) : A = a
-
data list (A : U) = nil | cons (a : A) (as : list A)
l : list nat = cons one (cons two nil)
reverse (A : U) : list A -> list A = split
nil -> nil
cons x xs -> append A (reverse A xs) (cons x nil)
-
\ No newline at end of file
+
+
+Id (A : U) (a0 a1 : A) : U = IdP (<?0> A) a0 a1
+
+refl (A : U) (a : A) : Id A a a = <?0> a
+
+mapOnPath (A B : U) (f : A -> B) (a b : A)
+ (p : Id A a b) : Id B (f a) (f b) = <?0> f (p @ ?0)
+
+funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
+ (p : (x : A) -> Id (B x) (f x) (g x)) :
+ Id ((y : A) -> B y) f g = <?0> \(a : A) -> (p a) @ ?0
+
+idnat : nat -> nat = split
+ zero -> zero
+ suc n -> suc (idnat n)
+
+test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id nat) rem
+ where
+ rem : (n : nat) -> Id nat (idnat n) n = split
+ zero -> refl nat zero
+ suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
\ No newline at end of file
projects / cubicaltt.git / commitdiff