nanoAgda 0.1.1 → 1.0.0
raw patch · 4 files changed
+25/−37 lines, 4 filesdep ~BNFC-meta
Dependency ranges changed: BNFC-meta
Files
- Normal.hs +13/−28
- Terms.hs +1/−0
- TypeCheckerNF.hs +9/−7
- nanoAgda.cabal +2/−2
Normal.hs view
@@ -11,30 +11,26 @@ data No data Ne-data Va type NF = Term No type Neutral = Term Ne-type Variable = Term Va-type NF' = (NF, NF) -- value, type. data Term n :: * where Neu :: Neutral -> NF- Var :: Variable -> Neutral- - Star :: Sort -> NF + Star :: Sort -> NF Pi :: Ident -> NF -> NF -> NF Lam :: Ident -> NF -> NF -> NF - App :: Neutral -> NF -> Neutral -- The sort is that of the argument.+ App :: Neutral -> NF -> Neutral Sigma :: Ident -> NF -> NF -> NF Pair :: Ident -> NF -> NF -> NF -- Pair does not bind any variable. Proj :: Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd. Irr String -> Neutral - V :: Int -> Variable -- deBruijn index - Hole :: String -> Variable+ V :: Int -> -- ^ deBruijn index + Neutral+ Hole :: String -> Neutral type Subst = [NF] @@ -42,9 +38,7 @@ deriving instance Show (Term n) var :: Int -> NF-var x = Neu $ var' x--var' x = Var $ V x+var x = Neu $ V x -- | Hereditary substitution subst0 :: NF -> NF -> NF@@ -53,18 +47,15 @@ subst :: Subst -> Term n -> NF subst f t = case t of Neu x -> s x- Var x -> s x- Star x -> Star x- Lam i ty bo -> Lam i (s ty) (s' bo)- (Pair i x y) -> Pair i (s x) (s y)+ Pair i x y -> Pair i (s x) (s y) Pi i a b -> Pi i (s a) (s' b) Sigma i a b -> Sigma i (s a) (s' b) (App a b) -> app (s a) (s b) (Proj x k f) -> proj (s x) k f- Hole x -> Neu $ Var $ Hole x- V x -> (f !! x)+ Hole x -> Neu $ Hole x+ V x -> f !! x where s,s' :: forall n. Term n -> NF s' = subst (var 0 : map wk f) s = subst f@@ -81,20 +72,16 @@ proj (Pair _ x y) False f = y proj (Neu x) k f = Neu (Proj x k f) +hole = Neu . Hole +-- | Weakening wkn :: Int -> NF -> NF wkn n = subst (map var [n..]) -wkdn :: Int -> Int -> NF -> NF-wkdn d n = subst (map var [0..d-1] ++ map var [d+n..])- wk = wkn 1-str = subst0 (Neu $ Var $ Hole "str: oops!") -wkv :: Int -> Variable -> Variable-wkv n (V x) = V (x + n)-wkv n (Hole x) = Hole x-+-- | Inverse of weakening+str = subst0 (Neu $ Hole "str: oops!") ----------------------------------- -- Display@@ -102,7 +89,6 @@ dec xs = [ x - 1 | x <- xs, x > 0] freeVars :: Term n -> [Int]-freeVars (Var x) = freeVars x freeVars (Neu x) = freeVars x freeVars (Pi _ a b) = freeVars a <> (dec $ freeVars b) freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b)@@ -123,7 +109,6 @@ | otherwise = s cPrint :: Int -> DisplayContext -> Term n -> Doc-cPrint p ii (Var x) = cPrint p ii x cPrint p ii (Neu x) = cPrint p ii x cPrint p ii (Hole x) = text x cPrint p ii (Star i) = pretty i
Terms.hs view
@@ -34,6 +34,7 @@ -- Type annotation. Not present in normal forms. Ann :: Term -> Term -> Term +-- | Position of a term, for error-reporting termPosition :: Term -> Irr Position termPosition (Hole p _) = p termPosition (Star p _) = p
TypeCheckerNF.hs view
@@ -10,6 +10,8 @@ -- -- are also used for this implementation. --+-- Additionally, this implementation performs evaluation to normal+-- form and type checking/inference at the same time. module TypeCheckerNF where @@ -69,8 +71,7 @@ -- FIXME: flag an error if impredicativity disabled and we use it anyway. -hole = Neu . Var . Hole-+-- | Infer a type and evaluate to normal form iType :: Context -> Term -> Result (Value,Type) iType g (Ann e tyt) = do (ty,o) <- iSort g tyt @@ -91,7 +92,7 @@ iType g e@(Terms.Bound _ 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+ val _ = var x -- We could do eta-expansion here: etaExpand (var x) typ Bind _ value typ = g `index` x iType g (Terms.Hole p x) = do@@ -130,12 +131,13 @@ (ve,t) <- iType (Bind x Abstract vty <| g) e return $ (Lam x vty ve, Pi x vty t) +-- | Infer a sort, and normalise iSort :: Context -> Term -> Result (Type,Sort) iSort g e = do (val,v) <- iType g e case v of Star i -> return (val,i)- (Neu (Var (Hole h))) -> do + (Neu (Hole h)) -> do report $ text h <+> "must be a type" return $ (hole h, Sort 1) _ -> throwError (e,displayT g e <+> "is not a type")@@ -147,8 +149,8 @@ constraint = report $ vcat ["constraint: " <> display g q', "equal to : " <> display g q] case (q,q') of- ((Neu (Var (Hole _))), t) -> constraint- (t, Neu (Var (Hole _))) -> constraint+ ((Neu (Hole _)), t) -> constraint+ (t, Neu (Hole _)) -> constraint _ -> unless (q == q') (throwError (e,hang "type mismatch: " 2 $ vcat ["inferred:" <+> display g q',@@ -156,7 +158,7 @@ "for:" <+> displayT g e , "context:" <+> dispContext g])) --- Check the type and normalize+-- | Check the type and normalize cType :: Context -> Term -> Type -> Result Value cType g (Terms.Lam name (Terms.Hole _ _) e) (Pi name' ty ty') = do e' <- cType (Bind name Abstract ty <| g) e ty'
nanoAgda.cabal view
@@ -1,5 +1,5 @@ name: nanoAgda-version: 0.1.1+version: 1.0.0 category: Dependent Types synopsis: A toy dependently-typed language description:@@ -39,7 +39,7 @@ build-depends: containers==0.4.* build-depends: pretty==1.1.* build-depends: parsec==2.1.*- build-depends: BNFC-meta==0.2.*+ build-depends: BNFC-meta==0.3.* build-depends: transformers == 0.2.* build-depends: mtl == 2.0.*