pisigma 0.1.0.1 → 0.1.0.2
raw patch · 8 files changed
+1070/−1 lines, 8 files
Files
- pisigma.cabal +8/−1
- src/PiSigma/Check.hs +189/−0
- src/PiSigma/Equality.hs +128/−0
- src/PiSigma/Evaluation.hs +151/−0
- src/PiSigma/Nf.hs +111/−0
- src/PiSigma/Parser.hs +141/−0
- src/PiSigma/Print.hs +108/−0
- src/PiSigma/Syntax.hs +234/−0
pisigma.cabal view
@@ -1,6 +1,6 @@ cabal-version: >= 1.6 name: pisigma-version: 0.1.0.1+version: 0.1.0.2 license: BSD3 license-file: LICENSE data-files: examples/*.pi@@ -15,6 +15,13 @@ executable pisigma main-is: PiSigma.hs+ other-modules: PiSigma.Check+ PiSigma.Equality+ PiSigma.Evaluation+ PiSigma.Nf+ PiSigma.Parser+ PiSigma.Print+ PiSigma.Syntax hs-source-dirs:src build-depends: base >= 4 && < 5, array >= 0.2 && < 0.3,
+ src/PiSigma/Check.hs view
@@ -0,0 +1,189 @@+module PiSigma.Check where++import Control.Monad++import PiSigma.Syntax+import PiSigma.Evaluation+import PiSigma.Print+import PiSigma.Equality++--import Debug.Trace+--trace "check\n" $++-- closures are the other way around+-- should be fixed by changing closures.++{-+fog :: CTerm -> Closure+fog (g,t) = (con2scope g,t)+-}++failc :: Env e => Clos Term -> [Msg] -> Eval e a+failc t m = failp ([S "Checking:\t",C t,S "\n"]++m)++-- | Takes a term and an (unevaluated) type. We first+-- handle the cases that may potentially change the+-- environment. If none of those cases match, we can+-- safely evaluate the type and call check'.+check :: Env e => Clos Term -> Clos Type -> Eval e ()+--check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined++check (Let p t,g) c = + do g' <- checkProg (p,g)+ check (t,g') c++check (gt @ (Split t (x,(y,u)),g)) c = + do sigab <- infer' (t,g)+ case sigab of+ (VQ Sigma ((a,(z,b)),s)) -> + do t' <- eval (t,g)+ (_,g') <- tdecl x g (a,s)+ b <- subst (z,(b,s)) (Var x, g')+ (_,g'') <- tdecl y g' b+ case t' of+ (Ne (NVar i)) ->+ letn' i (Pair (Var x,Var y), g'')+ (check (u,g'') c)+ -- this is a bit silly since we know the ids.+ _ -> check (u,g'') c+ -- instead of failing, we just omit the assignment.+ _ -> failc gt [S "split : Sigma type expected\nFound:\t",V sigab,S "\n(split)\n"]++check gt @ (t'@(Case t lus),g) c = + do enum <- infer' (t,g)+ case enum of+ VEnum ls -> + let ls' = map fst lus+ in if ls /= ls'+ then do -- pt' <- prt t'+ failc gt [S ("case: labels don't match"+ ++ "\n expected : " ++ show ls+ ++ "\n inferred : " ++ show ls'+ ++ "\n(match)\n")]+ -- set equivalence would be sufficent+ else do t' <- eval (t,g)+ case t' of+ -- if the scrutinee is a variable, we add a constraint+ -- while checking each of the branches+ (Ne (NVar i)) ->+ mapM_ (\ (l,u) -> + letn' i (label l)+ (check (u,g) c)) lus+ -- if the scrutinee is not a variable, we do not add+ -- a constraint, but continue+ _ -> mapM_ (\ (l,u) -> check (u,g) c) lus+ _ -> failc gt [S "case : enum type expected\nFound:\t",V enum,S "\n(case)\n"]+ {- Problem: here and other places: we try to print the term t which isn't yet + typechecked and may contain undefined variables which may crash the printer...+ see undef-bug.pi+ -}+check (Force t,g) (a , s) =+ check (t,g) (Lift a , s)++check t a = do a' <- feval a+ check' t a'++check' :: Env e => Clos Term -> Val -> Eval e ()+check' gt (VBox (Boxed a)) = check gt a -- do we still need this line?+check' (Lam (x,t),g) (VQ Pi ((a,(y,b)),s)) =+ do (i,g') <- tdecl x g (a,s)+ let s' = extendScope s y (i,Nothing)+ check (t,g') (b,s')+check' gt @ (Lam _,g) a = failc gt [S "Expected:\t",V a,S "\n(Lam)\n"]+check' (Pair (t,u),g) (VQ Sigma ((a,(y,b)),s)) =+ do check (t,g) (a,s)+ b <- subst (y,(b,s)) (t,g)+ check (u,g) b+check' gt @ (t @ (Pair _),g) a = failc gt [S "Expected\t",V a,S "\n(Pair)\n"]+-- Labels cannot be inferred because there is no way to know+-- what the other labels are.+check' gt @ (Label l,g) a @ (VEnum ls) | l `elem` ls = return ()+check' gt @ (Label l,g) a = failc gt [S "Expected\t",V a,S "\n(Label)\n"]+-- To check that [sigma] is a type, it's sufficient to know+-- that sigma is a type. The alternative would seem to be to+-- assume that ^Type == Type, but that does not work.+check' (Box a,g) VType =+ check (a,g) ty+check' (Box t,g) (VLift a) =+ check (t,g) a+check' gt @ (Box _,g) a = failc gt [S "Expected\t",V a,S "\n(Box)\n"]+check' t a =+ do b <- infer' t+ catchE (eq a b)+ (\ s -> failc t [S "Expected:\t",V a,+ S "\nFound:\t",V b,S $ "\n(check)\n"])+-- ++s++"\n"++(show a)++"\n"++(show b)])+-- useful for debugging.++inferVar :: Env e => Clos Name -> Eval e (Clos Type)+inferVar (x,g) =+ case lookupCon g x of+ Just a -> return a+ Nothing -> fail ("Undefined variable: "++x++"\n(inferVar)\n")++infer :: Env e => Clos Term -> Eval e (Clos Type)+--infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined++infer (Var x,g) = inferVar (x,g)++infer (Let tel t,g) = + do g' <- checkProg (tel,g)+ infer (t,g') ++infer (Type,g) = return ty++infer (Q _ (a,(x,b)),g) = + do check (a,g) ty+ (_,g') <- tdecl x g (a,g)+ check (b,g') ty+ return ty++infer gt@(t :. u,g) = + do piab <- infer' (t,g)+ case piab of + (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)+ subst (x,(b,s)) (u,g)+ _ -> failc gt [S "Pi type expected, but found:\t",+ V piab,+ S "\n(app)\n"]++infer (Enum _,_) = return ty++infer (Box t,g) =+ liftM (\ (a,s) -> (Lift a,s)) (infer (t,g))++-- TODO: either use infer', or explain why forced eval+-- cannot be used here.+infer gt@(Force t,g) =+ do a <- infer (t,g)+ a' <- eval a+ case a' of+ VLift b -> return b+ _ -> failc gt [S "Lifted type expected\n(Force)\n"]+infer (Lift a,g) =+ do check (a,g) ty+ return ty++infer gt = failc gt [S "Not inferable\n(infer)\n"]+++-- | Infers a type and evaluates it.+infer' :: Env e => Clos Term -> Eval e Val+infer' gt =+ do a <- infer gt+ feval a++checkProg :: Env e => Clos Prog -> Eval e Scope+checkProg ([],g) = return g+checkProg ((Decl x a):tel,g) = + do check (a,g) ty + (_,g') <- decl x (PrtInfo {name=x, expand=False}) g (Just (a,g))+ checkProg (tel,g')+checkProg ((Defn x t):tel,g) =+ do a <- inferVar (x,g)+ check (t,g) a+ i <- getId x g+ defn' i (t,g)+ checkProg (tel,g)+ +
+ src/PiSigma/Equality.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}+module PiSigma.Equality where++import Control.Monad++import PiSigma.Syntax+import PiSigma.Evaluation++class Equal a where+ eq :: Env e => a -> a -> Eval e ()++instance Equal (Clos Term) where+ eq t u = do t' <- eval t+ u' <- eval u+ eq t' u'++eq' :: Env e => Clos (Term,Term) -> Eval e ()+eq' ((t,u),s) = eq (t,s) (u,s)++eqBind :: (Env e,Closure a) =>+ (a -> a -> Eval e ()) ->+ Bind a -> Bind a -> Eval e ()+eqBind eq (x0,c0) (x1,c1) =+ do let s0 = getScope c0+ s1 = getScope c1+ (i,s0') <- decl' x0 s0+ let s1' = extendScope s1 x1 (i,Nothing)+ let c0' = putScope c0 s0'+ c1' = putScope c1 s1'+ eq c0' c1'++instance (Equal a,Closure a) => Equal (Bind a) where+ eq = eqBind eq++instance Equal Val where+ eq (Ne t0) (Ne t1) = eq t0 t1+ eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))+ | ps0 == ps1 = + do eq (a0,s0) (a1,s1)+ eq (x0,(b0,s0)) (x1,(b1,s1))+ eq (VLam xt0) (VLam xt1) = eq xt0 xt1+ eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = + do eq (t0,s0) (t1,s1)+ eq (u0,s0) (u1,s1)+ eq (VBox b) (VBox b') = eq b b' + eq (VLift a) (VLift a') = eq a a'+ eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum+ | otherwise = fail "Different values"++eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()+eqBox (Var x,s) (Var y,s') = + do x' <- getId x s+ y' <- getId y s'+ eq x' y'+{-+eqBox (Var x,s) u =+ do x' <- getId x s+ ei <- lookupId x'+ case ei of+ Closure t -> eqBox t u+ Id j -> fail "eqBox: var vs term"+ -- wrong level - this should use functions in Evaluation+ -- have to avoid races: don't unfold the same id twice!+eqBox t u @ (Var _,_) = eqBox u t +-}+eqBox (Let p t,s) c = fail "eqBox: let not implemented"+{-+ do s' <- evalProg (p,s)+ eqBox (t,s') c+-}+eqBox c c'@(Let p t,s) = eqBox c' c +eqBox (Q ps (a,(x,b)),s) (Q ps' (a',(x',b')),s')+ | ps == ps' = + do eqBox (a,s) (a',s')+ eq (x,Boxed (b,s)) (x',Boxed (b',s'))+eqBox (t :. u,s) (t' :. u',s') =+ do eqBox (t,s) (t',s')+ eqBox (u,s) (u',s')+eqBox (Split t (x,(y,u)),s) (Split t' (x',(y',u')),s') =+ do eqBox (t,s) (t',s')+ eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))+eqBox (Case t bs,s) (Case t' bs',s') =+ do eqBox (t,s) (t',s')+ zipWithM_ (\ (l,t) (l',t') -> + if l==l' then eqBox (t,s) (t',s')+ else fail "eqBox case") bs bs'+eqBox (Lift t,s) (Lift t',s') = eqBox (t,s) (t',s')+eqBox (Box t,s) (Box t',s') = eqBox (t,s) (t',s')+eqBox (Force t,s) (Force t',s') = eqBox (t,s) (t',s') +eqBox (t,s) (t',s') | t == t' = return () -- Type, Label, Enum+ | otherwise = fail "Different terms"+-- TODO: check that it cannot happen that t and t' are syntacically equal but not alpha equivalent!+ +instance Equal Boxed where+ eq (Boxed c) (Boxed c') = eqBox c c'++instance Equal Id where+ eq i0 i1 + | i0 == i1 = return ()+ | otherwise = do ei0 <- lookupId i0+ ei1 <- lookupId i1+ case (ei0,ei1) of+ (Id j0, Id j1) -> unless (j0 == j1)+ (fail "Different variables")+ (Closure t0, Closure t1) ->+ letn i0 (Id i0)+ (letn i1 (Id i0)+ (eq t0 t1))+ _ -> fail "Variable vs neutral"++instance Equal Ne where+ eq (NVar i0) (NVar i1) = eq i0 i1+ eq (t0 :.. u0) (t1 :.. u1) = + do eq t0 t1+ eq u0 u1+ eq (NSplit t0 xyu0) (NSplit t1 xyu1) =+ do eq t0 t1+ eq xyu0 xyu1+ eq (NCase t0 (lus0,s0)) (NCase t1 (lus1,s1)) =+ do eq t0 t1+ let eqBranches [] [] = return ()+ eqBranches ((l0,u0):lus0) ((l1,u1):lus1) | l0 == l1 =+ do eq (u0,s0) (u1,s1)+ eqBranches lus0 lus1+ eqBranches _ _ = fail "Case: branches differ"+ eqBranches lus0 lus1+ eq (NForce t) (NForce t') = eq t t'+ eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
+ src/PiSigma/Evaluation.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module PiSigma.Evaluation where++import Control.Monad.Error+import Control.Monad.State+import Control.Monad.Identity++import PiSigma.Syntax++-- * Monad used for evaluation++newtype Eval e a =+ Eval {unEval :: StateT e (ErrorT String Identity) a}+ deriving (Monad,MonadError String,MonadState e)++run :: e -> Eval e a -> Either String (a,e)+run e (Eval p) = runIdentity $ runErrorT $ runStateT p e ++catchE :: Eval e a -> (String -> Eval e a) -> Eval e a+catchE = catchError++getEnv :: Eval e e+getEnv = get++setEnv :: e -> Eval e ()+setEnv = put++getId :: Name -> Scope -> Eval e Id+getId x s = case lookupScope s x of + Just i -> return i+ Nothing -> fail ("Undefined Variable: "++x++"\n")++-- | Takes a name, a scope, and potentially a type.+-- It extends the environment and the scope with that name.+decl :: Env e =>+ Name -> PrtInfo -> Scope -> Maybe (Clos Type) ->+ Eval e (Id,Scope)+decl x x' s a =+ do e <- getEnv+ let (i,e') = extE e x'+ setEnv e'+ return (i,extendScope s x (i,a))++decl' :: Env e => Name -> Scope -> Eval e (Id,Scope)+decl' x s = decl x (PrtInfo {name = x, expand = True}) s Nothing++tdecl :: Env e => Name -> Scope -> (Clos Type) -> Eval e (Id,Scope)+tdecl x g a = decl x (PrtInfo {name = x, expand = True}) g (Just a)++-- | Updates the environment.+defn :: Env e => Id -> EnvEntry -> Eval e ()+defn i ei =+ do e <- getEnv+ setEnv (setE e i ei)++defn' :: Env e => Id -> Clos Type -> Eval e ()+defn' i t = defn i (Closure t)++-- | Locally updates the environment.+letn :: Env e => Id -> EnvEntry -> Eval e a -> Eval e a+letn i ei p =+ do eo <- lookupId i+ defn i ei+ a <- p+ defn i eo+ return a++letn' :: Env e => Id -> Clos Type -> Eval e a -> Eval e a+letn' i t p = letn i (Closure t) p++subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)+subst (x,(t,s)) u =+ do (i,s') <- decl' x s+ defn' i u + return (t,s')++evalApp :: Env e => Val -> (Clos Term) -> Eval e Val+evalApp (VLam xt) u = subst xt u >>= eval+evalApp (Ne t) u = return (Ne (t :.. u))+evalApp _ _ = fail "function expected"++lookupId :: Env e => Id -> Eval e EnvEntry+lookupId i = liftM (flip getE i) getEnv++evalId :: Env e => Id -> Eval e Val+evalId i =+ do ei <- lookupId i+ case ei of+ Closure t -> eval t+ Id j -> return (Ne (NVar j))++-- use subst!+evalSplit :: Env e => Val -> (Bind (Bind (Clos Term))) ->+ Eval e Val+evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = + do (x',s2) <- decl' x s'+ (y',s3) <- decl' y s2+ defn' x' (l,s)+ defn' y' (r,s)+ eval (t,s3)++evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))+evalSplit _ _ = fail "Pair expected"++evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val+evalCase (VLabel l) (lts,s) = + case lookup l lts of+ Nothing -> fail "case not matched"+ Just t -> eval (t,s)+evalCase (Ne n) lts = return (Ne (NCase n lts))+evalCase _ _ = fail "Label expected"++force :: Env e => Val -> Eval e Val+force (VBox (Boxed c)) = eval c+force (Ne n) = return (Ne (NForce n))+force _ = fail "Box expected"++eval :: Env e => (Clos Term) -> Eval e Val+eval (Var x, s) = getId x s >>= evalId+eval (Let g t, s) = evalProg (g,s) >>= curry eval t+eval (Type,s) = return VType+eval (Q ps axb,s) = return (VQ ps (axb,s))+eval (Lift t,s) = return (VLift (t,s))+eval (Lam (x,t), s) = return (VLam (x,(t,s)))+eval (t :. u ,s) = eval (t,s) >>= flip evalApp (u,s)+eval (Pair tu,s) = return (VPair (tu,s))+eval (Split t (x,(y,u)),s)+ = eval (t,s) >>= flip evalSplit (x,(y,(u,s)))+eval (Enum ls,s) = return (VEnum ls)+eval (Label l,s) = return (VLabel l)+eval (Case t lts,s) = eval (t,s) >>= flip evalCase (lts,s)+eval (Box t,s) = return (VBox (Boxed (t,s)))+eval (Force t,s) = eval (t,s) >>= force+++-- forced eval (should be integrated into eval?)+feval :: Env e => (Clos Term) -> Eval e Val+feval t = do t' <- eval t+ case t' of + VBox (Boxed u) -> feval u+ v -> return v++ ++evalProg :: Env e => Clos Prog -> Eval e Scope+evalProg ([],s) = return s+evalProg ((Decl x _):tel, s) = do (_,s') <- decl x (PrtInfo x False) s Nothing+ evalProg (tel,s')+evalProg ((Defn x t):tel, s) = do i <- getId x s+ defn' i (t,s)+ evalProg (tel,s)
+ src/PiSigma/Nf.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies,+ TypeSynonymInstances, FlexibleInstances #-}+module PiSigma.Nf where++{- Implementation of a normalisation function.+ Useful for testing.+-}++import Control.Monad++import PiSigma.Syntax+import PiSigma.Evaluation++type Vars = [String]++fresh :: Name -> Vars -> Name+fresh x xs = if x/="" && elem x xs then fresh (x++"'") xs+ else x++class Nf a b | a -> b where+ nf :: Env e => Vars -> a -> Eval e b+ nf = nf' True+ quote :: Env e => Vars -> a -> Eval e b+ quote = nf' False+ nf' :: Env e => Bool -> Vars -> a -> Eval e b+++instance Nf (Clos Term) Term where+ nf' True xs t = do t' <- eval t+ nf' True xs t'+ nf' False xs t = qq xs t++instance Nf Id Term where+ nf' b xs i = do e <- getEnv+ let (PrtInfo x exp) = prtE e i+ case getE e i of+ (Id _) -> return (Var x) + (Closure t) -> if exp then nf' b xs t+ -- this is bad, we should not+ -- expand inside a box!+ else return (Var x) ++qq :: Env e => Vars -> Clos Term -> Eval e Term+qq xs (Var x,s) = do i <- getId x s+ quote xs i+qq xs (Let g t, s) = fail "quote let: not implemented!"+{-do s' <- evalProg (g,s)+ qq xs (t,s') + -- this seems wrong! we should return a Let+ -- and we should extend xs!+-}+qq xs (Q ps (a,(x,b)),s) = + do a' <- qq xs (a,s)+ xb' <- quote xs (x,(b,s))+ return (Q ps (a',xb'))+qq xs (Lift t,s) = liftM Lift (qq xs (t,s))+qq xs (Lam (x,t), s) = liftM Lam (quote xs (x,(t,s)))+qq xs (t :. u ,s) = do t' <- qq xs (t,s)+ u' <- qq xs (u,s)+ return (t' :. u')+qq xs (Pair (t,u),s) = do t' <- qq xs (t,s)+ u' <- qq xs (u,s)+ return (Pair (t',u'))+qq xs (Split t (x,(y,u)),s) = do t' <- qq xs (t,s)+ xyu' <- quote xs (x,(y,(u,s)))+ return (Split t' xyu')+qq xs (Case t lts,s) = do t' <- qq xs (t,s)+ lts' <- mapM (\ (l,t) -> + do t' <- qq xs (t,s)+ return (l,t')) lts+ return (Case t' lts') +qq xs (Box t,s) = liftM Box (qq xs (t,s))+qq xs (Force t,s) = liftM Force (qq xs (t,s))+qq xs (t,s) = return t -- Type, Enum, Label++instance (Closure a,Nf a b) => Nf (Bind a) (Bind b) where+ nf' b xs (x,t) = do let x' = fresh x xs+ (i,s') <- decl x (PrtInfo x' True) (getScope t) Nothing+ t' <- nf' b (x':xs) (putScope t s')+ return (x',t')++instance Nf Val Term where+ nf' b xs (Ne n) = nf' b xs n+ nf' b xs VType = return Type+ nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) + xc' <- nf' b xs (x,(c,s))+ return (Q ps (a',xc'))+ nf' b xs (VLift c) = liftM Lift (nf' b xs c)+ nf' b xs (VLam xt) = liftM Lam (nf' b xs xt)+ nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)+ u' <- nf' b xs (u,s)+ return (Pair (t',u'))+ nf' b xs (VBox (Boxed c)) = liftM Box (nf' False xs c)+ nf' b xs (VEnum ls) = return (Enum ls)+ nf' b xs (VLabel l) = return (Label l)+++instance Nf Ne Term where+ nf' b xs (NVar i) = nf' b xs i+ nf' b xs (t' :.. u) = do t <- nf' b xs t'+ u' <- nf' b xs u+ return (t :. u')+ nf' b xs (NSplit t xyu) = do t' <- nf' b xs t+ xyu' <- nf' b xs xyu+ return (Split t' xyu')+ nf' b xs (NCase t (lus,s)) = do t' <- nf xs t+ lus' <- mapM (\ (l,u) -> + do u' <- nf' b xs (u,s)+ return (l,u')) lus+ return (Case t' lus')+ nf' b xs (NForce t) = liftM Force (nf xs t)
+ src/PiSigma/Parser.hs view
@@ -0,0 +1,141 @@+module PiSigma.Parser (module PiSigma.Parser, Parser) where++import Prelude hiding (pi)+import Data.Char+import Data.List++import Control.Monad+import Control.Applicative hiding ((<|>), many)++import Text.ParserCombinators.Parsec as P hiding (token, label)++import PiSigma.Syntax hiding (label)++type SParser = CharParser ()++-- * Comments and whitespace++blockComment :: SParser ()+blockComment = () <$ try (string "{-") <* inComment <* string "-}"++inComment :: SParser ()+inComment =+ () <$ many (choice [ () <$ noneOf "{-"+ , try $ () <$ char '-' <* notFollowedBy (char '}')+ , try $ () <$ char '{' <* notFollowedBy (char '-')+ , blockComment ])++lineComment :: SParser ()+lineComment = () <$ try (string "--") <* many (noneOf "\n")++whiteSpace :: SParser ()+whiteSpace = () <$ spaces <* many ((lineComment <|> blockComment) <* spaces)+ <?> ""++-- * Identifiers++identChar :: SParser Char+identChar = alphaNum <|> oneOf "_'"++ident :: SParser String+ident = + (try $ do+ xs <- (:) <$> letter <*> many identChar <* whiteSpace+ guard (xs `notElem` keywords)+ return xs) <?> "identifier"++keywords :: [String]+keywords = [ "case", "of", "let", "in", "split", "Type", "with" ]++label :: SParser Name+label = char '\'' *> ident++-- * Tokens++token :: String -> SParser String+token xs = (try $ (string xs <* whiteSpace)) <?> show xs++-- * Brackets++parensed = between (token "(") (token ")")+braced = between (token "{") (token "}")+bracketed = between (token "[") (token "]")++-- * Terms++sTerm5 :: SParser Term+sTerm5 =+ Type <$ token "Type"+ <|> (Enum <$> braced (many ident) <?> "enumeration")+ <|> Case <$ token "case" <*> sTerm <* token "of"+ <*> braced (sBranch `sepBy` token "|")+ <|> (Label <$> label <?> "label")+ <|> (Box <$> bracketed sTerm <?> "box")+ <|> (Lift <$ token "^" <*> sTerm5 <?> "'^'")+ <|> Var <$> ident+ <|> parensed sTerm++sTerm4 :: SParser Term+sTerm4 =+ try (parensed (curry Pair <$> sTerm <* token "," <*> sTerm))+ <|> sTerm5++sTerm3 :: SParser Term+sTerm3 =+ try (parensed (sigmas <$> many1 ident <* token ":" <*> sTerm) <* token "*")+ <*> sTerm3+ <|> Force <$ token "!" <*> sTerm4+ <|> foldl1 (:.) <$> many1 sTerm4++sTerm2 :: SParser Term+sTerm2 =+ foldl1 (-*-) <$> sTerm3 `sepBy1` token "*"++-- TODO: make more beautiful or renumber+sTerm1b :: SParser Term+sTerm1b =+ try (parensed (pis <$> many1 ident <* token ":" <*> sTerm) <* token "->")+ <*> sTerm+ <|> sTerm2+ +sTerm1 :: SParser Term+sTerm1 =+ flip ($) <$> sTerm1b <*> option id (flip (->-) <$ token "->" <*> sTerm)++sTerm :: SParser Term+sTerm =+ lam <$ token "\\" <*> many ident <* token "->" <*> sTerm+ <|> split <$ token "split" <*> sTerm <* token "with"+ <* token "(" <*> ident <* token "," <*> ident <* token ")"+ <* token "->" <*> sTerm+ <|> Let <$ token "let" <*> sProg <* token "in" <*> sTerm+ <|> sTerm1++sProg :: SParser Prog+sProg = concat <$> (sEntry `sepEndBy` token ";")++sEntry :: SParser [Entry]+sEntry = + do+ n <- ident+ b <- (True <$ token ":" <|> False <$ token "=")+ t <- sTerm+ if b+ then do+ d <- option Nothing (Just <$ token "=" <*> sTerm)+ case d of+ Nothing -> return [Decl n t]+ Just t' -> return [Decl n t, Defn n t']+ else return [Defn n t]++sBranch :: SParser (Label,Term)+sBranch = (,) <$> ident <* token "->" <*> sTerm++sPhrase :: SParser Phrase+sPhrase =+ (try $ Prog <$> sProg <* eof) <|> Term <$> sTerm <* eof++s2Terms :: SParser (Term, Term)+s2Terms = (,) <$> sTerm5 <*> sTerm5++parse p = P.parse (whiteSpace *> p <* eof)
+ src/PiSigma/Print.hs view
@@ -0,0 +1,108 @@+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+module PiSigma.Print where++import Control.Monad++import Text.PrettyPrint.ANSI.Leijen++import PiSigma.Syntax+import PiSigma.Evaluation+import PiSigma.Nf++-- * Print class for various types++class Print a where+ prt :: Env e => a -> Eval e String++instance Print Val where+ prt a = quote [] a >>= prt++instance Print (Clos Term) where+ prt a = quote [] a >>= prt++instance Print Ne where+ prt a = quote [] a >>= prt++instance Print Term where+ prt a = return (displayS (renderPretty 0.8 75 (pretty a)) "")+++data Msg = V Val | C (Clos Term) | T Term | S String++instance Print Msg where+ prt (V v) = prt v+ prt (C c) = prt c+ prt (T t) = prt t+ prt (S s) = return s++failp :: (Print a, Env e) => [a] -> Eval e b+failp ps = do msg <- foldM (\ msg p -> do s <- prt p+ return (msg++s)) "" ps+ fail msg++-- * Pretty printer for terms++-- | Context for printing. Determines whether parentheses are+-- required.+type PrintContext = Int++prettyTerm :: PrintContext -> Term -> Doc+prettyTerm _ (Var x) = text x+prettyTerm _ (Let p t) = pretty p <> pretty t+prettyTerm _ Type = text "Type"+prettyTerm c (Q Pi (t1,(n,t2))) =+ contextParens c 1 $+ group (binding 2 n t1 <$> text "->" <+> prettyTerm 1 t2)+prettyTerm c (Q Sigma (t1,(n,t2))) =+ contextParens c 2 $+ binding 2 n t1 <+> text "*" <+> prettyTerm 3 t2+prettyTerm _ (Lam (n,t)) =+ text "\\" <+> text n <+> text "->" <+> prettyTerm 0 t+prettyTerm c (t1 :. t2) =+ group (hang 2 (contextParens c 3 (prettyTerm 3 t1 <$> prettyTerm 4 t2)))+prettyTerm c (Pair (t1,t2)) =+ tupled (map (prettyTerm 0) [t1,t2])+prettyTerm _ (Split t1 (n1,(n2,t2))) =+ hang 2 (text "split" <+> prettyTerm 0 t1 <+> text "with"+ <+> parens (text n1 <> comma <> text n2)+ <+> text "->" <$> prettyTerm 0 t2)+prettyTerm _ (Enum ls) = braces (sep (map text ls))+prettyTerm _ (Label l) = text ('\'' : l)+prettyTerm _ (Case t bs) =+ hang 2 (text "case" <+> prettyTerm 0 t <+> text "of" <$> branches bs)+prettyTerm c (Lift t) =+ contextParens c 5 $+ text "^" <> prettyTerm 5 t+prettyTerm _ (Box t) =+ brackets (prettyTerm 0 t)+prettyTerm c (Force t) =+ contextParens c 3 $+ text "!" <> prettyTerm 4 t++prettyEntry :: Entry -> Doc+prettyEntry (Defn n t) =+ hang 2 (text n <+> text "=" <$> prettyTerm 0 t <> text ";")+prettyEntry (Decl n t) =+ hang 2 (text n <+> text ":" <$> prettyTerm 0 t <> text ";")++binding :: PrintContext -> String -> Term -> Doc+binding c "" t = prettyTerm c t+binding _ n t = parens (text n <+> colon <+> prettyTerm 0 t)++branches :: [(Label,Term)] -> Doc+branches bs = encloseSep lbrace rbrace (text "|") (map branch bs)+ where branch (n,t) = text n <+> text "->" <+> prettyTerm 0 t++-- | Prints parens if the current context is higher+-- than a certain limit.+contextParens :: PrintContext -> PrintContext -> Doc -> Doc+contextParens c d p | c > d = parens p+ | otherwise = p++instance Pretty Term where+ pretty = prettyTerm 0++instance Pretty Entry where+ pretty = prettyEntry+
+ src/PiSigma/Syntax.hs view
@@ -0,0 +1,234 @@+{-# LANGUAGE TypeSynonymInstances #-}+module PiSigma.Syntax where++import Prelude hiding (pi)++-- * Abstract syntax++data Phrase = Prog Prog | Term Term+ deriving (Show,Eq)++type Name = String++type Label = String++data Entry = Decl Name Type | Defn Name Term+ deriving (Show,Eq)++type Prog = [Entry]++{-+Maybe better+data Prog = Decl Type (Bind Prog) | Defn Name Term Prog+-}++type Type = Term++-- | The use of Bind indicates the scope of the+-- bound identifier.+type Bind a = (Name,a)++-- | For treating quantifiers in a uniform way.+data PiSigma = Pi | Sigma+ deriving (Show,Eq)++data Term =+ Var String+ | Let Prog Term+ | Type+ | Q PiSigma (Type,Bind Type)+ | Lam (Bind Term)+ | Term :. Term+ | Pair (Term,Term)+ | Split Term (Bind (Bind Term)) -- split t with (x,y) -> u+ | Enum [Label]+ | Label Label+ | Case Term [(Label,Term)] -- case t of { L -> u }+ | Lift Term+ | Box Term+ | Force Term+ deriving (Show,Eq)++-- * Smart constructors++-- | Smart constructor for lambda abstractions.+lam :: [Name] -> Term -> Term+lam [] t = t+lam (x:xs) t = Lam (x,lam xs t)++-- | Smart constructor for split.+split :: Term -> Name -> Name -> Term -> Term+split t1 x y t2 = Split t1 (x,(y,t2))++-- | Smart constructor for quantifiers.+q :: PiSigma -> [(Name,Type)] -> Type -> Type+q ps [] b = b+q ps ((x,a):xas) b = Q ps (a,(x,q ps xas b))++-- | Smart constructor for multiple Pi applications.+pis' :: [(Name,Type)] -> Type -> Type+pis' = q Pi++-- | Smart constructor for multiple Pi applications.+pis :: [Name] -> Type -> Type -> Type+pis ns t = pis' (map (\ n -> (n,t)) ns)++-- | Smart constructor for Pi.+pi :: Name -> Type -> Type -> Type+pi n t = pis' [(n,t)]++-- | Smart constructor for multiple Sigma applications.+sigmas' :: [(Name,Type)] -> Type -> Type+sigmas' = q Sigma++-- | Smart constructor for multiple Sigma applications.+sigmas :: [Name] -> Type -> Type -> Type+sigmas ns t = sigmas' (map (\ n -> (n,t)) ns)++-- | Smart constructor for Sigma.+sigma :: Name -> Type -> Type -> Type+sigma n t = sigmas' [(n,t)]++-- | Smart constructor for function space.+(->-) :: Type -> Type -> Type+(->-) = pi ""++-- | Smart constructor for product.+(-*-) :: Type -> Type -> Type+(-*-) = sigma ""++-- * Values (well-scoped WHNFs) and environments++-- ** Identifiers++type Id = Int -- index in (potentially multiple) environments++-- ** Scopes++data Scope = Scope [(Name,(Id,Maybe (Clos Type)))]+ deriving (Show,Eq)++{-++TODO:++Perhaps return to the following types for scopes:++data Sc a = Scope [(Name,(Id, a))]++type Scope = Sc ()+type Ctx = Sc (Clos Type)++We then need a forgetful mapping:++fog :: Ctx -> Scope+fog c = map (\ (x,(i,a)) -> (x,(i,()))) c ++Alternatively, we can try to make Scopes+existential, essentially:++type Scope = exists a. Sc a++-}++emptyScope :: Scope+emptyScope = Scope []++extendScope :: Scope -> Name -> (Id,Maybe (Clos Type)) -> Scope+extendScope (Scope s) x (i,a) = Scope ((x,(i,a)) : s)++lookupScope :: Scope -> Name -> Maybe Id+lookupScope (Scope s) x = do (i,_) <- lookup x s+ return i++lookupCon :: Scope -> Name -> Maybe (Clos Type)+lookupCon (Scope s) x = do (_,Just a) <- lookup x s+ return a++-- ** Closures++type Clos a = (a,Scope)++--type C a = (Con,a)++--c2clos :: C a -> Clos a+--c2clos (g,a) = (a,fog g)++-- fix order, name of C...++class Closure a where + getScope :: a -> Scope+ putScope :: a -> Scope -> a++instance Closure (Clos a) where+ getScope (_,s) = s+ putScope (a,_) s = (a,s)++instance Closure a => Closure (Bind a) where+ getScope (_,a) = getScope a+ putScope (x,a) s = (x,putScope a s)++instance Closure Boxed where+ getScope (Boxed c) = getScope c+ putScope (Boxed c) s = Boxed (putScope c s)++{- could be used to refactor the code using bindings. -}++ty :: Clos Type+ty = (Type,emptyScope)++label :: String -> Clos Term+label s = (Label s,emptyScope)++type VType = Val++newtype Boxed = Boxed (Clos Term) deriving (Show,Eq)++-- ** Values++data Val =+ Ne Ne+ | VType + | VQ PiSigma (Clos (Type,Bind Type))+ | VLift (Clos Type)+ | VLam (Bind (Clos Term))+ | VPair (Clos (Term, Term))+ | VEnum [Label]+ | VLabel Label + | VBox Boxed+ deriving (Show,Eq)++-- | Neutral terms.+data Ne =+ NVar Id+ | Ne :.. (Clos Term)+ | NSplit Ne (Bind (Bind (Clos Term)))+ | NCase Ne (Clos [(Label,Term)])+ | NForce Ne+ deriving (Show,Eq)++-- ** Environments++data EnvEntry = Id Id | Closure (Clos Term) deriving Show++data PrtInfo = PrtInfo {name :: Name, expand :: Bool}++class Env e where + emptyE :: e+ extE :: e -> PrtInfo -> (Id,e)+ setE :: e -> Id -> EnvEntry -> e+ getE :: e -> Id -> EnvEntry+ prtE :: e -> Id -> PrtInfo++set :: [a] -> Int -> a -> [a]+set (a:as) 0 b = b:as+set (a:as) i b = a:set as (i-1) b+ +type EnvEntries = [(EnvEntry,PrtInfo)]++instance Env EnvEntries where+ emptyE = []+ extE e x = let i = length e in (i,e++[(Id i,x)])+ setE e i v = let (_,x) = e!!i in set e i (v,x)+ getE e i = let (v,_) = e!!i in v+ prtE e i = let (_,x) = e!!i in x