uAgda 1.1.0.0 → 1.2.0.0
raw patch · 15 files changed
+664/−680 lines, 15 filesdep +arraydep +mtldep +splitdep −monads-fddep ~BNFC-metadep ~containers
Dependencies added: array, mtl, split
Dependencies removed: monads-fd
Dependency ranges changed: BNFC-meta, containers
Files
- AbsSynToTerm.hs +60/−31
- Basics.hs +62/−35
- Display.hs +11/−6
- Main.hs +3/−3
- Normal.hs +216/−266
- Options.hs +7/−4
- RawSyntax.hs +29/−19
- Terms.hs +48/−43
- TypeCheckerNF.hs +158/−99
- tutorial/01-Module.ua +2/−2
- tutorial/02.1-Relevance.ua +0/−60
- tutorial/03-Parametricity.ua +18/−16
- tutorial/03.1-Parametricity-Use.ua +43/−8
- tutorial/04-Data.ua +0/−75
- uAgda.cabal +7/−13
AbsSynToTerm.hs view
@@ -5,15 +5,17 @@ import Terms import qualified RawSyntax as A import RawSyntax (Identifier(..))-import "transformers" Control.Monad.Trans.State (runStateT, StateT)-import "transformers" Control.Monad.Trans.Reader-import "transformers" Control.Monad.Trans.Error hiding (throwError)-import "monads-fd" Control.Monad.Error-import "monads-fd" Control.Monad.State+import Control.Monad.Trans.State (runStateT, StateT)+import Control.Monad.Trans.Reader+import Control.Monad.Trans.Error hiding (throwError)+import Control.Monad.Error+import Control.Monad.State import Control.Applicative import Data.Functor.Identity import Data.List import Basics+import Permutation+import Data.List.Split type LocalEnv = [String] type GlobalEnv = ()@@ -26,12 +28,12 @@ Left err -> error err Right a -> fst a -look :: Identifier -> Resolver Term-look (ident@(Identifier (position,x))) = do+look :: BitVector -> Identifier -> Resolver Term+look bv (ident@(Identifier (position,x))) = do e <- ask case elemIndex x e of Nothing -> throwError ("unknown identifier: " ++ show ident)- Just x -> return $ Bound (Irr position) x+ Just x -> return $ Bound (Irr position) bv x insertVar :: Identifier -> LocalEnv -> LocalEnv insertVar (Identifier (_pos,x)) e = x:e@@ -40,52 +42,79 @@ dummyVar = Identifier ((0,0),"_") -manyDep binder a [] b = resolveTerm b-manyDep binder a (x:xs) b = binder (Irr x) <$> resolveTerm a <*> local (insertVar x) (manyDep binder a xs b)+manyDep o binder a [] b = resolveTerm b+manyDep o binder a (x:xs) b = binder (Irr x) <$> resolveMulti o a <*> local (insertVar x) (manyDep o binder a xs b) manyLam :: [A.Bind] -> A.Exp -> Resolver Term manyLam [] b = resolveTerm b-manyLam (A.NoBind (A.AIdent x):xs) b = Lam (Irr x) (Hole dummyPosition "") <$> local (insertVar x) (manyLam xs b)-manyLam (A.Bind (A.AIdent x) t:xs) b = Lam (Irr x) <$> resolveTerm t <*> local (insertVar x) (manyLam xs b)+manyLam (A.NoBind (A.AIdent x):xs) b = Lam Regu (Irr x) (unit $ Hole dummyPosition "") <$> local (insertVar x) (manyLam xs b)+manyLam (A.Bind (A.AIdent x) (A.Colon o) t:xs) b = Lam (toBnd o) (Irr x) <$> resolveMulti (toBnd o) t <*> local (insertVar x) (manyLam xs b) +toBnd ":" = Regu+toBnd "::" = Pred extractVars :: A.Exp -> Resolver [Identifier] extractVars (A.EVar (A.AIdent i)) = return [i] extractVars (A.EApp (A.EVar (A.AIdent i)) rest) = (i:) <$> extractVars rest extractVars _ = throwError "list of variables expected" +trailingHole Regu xs = xs+trailingHole Pred xs = xs ++ [Hole (Irr (0,0)) "⊘"]++resolveMulti :: Binder -> A.Exp -> Resolver (Cube Term)+resolveMulti o t = do+ xs <- trailingHole o <$> resolveMulti' t+ case cubeFromList xs of+ Just c -> return c+ Nothing -> throwError "incomplete cube"++resolveMulti' :: A.Exp -> Resolver [Term]+resolveMulti' (A.EMulti xs) = mapM resolveTerm xs+resolveMulti' x = (:[]) <$> resolveTerm x+ resolveTerm :: A.Exp -> Resolver Term-resolveTerm (A.EDestr x (A.Natural n)) = Destroy (read n) <$> resolveTerm x+resolveTerm (A.EMulti _) = throwError "expression list only allowed in some contexts"+-- resolveTerm (A.EDestr x (A.Natural n)) = Destroy (read n) <$> resolveTerm x resolveTerm (A.EHole (A.Hole (p,x))) = return $ Hole (Irr p) x resolveTerm (A.EParam x) = Param <$> resolveTerm x-resolveTerm (A.EUp x) = Shift (Sort 1) <$> resolveTerm x-resolveTerm (A.EVar (A.AIdent x)) = look x-resolveTerm (A.ESet (A.Sort (p,"#"))) = return $ Star (Irr p) $ Sort (-1)-resolveTerm (A.ESet (A.Sort (p,'*':s))) = return $ Star (Irr p) $ Sort (read ('0':s))-resolveTerm (A.EProj x (A.AIdent (Identifier (_,field)))) = Proj <$> resolveTerm x <*> pure field-resolveTerm (A.EExtr x (A.AIdent (Identifier (_,field)))) = Extr <$> resolveTerm x <*> pure field-resolveTerm (A.EApp f x) = (:$:) <$> resolveTerm f <*> resolveTerm x+resolveTerm (A.ESwap x (A.Permutation ('#':p))) = Swap (permFromString p) <$> resolveTerm x+-- resolveTerm (A.EUp x) = Shift (Sort 1) <$> resolveTerm x+resolveTerm (A.EVar (A.AIdent x)) = look nil x+resolveTerm (A.EVarI (A.AIdent x) (A.Natural ix)) = look (bvFromString ix) x+resolveTerm (A.ESet (A.Sort (p,c:s))) = return $ Star (Irr p) $ Sort level (read ('0':dim))+ where (lev:dim:_) = splitOn "|" s ++ [""]+ level = case c of+ '#' -> (-1)+ '*' -> read ('0':lev)+resolveTerm (A.EProj x (A.AIdent (Identifier (_,field)))) = Proj True <$> resolveTerm x <*> pure field+resolveTerm (A.EExtr x (A.AIdent (Identifier (_,field)))) = Proj False <$> resolveTerm x <*> pure field+resolveTerm (A.EApp f x) = App Regu <$> resolveTerm f <*> resolveMulti Regu x+resolveTerm (A.EAppP f x) = App Pred <$> resolveTerm f <*> resolveMulti Pred x resolveTerm (A.ESigma a b) = case a of- (A.EAnn vars a') -> do vs <- extractVars vars- manyDep Sigma a' vs b+ (A.EAnn vars colon a') -> do+ vs <- extractVars vars+ manyDep Regu (\i a b -> Sigma i (a!?nil) b) a' vs b (A.EAbs _ _ _) -> throwError "cannot use lambda for type" _ -> Sigma (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b) -resolveTerm (A.EPi a arrow b) = case a of- (A.EAnn vars a') -> do vs <- extractVars vars- manyDep (Pi o) a' vs b+resolveTerm (A.EPi a (A.Arrow arrow) b) = case a of+ (A.EAnn vars (A.Colon colon) a') -> do + vs <- extractVars vars+ manyDep o (Pi o) a' vs b (A.EAbs _ _ _) -> throwError "cannot use lambda for type"- _ -> Pi o (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)- where o = case arrow of - A.Arrow "=>" -> Ir- A.Arrow "->" -> Re-resolveTerm (A.EAbs ids _arrow_ b) = manyLam ids b+ _ -> Pi o (Irr dummyVar) <$> resolveMulti o a <*> local (insertVar dummyVar) (resolveTerm b)++ where o = case arrow of+ "->" -> Regu+ "=>" -> Pred++resolveTerm (A.EAbs ids _ b) = manyLam ids b resolveTerm (A.EPair (A.Decl (A.AIdent i) e) rest) = Pair (Irr i) <$> resolveTerm e <*> local (insertVar i) (resolveTerm rest) resolveTerm (A.EPair (A.PDecl (A.AIdent i) e t) rest) = Pair (Irr i) <$> (Ann <$> (OfParam (Irr i) <$> resolveTerm e) <*> resolveTerm t) <*> local (insertVar i) (resolveTerm rest) -resolveTerm (A.EAnn e1 e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2+resolveTerm (A.EAnn e1 _colon_ e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2
Basics.hs view
@@ -4,12 +4,12 @@ module Control.Applicative, Irr(..), Sort(..),- above, oneLev, zero, Ident, Identifier(..), DisplayContext, Position, dummyPosition, identPosition, isDummyId, modId, synthId, dummyId, idString,- Relevance(..), arrow, colon,- Lattice(..)) where+ Binder(..), arrow, colon, cross, appl, comm,+ Lattice(..), above,+ module Cubes) where import Display import qualified RawSyntax as A@@ -17,16 +17,13 @@ import Control.Applicative import Data.Monoid import Data.Sequence (Seq)---(<>) :: Monoid a => a -> a -> a-(<>) = mappend+import Cubes ----------- -- Irr newtype Irr a = Irr {fromIrr :: a}- deriving Show+ deriving (Show,Monoid) instance Eq (Irr a) where x == y = True@@ -39,14 +36,19 @@ instance Pretty Identifier where pretty (Identifier (_,x)) = text x +instance Monoid Identifier where+ Identifier (p,t1) `mappend` Identifier (_,t2) = Identifier (p, t1 <> t2)+ mempty = Identifier (fromIrr dummyPosition,"") type Ident = Irr Identifier -isDummyId (Irr (Identifier (_,"_"))) = True-isDummyId _ = False +isDummyIdS ('_':x) = True+isDummyIdS _ = False +isDummyId (Irr (Identifier (_,xs))) = isDummyIdS xs+ synthId :: String -> Ident-synthId x = Irr (Identifier (fromIrr $ dummyPosition,x))+synthId x = Irr (Identifier (fromIrr dummyPosition,x)) dummyId = synthId "_" @@ -67,51 +69,76 @@ modId :: (String -> String) -> Ident -> Ident modId f (Irr (Identifier (pos ,x))) = (Irr (Identifier (pos,f x))) -------------------+-------+----------- -- Sort -instance Lattice Int where- (⊔) = max -data Relevance = Re | Ir- deriving (Enum,Ord,Eq,Show)+instance Lattice Int where -- Lattice is a misnomer here.+ x ⊔ (-1) = (-1)+ x ⊔ y = max x y +data Binder = Pred | Regu+ deriving (Ord,Eq,Show)+ class Lattice a where (⊔) :: a -> a -> a +-- instance Ord Sort where+-- compare (Sort x) (Sort y) = compare x y -newtype Sort = Sort {sortLevel :: Int}- deriving (Eq,Num)+data Sort = Sort {sortLevel :: Int,+ sortDimension :: Int}+ deriving (Eq) instance Lattice Sort where- x ⊔ Sort (-1) = Sort (-1) -- is this a lattice? - Sort x ⊔ Sort y = Sort (x ⊔ y)+ Sort x m ⊔ Sort y n = Sort (x ⊔ y) (min m n)+ instance Show Sort where show s = render (pretty s) -instance Pretty Relevance where- pretty (Re) = mempty- pretty (Ir) = "÷"+instance Pretty Binder where+ pretty = colon instance Pretty Sort where- pretty s = prettyLev s- + pretty (Sort s d) = showLev <> showDim++ where showDim = case d of+ 0 -> mempty+ _ -> superscriptPretty d+ showLev = case s of+ (-1) -> "□"+ 0 -> star+ l -> star <> subscriptPretty l+ ++above (Sort s n) = Sort (s+1) n + star = "∗" -- ⋆★*∗ -prettyLev (Sort (-1) ) = "□"-prettyLev (Sort 0 ) = star <> mempty-prettyLev (Sort l ) = star <> subscriptPretty l -above (Sort l) = Sort (l + 1)-oneLev = Sort 1+arrow, colon, cross, comm, appl :: Binder -> Doc -zero = Sort 0+arrow Pred = "⇛"+arrow Regu = "→"+-- ⟴ -arrow Ir = "⇒"-arrow Re = "→"+colon Regu = text ":"+colon Pred = text "::"+-- :⋮∷∴∵ -colon Ir = text "÷" -colon Re = text "∶" ++cross Regu = "×" +cross Pred = "⋇" +-- ⊗⊠+-- ⚔⤬⤫⨯++comm Pred = "⍮"+comm Regu = ","+++appl Regu = "" +appl Pred = "· "
Display.hs view
@@ -1,22 +1,26 @@ {-# LANGUAGE PackageImports, GADTs, KindSignatures, StandaloneDeriving, EmptyDataDecls, FlexibleInstances, OverloadedStrings #-} module Display (Pretty(..), Doc, ($$), (<+>), text, hang, vcat, parensIf, sep, comma, nest, parens,- subscriptPretty, superscriptPretty, subscriptShow, render) where+ subscriptPretty, superscriptPretty, subscriptShow, punctuate, render, module Data.Monoid, (Display.<>)) where import GHC.Exts( IsString(..) ) import Prelude hiding (length, reverse)-import Text.PrettyPrint.HughesPJ +import Text.PrettyPrint.HughesPJ hiding ((<>))+import qualified Text.PrettyPrint.HughesPJ import Numeric (showIntAtBase) import Control.Arrow (second)-import "monads-fd" Control.Monad.Error+import Control.Monad.Error import Data.Monoid import Data.Sequence hiding (empty) import Data.Foldable +(<>) :: Monoid a => a -> a -> a+(<>) = mappend+ instance Monoid Doc where mempty = empty- mappend = (<>)+ mappend = (Text.PrettyPrint.HughesPJ.<>) class Pretty a where pretty :: a -> Doc@@ -24,6 +28,9 @@ instance Pretty x => Pretty [x] where pretty x = brackets $ sep $ punctuate comma (map pretty x) +instance (Pretty a,Pretty b) => Pretty (a,b) where+ pretty (a,b) = parens $ pretty a <> comma <+> pretty b + instance IsString Doc where fromString = text @@ -44,8 +51,6 @@ subscriptShow :: Int -> String subscriptShow = scriptShow "-₀₁₂₃₄₅₆₇₈₉"-- parensIf :: Bool -> Doc -> Doc parensIf True = parens
Main.hs view
@@ -23,11 +23,11 @@ import qualified Data.Sequence as S -import Language.LBNF(Err(..))+import Language.LBNF.Runtime (ParseMonad(..)) -- type ParseFun a = [Token] -> Err a -myLLexer = myLexer+myLLexer = tokens -- myLexer type Verbosity = Int @@ -61,7 +61,7 @@ [] -> return () _ -> putStrV 0 $ vcat info -- display constraints, etc. case checked of- Right (a,b) -> do + Right (a,b,_) -> do putStrV 0 $ "nf =" <+> pretty a putStrV 0 $ "ty =" <+> pretty b {-
Normal.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs, KindSignatures, OverloadedStrings, EmptyDataDecls, StandaloneDeriving, TypeSynonymInstances, TypeFamilies, MultiParamTypeClasses #-}+{-# LANGUAGE GADTs, KindSignatures, OverloadedStrings, EmptyDataDecls, StandaloneDeriving, TypeSynonymInstances, TypeFamilies, MultiParamTypeClasses, ViewPatterns, RankNTypes #-} module Normal where import Prelude hiding (length,elem,foldl)@@ -8,6 +8,8 @@ import Control.Arrow (first, second) import Data.Sequence hiding (zip,replicate,reverse) import Options+import qualified Data.List as L+import Permutation data No data Ne@@ -18,42 +20,39 @@ type Variable = Term Va type NF' = (NF, NF) -- value, type. +data Role = Index | Thing deriving (Eq, Show)++showRole Index = "?"+showRole Thing = "!"+ data Term n :: * where Neu :: Neutral -> NF Var :: Variable -> Neutral Star :: Sort -> NF - Pi :: Relevance -> Ident -> NF -> NF -> NF- Lam :: Relevance -> Ident -> NF -> NF -> NF - App :: Relevance -> Neutral -> NF -> Neutral -- The sort is that of the argument.+ Pi :: Binder -> Ident -> Cube NF -> NF -> NF+ Lam :: Binder -> Ident -> Cube NF -> NF -> NF + App :: Binder -> Neutral -> Cube NF -> Neutral -- The sort is that of the argument. - Sigma :: Relevance -> Ident -> NF -> NF -> NF- Pair :: Relevance -> Ident -> NF -> NF -> NF -- Pair does not bind any variable.- Proj :: Relevance -> -- ^ Sort of the argument (only needed for+ Sigma :: Binder -> Ident -> NF -> NF -> NF+ Pair :: Binder -> Ident -> NF -> NF -> NF -- Pair does not bind any variable.+ Proj :: Binder -> -- ^ Sort of the argument (only needed for -- the 1st projection: 2nd projection does -- not change relevance) Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.- Irr String -> Neutral + Ident -> Neutral - OfParam :: Ident -> NF -> Neutral+ -- OfParam :: Ident -> NF -> Neutral - Destr :: Int -> Variable -> Variable -- argument: depth where destruction occurs.- Param :: Variable -> Variable - V :: Sort -> Int -> Variable -- shift, deBruijn + -- Destr :: Int -> Variable -> Variable -- argument: depth where destruction occurs.+ Swap :: Permutation -> Variable -> Variable+ Param :: Role {-TODO: Maybe the swap should be merged into the role -} -> Variable -> Variable + V :: BitVector -> Int -> Variable -- shift, deBruijn Hole :: String -> Variable -etaExpand :: Relevance -> Neutral -> NF -> NF-etaExpand o' v (Pi o i a b) = Lam o i a (etaExpand o' (App o (wkne 1 v) - $ etaExpand o (var' 0) a) b)-etaExpand o' v (Sigma o i a b) = Pair o i (etaExpand o (Proj o' v True (Irr $ idString i)) a) - (etaExpand o' (Proj o' v False (Irr $ idString i)) b)-etaExpand o' v _ = Neu v----type Subst = [NF]+type Subst = [Cube NF] deriving instance Eq (Term n) deriving instance Show (Term n)@@ -61,16 +60,16 @@ var :: Int -> NF var x = Neu $ var' x -var'' = V (Sort 0)+var'' = V nil -var' x = Var $ V (Sort 0) x+var' x = Var $ V nil x -- | Hereditary substitution-subst0 :: NF -> NF -> NF-subst0 u = subst (u:map (var) [0..]) +subst0 :: Cube NF -> NF -> NF+subst0 u = subst (u:map (unit . var) [0..]) -showShift (Sort l) = replicate l '^' +hole = Neu . Var . Hole subst :: Subst -> Term n -> NF subst f t = case t of@@ -79,144 +78,65 @@ Star x -> Star x - Lam o i ty bo -> Lam o i (s ty) (s' bo)+ Lam o i ty bo -> Lam o i (fmap s ty) (s' bo) (Pair o i x y) -> Pair o i (s x) (s y)- Pi o i a b -> Pi o i (s a) (s' b)+ Pi o i a b -> Pi o i (fmap s a) (s' b) Sigma o i a b -> Sigma o i (s a) (s' b)- (App o a b) -> app o (s a) (s b)+ (App o a b) -> app o (s a) (fmap s b) (Proj o x k f) -> proj o (s x) k f - OfParam i x -> Neu (OfParam i (s x))+-- OfParam i x -> Neu (OfParam i (s x)) - Destr d x -> destroy d (s x)- Hole x -> Neu $ Var $ Hole x- V s x -> shift s (f !! x)- Param x -> param (s x)- where s' = subst (var 0 : map wk f)+-- Destr d x -> destroy d (s x)+ Hole x -> hole x+ V bv x -> let fx = f!!x in+ case cubeElems fx of + [Neu (Var (V bv' y))] -> Neu $ Var $ V (bv' <> bv) y+ _ | dim (f !! x) /= bvDim bv -> hole $ "error: variable access dim " ++ show (bvDim bv) ++ " expected " ++ show (dim (f!!x))+ _ -> (f !! x) !? bv + Param r x -> param r (s x)+ Swap q x -> swap q (s x)+ where s,s' :: forall n. Term n -> NF+ s' = subst (unit (var 0) : map (cmap wk) f) s = subst f ---- Double renaming substitution--- 1st component: regular; 2nd component: param-subst2 :: [(NF,NF)] -> Term n -> NF-subst2 f t = case t of- Neu x -> s x- Var x -> s x- - Star x -> Star x- - Lam o i ty bo -> Lam o i (s ty) (s' bo)- (Pair o i x y) -> Pair o i (s x) (s y)- Pi o i a b -> Pi o i (s a) (s' b)- Sigma o i a b -> Sigma o i (s a) (s' b)- (App o a b) -> app o (s a) (s b)- (Proj o x k f) -> proj o (s x) k f-- OfParam i x -> Neu (OfParam i (s x))- - Hole x -> Neu $ Var $ Hole x- V s x -> shift s (fst $ f !! x)- Param (V s x) -> shift s (snd $ f !! x)- Destr d x -> destroy d (s x)- Param x -> param (s x)- where s' = subst2 ((var 0, param $ var 0) : map (both wk) f)- s = subst2 f---subst2d :: Int -> (NF,NF) -> Term n -> NF-subst2d d u = subst2 $ [(var i,param $ var i) | i <- [0..d-1]] ++ u : - [(var i,param $ var i) | i <- [d..]]---{--subst' :: [(Variable,Variable)] -> Term n -> Term n-subst' f t = case t of- Neu x -> Neu (s x)- Var x -> Var (s x)- - Star x -> Star x- - Lam o i ty bo -> Lam o i (s ty) (s' o bo)- (Pair o i x y) -> Pair o i (s x) (s y)- Pi o i a b -> Pi o i (s a) (s' o b)- Sigma o i a b -> Sigma o i (s a) (s' o b)- (App o a b) -> App o (s a) (s b)- (Proj o x k f) -> Proj o (s x) k f-- OfParam i x -> OfParam i (s x)- - Hole x -> Hole x- V s x -> shift s (fst $ f !! x)- Param (V s x) -> shift s (snd $ f !! x)- Param x -> Param (s x)- where s' o = subst' (p f)- s = subst' f- p xs = (V zero 0, Param $ V zero 0) : map (both $ wkv 1) xs--} - both f (x,y) = (f x, f y) -shift' :: Int -> Sort -> Term n -> Term n-shift' n d t = case t of- Neu x -> Neu $ s x- Var x -> Var (s x)- - Star o -> Star (o + d)- - Lam o i ty bo -> Lam o i (s ty) (s' bo)- (Pair o i x y) -> Pair o i (s x) (s y)- Pi o i a b -> Pi o i (s a) (s' b)- Sigma o i a b -> Sigma o i (s a) (s' b)- (App o a b) -> App o (s a) (s b)- (Proj o x k f) -> Proj o (s x) k f- - OfParam i x -> OfParam (modId (++showShift d) i) (s x)-- Hole x -> Hole x- Param x -> Param (s x)- V s x | x < n -> V s x- | x >= n -> V (s + d) x- where s = shift' n d- s' = shift' (1 + n) d--shift = shift' 0- ----------------------------- -- Hereditary operations- -app :: Relevance -> NF -> NF -> NF ++app :: Binder -> NF -> Cube NF -> NF +app Pred x u | dim u == 0 = x app _ (Lam _ i _ bo) u = subst0 u bo app o (Neu n) u = Neu (App o n u) -proj :: Relevance -> NF -> Bool -> Irr String -> NF+-- TODO: merge App Pred's++proj :: Binder -> NF -> Bool -> Ident -> NF proj _ (Pair _ _ x y) True f = x proj _ (Pair _ _ x y) False f = y proj o (Neu x) k f = Neu (Proj o x k f) wkn :: Int -> NF -> NF-wkn n = subst (map var [n..])+wkn = wkdn 0 wkdn :: Int -> Int -> NF -> NF-wkdn d n = subst (map var [0..d-1] ++ map var [d+n..])+wkdn d n = subst (map (unit . var) [0..d-1] ++ map (unit . var) [d+n..]) wk = wkn 1-str = subst0 (Neu $ Var $ Hole "str: oops!")+str = strn 1+strn n = subst (replicate n (unit $ Neu $ Var $ Hole "str: oops!") ++ map (unit . var) [0..]) wkv :: Int -> Variable -> Variable-wkv n (Param x) = Param (wkv n x)+wkv n (Param r x) = Param r (wkv n x)+wkv n (Swap q x) = Swap q (wkv n x) wkv n (V s x) = V s (x + n) wkv n (Hole x) = Hole x -wkne :: Int -> Neutral -> Neutral-wkne n (Var x) = Var (wkv n x)-wkne n (App o a b) = App o (wkne n a) (wkn n b)-wkne n (Proj o a k f) = Proj o (wkne n a) k f-wkne n (OfParam i a) = OfParam i (wkn n a) --param :: NF -> NF-param t = transNF 0 t+param :: Role -> NF -> NF+param r = transNF r noAction -----------------------------------@@ -224,206 +144,236 @@ dec xs = [ x - 1 | x <- xs, x > 0] +allFreeVars :: Cube (Term n) -> [Int]+allFreeVars = L.concat . fmap freeVars . cubeElems+ freeVars :: Term n -> [Int] freeVars (Var x) = freeVars x-freeVars (Destr _ x) = freeVars x+--freeVars (Destr _ x) = freeVars x freeVars (Neu x) = freeVars x-freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (Pi _ _ a b) = allFreeVars a <> (dec $ freeVars b) freeVars (Sigma _ _ a b) = freeVars a <> (dec $ freeVars b) freeVars (V _ x) = [x]-freeVars (App _ a b) = freeVars a <> freeVars b-freeVars (Lam _ _ ty b) = freeVars ty <> (dec $ freeVars b)+freeVars (App _ a b) = freeVars a <> allFreeVars b+freeVars (Lam _ _ ty b) = allFreeVars ty <> (dec $ freeVars b) freeVars (Star _) = mempty freeVars (Hole _) = mempty freeVars (Pair _ _ x y) = freeVars x <> freeVars y freeVars (Proj _ x _ _) = freeVars x-freeVars (Param x) = freeVars x-freeVars (OfParam _ x) = freeVars x+freeVars (Param _ x) = freeVars x+freeVars (Swap _ x) = freeVars x+-- freeVars (OfParam _ x) = freeVars x iOccursIn :: Int -> Term n -> Bool iOccursIn x t = x `elem` (freeVars t) +allocName :: DisplayContext -> Ident -> Ident+allocName g s + | fromIrr s `elem` (fmap fromIrr g) = allocName g (modId (++ "'") s)+ | otherwise = s++printIndex :: DisplayContext -> Int -> Doc+printIndex ii k + | k < 0 || k >= length ii = text "<deBrujn index" <+> pretty k <+> text "out of range>"+ | otherwise = pretty (ii `index` k)+ cPrint :: Int -> DisplayContext -> Term n -> Doc+cPrint p ii (Swap q x) = cPrint p ii x <> "#" <> pretty q cPrint p ii (Var x) = cPrint p ii x cPrint p ii (Neu x) = cPrint p ii x-cPrint p ii (Param x) = cPrint p ii x <> "!"-cPrint p ii (Destr d x) = cPrint p ii x <> "%" <> pretty d-cPrint p ii (OfParam i x) = pretty i+cPrint p ii (Param r x) = cPrint p ii x <> text (showRole r)+-- cPrint p ii (Destr d x) = cPrint p ii x <> "%" <> pretty d+-- cPrint p ii (OfParam i x) = pretty i -- "⌊" <> cPrint (-1) ii x <> "⌋" cPrint p ii (Hole x) = text x cPrint p ii (Star i) = pretty i-cPrint p ii (V o@(Sort l) k) - | k < 0 || k >= length ii = text "<deBrujn index" <+> pretty k <+> text "out of range>"- | otherwise = pretty (ii `index` k) <> shft- where shft = text (showShift o)-cPrint p ii (Proj o x k (Irr f)) = cPrint p ii x <> sss (pretty o) <> (if k then "." <> text f else "/")-cPrint p ii t@(App _ _ _) = let (fct,args) = nestedApp t in - parensIf (p > 3) (cPrint 3 ii fct <+> sep [ sss (pretty o <> "· ") <> cPrint 4 ii a | (o,a) <- args]) +cPrint p ii (V bv k) = printIndex ii k <> (mconcat $ map subscriptPretty $ map b2i $ bits bv)+cPrint p ii (Proj o x k (Irr f)) = cPrint p ii x <> (if k then "." <> pretty f else "/")+cPrint p ii t@(App _ _ _) = parensIf (p > 3) (cPrint 3 ii fct <+> sep [appl o <> printCube o 4 ii a | (o,a) <- args]) + where (fct,args) = nestedApp t cPrint p ii t@(Pi _ _ _ _) = parensIf (p > 1) (printBinders arrow ii mempty $ nestedPis t) cPrint p ii t@(Sigma _ _ _ _) = parensIf (p > 1) (printBinders cross ii mempty $ nestedSigmas t) cPrint p ii (t@(Lam _ _ _ _)) = parensIf (p > 1) (nestedLams ii mempty t)-cPrint p ii (Pair _ name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comma,+cPrint p ii (Pair o name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comm o, cPrint (-1) ii y]) -cross Ir = "⤬" -- ⚔⤬⤫⨯-cross Re = "×" -- ×⨯--nestedPis :: NF -> ([(Ident,Bool,NF,Relevance)], NF)+nestedPis :: NF -> ([(Ident,Bool,Cube NF,Binder)], NF) nestedPis (Pi o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedPis b) nestedPis x = ([],x) -nestedSigmas :: NF -> ([(Ident,Bool,NF,Relevance)], NF)-nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedSigmas b)+nestedSigmas :: NF -> ([(Ident,Bool,Cube NF,Binder)], NF)+nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,unit a,o)] ++)) (nestedSigmas b) nestedSigmas x = ([],x) -printBinders :: (Relevance -> Doc) -> DisplayContext -> Seq Doc -> ([(Ident,Bool,NF,Relevance)], NF) -> Doc-printBinders sep ii xs (((i,occurs,a,o):pis),b) = printBinders sep (i <| ii) (xs |> (printBind' ii i occurs a o <+> sss (pretty o) <> sep o)) (pis,b)+printBinders :: (Binder -> Doc) -> DisplayContext -> Seq Doc -> ([(Ident,Bool,Cube NF,Binder)], NF) -> Doc+printBinders sep ii xs (((x,occurs,a,o):pis),b) = printBinders sep (i <| ii) (xs |> (printBind' ii i occurs a o <+> sep o)) (pis,b)+ where i = allocName ii x printBinders _ ii xs ([],b) = sep $ toList $ (xs |> cPrint 1 ii b) nestedLams :: DisplayContext -> Seq Doc -> Term n -> Doc-nestedLams ii xs (Lam o x ty c) = nestedLams (x <| ii) (xs |> parens (sss (pretty o) <> pretty x <+> colon o <+> cPrint 0 ii ty)) c+nestedLams ii xs (Lam o x ty c) = nestedLams (i <| ii) (xs |> parens (pretty i <+> colon o <+> printCube o 0 ii ty)) c+ where i = allocName ii x nestedLams ii xs t = (text "\\ " <> (sep $ toList $ (xs |> "->")) <+> nest 3 (cPrint 0 ii t)) +printCube :: Binder -> Int -> DisplayContext -> Cube (Term n) -> Doc+printCube o p ii d | dim d == 0 = cPrint p ii (d !? nil)+ | otherwise = "{" <> sep (punctuate ";" [(if showIndices options then pretty i <> "↦" else mempty ) <>+ cPrint 0 ii x | (i,x) <- adjust $ cubeAssocs d]) <> "}"+ where adjust = case o of+ Pred -> init+ Regu -> id+ printBind' ii name occurs d o = case not (isDummyId name) || occurs of- True -> parens (pretty name <+> colon o <+> cPrint 0 ii d)- False -> cPrint 2 ii d+ True -> parens $ pretty name <+> colon o <+> printCube o 0 ii d+ False -> printCube o 2 ii d -nestedApp :: Neutral -> (Neutral,[(Relevance, NF)])+nestedApp :: Neutral -> (Neutral,[(Binder, Cube NF)]) nestedApp (App o f a) = (second (++ [(o,a)])) (nestedApp f) nestedApp t = (t,[]) --sss x = if showSorts options then x else mempty- prettyTerm = cPrint (-100) instance Pretty (Term n) where pretty = prettyTerm mempty +type Action = [(NF,NF)] -- TODO: use Seq -mv :: Int -> Int -> Int-mv d x | x < d = (arity + 1) * x + idx- | otherwise = (x - d) + (arity + 1) * d- -- x + arity * d+paramv :: BitVector -> Role -> Int -> NF+paramv bv Thing x = Neu $ Var $ Param Thing $ V bv x+paramv bv Index x = Neu $ Var $ V bv x -mv' :: Int -> Int -> (Variable, Variable)-mv' d x | x < d = let v = (arity + 1) * x - in (V zero $ v + idx, V zero v)- | otherwise = let v = V zero $ (x - d) + (arity + 1) * d - in (v, Hole "does not appear!")- -- Param evil v)+noAction = []+wka = map (both wk)+addAct1 as = (Neu $ Var $ V (zeros 1) 0, Neu $ Var $ V (ones 1) 0) : wka as+addAct2 as = error "accessing crap" : wka as --- paramShift = if collapseRelevance options then zero else oneRel- -- TODO: have this as an argument to- -- Param. Alternatively, add a construct to collapse- -- levels. -next :: Relevance -> Relevance-next _ = Ir -- (+ (sortRelevance paramShift))+recVarName = synthId "°" +scopeCheck c k | 0 `iOccursIn` c = error "swapTy: improperly scoped Sigma"+ | otherwise = c --- renam :: Int -> Int -> NF -> NF--- renam d idx = id -- subst [var $ mv d $ x | x <- [0..]] +swap q = swapNF q 0 --- renam' d = subst' (map (mv' d) [0..])+swapV :: Permutation -> Variable -> Variable+swapV q x | isIdentity q = x+swapV q (V bv x) = Swap q $ V bv x -re :: Ident -> Ident-re (Irr (Identifier (pos ,x))) = (Irr (Identifier (pos,x++"°")))+swapV q (Swap q' v) = swapV (q `after` q') v +swapV q v@(Param _ _) = power n (Param Thing) $ swapV (simplifyPerm n q) x+ where (n,x) = countParam v+swapV q (Hole s) = Hole (s ++ "#")+swapV q x = Swap q x -arity, idx :: Int-arity = 1-idx = 1+power 0 f = id+power n f = f . power (n-1) f +(f *** g) (x,y) = (f x, g y) --- | Transform a term to its relational interpretation-transV :: Int -> Variable -> Variable+-- FIXME: what about the role=Index? There should not be a (Param Index) in the syntax.+countParam (Param _ x) = ((1+) *** id) (countParam x)+countParam x = (0,x) -transV d (V o x) = Param $ V o x-transV d (Param x) = Param $ transV d x-transV d (Hole s) = Hole (s ++ "!")+fullVarCube x = full (\i -> Neu $ Var $ V i x) -transNe :: Int -> Neutral -> NF-transNe d (Var v) = Neu $ Var $ transV d v-transNe d (App Re f a) = app Re (app Ir (transNe d f) a) (transNF d a) -transNe d (App Ir f a) = app Ir (transNe d f) a-transNe d (Proj o x k f) = proj o (transNe d x) k f-transNe d (OfParam i t) = app Ir t (Neu $ OfParam i t)+swapSubst :: Permutation -> NF -> NF+swapSubst q = subst $ (apply (invert q) $ fullVarCube 0 $ permLength q) : map (unit . var) [1..] -transNF :: Int -> NF -> NF-transNF d (Neu v) = transNe d v-transNF d (Lam o i ty bo) = transBind d Lam o i ty (transNF (d+1) bo)-transNF d (Pair o i x y) = Pair o i (transNF d x) (transNF d y) -transNF d ty@(Star _) = trans' d ty-transNF d ty@(Pi _ _ _ _) = trans' d ty-transNF d ty@(Sigma _ _ _ _) = trans' d ty+swapNe :: Permutation -> Int -> Neutral -> Neutral+swapNe q d (Var v) = Var $ swapV q v+swapNe q d (App o f a) = App o (swapNe q d f) (swapCube q d a)+swapNe q d (Proj o x k f) = Proj o (swapNe q d x) k f -trans' d ty = Lam Ir (synthId "z") ty (zerInRel d ty)+swapCube :: Permutation -> Int -> Cube NF -> Cube NF+swapCube q0 d c = apply q . subAppl q (\p -> swapNF p d) $ c+ where q = reducePerm q0 (dim c) -- FIXME: reduction should never be necessary --- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)-zerInRel d ty = inTrans (d + 1) (wk ty) (var 0)+swapBinder :: Permutation -> Int -> Cube NF -> Cube NF+swapBinder = swapCube --- | Build a relation z ∈ ⟦ty⟧. z is a term that, after renaming,--- gives the vector of terms member of the relation. Note that--- 'trans' is never applied to 'z', therefore 'zR' never occurs in the result.+swapNF :: Permutation -> Int -> NF -> NF+swapNF q d (Neu v) = Neu $ swapNe q d v+swapNF q d (Star x) = Star x+-- swapNF q d (Pair o i a b) = Pair o i (swapBinder q d a) (swapNF q d b)+swapNF q d (Lam o i a b) = Lam o i (swapBinder q d a) (swapSubst q $ swapNF q (d+1) b)+swapNF q d (Pi o i a b) = Pi o i (swapBinder q d a) (swapSubst q $ swapNF q (d+1) b)+-- swapNF q d (Sigma o i a b) = Sigma o i (swapBinder q d a) (swapNF q (d+1) b) +getVar :: Variable -> Int+getVar (Param _ x) = getVar x+getVar (V _ x) = x+getVar (Hole x) = (-1)+getVar (Swap _ x) = getVar x -inTrans :: Int -> NF -> NF -> NF-inTrans d (Star s) z = (Pi Ir dummyId z (Star s))-inTrans d (Pi o i a b) z = transBind d Pi o i a (inTrans (d + 1) b (app o (wk z) (var 0)))-inTrans d (Sigma o i a b) z = Sigma o (re i) (inTrans d a (proj o z True f)) $- subst2d 1 (wk $ proj o z True f, var 0) $ wk $- inTrans (1 + d) b (proj o (wk z) False f) -- TEST: is depth ok?- where (Irr (Identifier (_,nam))) = i- f = Irr nam-inTrans d t z = app Ir (transNF d t) z+getDepth :: Variable -> Int+getDepth (Param _ x) = 1 + getDepth x+getDepth (V _ x) = 0+getDepth (Hole x) = 0+getDepth (Swap _ x) = getDepth x --- | Translate a binding (x : A) into (x₁ : A₁) (⟦x⟧ : ⟦A⟧ x₁)-transBind :: Int -> (Relevance -> Ident -> NF -> NF -> NF) -> Relevance -> Ident -> NF -> NF -> NF-transBind d binder Re i a rest = binder Ir i a $ - binder Re (re i) (zerInRel d a) $ - subst2d 2 (var 1,var 0) $ wkn 2 rest+-- | Transform a term to its relational interpretation+transV :: Role -> Action -> Variable -> NF+transV Thing d (Swap q x) = swap (extendPerm q) $ transV Thing d x+transV Index d (Swap q x) = swap q $ transV Index d x+transV r d (V bv x) | x < L.length d = Neu $ Var $ case r of Thing -> V (bv <> ones 1) x; Index -> V (bv <> zeros 1) x+ | otherwise = paramv bv r x+-- transV r [] (Param r' x) = Neu $ Var $ Param r $ Param r' x +transV r d (Param r' x) + | getVar x < L.length d = maybeSwap $ param r' $ transV r d x -- the inner variable is known; go through + | otherwise = Neu $ Var $ maybeParam $ Param r' x -- the inner variable is not known ~> stop here and forget about other variables+ where maybeSwap = if r == Thing then swap (swap2 (n+2) (n+1) n) else id -- add a swap if we are doing "proper" parametricity+ maybeParam = if r == Thing then Param r else id -- keep only "proper" parametricity+ n = getDepth x -transBind d binder Ir i a rest = binder Ir i a rest+transV r d (Hole s) = Neu $ Var $ Hole (s ++ showRole r) --- Invariant: the whole term is not destroyed.-destroy :: Int -> Term n -> Term n-destroy d t = case t of- Var x -> Var $ pr x- Neu x -> Neu $ pr x+transNe :: Role -> Action -> Neutral -> NF+transNe r d (Var v) = transV r d v+transNe Thing d (App o f a) = app o (transNe Thing d f) (extend d a)+transNe Index d (App o f a) = app o (transNe Index d f) (cmap (transNF Index d) a)+transNe r d (Proj o x k f) = proj o (transNe r d x) k f - V o x -> V o x- Hole x -> Hole x- Destr d' t -> destroy (min d d') t -- coalesce- Param x | d == 0 -> x- | otherwise -> Destr d $ Param x +isLam :: Term n -> Bool+isLam (Lam _ _ _ _) = True+isLam _ = False - (Star o) -> Star o- (Pi o i a b) -> mb Pi o i a b - (Sigma o i a b) -> mb Sigma o i a b - (Lam o i ty bo) -> mb Lam o i ty bo - (Pair o i a b) - | isDestroyed o -> pr b- | otherwise -> Pair o i (pr' o a) (pr b) - (App o a b) -> case isDestroyed o of- True -> pr a- False -> App o (pr a) (pr' o b)- (Proj o x k f) -> case isDestroyed o of- True -> pr x -- result of the projection is not destroyed (by- -- assumpt.) but the whole pair would be -> we must- -- keep the 1st component.- False -> Proj o (pr x) k f -- FIXME: hmmm, here we should probably use pr' (symmetry)- (OfParam n x) -> OfParam (modId (++ "%" ++ show d) n) $ pr x- - where - isDestroyed o = d == 0 && o == Ir- mb :: (Relevance -> Ident -> NF -> NF -> NF) -> Relevance -> Ident -> NF -> NF -> NF- mb binder o i a b = case isDestroyed o of- True -> str (pr b)- False -> binder o i (pr' o a) (pr b)- pr x = destroy d x- pr' Ir x = destroy (d-1) x- pr' Re x = pr x+transNF :: Role -> Action -> NF -> NF+transNF r d (Neu v) = transNe r d v+transNF r d p@(Lam Pred i ty bo) = Lam Pred i (updateCube ix p $ extend d ty) (inTrans (addAct1 d) bo (Neu $ Var $ V ix 0))+ where ix = ones (dim ty) <> zeros 1+transNF r d (Lam o i ty bo) = Lam o i (extend d ty) (transNF r (addAct1 d) bo)+transNF r d (Pair o i x y) = Pair o i (transNF r d x) (transNF r d y) +transNF Index d (Star x) = Star x+transNF Index d (Pi o i a b) = Pi o i (cmap (transNF Index d) a) (transNF Index d b)+transNF Index d (Sigma o i a b) = Sigma o i ((transNF Index d) a) (transNF Index d b)+transNF r d ty@(Star _) = trans' r d ty+transNF r d ty@(Pi _ _ _ _) = trans' r d ty+transNF r d ty@(Sigma _ _ _ _) = trans' r d ty++extend d a = cubeCons (cmap (transNF Index d) a) (cmap (transNF Thing d) a) ++trans' :: Role -> Action -> NF -> NF+trans' Index d ty = error $ "trans': Index: wrong arg: " ++ show ty+trans' Thing d ty = Lam Pred (synthId "z") (pair (transNF Index d ty) (hole "⊘")) (zerInRel d ty)++-- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)+zerInRel :: Action -> NF -> NF+zerInRel d ty = inTrans (addAct2 d) (wk ty) (Neu $ Var $ V (zeros 1) 0)++-- | Build a relation z ∈ ⟦ty⟧. z is a term that, after renaming,+-- gives the vector of terms member of the relation. Note that+-- 'trans' is never applied to 'z', therefore 'zR' never occurs in the result.+++inTrans :: Action -> NF -> NF -> NF+inTrans d (Neu (App Pred f a)) z = app Pred (transNe Thing d f) (updateCube (ones (dim a) <> zeros 1) z (extend d a))+inTrans d (Star (Sort l δ)) z = (Pi Pred dummyId (pair z (hole "⊘")) (Star $ Sort l (δ+1)))+inTrans d (Pi Pred i a (Star (Sort l δ))) z = Pi Pred i (updateCube (ones (dim a) <> zeros 1) z (extend d a)) (Star $ Sort l (δ+1))+inTrans d (Pi o i a b) z = Pi o i (extend d a) (inTrans (addAct1 d) b (app o (wk z) (unit $ transNF Index (addAct1 d) $ var 0)))+inTrans d (Sigma o i a b) z = Sigma o i (inTrans d a (proj o z True i))+ (inTrans ((wk $ proj o z True i,var 0):wka d) b (proj o (wk z) False i))+inTrans d ty z = app Pred (transNF Thing d ty) (pair z (hole "⊘"))
Options.hs view
@@ -12,19 +12,22 @@ data Args = Args {verb :: Int, typeSystem :: TypeSystem,- showSorts :: Bool,+ showIndices :: Bool, collapseRelevance :: Bool,+ ignoreBinder :: Bool, files :: [String] } deriving (Show, Data, Typeable) sample = cmdArgsMode $ Args { verb = 0 &= help "verbosity" &= opt (0 :: Int),- typeSystem = enum [Predicative &= name "P" &= help "Agda (Predicative)", - CCω &= name "I" &= help "CCω (Impredicative)"]+ typeSystem = enum [CCω &= name "I" &= help "CCω (Impredicative)",+ Predicative &= name "P" &= help "Martin-Löf (Predicative)"+ ] , -- &= opt (0 :: Int),- showSorts = False &= help "display sort annotations in normal forms",+ showIndices = False &= help "show indices in cubes", collapseRelevance = False &= help "! (param) does not generate new relevance levels.",+ ignoreBinder = False &= help "ignore binder annotations.", files = [] &= args &= typFile }
RawSyntax.hs view
@@ -1,51 +1,61 @@-{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE QuasiQuotes, TemplateHaskell #-} module RawSyntax where import Language.LBNF -compile [$cf|+bnfc [$lbnf| comment "--" ; comment "{-" "-}" ; +token Colon (':')+ ;+token Commas ','+ ;+token Cross ';'+ ;++token Natural digit+;+-- token Index (('0'|'1')+);+token Permutation '#' digit+;+token Arrow {"->"}|{"=>"};++position token Identifier ('!'|'['|']'|letter|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;+position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;++position token Sort ('#' | '*' (digit*)) ('|' (digit+))?;+++EMulti. Exp6 ::= "{" [Exp] "}" ; EHole. Exp6 ::= Hole ; EVar. Exp6 ::= AIdent ;+EVarI. Exp6 ::= AIdent Natural; ESet. Exp6 ::= Sort ; EParam. Exp4 ::= Exp4 "!";+ESwap. Exp4 ::= Exp4 Permutation; EUp. Exp4 ::= Exp4 "^";--- ELeft. Exp4 ::= Exp4 "<";-EDestr. Exp4 ::= Exp4 "%" Natural ;+-- EDestr. Exp4 ::= Exp4 "%" Natural ; EProj. Exp4 ::= Exp4 "." AIdent ; EExtr. Exp4 ::= Exp4 "/" AIdent ; EApp. Exp3 ::= Exp3 Exp4 ;+EAppP. Exp3 ::= Exp3 "@" Exp4 ; EPi. Exp2 ::= Exp3 Arrow Exp2 ;-ESigma. Exp2 ::= Exp3 ";" Exp2 ;+ESigma. Exp2 ::= Exp3 ";;" Exp2 ; EAbs. Exp2 ::= "\\" [Bind] Arrow Exp2 ;-EAnn. Exp1 ::= Exp2 ":" Exp1 ;+EAnn. Exp1 ::= Exp2 Colon Exp1 ; EPair. Exp ::= Decl "," Exp ; coercions Exp 6 ;+separator Exp ";" ; Decl. Decl ::= AIdent "=" Exp1 ;-PDecl. Decl ::= "param" AIdent "=" Exp1 "::" Exp2;-terminator AIdent "" ;-terminator Decl ";" ;--token Arrow ('-' '>') | ('=' '>') ;+PDecl. Decl ::= "param" AIdent "=" Exp1 "ofErasedType" Exp2;+-- terminator Decl ";" ; NoBind. Bind ::= AIdent ; -Bind. Bind ::= "(" AIdent ":" Exp ")" ;+Bind. Bind ::= "(" AIdent Colon Exp ")" ; AIdent. AIdent ::= Identifier ;-terminator Bind "" ; -token Natural digit+;--position token Identifier ('!'|'['|']'|letter|digit|'-'|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;--position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;+terminator Bind "" ; -position token Sort ('#' | '*' (digit*)); |]
Terms.hs view
@@ -16,21 +16,19 @@ import Data.Sequence hiding (zip,replicate,reverse) import Control.Arrow (second) import Data.Foldable+import Permutation data Term :: * where Hole :: Irr Position -> String -> Term -- placeholder Star :: Irr Position -> Sort -> Term -- sort- Bound :: Irr Position -> Int -> Term -- variable- Pi :: Relevance -> Ident -> Term -> Term -> Term + Bound :: Irr Position -> BitVector -> Int -> Term -- variable+ Pi :: Binder -> Ident -> Cube Term -> Term -> Term Sigma :: Ident -> Term -> Term -> Term- Lam :: Ident -> Term -> Term -> Term + Lam :: Binder -> Ident -> Cube Term -> Term -> Term Pair :: Ident -> Term -> Term -> Term - (:$:) :: Term -> Term -> Term- -- 1st projection.- Proj :: Term -> String -> Term - -- 2nd projection. FIXME: remove- Extr :: Term -> String -> Term - + App :: Binder -> Term -> Cube Term -> Term+ Proj :: Bool {- 1st projection? -} -> Term -> String -> Term + -- term such that its relational interpretation is its argument. OfParam :: Ident -> Term -> Term @@ -43,21 +41,22 @@ -- relational interpretations and world destruction. In normal -- form, arguments to these are either themselves or a variable. Param :: Term -> Term + Swap :: Permutation -> Term -> Term Destroy :: Int -> Term -> Term termPosition :: Term -> Irr Position termPosition (Hole p _) = p termPosition (Star p _) = p-termPosition (Bound p _) = p+termPosition (Bound p _ _) = p termPosition (Pi _ i _ _) = identPosition i termPosition (Sigma i _ _) = identPosition i-termPosition (Lam i _ _) = identPosition i+termPosition (Lam _ i _ _) = identPosition i termPosition (Pair i _ _) = identPosition i-termPosition (x :$: y) = termPosition x-termPosition (Proj x _) = termPosition x-termPosition (Extr x _) = termPosition x+termPosition (App _ x y) = termPosition x+termPosition (Proj _ x _) = termPosition x termPosition (Ann x _) = termPosition x termPosition (Param x) = termPosition x+termPosition (Swap _ x) = termPosition x termPosition (OfParam _ x) = termPosition x termPosition (Shift _ x) = termPosition x termPosition (Destroy _ x) = termPosition x@@ -69,7 +68,7 @@ -- invariant: preserves normal forms app :: Term -> Term -> Term app (Lam i _ bo) u = subst0 u bo-app neutral u = neutral :$: u+app neutral u = neutral `App` u subst0 :: Term -> Term -> Term subst0 u = subst (u:map bound [0..]) @@ -85,7 +84,7 @@ Lam i ty bo -> Lam i (s ty) (s' bo) Pi i a b -> Pi i (s a) (s' b) Sigma i a b -> Sigma i (s a) (s' b)- (a :$: b) -> (s a) `app` (s b)+ (a `App` b) -> (s a) `app` (s b) (Ann e t) -> Ann (s e) (s t) (Pair i x y) -> Pair i (s x) (s' y) (Proj x f) -> proj (s x) f@@ -107,7 +106,7 @@ Lam i ty bo -> Lam i (s ty) (s' bo) Pi i a b -> Pi i (s a) (s' b) Sigma i a b -> Sigma i (s a) (s' b)- (a :$: b) -> (s a) `app` (s b)+ (a `App` b) -> (s a) `app` (s b) (Ann e t) -> Ann (s e) (s t) (Pair i x y) -> Pair i (s x) (s' y) (Proj x f) -> Proj (s x) f@@ -145,19 +144,22 @@ dec xs = [ x - 1 | x <- xs, x > 0] +allFreeVars :: Cube Term -> [Int]+allFreeVars = Prelude.concat . fmap freeVars . cubeElems+ freeVars :: Term -> [Int] freeVars (Ann a b) = freeVars a <> freeVars b-freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (Pi _ _ a b) = allFreeVars a <> (dec $ freeVars b) freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b)-freeVars (Bound _ x) = [x]-freeVars (a :$: b) = freeVars a <> freeVars b-freeVars (Lam _ ty b) = freeVars ty <> (dec $ freeVars b)+freeVars (Bound _ _ x) = [x]+freeVars (App _ a b) = freeVars a <> allFreeVars b+freeVars (Lam _ _ ty b) = allFreeVars ty <> (dec $ freeVars b) freeVars (Star _ _) = mempty freeVars (Hole _ _) = mempty freeVars (Pair _ x y) = freeVars x <> (dec $ freeVars y)-freeVars (Proj x _) = freeVars x-freeVars (Extr y _) = freeVars y+freeVars (Proj _ x _) = freeVars x freeVars (Param x) = freeVars x+freeVars (Swap _ x) = freeVars x freeVars (OfParam _ x) = freeVars x freeVars (Shift _ x) = freeVars x freeVars (Destroy _ x) = freeVars x@@ -170,40 +172,43 @@ cPrint :: Int -> DisplayContext -> Term -> Doc cPrint p ii (Destroy i x) = cPrint p ii x <> "%" <> pretty i-cPrint p ii (Shift (Sort l) x) = cPrint 6 ii x <> text (replicate l '^') - -- "⇧" <> prettySortNam o+-- cPrint p ii (Shift (Sort l) x) = cPrint 6 ii x <> text (replicate l '^') -- "⇧" <> prettySortNam o cPrint p ii (Param x) = cPrint p ii x <> "!"+cPrint p ii (Swap q x) = cPrint p ii x <> "#" <> pretty q cPrint p ii (OfParam i x) = pretty i -- "⌊" <> cPrint (-1) ii x <> "⌋" cPrint p ii (Hole _ x) = text x cPrint p ii (Star _ i) = pretty i-cPrint p ii (Bound _ k) +cPrint p ii (Bound _ bv k) | k < 0 || k >= length ii = text "<deBrujn index" <+> pretty k <+> text "out of range>"- | otherwise = pretty (ii `index` k)-cPrint p ii (Proj x f) = cPrint p ii x <> "#" <> text f-cPrint p ii (Extr x f) = cPrint p ii x <> "/" <> text f-cPrint p ii t@(_ :$: _) = let (fct,args) = nestedApp t in - parensIf (p > 3) (cPrint 3 ii fct <+> sep (map (cPrint 4 ii) args))+ | otherwise = pretty (ii `index` k) <> subscriptPrettyBV bv+cPrint p ii (Proj True x f) = cPrint p ii x <> "#" <> text f+cPrint p ii (Proj False x f) = cPrint p ii x <> "/" <> text f+cPrint p ii t@(App _ _ _) = let (fct,args) = nestedApp t in + parensIf (p > 3) (cPrint 3 ii fct <+> sep (map (cPrintCube 4 ii) args)) cPrint p ii (Pi o name d r) = parensIf (p > 1) (sep [printBind ii name d r <+> arrow o, cPrint 1 (name <| ii) r]) -cPrint p ii (Sigma name d r) = parensIf (p > 1) (sep [printBind ii name d r <+> text "×", cPrint 1 (name <| ii) r])-cPrint p ii (t@(Lam _ _ _)) = parensIf (p > 1) (nestedLams ii mempty t)+cPrint p ii (Sigma name d r) = parensIf (p > 1) (sep [printBind ii name (unit d) r <+> cross Regu, cPrint 1 (name <| ii) r])+cPrint p ii (t@(Lam _ _ _ _)) = parensIf (p > 1) (nestedLams ii mempty t) cPrint p ii (Ann c ty) = parensIf (p > 0) (cPrint 1 ii c <+> text ":" <+> cPrint 0 ii ty) cPrint p ii (Pair name (OfParam _ x) y) = parensIf (p > (-1)) (sep ["⟦"<>pretty name<>"⟧" <+> text "=" <+> cPrint 0 ii x <> comma, cPrint (-1) (name <| ii) y]) cPrint p ii (Pair name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comma, cPrint (-1) (name <| ii) y]) nestedLams :: DisplayContext -> Seq Doc -> Term -> Doc-nestedLams ii xs (Lam x (Hole _ _) c) = nestedLams (x <| ii) (xs |> pretty x) c-nestedLams ii xs (Lam x ty c) = nestedLams (x <| ii) (xs |> parens (pretty x <+> ":" <+> cPrint 0 ii ty)) c+-- nestedLams ii xs (Lam o x (Hole _ _) c) = nestedLams (x <| ii) (xs |> pretty x) c+nestedLams ii xs (Lam o x ty c) = nestedLams (x <| ii) (xs |> parens (pretty x <+> colon o <+> cPrintCube 0 ii ty)) c nestedLams ii xs t = (text "\\ " <> (sep $ toList $ xs) <+> text "->" <+> nest 3 (cPrint 0 ii t)) printBind ii name d r = case not (isDummyId name) || 0 `iOccursIn` r of- True -> parens (pretty name <+> text ":" <+> cPrint 0 ii d)- False -> cPrint 2 ii d+ True -> parens (pretty name <+> colon Regu <+> cPrintCube 0 ii d)+ False -> cPrintCube 2 ii d -nestedApp :: Term -> (Term,[Term])-nestedApp (f :$: a) = (second (++ [a])) (nestedApp f)+cPrintCube p ii d | dim d == 0 = cPrint p ii (d !? nil)+ | otherwise = "{" <> sep (punctuate ";" [pretty i <> "↦" <> cPrint 0 ii x | (i,x) <- cubeAssocs d]) <> "}"++nestedApp :: Term -> (Term,[Cube Term])+nestedApp (App _ f a) = (second (++ [a])) (nestedApp f) nestedApp t = (t,[]) prettyTerm = cPrint (-100)@@ -221,7 +226,7 @@ Lam i ty bo -> Lam i (s ty) (s bo) Pi i a b -> Pi i (s a) (s b) Sigma i a b -> Sigma i (s a) (s b)- (a :$: b) -> (s a) :$: (s b)+ (a `App` b) -> (s a) `App` (s b) (Ann e t) -> Ann (s e) (s t) (Pair i x y) -> Pair i (s x) (s y) (Proj x f) -> Proj (s x) f@@ -266,7 +271,7 @@ (paramProg (map (\d -> Hole dummyPosition "pair not in nf!":map wk d) g) y) -- because the input is in normal form, the variable bound by the -- pair can never appear in y.- paramProg g (f :$: a) = foldl app (paramProg g f) [renam g idx a | idx <- [1..arity]] `app` paramProg g a+ paramProg g (f `App` a) = foldl app (paramProg g f) [renam g idx a | idx <- [1..arity]] `app` paramProg g a paramProg g (Proj e f) = proj (paramProg g e) f paramProg g (Extr e f) = extr (paramProg g e) f paramProg g (Ann _ _) = error "Ann should not be in nf term"@@ -334,9 +339,9 @@ (Lam i ty bo) -> mb d Lam i ty bo (Pair i a b) -> mb d Pair i a b (Ann e t) -> Ann <$> pr e <*> pr t - (a :$: b) -> case pr b of+ (a `App` b) -> case pr b of Nothing -> pr a- Just b' -> (:$: b') <$> pr a + Just b' -> (`App` b') <$> pr a (Proj x f) -> (\x -> Proj x f) <$> pr x (Extr x f) -> (\x -> Extr x f) <$> pr x
TypeCheckerNF.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE PackageImports, TypeSynonymInstances, FlexibleInstances, GADTs #-}+{-# LANGUAGE PackageImports, TypeSynonymInstances, FlexibleInstances, GADTs, PatternGuards, GeneralizedNewtypeDeriving #-} -- Type checker loosely based on --@@ -10,50 +10,57 @@ -- -- are also implemented. ----- The ideas related to parametricity and erasure are developed in------ "Realizability and Parametricity in Pure Type Systems", Bernardy, Lasson--- module TypeCheckerNF where -import Prelude hiding (length)+import Prelude hiding (length,sequence) import Basics import qualified Terms import Terms (Term (Ann)) import Display-import Control.Monad.Error+import Control.Monad.Error hiding (sequence) import Data.Char import Data.Maybe (isJust) import Control.Monad.Trans.Error (ErrorT, runErrorT)-import Control.Monad.Trans.Writer+import Control.Monad.Writer.Class+import Control.Monad.Writer hiding (sequence)+import Control.Monad.Trans.State (StateT, execStateT, modify, get) import Data.Functor.Identity import Data.Sequence hiding (replicate)-import Data.Foldable (toList)+import Data.Foldable (toList,Foldable)+import qualified Data.List as L+import Data.Traversable import Normal hiding (Term)+import qualified Normal import Options+import Data.Array.IArray (assocs,array)+import Data.Function+import Debug.Trace+import Permutation (permLength) instance Error (Term,Doc) where strMsg s = (Terms.Hole dummyPosition "strMsg: panic!",text s) -type Result a = (ErrorT (Term,Doc)) -- term is used for position information- (WriterT [Doc] Identity) a+newtype Result a = Result ((ErrorT (Term,Doc)) -- term is used for position information+ (WriterT [Doc] Identity) a)+ deriving (Functor,Monad, MonadError (Term,Doc), MonadWriter [Doc]) report :: Doc -> Result ()-report x = lift $ tell [x]+report x = tell [x] runChecker :: Result a -> (Either (Term,Doc) a,[Doc])-runChecker x = runIdentity $ runWriterT $ runErrorT x+runChecker (Result x) = runIdentity $ runWriterT $ runErrorT x data Definition = Abstract -- ^ lambda, pi, sigma bound | Direct Value -- ^ pair bound type Value = NF type Type = Value+type Dimension = Int data Bind = Bind {entryIdent :: Ident, entryValue :: Definition, -- ^ Value for identifier. - entryType :: Type, -- ^ Attention: context of the type does not contain the variable bound here.- entryRelevance :: Relevance+ entryType :: Cube Type, -- ^ Attention: context of the type does not contain the variable bound here.+ entryBinder :: Binder } type Context = Seq Bind @@ -64,109 +71,138 @@ displayT = Terms.prettyTerm . fmap entryIdent dispContext :: Context -> Doc-dispContext ctx = case viewl ctx of+dispContext ctx0 = case viewl ctx0 of EmptyL -> mempty- Bind x val typ o :< ctx' -> let di = display ctx' in (case val of- Abstract -> pretty x <+> colon o <+> di typ--- Direct (OfParam _ v) -> "⟦"<>pretty x<>"⟧" <+> sep ["=" <+> parens (di v), "::" <+> di typ]- Direct v -> pretty x <+> sep ["=" <+> parens (di v), colon o <+> di typ]- ) $$ dispContext ctx'---- FIXME: flag an error if impredicativity disabled and we use it anyway.+ Bind x val typ o :< ctx0' -> (let ctx = fmap entryIdent ctx0 + ctx' = fmap entryIdent ctx0'+ in case val of+ Abstract -> pretty x <+> colon o <+> printCube o 0 ctx' typ+ Direct v -> pretty x <+> sep ["=" <+> parens (cPrint 0 ctx v), colon o <+> printCube o 0 ctx' typ]+ ) $$ dispContext ctx0' -hole = Neu . Var . Hole+todo = Regu -- for now sigma types are always of the "complete" cube kind. -todo = Re+resurrect :: Binder -> Context -> Context+resurrect _ = id -resurrect :: Relevance -> Context -> Context-resurrect Re = id-resurrect Ir = fmap (\e -> e {entryRelevance = Re})+subCubeAt' bv c = updateCube (ones $ dim c) (hole "⊘") $ subCubeAt bv c -iType :: Context -> Term -> Result (Value,Type)+iType :: Context -> Term -> Result (Value,Type,Dimension) iType g (Ann e tyt) = do (ty,o) <- iSort g tyt - v <- cType g e ty- return (v,ty) -- annotations are removed+ (v,d) <- cType g e ty+ return (v,ty,d) -- annotations are removed iType g t@(Terms.Star p s)- = return (Star s,Star $ above s) + = return (Star s,Star $ above s, 0) iType g (Terms.Pi r1 ident tyt tyt') - = do (ty ,s1) <- iSort (resurrect r1 g) tyt + = do (ty ,s1) <- iSortCube r1 (resurrect Regu g) tyt (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt' let o = s1 ⊔ s2- return (Pi r1 ident ty ty', Star o)+ return (Pi r1 ident ty ty', Star o, 0) iType g (Terms.Sigma ident tyt tyt') - = do let r1 = todo- (ty,s1) <- iSort (resurrect r1 g) tyt - (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'+ = do (ty,s1) <- iSort (resurrect Regu g) tyt + let r1 = todo+ (ty',s2) <- iSort (Bind ident Abstract (unit ty) r1 <| g) tyt' let o = s1 ⊔ s2- return (Sigma r1 ident ty ty', Star o)-iType g e@(Terms.Bound _ x) = case o of- Ir -> throwError (e,"Cannot use irrelevant variable in relevant context")- Re -> return $ (val $ value, wkn (x+1) $ typ)+ return (Sigma r1 ident ty ty', Star o, 0)+iType g e@(Terms.Bound _ bv x) = do+ when (bvDim bv /= dim typ0) $ + throwError (e,"inexact cube access: expected dimension " <> pretty (dim typ0) )+ return $ (val $ value, finalTyp, setBits bv) where val (Direct v) = wkn (x+1) v- val _ = var x -- etaExpand o (var' x) typ- Bind _ value typ o = g `index` x+ val _ = Neu $ Var $ V bv x+ typ = cubeAccess "iType var" typ0 bv+ arg = updateCube (ones da) (hole "⊘") arg0+ arg0 = subCubeAt bv $ fullVarCube x (dim typ0)+ finalTyp = app Pred (wkn (x+1) typ) arg+ da = dim arg0+ Bind _ value typ0 o = g `index` x iType g (Terms.Hole p x) = do report $ hang (text ("context of " ++ x ++ " is")) 2 (dispContext g)- return (hole x, hole ("type of " ++ x))-iType g (e1 Terms.:$: e2)- = do (v1,si) <- iType g e1- case si of+ return (hole x, hole ("type of " ++ x),0)+iType g (Terms.App o' e1 e2)+ = do (v1,ti,d) <- iType g e1+ case ti of Pi o _ ty ty' -> do - v2 <- cType (resurrect o g) e2 ty- return (app o v1 v2, subst0 v2 ty') + when (o /= o') $ throwError (e1,"application: non-matching binder kinds")+ v2 <- cTypeCube o (resurrect o g) e2 ty+ return (app o v1 v2, subst0 v2 ty',d) _ -> throwError (e1,"invalid application")-iType g (Terms.Proj e f) = do- (v,t) <- iType g e+iType g (Terms.Proj isFirst e f) = do+ (v,t,_) <- iType g e search v t- where search :: NF -> NF -> Result (Value,Type)- search v (Sigma o (Irr (Identifier (_,f'))) ty ty') - | f == f' = return (π1,ty)- | otherwise = search π2 (subst0 π1 ty')+ where search :: NF -> NF -> Result (Value,Type,Dimension)+ search v (Sigma o i ty ty') + | f == f' = return $ if isFirst then (π1,ty,0) else (π2,subst0 (unit π1) ty',0)+ | otherwise = search π2 (subst0 (unit π1) ty') where + f' = idString i (π1,π2) = (case v of Pair _ _ x y -> (x,y) -- substitution is useless if the pair is in normal form.- _ -> (proj o v True (Irr f'),proj o v False (Irr f')) -- This could not happen if eta-expansion were done.+ _ -> (proj o v True i,proj o v False i) -- This could not happen if eta-expansion were done. ) :: (NF,NF) search _ _ = throwError (e,"field not found") iType g (Terms.Pair ident e1 e2) = do- (v1,t1) <- iType g e1+ (v1,t1,_) <- iType g e1 let r1 = todo- (v2,t2) <- iType (Bind ident (Direct v1) t1 r1 <| g) e2- return $ (Pair r1 ident v1 (str v2),Sigma r1 ident t1 t2)+ (v2,t2,_) <- iType (Bind ident (Direct v1) (unit t1) r1 <| g) e2+ return $ (Pair r1 ident v1 (str v2),Sigma r1 ident t1 t2,0) -- Note: the above does not infer a most general type: any potential dependency is discarded. -iType g t@(Terms.Lam x (Terms.Hole _ _) e) = throwError (t,"cannot infer type for" <+> displayT g t)-iType g (Terms.Lam x ty e) = do- (vty,Sort _) <- iSort g ty- let o = todo- (ve,t) <- iType (Bind x Abstract vty o <| g) e- return $ (Lam o x vty ve, Pi o x vty t)+iType g t@(Terms.Lam o x h e) + | dim h == 0, (Terms.Hole _ _) <- h !? nil+ = throwError (t,"cannot infer type for" <+> displayT g t)+iType g (Terms.Lam o x ty e) = do+ (vty,vs) <- iSortCube o (resurrect Regu g) ty+ (ve,t,d) <- iType (Bind x Abstract vty o <| g) e+ return $ (Lam o x vty ve, Pi o x vty t,min d (dim vty)) iType g (Terms.Param e) = do- (v,t) <- iType g e- return (param v, app Ir (param t) v)+ (v,t,d) <- iType g e+-- report $ "param: " <> vcat [displayT g e, display g t, display g (param Thing t)]+ return (param Thing v, inTrans [] t v,1+d) -iType g (Terms.Shift f e) = do- (v,t) <- iType g e- return (shift f v, shift f t)+iType g (Terms.Swap q e) = do+ (v,t,d) <- iType g e+ when (d /= permLength q) $ + throwError (e,"swapped term has wrong dimension: " <> pretty d)+ return (swap q v, swap q t,d) -iType g x@(Terms.Destroy d e) = do- (v,t) <- iType g e - return (destroy d v,destroy d t) iSort :: Context -> Term -> Result (Type,Sort) iSort g e = do- (val,v) <- iType g e+ (val,v,_) <- iType g e case v of Star i -> return (val,i) (Neu (Var (Hole h))) -> do report $ text h <+> "must be a type"- return $ (hole h, Sort 1)- _ -> throwError (e,displayT g e <+> "is not a type")+ return $ (hole h, Sort 1 0)+ _ -> throwError (e,displayT g e <+> "is not a type. Instead: " <+> display g v) +iSortCube' :: Int -> Context -> Term -> BitVector -> StateT (Cube Type) Result ()+iSortCube' s g e i = do+ types <- get+ t <- fst <$> (lift $ cType g e (Pi Pred dummyId (subCubeAt i types) (Star $ Sort s $ setBits i)))+ modify (updateCube i t)+++-- | Return the cube contents, stuff on the "lower" corner first. Top+-- corner excluded if Pred cube.+cubeContents :: Binder -> Cube a -> [(BitVector,a)]+cubeContents o = L.sortBy (compare `on` (setBits . fst)) . tweak o . assocs++iSortCube :: Binder -> Context -> Cube Term -> Result (Cube Type,Sort)+iSortCube o g c = do+ (t0,Sort l _) <- iSort g (c !? zeros (dim c))+ + ts <- execStateT (sequence [iSortCube' l g a i | (i,a) <- L.drop 1 $ -- exclude the lower corner, as it's not a Pi here. (and already checked)+ cubeContents o c])+ (updateCube (zeros (dim c)) t0 $ full (const $ hole "⊘") (dim c))+ return (ts,Sort l (dim c)) + where d = dim c+ unify :: Context -> Term -> Type -> Type -> Result () unify g e q q' = do let ii = length g@@ -179,50 +215,73 @@ (throwError (e,hang "type mismatch: " 2 $ vcat ["inferred:" <+> display g q', "expected:" <+> display g q ,+ -- "q'" <+> text (show q'),+ -- "q " <+> text (show q), "for:" <+> displayT g e , "context:" <+> dispContext g])) +unifyAll :: Binder -> Context -> Term -> Cube Type -> Cube Type -> Result ()+unifyAll o g e q q' = do+ when (dim q /= dim q') $ throwError (e,"non-matching dimensions")+ -- FIXME: skip if Pred+ sequence_ $ tweak o $ Prelude.zipWith (unify g e) (cubeElems q) (cubeElems q')+ -- Check the type and normalize-cType :: Context -> Term -> Type -> Result Value-cType g (Terms.Lam name (Terms.Hole _ _) e) (Pi o name' ty ty') = do- e' <- cType (Bind name Abstract ty o <| g) e ty'- return (Lam o name ty e') -- the type is filled in.+cType :: Context -> Term -> Type -> Result (Value,Dimension)+cType g (Terms.Lam _ name h e) (Pi o name' ty ty') | dim h == 0, (Terms.Hole _ _) <- h !? nil = do+ (e',d) <- cType (Bind name Abstract ty o <| g) e ty'+ return (Lam o name ty e',min d (dim ty)) -- the type and binder is filled in. -cType g (Terms.Lam name ty0 e) (Pi o name' ty ty')- = do (t,_o) <- iSort g ty0- unify g (Terms.Hole (identPosition name) (show name)) t ty- e' <- cType (Bind name Abstract ty o <| g) e ty'- return (Lam o name ty e')+cType g e0@(Terms.Lam o' name ty0 e) (Pi o name' ty ty')+ = do when (o /= o') $ throwError (e0,"Unmatching flavours of quantification")+ (t,_o) <- iSortCube o (resurrect o g) ty0+ unifyAll o g (Terms.Hole (identPosition name) (show name)) t ty+ (e',d) <- cType (Bind name Abstract ty o <| g) e ty'+ return (Lam o name ty e',min d (dim ty)) cType g (Terms.Pair name e1 e2) (Sigma o name' ty ty') = do -- note that names do not have to match.- v1 <- cType g e1 ty - v2 <- cType (Bind name (Direct v1) ty o <| g) e2 (wk $ subst0 v1 ty') + (v1,d1) <- cType g e1 ty + (v2,d2) <- cType (Bind name (Direct v1) (unit ty) o <| g) e2 (wk $ subst0 (unit v1) ty') -- The above weakening is there because: -- * the type contains no occurence of the bound variable after substitution, but -- * the context is extended anyway, to bind the name to its value.- return $ Pair o name' v1 (str v2)+ return (Pair o name' v1 (str v2),min d1 d2) -- note that the pair must use the name of the sigma for the -- field. (The context will use the field name provided by the type)-+{- -- Γ ⊢ ⌊A⌋ : B cType g (Terms.OfParam i e) t = do -- Γ ⊢ A ⌊A⌋ : ⟦B⟧ ⌊A⌋ -- Γ ⊢ A x : ⟦B⟧ x -- Γ ⊢ A : (x : ⌊B⌋) → ⟦B⟧ x- e' <- cType g e $ Pi Ir i t (zerInRel 0 t)+ e' <- cType g e $ Pi Ty i t (zerInRel 0 t) return (Neu $ OfParam i e')--cType g (Terms.Shift f e) t = do- shift f <$> cType g e (shift (negate f) t) - -- there might be negative sorts in there, but that should be fine;- -- if they occur the type checker will simply reject the term- -- because it's impossible to create an inhabitant of a negative- -- sort.+-} cType g e v - = do (e',v') <- iType g e+ = do (e',v',d) <- iType g e unify g e v v'- return e'+ return (e',d) +cTypeCube' :: Context -> Term -> Cube Type -> BitVector -> StateT (Cube Value) Result ()+cTypeCube' g e t i = do+ values <- get+ v <- fst <$> (lift $ cType g e (app Pred (t !? i) (subCubeAt i values)))+ modify (updateCube i v)+ +tweak Regu = id+tweak Pred = init++cTypeCube :: Binder -> Context -> Cube Term -> Cube Type -> Result (Cube Value)+cTypeCube o g e t = do+ when (dim e /= dim t) $ + throwError (cubeFirstElemForErr e,"type cube: non-matching dimensions")+ execStateT (sequence [cTypeCube' g a t i | (i,a) <- cubeContents o e])+ (full (const $ hole "⊘") (dim e))+++cubeFirstElemForErr :: Cube Term -> Term+cubeFirstElemForErr c = (cubeElems c ++ [error "empty cube!"]) !! 0+
tutorial/01-Module.ua view
@@ -43,11 +43,11 @@ four = exp two (mul two two), -- The syntax for pairs is "first class", we can have them anywhere:-somePair = (pi1 = two, plus two four) : (Nat ; Nat),+somePair = (pi1 = two, plus two four) : (Nat ;; Nat), -- Dependent pairs can also be declared-depPair = (A = Nat, suc) : ((A : *1) ; A -> A),+depPair = (A = Nat, suc) : ((A : *1) ;; A -> A), -- fields named in the type can be extracted using .: extract = depPair.A,
− tutorial/02.1-Relevance.ua
@@ -1,60 +0,0 @@--- Relevance and erasure------------------------------ In uAgda, there are two flavours of quantification:--- relevant and irrelevant. (We borrow the notion from Pfenning (2001)).---- One can roughly thing as irrelevant things as things whose--- computational content is inaccessible ("proofs"), while relevant--- ones are regular terms whose computational content is relevant.--- Irrelevant product is denoted with =>. Irrelevancy of abstraction--- and applications is inferred.---- Irrelevancy is enforced by making sure irrelevant variables are--- never directly returned. They can only be used as arguments to--- irrelevant applications or on the LHS of =>.---- For example the following term does not type-check because 'A' is--- used in the result directly, while it is irrelevant: --{--Wrong = \(A : *) -> A - : * => *,--}---- An example where irrelevance can be used for more precise typing is--- the following. We can use a more precise type of the Leibniz--- equality that says that the actual type used is irrelevant for the--- predicate:--Eq = \ A a b -> (P : A => *) -> P a -> P b- : (A : *) -> (a b : A) => *1,---- Another example is the following: the inductive principle for--- natural numbers is independent on the actual representation of the--- naturals, so they are irrelevant. This can be expressed as--- follows...---Nat = - -- We assume an (abstract) representation N of naturals, as well as- -- constructors for successor and zero.- \(N : *) (s : N -> N) (z : N) ->-- -- Then define the induction principle:- \(n : N) -> (P : N => *) -> P z -> ((m : N) => P m -> P (s m)) -> P n,----- We know that all the programs we have written using naturals--- satisfying the above induction principle can be represented by--- Naturals where the irrelevant parts are erased. We can access this--- erasure within uAgda by using the % operator. The second argument--- is the depth of irrelevancy to erase. --Nat-representation = Nat % 0,---- The normal form of the above term reveals that the result is the--- usual Church encoding for naturals.---*
tutorial/03-Parametricity.ua view
@@ -1,32 +1,34 @@--- Parametricity, relevance and erasure------------------------------------------+-- Parametricity+----------------- --- In uAgda every term is assumed to be parametric.+-- In uAgda every term is known to be parametric. -- hence for an arbitrary function f... \(A : *) (B : *) (f : A -> B) -> ( -- we can use the fact that it is parametric by using the postfix '!' operator:-fparam = f! : (x : A) => A! x -> B! (f x),+fparam = f! : (x : {A ; A!}) -> B! @ {f (x 0)}, --- It is also possible to erase all the stuff less relevant than a--- certain world by using the operator '%'. For example, after--- erasing all the (level one) irrelevant stuff from the above type we--- recover the original (check the normal form):+-- Note here that we introduce the cube syntax.+-- {A; A!} is a 2-element cube; and +-- x 0 accesses the 1st component of the cube x. -eraseType = ((x : A) => A! x -> B! (f x)) % 0,+-- We also have an example of an incomplete cube: +-- {f (x 0)} +-- In the above, it is inferred to be incomplete thanks to the special+-- application operator: --- Indeed, f!%0 = f.-fAgain = fparam %0,+-- @ (Relation membership test) +-- Finally, relation types can be formed using the double arrow:+-- => --- We can get binary parametricity by combination of unary--- parametricity and erasure. See the following reference for--- the explanation:+-- Note that, so far, there was no explicit mention of cubes, because+-- a 1-element cube can be just written as its contents. That is, A+-- really stands for {A} in a cube context. --- http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466+-- See the paper for a detailed explanation of the role of cubes. -fparam2 = f!!%1, -- : (x y : A) => A!!%2 x y => B!!%2 (f x) (f y), *)
tutorial/03.1-Parametricity-Use.ua view
@@ -1,23 +1,58 @@ -- let's use parametricity in a useful way: prove that any -- function of type (X : #) -> X -> X is the identity. --- To simplify the example we use impredicativity here.+-- To simplify the example we use impredicativity here; the impredicative sort is written #. -Eq = \A a b -> (P : A => #) -> P a -> P b- : (A : #) -> A => A => #++-------------------------+-- Preliminaries++-- Type of propositions, at dimension 1. (Optionally, the dimension of+-- a sort is written after a pipe; otherwise it is 0)+prop = #|1, ++-- Truth+Top = (A : #) -> A -> A+ : #,++-- ... and its inhabitant+tt = \A x -> x+ : Top,+++---------------------------------------------------+-- Leibniz equality (modified to support cubes.)++-- The regular definition for Leibniz equality is+-- Eq = \A a b -> (P : A -> #) -> P a -> P b++-- We face a number of superficial complications, because we want Eq A+-- a b to be of dimension 1, instead of dimension 0.++-- 1. we must use #|1 instead of #|0;+-- 2. we have to extend quantifications in such a way that they are always over cubes of dimension 1.+-- this is done by adding dummy arguments in cubes (# and Top below)++Eq = \A a b -> (P : {# ; \t => (z : A) => prop} ) -> {Top ; \t => P 1 @ a} -> P 1 @ (b 0)+ : (A : #) -> A -> A => prop , +refl = \A x P p -> p 1+ : (A : #) -> (x : A) -> Eq A x @ x,++-- The theorem is expressed as normal: Theorem = (f : (A : #) -> A -> A) -> (A : #) -> (x : A) ->- Eq A x (f A x),-+ Eq A x @ (f A x), +-- The proof follows the usual technique; see the paper for details. proof = \(f : (A : #) -> (a : A) -> A) -> \(A : #) ->- \(x : A) -> f! A (\y -> Eq A x y) x (\_ p -> p)- : Theorem-,+ \(x : A) -> f! {A ; \y => Eq A x @ (y 0) } {x ; refl A x}+ : Theorem,++ #
− tutorial/04-Data.ua
@@ -1,75 +0,0 @@--- Data-------------- In the Calculus of Constructions, it is possible to encode data via--- Church-style encodings. However, it is then impossible to do--- inductive reasoning on these. This led to the addition of inductive--- constructions (CiC). Agda features inductive families as a native--- construct.---- Even though uAgda does not feature a native construction for data,--- it is possible to encode data using parametricity, erasure and a--- little bit of special sauce. The trick is that ---- 1. The erasure of the induction principle for a given inductive--- family is equal to its Church representation, and---- 2. The relational interpretation of the representation yields back--- the inductive principle.---- More theoretical background can be found in Phil Wadler's "The--- Girard-Reynolds isomorphism".----- In uAgda, we proceed as follows. First define the appropriate--- induction principle and the proof that the constructors respect--- induction. (Note that these definitions are parameterised over an--- arbitrary module "q" containing an *abstract* version of the stuff--- we want to define (here with fields Nat, suc and zer).--param Q = \ q -> (--Nat = \n -> (P : q.Nat => *) -> ((n : q.Nat) => P n -> P (q.suc n)) -> (P q.zer) -> P n,-zer = \P s z -> z,-suc = \m n P s z -> s m (n P s z),-\ _ -> *)--:: ((Nat : *1) ; (zer : Nat) ; (suc : Nat -> Nat) ; *1),---- The keyword "param" and the double colon are special syntax to--- construct a concrete representation (here "Q") that is--- computationally equal to the erasure of the above, but whose--- relational interpretation is the one given.---- (The last component of the tuple is just noise, as usual).----- From there we can do simple computations:-one = Q.suc Q.zer : Q.Nat,-two = Q.suc one,------ And we can also do inductive reasoning (but indexed by a less--- relevant version of the type/values):-Nat-elim = \n -> n!- : (n : Q.Nat) -> (P : Q.Nat => *) -> ((n : Q.Nat) => P n -> P (Q.suc n)) -> (P Q.zer) -> P n,----- In particular, we can also inductive computation. In that case,--- because we work in a predicative type system, we need to apply the--- induction on a copy of the natural lifted to a higher universe.--- That's fine, because we also have an operator for that: postfix ^.--lift = \n -> n^- : Q.Nat -> Q.Nat^,--plus - = \m n -> n^! (\_ -> Q.Nat) (\_ r -> Q.suc r) m - : Q.Nat -> Q.Nat -> Q.Nat,---four = plus two two,--*-
uAgda.cabal view
@@ -1,17 +1,11 @@ name: uAgda-version: 1.1.0.0+version: 1.2.0.0 category: Dependent Types synopsis: A simplistic dependently-typed language with parametricity. description: uAgda implements an experimental dependently-typed language- (and proof assistant by the Curry-Howard isomorphism). The- goal of the project is twofold:- .- 1. Experiment with a minimalistic language that is strong enough to- program and reason in.- .- 2. Give a simple implementation of its type-checker (ours is ~200 lines).+ (and proof assistant by the Curry-Howard isomorphism), extended with support for parametricity. . See the share/tutorial directory for how to get started. @@ -28,10 +22,8 @@ tutorial/00-Start-Here.ua tutorial/01-Module.ua tutorial/02-Holes.ua- tutorial/02.1-Relevance.ua tutorial/03-Parametricity.ua tutorial/03.1-Parametricity-Use.ua- tutorial/04-Data.ua executable uAgda@@ -50,11 +42,13 @@ TypeCheckerNF build-depends: base==4.*+ build-depends: array==0.3.* build-depends: cmdargs==0.6.*- build-depends: containers==0.3.*+ build-depends: containers==0.4.* build-depends: pretty==1.0.* build-depends: parsec==2.1.*- build-depends: BNFC-meta==0.1.*+ build-depends: BNFC-meta==0.3.* build-depends: transformers == 0.2.*- build-depends: monads-fd == 0.1.*+ build-depends: mtl == 2.0.*+ build-depends: split == 0.1.*