diff options
| -rw-r--r-- | obs.ipkg | 3 | ||||
| -rw-r--r-- | src/CC/Name.idr | 25 | ||||
| -rw-r--r-- | src/CC/Term.idr | 109 | ||||
| -rw-r--r-- | src/CC/Term/Elaborate.idr | 221 | ||||
| -rw-r--r-- | src/CC/Term/Eval.idr | 78 | ||||
| -rw-r--r-- | src/CC/Term/Parse.idr | 155 | ||||
| -rw-r--r-- | src/CC/Term/Pretty.idr | 58 | ||||
| -rw-r--r-- | src/CC/Term/Raw.idr | 31 | ||||
| -rw-r--r-- | src/CC/Thinning.idr | 29 | ||||
| -rw-r--r-- | src/Main.idr | 37 |
10 files changed, 646 insertions, 100 deletions
@@ -6,12 +6,13 @@ depends = contrib options = "--total" -executable = "cc-eval" +executable = "cc-check" main = Main modules = CC.Name , CC.Term + , CC.Term.Elaborate , CC.Term.Eval , CC.Term.Parse , CC.Term.Pretty diff --git a/src/CC/Name.idr b/src/CC/Name.idr index 4c25f5c..d1df253 100644 --- a/src/CC/Name.idr +++ b/src/CC/Name.idr @@ -2,6 +2,10 @@ module CC.Name import public Control.Relation +import Data.List +import Data.Singleton +import Data.Stream + import Decidable.Equality import Text.Bounded @@ -65,3 +69,24 @@ decEquiv m n = decEq m.val n.val export bounds : (name : Name) -> Maybe Bounds bounds name = if name.isIrrelevant then Nothing else Just name.bounds + +||| Returns a new name not in the set. +export +fresh : Foldable f => f Name -> Name +fresh xs = + irrelevantBounds $ + select (unfoldr (\n => ("_\{show n}", S n)) 0) $ + sort $ + foldMap (singleton . val) xs + where + select : Ord a => Stream a -> List a -> a + select (x :: xs) [] = x + select (x :: xs) (y :: ys) = + case compare x y of + LT => x + EQ => select xs ys + GT => select (x :: xs) ys + +export +fresh' : Foldable f => Singleton {a = f Name} xs -> Name +fresh' (Val xs) = fresh xs diff --git a/src/CC/Term.idr b/src/CC/Term.idr index 1806904..233afda 100644 --- a/src/CC/Term.idr +++ b/src/CC/Term.idr @@ -3,6 +3,12 @@ module CC.Term import CC.Name import CC.Thinning +import Control.Function + +import Data.Nat +import Data.Singleton +import Data.SnocList.Elem + -- Definition ------------------------------------------------------------------ public export @@ -17,28 +23,41 @@ data IsVar : Nat -> Name -> Context -> Type where public export data Term : Context -> Type where Var : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Term ctx + + Let : + (n : Name) -> + (ty : Maybe (Term ctx)) -> + (val : Term ctx) -> + (t : Term (ctx :< n)) -> + Term ctx + + Set : Term ctx + + Pi : (n : Maybe Name) -> Term ctx -> Term (ctx ++ maybe [<] ([<] :<) n) -> Term ctx Abs : (n : Name) -> Term (ctx :< n) -> Term ctx App : Term ctx -> Term ctx -> Term ctx - Let : (n : Name) -> Term ctx -> Term (ctx :< n) -> Term ctx public export data Value : Context -> Type public export data Neutral : Context -> Type -public export -data Closure : Context -> Type public export data Env : (local, global : Context) -> Type where Lin : Env [<] global (:<) : Env local global -> (p : (Name, Lazy (Value global))) -> Env (local :< fst p) global -data Closure : Context -> Type where - Close : (n : Name) -> Env local global -> Term (local :< n) -> Closure global - data Value where Ntrl : Neutral ctx -> Value ctx - VAbs : Closure ctx -> Value ctx + VSet : Value ctx + VPi : + (n : Name) -> + Lazy (Value ctx) -> + Env local ctx -> + Term (local :< n) -> + Value ctx + VFunc : Env local ctx -> Term local -> Term local -> Value ctx + VAbs : Env local ctx -> (n : Name) -> Term (local :< n) -> Value ctx data Neutral where VVar : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Neutral ctx @@ -48,7 +67,6 @@ data Neutral where %name Term t, u %name Value v %name Neutral n -%name Closure close %name Env env -- Operations ------------------------------------------------------------------ @@ -58,6 +76,31 @@ index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value glob index (env :< (n, v)) 0 (Here eq) = v index (env :< _) (S k) (There prf) = index env k prf +export +fromElem : {n : Name} -> (prf : Elem n ctx) -> IsVar (elemToNat prf) n ctx +fromElem Here = Here (reflexive {rel = (~~)}) +fromElem (There i) = There (fromElem i) + +export +tabulate : + {local : Context} -> + (f : Nat -> Nat) -> + (0 prf : {k, n : _} -> IsVar k n local -> IsVar (f k) n global) -> + Env local global +tabulate {local = [<]} f prf = [<] +tabulate {local = _ :< n} f prf = + tabulate (f . S) (prf . There) :< + (n, Ntrl $ VVar (f 0) n (prf $ fromElem Here)) + +export +(++) : Env local1 global -> Env local2 global -> Env (local1 ++ local2) global +env ++ [<] = env +env ++ env' :< p = (env ++ env') :< p + +recomputeLocal : Env local global -> Singleton local +recomputeLocal [<] = Val [<] +recomputeLocal (env :< (n, _)) = Val (:< n) <*> recomputeLocal env + -- Weakening ------------------------------------------------------------------- wknVar' : @@ -95,26 +138,64 @@ wknIsVar prf thin = wknIsVar' prf (view thin) export wknTerm : Term src -> src `Thins` tgt -> Term tgt wknTerm (Var k n prf) thin = Var (wknVar thin prf) n (wknIsVar prf thin) +wknTerm (Let n Nothing val t) thin = Let n Nothing (wknTerm val thin) (wknTerm t (keep thin)) +wknTerm (Let n (Just ty) val t) thin = + Let n (Just $ wknTerm ty thin) (wknTerm val thin) (wknTerm t (keep thin)) +wknTerm Set thin = Set +wknTerm (Pi Nothing dom cod) thin = Pi Nothing (wknTerm dom thin) (wknTerm cod thin) +wknTerm (Pi (Just n) dom cod) thin = Pi (Just n) (wknTerm dom thin) (wknTerm cod (keep thin)) wknTerm (Abs n t) thin = Abs n (wknTerm t (keep thin)) wknTerm (App t u) thin = App (wknTerm t thin) (wknTerm u thin) -wknTerm (Let n t u) thin = Let n (wknTerm t thin) (wknTerm u (keep thin)) export wknNtrl : Neutral src -> src `Thins` tgt -> Neutral tgt export wknVal : Value src -> src `Thins` tgt -> Value tgt export -wknClose : Closure src -> src `Thins` tgt -> Closure tgt -export wknEnv : Env local src -> src `Thins` tgt -> Env local tgt wknNtrl (VVar k n prf) thin = VVar (wknVar thin prf) n (wknIsVar prf thin) wknNtrl (VApp n v) thin = VApp (wknNtrl n thin) (wknVal v thin) wknVal (Ntrl n) thin = Ntrl (wknNtrl n thin) -wknVal (VAbs close) thin = VAbs (wknClose close thin) - -wknClose (Close n env t) thin = Close n (wknEnv env thin) t +wknVal VSet thin = VSet +wknVal (VPi n dom env cod) thin = VPi n (wknVal dom thin) (wknEnv env thin) cod +wknVal (VFunc env dom cod) thin = VFunc (wknEnv env thin) dom cod +wknVal (VAbs env n t) thin = VAbs (wknEnv env thin) n t wknEnv [<] thin = [<] wknEnv (env :< (n, v)) thin = wknEnv env thin :< (n, wknVal v thin) + +-- Renaming -------------------------------------------------------------------- + +renVar : {src, tgt : Context} -> length src = length tgt -> IsVar k n src -> (m ** IsVar k m tgt) +renVar prf (Here eq) {tgt = _ :< m} = (m ** fromElem Here) +renVar prf (There prf') {tgt = _ :< m} = + let rec = renVar (injective prf) prf' in (rec.fst ** There rec.snd) + +export +renTerm : length src = length tgt -> Term src -> Term tgt +renTerm prf (Var k n prf') = let 0 var = renVar prf prf' in Var k var.fst var.snd +renTerm prf (Let n Nothing val t) = + Let n Nothing (renTerm prf val) (renTerm (cong S prf) t) +renTerm prf (Let n (Just ty) val t) = + Let n (Just $ renTerm prf ty) (renTerm prf val) (renTerm (cong S prf) t) +renTerm prf Set = Set +renTerm prf (Pi Nothing t u) = Pi Nothing (renTerm prf t) (renTerm prf u) +renTerm prf (Pi (Just n) t u) = Pi (Just n) (renTerm prf t) (renTerm (cong S prf) u) +renTerm prf (Abs n t) = Abs n (renTerm (cong S prf) t) +renTerm prf (App t u) = App (renTerm prf t) (renTerm prf u) + +-- Lifting --------------------------------------------------------------------- + +inrVar : IsVar k n ctx -> IsVar k n (global ++ ctx) +inrVar (Here eq) = Here eq +inrVar (There prf) = There (inrVar prf) + +liftEnv : + {global : Context} -> + (ctx : Context) -> + Env local global -> + Env (local ++ ctx) (global ++ ctx) +liftEnv [<] env = env +liftEnv ctx env = wknEnv env (id ++ empty) ++ tabulate id inrVar diff --git a/src/CC/Term/Elaborate.idr b/src/CC/Term/Elaborate.idr new file mode 100644 index 0000000..458ec38 --- /dev/null +++ b/src/CC/Term/Elaborate.idr @@ -0,0 +1,221 @@ +module CC.Term.Elaborate + +import CC.Name +import CC.Term +import CC.Term.Eval +import CC.Term.Raw +import CC.Thinning + +import Data.DPair +import Data.List1 +import Data.Singleton +import Data.SnocList +import Data.SnocList.Elem + +import Text.Bounded + +%prefix_record_projections off + +-- Elaboration Errors ---------------------------------------------------------- + +export +data ElabError : Type -> Type where + Ok : ty -> ElabError ty + Error : List1 (Either Name (String, Maybe Bounds)) -> ElabError ty + +Functor ElabError where + map f (Ok x) = Ok (f x) + map f (Error xs) = Error xs + +Applicative ElabError where + pure = Ok + + Ok f <*> Ok v = Ok (f v) + Ok f <*> Error ys = Error ys + Error xs <*> Ok v = Error xs + Error xs <*> Error ys = Error (xs ++ ys) + +Monad ElabError where + join (Ok (Ok x)) = Ok x + join (Ok (Error xs)) = Error xs + join (Error xs) = Error xs + +export +runElabError : ElabError ty -> Either (List1 (Either Name (String, Maybe Bounds))) ty +runElabError (Ok x) = Right x +runElabError (Error xs) = Left xs + +fromNameError : NameError ty -> ElabError ty +fromNameError v = + case runNameError v of + Left errs => Error (map Left errs) + Right v => Ok v + +-- Elaboration Context --------------------------------------------------------- + +record ElabCtx (local, global : Context) where + constructor MkCtx + env : Env local global + types : (k : Nat) -> forall n. (0 prf : IsVar k n local) -> Lazy (Value global) + pos : Maybe Bounds + +%name ElabCtx ctx + +wknCtx : + {global : Context} -> + ElabCtx local global -> + (n : Name) -> + ElabCtx local (global :< n) +wknCtx ctx n = { env $= flip wknEnv (drop id), types := types } ctx + where + types : (k : Nat) -> forall m. (0 _ : IsVar k m local) -> Lazy (Value (global :< n)) + types k prf = wknVal (ctx.types k prf) (drop id) + +define : + ElabCtx local global -> + (n : Name) -> + (val : Lazy (Value global)) -> + (ty : Lazy (Value global)) -> + ElabCtx (local :< n) global +define ctx n val ty = { env $= (:< (n, val)), types := types } ctx + where + types : (k : Nat) -> forall m. (0 _ : IsVar k m (local :< n)) -> Lazy (Value global) + types 0 (Here eq) = ty + types (S k) (There prf) = ctx.types k prf + +bind : + {global : Context} -> + ElabCtx local global -> + (n : Name) -> + (ty : Lazy (Value global)) -> + ElabCtx (local :< n) (global :< n) +bind ctx n ty = define (wknCtx ctx n) n (Ntrl $ VVar 0 _ $ fromElem Here) (wknVal ty (drop id)) + +updatePos : ElabCtx local global -> (irrel : Bool) -> Bounds -> ElabCtx local global +updatePos ctx irrel bounds = { pos := if irrel then Nothing else Just bounds } ctx + +-- Checking and Inference ------------------------------------------------------ + +record PiType (ctx : Context) where + constructor MkPi + {0 local : Context} + name : Name + dom : Lazy (Value ctx) + env : Env local ctx + cod : Term (local :< name) + +check : + {local, global : Context} -> + ElabCtx local global -> + RawTerm -> + Lazy (Value global) -> + ElabError (Term local) +checkType : + {local, global : Context} -> + ElabCtx local global -> + RawTerm -> + ElabError (Term local) +infer : + {local, global : Context} -> + ElabCtx local global -> + RawTerm -> + ElabError (Term local, Lazy (Value global)) +inferPi : + {local, global : Context} -> + ElabCtx local global -> + RawTerm -> + ElabError (Term local, PiType global) +inferType : + {local, global : Context} -> + ElabCtx local global -> + RawTerm -> + ElabError (Term local) + +check ctx (Bounded (MkBounded t irrel bounds)) ty = check (updatePos ctx irrel bounds) t ty + +check ctx (Let n Nothing val t) ty = do + (val, ty') <- infer ctx val + t <- check (define ctx n (eval ctx.env val) ty') t ty + pure $ Let {n, ty = Nothing, val, t} +check ctx (Let n (Just ty') val t) ty = do + ty' <- checkType ctx ty' + let vty : Lazy (Value global) = eval ctx.env ty' + val <- check ctx val vty + t <- check (define ctx n (eval ctx.env val) vty) t ty + pure $ Let {n, ty = Just ty', val, t} + +check ctx Set VSet = pure $ Set + +check ctx (Abs Nothing t) (VFunc env dom cod) = do + t <- check ctx t (eval env cod) + pure $ Abs (fresh local) (wknTerm t (drop id)) +check ctx (Abs (Just n) t) (VFunc env dom cod) = do + t <- check (bind ctx n (eval env dom)) t (eval (wknEnv env (drop id)) cod) + pure $ Abs n t +check ctx (Abs Nothing t) (VPi m dom env cod) = do + t <- check (wknCtx ctx m) t (eval (liftEnv [<m] env) cod) + pure $ Abs m (wknTerm t (drop id)) +check ctx (Abs (Just n) t) (VPi m dom env cod) = do + t <- check (bind ctx n dom) t (eval (liftEnv [<n] env) $ renTerm Refl cod) + pure $ Abs n t + +check ctx t ty = do + (t, ty') <- infer ctx t + let True = convert ty ty' + | False => Error $ singleton $ Right ("conversion failed", ctx.pos) + pure t + +checkType ctx t = check ctx t VSet + +infer ctx (Bounded (MkBounded t irrel bounds)) = infer (updatePos ctx irrel bounds) t +infer ctx (Var n) = do + Element k prf <- fromNameError $ lookup local n + pure (Var k n prf, ctx.types k prf) +infer ctx (Let n Nothing val t) = do + (val, ty') <- infer ctx val + (t, ty) <- infer (define ctx n (eval ctx.env val) ty') t + pure $ (Let {n, ty = Nothing, val, t}, ty) +infer ctx (Let n (Just ty) val t) = do + ty' <- checkType ctx ty + let vty : Lazy (Value global) = eval ctx.env ty' + val <- check ctx val vty + (t, ty) <- infer (define ctx n (eval ctx.env val) vty) t + pure $ (Let {n, ty = Just ty', val, t}, ty) +infer ctx Set = pure (Set, delay VSet) +infer ctx (Pi (Nothing `Of` dom) cod) = do + (dom, cod) <- [| MkPair (inferType ctx dom) (inferType ctx cod) |] + pure $ (Pi Nothing dom cod, delay VSet) +infer ctx (Pi (Just n `Of` dom) cod) = do + dom <- inferType ctx dom + let vdom : Lazy (Value global) = eval ctx.env dom + cod <- inferType (bind ctx n vdom) cod + pure $ (Pi (Just n) dom cod, delay VSet) +infer ctx (App t u) = do + (t, ty) <- inferPi ctx t + u <- check ctx u ty.dom + let vu : Lazy (Value global) = eval ctx.env u + pure $ (App t u, delay $ eval (ty.env :< (ty.name, vu)) ty.cod) +infer ctx t = Error $ singleton $ Right ("cannot infer type", ctx.pos) + +inferPi ctx t = do + (t, ty) <- infer ctx t + case force ty of + VPi n dom env cod => + pure $ (t, MkPi n dom env cod) + VFunc env dom cod => + let local' = recomputeLocal env in + pure $ (t, MkPi (fresh' local') (eval env dom) env (wknTerm cod (drop $ id' local'))) + ty => Error $ singleton $ Right ("expected pi type", ctx.pos) + +inferType ctx t = do + (t, ty) <- infer ctx t + case force ty of + VSet => pure t + ty => Error $ singleton $ Right ("expected set type", ctx.pos) + +export +inferTerm : RawTerm -> ElabError (Term [<], Lazy (Value [<])) +inferTerm = infer (MkCtx [<] types Nothing) + where + types : (k : Nat) -> forall n. (0 _ : IsVar k n [<]) -> Lazy (Value [<]) + types k prf impossible diff --git a/src/CC/Term/Eval.idr b/src/CC/Term/Eval.idr index 311bc34..7029893 100644 --- a/src/CC/Term/Eval.idr +++ b/src/CC/Term/Eval.idr @@ -4,22 +4,28 @@ import CC.Name import CC.Term import CC.Thinning +import Data.SnocList.Elem + -- Evaluation ------------------------------------------------------------------ export -app : Closure ctx -> Lazy (Value ctx) -> Value ctx +app : (n : Name) -> Env local global -> Term (local :< n) -> Lazy (Value global) -> Value global export eval : Env local global -> Term local -> Value global -app (Close n env t) v = assert_total $ eval (env :< (n, v)) t +app n env t v = eval (env :< (n, v)) t eval env (Var k n prf) = index env k prf -eval env (Abs n t) = VAbs (Close n env t) +eval env (Let n ty val t) = eval (env :< (n, eval env val)) t +eval env Set = VSet +eval env (Pi Nothing t u) = VFunc env t u +eval env (Pi (Just n) t u) = VPi n (eval env t) env u +eval env (Abs n t) = VAbs env n t eval env (App t u) = case eval env t of Ntrl n => Ntrl $ VApp n (eval env u) - VAbs close => app close (eval env u) -eval env (Let n t u) = eval (env :< (n, eval env t)) u + VAbs env' n t => assert_total $ app n env' t (eval env u) + _ => assert_total $ idris_crash "eval invariant broken" -- Quoting --------------------------------------------------------------------- @@ -28,11 +34,17 @@ quote : {ctx : _} -> Value ctx -> Term ctx quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx quote (Ntrl n) = quoteNtrl n -quote (VAbs close@(Close n _ _)) = - Abs n $ - assert_total $ - quote $ - app (wknClose close (drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)}) +quote VSet = Set +quote (VPi n t env u) = + Pi (Just n) + (quote t) + (assert_total $ quote $ eval (liftEnv [<n] env) u) +quote (VFunc env t u) = + Pi Nothing + (assert_total $ quote $ eval env t) + (assert_total $ quote $ eval env u) +quote (VAbs env n t) = + Abs n $ assert_total $ quote $ app n (wknEnv env (drop id)) t (Ntrl $ VVar 0 _ $ fromElem Here) quoteNtrl (VVar k n prf) = Var k n prf quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v) @@ -40,3 +52,49 @@ quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v) export normalise : {global : _} -> Env local global -> Term local -> Term global normalise env t = quote $ eval env t + +-- Conversion ------------------------------------------------------------------ + +export +convert : {ctx : Context} -> Value ctx -> Value ctx -> Bool +convertNtrl : {ctx : Context} -> Neutral ctx -> Neutral ctx -> Bool + +convert VSet VSet = True + +convert (VFunc env t u) (VFunc env' t' u') = + assert_total $ + convert (eval env t) (eval env' t') && + convert (eval env u) (eval env' u') +convert (VFunc env t u) (VPi m t' env' u') = + assert_total $ + convert (eval env t) t' && + convert (eval (wknEnv env (drop id)) u) (eval (liftEnv [<m] env') u') +convert (VPi n t env u) (VFunc env' t' u') = + assert_total $ + convert t (eval env' t') && + convert (eval (liftEnv [<n] env) u) (eval (wknEnv env' (drop id)) u') +convert (VPi n t env u) (VPi m t' env' u') = + convert t t' && + (assert_total $ convert (eval (liftEnv [<n] env) u) (eval (liftEnv [<n] env') $ renTerm Refl u')) + +convert (VAbs env n t) (VAbs env' m u) = + assert_total $ + convert (eval (liftEnv [<n] env) t) (eval (liftEnv [<n] env') $ renTerm Refl u) +convert (VAbs env n t) (Ntrl m) = + assert_total $ + convert + (eval (liftEnv [<n] env) t) + (Ntrl (VApp (wknNtrl m (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here))) +convert (Ntrl n) (VAbs env m t) = + assert_total $ + convert + (Ntrl (VApp (wknNtrl n (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here))) + (eval (liftEnv [<m] env) t) + +convert (Ntrl n) (Ntrl m) = convertNtrl n m + +convert _ _ = False + +convertNtrl (VVar k _ _) (VVar j _ _) = k == j +convertNtrl (VApp n v) (VApp m u) = convertNtrl n m && convert v u +convertNtrl _ _ = False diff --git a/src/CC/Term/Parse.idr b/src/CC/Term/Parse.idr index 3615956..5c8956a 100644 --- a/src/CC/Term/Parse.idr +++ b/src/CC/Term/Parse.idr @@ -4,40 +4,65 @@ import CC.Name import CC.Term import CC.Term.Raw +import Data.Bool import Data.List import Text.Lexer import Text.Parser +%hide Text.Parser.match + +-- Utilities ------------------------------------------------------------------- + +expandBindList : Functor f => (f (Maybe Name), RawTerm) -> f RawBinding +expandBindList (xs, t) = map (`Of` t) xs + -- Tokens ---------------------------------------------------------------------- data CCTokenKind = TIgnore + -- Variables | TIdent - -- Keywords + -- Let Syntax | TLet - -- Symbols + | TDef + | TSemi + -- Universes + | TSet + -- Abstraction + | TThinArrow | TLambda - | TPOpen - | TPClose | TComma | TFatArrow - | TDef - | TSemi + -- Symbols + | TUnderscore + | TColon + | TPOpen + | TPClose %name CCTokenKind k Eq CCTokenKind where TIgnore == TIgnore = True + TIdent == TIdent = True + TLet == TLet = True + TDef == TDef = True + TSemi == TSemi = True + + TSet == TSet = True + + TThinArrow == TThinArrow = True TLambda == TLambda = True - TPOpen == TPOpen = True - TPClose == TPClose = True TComma == TComma = True TFatArrow == TFatArrow = True - TDef == TDef = True - TSemi == TSemi = True + + TUnderscore == TUnderscore = True + TColon == TColon = True + TPOpen == TPOpen = True + TPClose == TPClose = True + _ == _ = False TokenKind CCTokenKind where @@ -45,15 +70,45 @@ TokenKind CCTokenKind where TokType _ = () tokValue TIgnore s = () + tokValue TIdent s = s + tokValue TLet s = () + tokValue TDef s = () + tokValue TSemi s = () + + tokValue TSet s = () + + tokValue TThinArrow s = () tokValue TLambda s = () - tokValue TPOpen s = () - tokValue TPClose s = () tokValue TComma s = () tokValue TFatArrow s = () - tokValue TDef s = () - tokValue TSemi s = () + + tokValue TUnderscore s = () + tokValue TColon s = () + tokValue TPOpen s = () + tokValue TPClose s = () + +Interpolation CCTokenKind where + interpolate TIgnore = "whitespace" + + interpolate TIdent = "identifier" + + interpolate TLet = #""let""# + interpolate TDef = #""=""# + interpolate TSemi = #"";""# + + interpolate TSet = #""Set""# + + interpolate TThinArrow = #""->""# + interpolate TLambda = #""\""# + interpolate TComma = #"",""# + interpolate TFatArrow = #""=>""# + + interpolate TUnderscore = #""_""# + interpolate TColon = #"":""# + interpolate TPOpen = #""(""# + interpolate TPClose = #"")""# export CCToken : Type @@ -68,47 +123,92 @@ identifier : Lexer identifier = alpha <+> many alphaNum keywords : List (String, CCTokenKind) -keywords = [("let", TLet)] +keywords = [("let", TLet), ("Set", TSet)] tokenMap : TokenMap CCToken tokenMap = + -- Ignored toTokenMap (map (, TIgnore) ignored) ++ + -- Identifiers [(identifier, \s => case lookup s keywords of Just kind => Tok kind s Nothing => Tok TIdent s) ] ++ toTokenMap [ + -- Abstraction + (exact "->", TThinArrow), (exact "\\", TLambda), (exact "\x03BB", TLambda), - (exact "(", TPOpen), - (exact ")", TPClose), (exact ",", TComma), (exact "=>", TFatArrow), + -- Symbols + (exact "_", TUnderscore), + (exact ":", TColon), + (exact "(", TPOpen), + (exact ")", TPClose), + -- Let syntax (has to be after fat arrow) (exact "=", TDef), (exact ";", TSemi) ] -- Parser ---------------------------------------------------------------------- +match : (kind : CCTokenKind) -> Grammar state CCToken True (TokType kind) +match k = terminal "expected \{k}" $ + \t => if t.kind == k then Just $ tokValue k t.text else Nothing + %tcinline parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty -parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t) +parens p = match TPOpen >> p >>= (\t => match TPClose *> pure t) parseIdent : Grammar state CCToken True Name parseIdent = MkName <$> (bounds $ match TIdent) +parseBinder : Grammar state CCToken True (Maybe Name) +parseBinder = either Just (const Nothing) <$> (parseIdent <||> match TUnderscore) + +%tcinline +withBounds : Grammar state CCToken True RawTerm -> Grammar state CCToken True RawTerm +withBounds p = Bounded <$> bounds p + +parseBindList : Grammar state CCToken True (List1 (Maybe Name)) +parseBindList = sepBy1 (match TComma) parseBinder + +parseAnnot : (commit : Bool) -> Grammar state CCToken True RawTerm +parseMaybeAnnot : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm) +parseAnnotArgs : (commit : Bool) -> Grammar state CCToken True (List1 (Maybe Name), RawTerm) +parseOptArrow : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm) + parseTerm : Grammar state CCToken True RawTerm +parsePi : Grammar state CCToken True RawTerm parseLambda : Grammar state CCToken True RawTerm parseLet : Grammar state CCToken True RawTerm +parseChain : Grammar state CCToken True RawTerm parseSpine : Grammar state CCToken True RawTerm parseAtom : Grammar state CCToken True RawTerm -parseTerm = parseLambda <|> parseLet <|> parseSpine +parseAnnot False = match TColon >> parseTerm +parseAnnot True = match TColon >> commit >> parseTerm + +parseMaybeAnnot b = Just <$> parseAnnot b <|> pure Nothing + +parseAnnotArgs b = [| MkPair parseBindList (parseAnnot b) |] + +parseOptArrow False = Just <$> (match TThinArrow >> parseTerm) <|> pure Nothing +parseOptArrow True = Just <$> (match TThinArrow >> commit >> parseTerm) <|> pure Nothing + +parseTerm = withBounds (parsePi <|> parseLambda <|> parseLet <|> parseChain) + +parsePi = do + dom <- parens (parseAnnotArgs False) + match TThinArrow + cod <- parseTerm + pure $ foldr1By Pi (flip Pi cod) $ expandBindList dom parseLambda = do match TLambda commit - names <- sepBy1 (match TComma >> commit) parseIdent + names <- parseBindList commit match TFatArrow commit @@ -120,19 +220,28 @@ parseLet = do commit n <- parseIdent commit + ty <- parseMaybeAnnot True match TDef commit t <- parseTerm match TSemi commit u <- parseTerm - pure $ Let n t u + pure $ Let n ty t u + +parseChain = do + spine <- parseSpine + maybeCod <- parseOptArrow True + pure $ case maybeCod of + Just cod => Pi (Nothing `Of` spine) cod + Nothing => spine parseSpine = foldl1 App <$> some parseAtom parseAtom = - (Var <$> parseIdent <* commit) <|> - (parens parseTerm) + withBounds (Var <$> parseIdent <* commit) <|> + withBounds (Set <$ match TSet <* commit) <|> + parens parseTerm parseSrc : Grammar state CCToken True RawTerm parseSrc = parseTerm <* eof diff --git a/src/CC/Term/Pretty.idr b/src/CC/Term/Pretty.idr index 04e3109..2b56e16 100644 --- a/src/CC/Term/Pretty.idr +++ b/src/CC/Term/Pretty.idr @@ -7,36 +7,46 @@ import Text.PrettyPrint.Prettyprinter -------------------------------------------------------------------------------- -startPrec, leftAppPrec, appPrec : Prec +startPrec, leftArrowPrec, leftAppPrec, appPrec : Prec startPrec = Open -leftAppPrec = Backtick +leftArrowPrec = Backtick +leftAppPrec = Open appPrec = App prettyVar : (ctx : Context) -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Doc ann prettyVar (_ :< n) 0 (Here eq) = pretty n prettyVar (ctx :< _) (S k) (There prf) = prettyVar ctx k prf -prettyTerm : {ctx : Context} -> Prec -> Term ctx -> Doc ann -prettyTerm d (Var k _ prf) = prettyVar ctx k prf -prettyTerm d (Abs n t) = - let (names, body) = mapFst (pretty n ::) $ getNames t in - parenthesise (d > startPrec) $ group $ - backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++> - pretty "=>" <+> softline <+> body - where - getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann) - getNames (Abs n t) = mapFst (pretty n ::) (getNames t) - getNames t = ([], prettyTerm startPrec t) -prettyTerm d (App t u) = - parenthesise (d >= appPrec) $ group $ - prettyTerm leftAppPrec t <++> prettyTerm appPrec u -prettyTerm d (Let n t u) = - parenthesise (d > startPrec) $ group $ align $ - pretty "let" <++> - (group $ align $ hang 2 $ pretty n <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+> - pretty ";" <+> line <+> - prettyTerm startPrec u - export {ctx : Context} -> Pretty (Term ctx) where - prettyPrec = prettyTerm + prettyPrec d (Var k n prf) = prettyVar ctx k prf + prettyPrec d (Let n Nothing val t) = + parenthesise (d > startPrec) $ group $ align $ + pretty "let" <++> + (group $ align $ hang 2 $ pretty n <++> equals <+> line <+> pretty val) <+> + pretty ";" <+> line <+> pretty t + prettyPrec d (Let n (Just ty) val t) = + parenthesise (d > startPrec) $ group $ align $ + pretty "let" <++> + (group $ align $ hang 2 $ + pretty n <++> colon <++> pretty ty <++> equals <+> line <+> pretty val) <+> + pretty ";" <+> line <+> pretty t + prettyPrec d Set = pretty "Set" + prettyPrec d (Pi Nothing dom cod) = + parenthesise (d > startPrec) $ group $ + prettyPrec leftArrowPrec dom <++> pretty "->" <++> pretty cod + prettyPrec d (Pi (Just n) dom cod) = + parenthesise (d > startPrec) $ group $ + parens (pretty n <++> colon <++> pretty dom) <++> pretty "->" <+> softline <+> pretty cod + prettyPrec d (Abs n t) = + let (names, body) = mapFst (pretty n ::) $ getNames t in + parenthesise (d > startPrec) $ group $ + backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++> + pretty "=>" <+> softline <+> body + where + getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann) + getNames (Abs n t) = mapFst (pretty n ::) (getNames t) + getNames t = ([], pretty t) + prettyPrec d (App t u) = + parenthesise (d >= appPrec) $ group $ + prettyPrec leftAppPrec t <++> prettyPrec appPrec u diff --git a/src/CC/Term/Raw.idr b/src/CC/Term/Raw.idr index 833daf5..10e74bb 100644 --- a/src/CC/Term/Raw.idr +++ b/src/CC/Term/Raw.idr @@ -6,15 +6,33 @@ import CC.Term import Data.DPair import Data.List1 +import Text.Bounded + -- Definition ------------------------------------------------------------------ public export -data RawTerm : Type where +data RawTerm : Type + +public export +record RawBinding where + constructor Of + name : Maybe Name + bound : RawTerm + +data RawTerm where + Bounded : WithBounds RawTerm -> RawTerm + Var : (n : Name) -> RawTerm - Abs : (n : Name) -> RawTerm -> RawTerm + + Let : Name -> Maybe RawTerm -> RawTerm -> RawTerm -> RawTerm + + Set : RawTerm + + Pi : RawBinding -> RawTerm -> RawTerm + Abs : (n : Maybe Name) -> RawTerm -> RawTerm App : RawTerm -> RawTerm -> RawTerm - Let : (n : Name) -> RawTerm -> RawTerm -> RawTerm +%name RawBinding bind %name RawTerm t, u -- Error Type ------------------------------------------------------------------ @@ -52,10 +70,3 @@ lookup (ctx :< m) n = case decEquiv n m of Yes eq => Ok (Element 0 (Here eq)) No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx n) - -export -translate : (ctx : Context) -> RawTerm -> NameError (Term ctx) -translate ctx (Var n) = (\p => Var p.fst n p.snd) <$> lookup ctx n -translate ctx (Abs n t) = pure (Abs n) <*> translate (ctx :< n) t -translate ctx (App t u) = [| App (translate ctx t) (translate ctx u) |] -translate ctx (Let n t u) = pure (Let n) <*> translate ctx t <*> translate (ctx :< n) u diff --git a/src/CC/Thinning.idr b/src/CC/Thinning.idr index 284a230..d1e7745 100644 --- a/src/CC/Thinning.idr +++ b/src/CC/Thinning.idr @@ -1,10 +1,12 @@ module CC.Thinning +import Data.Singleton + -- Definition ------------------------------------------------------------------ export data Thins : (src, tgt : SnocList a) -> Type where - IsEmpty : [<] `Thins` [<] + IsDone : [<] `Thins` [<] IsDrop : src `Thins` tgt -> src `Thins` tgt :< x IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x @@ -13,8 +15,8 @@ data Thins : (src, tgt : SnocList a) -> Type where -- Operations ------------------------------------------------------------------ export -empty : [<] `Thins` [<] -empty = IsEmpty +done : [<] `Thins` [<] +done = IsDone export drop : src `Thins` tgt -> src `Thins` tgt :< x @@ -25,15 +27,30 @@ keep : src `Thins` tgt -> src :< x `Thins` tgt :< x keep thin = IsKeep thin export +empty : {ctx : SnocList a} -> [<] `Thins` ctx +empty {ctx = [<]} = done +empty {ctx = _ :< _} = drop empty + +export id : {ctx : SnocList a} -> ctx `Thins` ctx -id {ctx = [<]} = empty +id {ctx = [<]} = done id {ctx = _ :< _} = keep id +export +id' : Singleton ctx -> ctx `Thins` ctx +id' (Val ctx) = id + +export +(++) : src1 `Thins` tgt1 -> src2 `Thins` tgt2 -> src1 ++ src2 `Thins` tgt1 ++ tgt2 +thin ++ IsDone = thin +thin ++ IsDrop thin' = IsDrop (thin ++ thin') +thin ++ IsKeep thin' = IsKeep (thin ++ thin') + -- Views ----------------------------------------------------------------------- public export data View : src `Thins` tgt -> Type where - Empty : View CC.Thinning.empty + Done : View CC.Thinning.done Drop : (thin : src `Thins` tgt) -> View (drop thin) Keep : (thin : src `Thins` tgt) -> View (keep thin) @@ -41,6 +58,6 @@ data View : src `Thins` tgt -> Type where public export view : (thin : src `Thins` tgt) -> View thin -view IsEmpty = Empty +view IsDone = Done view (IsDrop thin) = Drop thin view (IsKeep thin) = Keep thin diff --git a/src/Main.idr b/src/Main.idr index 2f05ccf..6f3fafe 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -2,6 +2,7 @@ module Main import CC.Name import CC.Term +import CC.Term.Elaborate import CC.Term.Eval import CC.Term.Parse import CC.Term.Pretty @@ -56,24 +57,36 @@ parseStdin = do helpMsg : String helpMsg = unlines [ - "usage: cc-eval [--help|nf]", + "usage: cc-check [--help|nf|type]", " --help : display this message", - " nf : read expression from stdin, print its normal form" + " nf : read & typecheck expression from stdin, print its normal form and type", + " type : read & typecheck expression from stdin, print its type" ] + + mainWith : IO (List String) -> IO RawTerm -> IO () mainWith getOpt getTerm = do - [_, "nf"] <- getOpt - | [_, "--help"] => putStrLn helpMsg - | _ => putErrLn helpMsg >> exitFailure - rawTerm <- getTerm - let Right term = runNameError $ translate [<] rawTerm - | Left errs => for_ errs putErr >> exitFailure - let nf : Term [<] = normalise [<] term - putDoc (pretty nf) + opts <- getOpt + case opts of + [_, "--help"] => putStrLn helpMsg + [_, "nf"] => do + rawTerm <- getTerm + let Right (t, ty) = runElabError $ inferTerm rawTerm + | Left errs => for_ errs putErr >> exitFailure + let nf : Term [<] = normalise [<] t + let ty = quote ty + putDoc (group $ pretty nf <++> colon <+> line <+> pretty ty) + [_, "type"] => do + rawTerm <- getTerm + let Right (t, ty) = runElabError $ inferTerm rawTerm + | Left errs => for_ errs putErr >> exitFailure + putDoc (group $ pretty $ quote ty) + _ => putErrLn helpMsg >> exitFailure where - putErr : Name -> IO () - putErr n = putBoundErrLn (bounds n) "undefined name: \{n}" + putErr : Either Name (String, Maybe Bounds) -> IO () + putErr (Left n) = putBoundErrLn (bounds n) "undefined name: \{n}" + putErr (Right (s, bounds)) = putBoundErrLn bounds s partial main : IO () |