Skip to content
Browse files

add finite types;

some restructuration around recursion
  • Loading branch information...
1 parent b932fe1 commit 7e0563a1f67d90bfe344417a05127c34e518b8c4 @jyp committed Apr 15, 2012
Showing with 150 additions and 77 deletions.
  1. +7 −1 AbsSynToTerm.hs
  2. +6 −4 Main.hs
  3. +29 −24 Normal.hs
  4. +6 −2 RawSyntax.hs
  5. +93 −46 TypeCheckerNF.hs
  6. +9 −0 examples/Or.na
View
8 AbsSynToTerm.hs
@@ -71,7 +71,13 @@ resolveTerm (A.EPair defs) = pair <$> (forM defs $ \(A.Def (A.AIdent i@(Identifi
e' <- resolveTerm e
return (f,e'))
resolveTerm (A.EAnn e1 e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2
-resolveTerm (A.EBox (A.AIdent i) e) = Box (i2i i) <$> local (insertVar i) (resolveTerm e) <*> pure (map var [0..])
+resolveTerm (A.EBox (A.AIdent i) t e) = Box (i2i i) <$> resolveTerm t <*> local (insertVar i) (resolveTerm e)
+
+resolveTerm (A.EFin ts) = return $ Fin [t | (A.AIdent i@(Identifier (_p,t))) <- ts]
+resolveTerm (A.ETag (A.AIdent i@(Identifier (_p,t)))) = return $ Tag t
+resolveTerm (A.ECas x cs) = Cas <$> resolveTerm x <*> (forM cs $ \(A.Def (A.AIdent i@(Identifier (_p,t))) e) -> do
+ e' <- resolveTerm e
+ return (t,e'))
decodeDecl d = case d of
(A.EAnn vars a') -> do vs <- extractVars vars
View
10 Main.hs
@@ -45,10 +45,12 @@ run s fname = let ts = myLLexer s in case pExp ts of
process fname modul = do
let resolved = runResolver $ resolveTerm modul
- -- putStrV 2 $ "\n[Abstract Syntax]\n\n" ++ show tree
- -- putStrV 2 $ "\n[Linearized tree]\n\n" ++ printTree tree
- putStrV 2 $ "[Resolved into]" $$ pretty resolved
- let (checked,info) = runChecker $ iType mempty resolved
+ putStrV 3 $ "[Resolved into]" $$ pretty resolved
+ let evaluated = case evaluate resolved of
+ Nothing -> resolved
+ Just x -> x
+ putStrV 2 $ "[Evaluated into]" $$ pretty evaluated
+ let (checked,info) = runChecker $ iType mempty evaluated
mapM (putStrV 0) info -- display constraints, etc.
case checked of
Right (a,b) -> do
View
53 Normal.hs
@@ -23,11 +23,15 @@ data Term :: * where
Pair :: Position -> [(String,NF)] -> NF -- Note: Unlike Sigma, Pair do not bind variables
Proj :: Neutral -> String -> Neutral
+ Fin :: [String] -> NF
+ Tag :: String -> NF
+ Cas :: Neutral -> [(String, NF)] -> Neutral
+
V :: Position -> Int -> -- ^ deBruijn index
Neutral
Hole :: Position -> String -> Neutral
- Box :: Ident -> Term -> Subst -> NF
+ Box :: Ident -> NF -> Term -> NF
-- | type annotation
Ann :: Neutral -> NF -> NF
deriving (Show)
@@ -42,29 +46,12 @@ termPosition t = case t of
(Pair p _ ) -> p
(App x y) -> s x
(Proj x _) -> s x
- (Ann x _) -> s x
+ (Ann x _) -> s x
+ (Cas c _) -> termPosition c
+ _ -> dummyPosition
where s = termPosition
-instance Eq Term where
- Star _ s == Star _ s' = s == s'
- Pi _ a b == Pi _ a' b' = a == a' && b == b'
- Lam _ a b == Lam _ a' b' = a == a' && b == b'
- App a b == App a' b' = a == a' && b == b'
- Sigma _ xs == Sigma _ xs' = xs == xs'
- Pair _ xs == Pair _ xs' = xs == xs'
- Proj x f == Proj x' f' = x == x' && f == f'
- V _ x == V _ x' = x == x'
- Hole _ _ == Hole _ _ = True
- Box n t g == Box n' t' g' = n == n' && and [g!!v == g'!!v | v <- freeVars t]
- Ann x _ == Ann x' _ = x == x'
- _ == _ = False
-
--- | Untyped evaluation -- of boxes only.
-evaluate box@(Box n e0 env) = return $ apply (box:wk env) e0
-evaluate (Proj x f) = (\t -> proj t f) <$> evaluate x
-evaluate (App f x) = (`app` x) <$> evaluate f
-evaluate _ = Nothing
type Subst = [NF]
@@ -74,6 +61,8 @@ hole = Hole dummyPosition
star = Star dummyPosition
sigma = Sigma dummyPosition
pair = Pair dummyPosition
+tag = Tag
+fin = Fin
identity = map var [0..]
@@ -93,8 +82,12 @@ apply f t = case t of
(Proj x k) -> proj (s x) k
Hole p x -> Hole p x
V _ x -> f !! x
- Box p x g -> Box p x (map s g)
+ Box n t e -> Box n (s t) (s' e)
Ann x t -> Ann (s x) (s t)
+
+ Cas x cs -> cas (s x) (map (second s) cs)
+ Fin x -> Fin x
+ Tag x -> Tag x
where s' = apply (var 0 : wk f)
s = apply f
@@ -111,6 +104,10 @@ proj :: NF -> String -> NF
proj (Pair _ fs) f | Just x <- lookup f fs = x
proj x k = Proj x k
+cas :: NF -> [(String,NF)] -> NF
+cas (Tag t) cs | Just x <- lookup t cs = x
+cas x cs = Cas x cs
+
-- | Weakening
wkn :: Int -> Subst
wkn n = map var [n..]
@@ -136,8 +133,11 @@ freeVars (Star _ _) = mempty
freeVars (Hole _ _) = mempty
freeVars (Pair _ xs) = concatMap (freeVars . snd) xs
freeVars (Proj x _) = freeVars x
-freeVars (Box _ b _) = dec (freeVars b)
+freeVars (Box _ t e) = freeVars t <> dec (freeVars e)
freeVars (Ann x t) = freeVars x <> freeVars t
+freeVars (Fin _) = []
+freeVars (Tag _) = []
+freeVars (Cas t cs) = freeVars t <> concatMap (freeVars . snd) cs
iOccursIn :: Int -> Term -> Bool
iOccursIn x t = x `elem` (freeVars t)
@@ -160,8 +160,13 @@ cPrint p ii t@(Pi _ _ _) = parensIf (p > 1) (printBinders "→" ii mempty $ n
cPrint p ii t@(Sigma _ _) = parensIf (p > 1) (printBinders "×" ii mempty $ nestedSigmas t)
cPrint p ii (t@(Lam _ _ _)) = parensIf (p > 1) (nestedLams ii mempty t)
cPrint p ii (Pair _ fs) = parensIf (p > (-1)) (sep (punctuate comma [text name <+> text "=" <+> cPrint 0 ii x | (name,x) <- fs ]))
-cPrint p ii (Box i t g) = pretty i <> {- cPrint 100 (i <| ii) t <> -} "[" <> sep (punctuate ";" (dispEnv ii [(ii `index` f,g!!f) | f <- dec (freeVars t)])) <> "]"
+cPrint p ii (Box x t e) = "<" <> pretty i <> ":" <> cPrint 0 ii t <> ">" <> cPrint 2 (i <| ii) e
+ where i = allocName ii x
+{- {- cPrint 100 (i <| ii) t <> -} "[" <> sep (punctuate ";" (dispEnv ii [(ii `index` f,g!!f) | f <- dec (freeVars t)])) <> "]" -}
cPrint p ii (Ann x t) = parensIf (p > 0) (cPrint 0 ii x <+> ":" <+> cPrint 0 ii t)
+cPrint p ii (Fin ts) = "[" <> sep (punctuate comma (map text ts)) <> "]"
+cPrint p ii (Tag t) = "'" <> text t
+cPrint p ii (Cas x cs) = "case" <+> cPrint 0 ii x <+> "of {" <> sep (punctuate ";" [text c <> "" <> cPrint 0 ii a | (c,a) <- cs]) <> "}"
dispEnv :: DisplayContext -> [(Ident,NF)] -> [Doc]
dispEnv ii g = [pretty i <> "" <> cPrint 0 ii v | (i,v) <- g]
View
8 RawSyntax.hs
@@ -8,6 +8,9 @@ bnfc [lbnf|
comment "--" ;
comment "{-" "-}" ;
+ETag. Exp6 ::= "'" AIdent;
+EFin. Exp6 ::= "[" [AIdent] "]";
+ECas. Exp6 ::= "case" Exp "of" "{" [Defin] "}" ;
EHole. Exp6 ::= Hole ;
EVar. Exp6 ::= AIdent ;
ESet. Exp6 ::= Sort ;
@@ -16,7 +19,7 @@ EApp. Exp3 ::= Exp3 Exp4 ;
EPi. Exp2 ::= Exp3 Arrow Exp2 ;
ESigma. Exp2 ::= "{" [Exp] "}" ;
EAbs. Exp2 ::= "\\" [Bind] Arrow Exp2 ;
-EBox. Exp2 ::= "<" AIdent ">" Exp2 ;
+EBox. Exp2 ::= "<" AIdent ":" Exp ">" Exp2 ;
EAnn. Exp1 ::= Exp2 ":" Exp1 ;
EPair. Exp ::= [Defin] ;
@@ -27,6 +30,7 @@ separator Exp ";";
Def. Defin ::= AIdent "=" Exp ;
separator nonempty Defin ",";
+separator AIdent ",";
token Arrow ('-' '>') ;
@@ -37,7 +41,7 @@ terminator Bind "" ;
token Natural digit+;
-position token Identifier ('!'|letter|digit|'-'|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;
+position token Identifier ('!'|letter|digit|'-'|'_'|'\'')((letter|digit|'-'|'_'|'\'')*) ;
position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;
position token Sort ('#' | '*' (digit*));
View
139 TypeCheckerNF.hs
@@ -29,13 +29,9 @@ report x = lift $ tell [x]
runChecker :: Result a -> (Either (Term,Doc) a,[Doc])
runChecker x = runIdentity $ runWriterT $ runErrorT x
-data Definition = Abstract -- ^ lambda, pi, sigma bound
- | Direct Value -- ^ pair bound
-
type Value = NF
type Type = Value
data Bind = Bind {entryIdent :: Ident,
- entryValue :: Definition, -- ^ Value for identifier.
entryType :: Type -- ^ Attention: context of the type does not contain the variable bound here.
}
type Context = Seq Bind
@@ -46,10 +42,7 @@ display c = prettyTerm (fmap entryIdent c)
dispContext :: Context -> Doc
dispContext ctx = case viewl ctx of
EmptyL -> mempty
- Bind x val typ :< ctx' -> let di = display ctx' in (case val of
- Abstract -> pretty x <+> ":" <+> di typ
- Direct v -> pretty x <+> sep ["=" <+> parens (di v), ":" <+> di typ]
- ) $$ dispContext ctx'
+ Bind x typ :< ctx' -> (pretty x <+> ":" <+> display ctx' typ) $$ dispContext ctx'
-- FIXME: flag an error if impredicativity disabled and we use it anyway.
@@ -63,20 +56,18 @@ iType g t@(Star p s)
= return (star s,star $ above s)
iType g (Pi ident tyt tyt')
= do (ty ,s1) <- iSort g tyt
- (ty',s2) <- iSort (Bind ident Abstract ty <| g) tyt'
+ (ty',s2) <- iSort (Bind ident ty <| g) tyt'
let o = s1 s2
return (Pi ident ty ty', star o)
iType g (Sigma _ []) = return (sigma [],star 0)
iType g (Sigma _ ((f,t):ts))
= do (t',s1) <- iSort g t
- (Sigma _ ts',s2) <- iSort (Bind (synthId f) Abstract t' <| g) (sigma ts)
+ (Sigma _ ts',s2) <- iSort (Bind (synthId f) t' <| g) (sigma ts)
let o = s1 s2
return (sigma ((f,t'):ts'), star o)
iType g e@(V _ x) = do
- return $ (val $ value, wkn (x+1) typ)
- where val (Direct v) = wkn (x+1) v
- val _ = var x -- We could do eta-expansion here: etaExpand (var x) typ
- Bind _ value typ = g `index` x
+ return $ (var x, wkn (x+1) typ)
+ where Bind _ typ = g `index` x
iType g (Hole p x) = do
report $ hang (text ("context of " ++ x ++ " is")) 2 (dispContext g)
@@ -85,7 +76,7 @@ iType g (Hole p x) = do
iType g t@(Lam x (Hole _ _) e) = throwError (t,"cannot infer type for" <+> display g t)
iType g (Lam x ty e) = do
(vty,vs) <- iSort g ty
- (ve,t) <- iType (Bind x Abstract vty <| g) e
+ (ve,t) <- iType (Bind x vty <| g) e
return $ (Lam x vty ve, Pi x vty t)
iType g (Pair _ fs) = do
@@ -95,14 +86,18 @@ iType g (Pair _ fs) = do
return (pair (zip fs vs),sigma (zip fs [ wkn n t | (n,t) <- zip [0..] ts]))
-- possible dependencies in the type are not discovered
-iType g e | Just e' <- evaluate e = iType g =<< comput g e e'
+iType g (Tag t) = return (Tag t,Fin [t])
+iType g (Fin ts) = return (Fin ts,star 0)
+
+-- iType g e | Just e' <- evaluate e = iType g =<< comput g e e'
iType g (App e1 e2)
- = do (v1,si) <- iType g e1
- case si of
+ = do (e1',et) <- iType g e1
+ et' <- eval et
+ case et' of
Pi _ ty ty' -> do
v2 <- cType g e2 ty
- return (app v1 v2, subst0 v2 ty')
+ return (app e1' v2, subst0 v2 ty')
_ -> throwError (e1,"invalid application")
iType g (Proj e f) = do
@@ -115,6 +110,10 @@ iType g (Proj e f) = do
_ -> throwError (e,"field" <+> text f <+> "not found in type" <+> display g et)
_ -> throwError (e,"type should be record:" <+> display g et)
+iType g (Box n t e) = do
+ (t',_) <- iSort g t
+ return (Box n t' e,t')
+ -- checking inside the box is delayed until one needs to actually evaluate its contents.
iType g t = throwError (t,"cannot infer type for" <+> display g t)
@@ -129,32 +128,17 @@ iSort g e = do
return $ (hole h, Sort 1)
_ -> throwError (e,display g e <+> "is not a type")
--- | Test if two types are equal.
-unify :: Context -> Term -> Type -> Type -> Result ()
-unify g e q q' =
- do let ii = length g
- constraint = report $ vcat ["constraint: " <> display g q',
- "equal to : " <> display g q]
- case (q,q') of
- ((Hole _ _), t) -> constraint
- (t, Hole _ _) -> constraint
- _ -> unless (q == q')
- (throwError (e,hang "type mismatch: " 2 $ vcat
- ["inferred:" <+> display g q',
- "expected:" <+> display g q ,
- "for:" <+> display g e ,
- "context:" <+> dispContext g]))
-- | Check the type and normalize
cType :: Context -> Term -> Type -> Result Value
cType g (Lam name (Hole _ _) e) (Pi name' ty ty') = do
- e' <- cType (Bind name Abstract ty <| g) e ty'
+ e' <- cType (Bind name ty <| g) e ty'
return (Lam name ty e') -- the type and binder is filled in.
cType g (Lam name ty0 e) (Pi name' ty ty')
= do (t,_o) <- iSort g ty0
- unify g (Hole (identPosition name) (show name)) t ty
- e' <- cType (Bind name Abstract ty <| g) e ty'
+ unify g (Hole (identPosition name) (show name)) ty t
+ e' <- cType (Bind name ty <| g) e ty'
return (Lam name ty e')
cType g (Pair _ ignored) (Sigma _ []) = return $ pair ignored
@@ -169,23 +153,86 @@ cType g (Pair _ ((f,x):xs)) (Sigma i fs@((f',xt):xts))
Pair _ xs' <- cType g (pair xs) (subst0 x sigma xts)
return (pair ((f,x'):xs'))
--- cType g (Box name e _) et = do
--- e' <- cType (Bind name (Direct (Box name e (map var [0..]))) et <| g) e et -- FIXME: env.
--- return (Box name e' $ map var [0..])-- FIXME: env.
+cType g (Cas c cs) t = do
+ let ct = Fin $ map fst cs
+ c' <- cType g c ct
+ cs' <- forM cs $ \ (p,v) -> do
+ v' <- cType g v t
+ return (p,v')
+ return (cas c' cs')
+
+-- cType g e v | Just v' <- evaluate v = cType g e =<< comput g v v'
+-- cType g e v | Just e' <- evaluate e = (\x -> cType g x v) =<< comput g e e'
+
+{-
cType g (Proj e f) t = do
e' <- cType g e (sigma [(f,t)])
return (proj e' f)
-
-
-cType g e v | Just v' <- evaluate v = cType g e =<< comput g v v'
-cType g e v | Just e' <- evaluate e = (\x -> cType g x v) =<< comput g e e'
+-}
cType g e v = do
(e',v') <- iType g e
- unify g e v v'
+ unify g e v' v
return e'
comput g x y = do
report $ display g x <> " --> " <> display g y
- return y
+ return y
+
+
+-- | Unification with subtyping
+unify :: Context -> Term -> Type -> Type -> Result ()
+unify g e q' q = unif g q' q where
+ crash :: Result ()
+ crash = throwError (e,hang "type mismatch: " 2 $ vcat
+ ["inferred:" <+> display g q',
+ "expected:" <+> display g q ,
+ "for:" <+> display g e ,
+ "context:" <+> dispContext g])
+ check :: Bool -> Result ()
+ check c = unless c crash
+ eqList p [] [] = return ()
+ eqList p (x:xs) (x':xs') = p x x' >> eqList p xs xs'
+ eqList p _ _ = crash
+ unif :: Context -> Type -> Type -> Result ()
+ unif g q' q = case (q',q) of
+ (Star _ s , Star _ s') -> check $ s == s'
+ (Pi i a b , Pi _ a' b') -> (a' <: a) >> unif (Bind i a <| g) b b'
+ (Lam i a b , Lam _ a' b') -> (a' <: a) >> unif (Bind i a <| g) b b'
+ (App a b , App a' b') -> (a <: a') >> (b <: b')
+ (Sigma _ xs, Sigma _ []) -> return ()
+ (Sigma _ ((f,x):xs) , Sigma _ ((f',x'):xs')) -> do
+ check $ f == f'
+ x <: x'
+ unif (Bind (synthId f) x' <| g) (sigma xs) (sigma xs')
+ (Pair _ xs , Pair _ xs') -> eqList (\(f,x) (f',x') -> check (f == f') >> x <: x') xs xs'
+ (Proj x f , Proj x' f') -> x <: x' >> check (f == f')
+ (V _ x , V _ x') -> check (x == x')
+ (Hole _ _, _) -> constraint
+ (_, Hole _ _) -> constraint
+ (Box _ t e , Box _ t' e') -> t <: t' >> e <: e'
+ (Ann x _ , Ann x' _) -> x <: x'
+ (Tag t , Tag t') -> check $ t == t'
+ (Fin ts , Fin ts') -> check $ ts == ts'
+ (Cas x xs , Cas x' xs') -> x <: x' >> eqList (\(f,x) (f',x') -> check (f == f') >> x <: x') xs xs'
+ _ | Just x' <- evaluate q' -> do
+ comput g q' x' -- FIXME: x' should be type-checked.
+ x' <: q
+ _ -> crash
+ where (<:) :: Type -> Type -> Result ()
+ (<:) = unif g
+ infix 4 <:
+ constraint = report $ vcat ["constraint: " <> display g q',
+ "subtype of: " <> display g q]
+
+eval g (x,t) = case evaluate x of
+ Nothing -> return (x,t)
+ Just x' -> comput g x x' >> return (x',t) -- FIXME: x' should be type-checked.
+
+-- | Dynamically-typed evaluation -- of boxes only.
+evaluate box@(Box _ t e) = return (subst0 box e)
+evaluate (Proj x f) = (`proj` f) <$> evaluate x
+evaluate (App f x) = (`app` x) <$> evaluate f
+evaluate (Cas x cs) = (`cas` cs) <$> evaluate x
+evaluate _ = Nothing
View
9 examples/Or.na
@@ -0,0 +1,9 @@
+<m: {Bool : *
+ ;Or : *}>
+(Bool = [true,false]
+,Or = \ (A:*) (B:*) -> {t : m.Bool : *; v : case t of
+ {true = A,
+ false = B} : * }
+,TT = [tt]
+,Nat = m.Or m.TT
+)

0 comments on commit 7e0563a

Please sign in to comment.
Something went wrong with that request. Please try again.