diff --git a/pisigma.cabal b/pisigma.cabal --- a/pisigma.cabal +++ b/pisigma.cabal @@ -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, diff --git a/src/PiSigma/Check.hs b/src/PiSigma/Check.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Check.hs @@ -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) + + diff --git a/src/PiSigma/Equality.hs b/src/PiSigma/Equality.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Equality.hs @@ -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") diff --git a/src/PiSigma/Evaluation.hs b/src/PiSigma/Evaluation.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Evaluation.hs @@ -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) diff --git a/src/PiSigma/Nf.hs b/src/PiSigma/Nf.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Nf.hs @@ -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) diff --git a/src/PiSigma/Parser.hs b/src/PiSigma/Parser.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Parser.hs @@ -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) diff --git a/src/PiSigma/Print.hs b/src/PiSigma/Print.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Print.hs @@ -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 + diff --git a/src/PiSigma/Syntax.hs b/src/PiSigma/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/PiSigma/Syntax.hs @@ -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