packages feed

uAgda 1.0.0.2 → 1.1.0.0

raw patch · 14 files changed

+326/−283 lines, 14 files

Files

AbsSynToTerm.hs view
@@ -55,18 +55,13 @@ extractVars _ = throwError "list of variables expected"  resolveTerm :: A.Exp -> Resolver Term+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.EDestr x (A.Natural n)) = Destroy (Relevance $ read n) <$> resolveTerm x-resolveTerm (A.EUp x) = Shift (Sort 1 0) <$> resolveTerm x-resolveTerm (A.ELeft x) = Shift oneRel <$> 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,'*':s))) = return $ Star (Irr p) $ Sort lvl rel-    where (l,r) = break (== '@') s-          lvl = read ('0':l)-          rel = case r of-            ('@':xs) -> Relevance $ read ('0':xs)-            _ -> 0+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@@ -76,12 +71,15 @@                               (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+resolveTerm (A.EPi a arrow b) = case a of    (A.EAnn vars a') -> do vs <- extractVars vars-                          manyDep Pi a' vs b+                          manyDep (Pi o) a' vs b                               (A.EAbs _ _ _) -> throwError "cannot use lambda for type"-   _              -> Pi (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)+   _              -> 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 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) =
Basics.hs view
@@ -3,12 +3,12 @@        (module Data.Monoid, (<>),         module Control.Applicative,         Irr(..), -        Sort(..), prettySortNam, prettyRel,-        above, oneLev, next, oneRel, zero,+        Sort(..),+        above, oneLev, zero,         Ident, Identifier(..), DisplayContext,         Position, dummyPosition, identPosition,          isDummyId, modId, synthId, dummyId, idString,-        Relevance(..), (+.),+        Relevance(..), arrow, colon,         Lattice(..)) where  import Display@@ -73,46 +73,45 @@ instance Lattice Int where     (⊔) = max -newtype Relevance = Relevance {fromRel :: Int}-  deriving (Real,Enum,Integral,Num,Ord,Eq,Show,Lattice)+data Relevance = Re | Ir+  deriving (Enum,Ord,Eq,Show)  class Lattice a where     (⊔) :: a -> a -> a  -data Sort = Sort {sortLevel :: Int, sortRelevance :: Relevance}-  deriving Eq+newtype Sort = Sort {sortLevel :: Int}+  deriving (Eq,Num) +instance Lattice Sort where+  x ⊔ Sort (-1) = Sort (-1) -- is this a lattice? +  Sort x ⊔ Sort y = Sort (x ⊔ y)+ instance Show Sort where-    show s = render (prettySortNam s)+    show s = render (pretty s)   instance Pretty Relevance where-    pretty (Relevance 0) = mempty-    pretty (Relevance r) = superscriptPretty r+    pretty (Re) = mempty+    pretty (Ir) = "÷"  instance Pretty Sort where-    pretty s = "∗" <> prettySortNam s  -- ⋆★*∗+    pretty s = prettyLev s     -prettySortNam s = prettyLev s <> prettyRel s--prettyRel (Sort _ r) = pretty r+star = "∗" -- ⋆★*∗ -prettyLev (Sort 0 _) = mempty-prettyLev (Sort l _) = subscriptPretty l+prettyLev (Sort (-1) ) = "□"+prettyLev (Sort 0    ) = star <> mempty+prettyLev (Sort l    ) = star <> subscriptPretty l -instance Num Sort where-    Sort l1 r1 + Sort l2 r2 = Sort (l1 + l2) (r1 + r2)-    negate (Sort l r) = Sort (negate l) (negate r)+above (Sort l) = Sort (l + 1)+oneLev = Sort 1 -above (Sort l r) = Sort (l + 1) r-oneLev = Sort 1 0+zero = Sort 0 -oneRel = Sort 0 1-next :: Relevance -> Relevance-next = (+ 1)+arrow Ir = "⇒"+arrow Re = "→" -zero = Sort 0 0 +colon Ir = text "÷"                  +colon Re = text "∶"                   -(+.) :: Relevance -> Sort -> Relevance-r +. (Sort _ r') = r + r'
Main.hs view
@@ -47,6 +47,7 @@      putStrLn "Parse Failed."      putStrV 1 $ "Tokens:" <+> pretty ts      putStrLn $ fname ++ ":" ++ err+     return False    Ok tree -> do       process fname tree @@ -60,7 +61,7 @@     [] -> return ()     _ -> putStrV 0 $ vcat info -- display constraints, etc.   case checked of-    Right (a,b,_o) -> do +    Right (a,b) -> do         putStrV 0 $ "nf =" <+> pretty a        putStrV 0 $ "ty =" <+> pretty b {-@@ -70,9 +71,10 @@            putStrV v $ "T =" <+> prettyTerm (S.singleton i) t          _ -> putStrV v "not a function!" -}-       putStrLn "Done!"-    Left (e,err) -> let Irr (line,col) = termPosition e -                    in putStrV 0 (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ":" <+> err)+       return True+    Left (e,err) -> do let Irr (line,col) = termPosition e +                       putStrV 0 (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ":" <+> err)+                       return False        {- showTree tree@@ -83,7 +85,9 @@  main :: IO () main = do -  mapM_ runFile (files options)+  results <- mapM runFile (files options)+  let oks = filter id results+  putStrV 0 $ pretty (length oks) <> "/" <> pretty (length results) <+> "files typecheck."
Normal.hs view
@@ -24,39 +24,53 @@            Star :: Sort -> NF           -     -- FIXME: only "column" / relevance should be here.      Pi  :: Relevance -> Ident -> NF -> NF -> NF      Lam :: Relevance -> Ident -> NF -> NF -> NF       App :: Relevance -> Neutral -> 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+     Proj  :: Relevance -> -- ^ 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                   OfParam :: Ident -> NF -> Neutral -     Destr :: Relevance -> Variable -> Variable -- argument: level destroyed-     Param :: Relevance -> Variable -> Variable +     Destr :: Int -> Variable -> Variable -- argument: depth where destruction occurs.+     Param :: Variable -> Variable       V :: Sort -> 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]  deriving instance Eq (Term n)+deriving instance Show (Term n)  var :: Int -> NF var x = Neu $ var' x -var' x = Var $ V (Sort 0 0) x+var'' = V (Sort 0) +var' x = Var $ V (Sort 0) x + -- | Hereditary substitution subst0 :: NF -> NF -> NF subst0 u = subst (u:map (var) [0..])   +showShift (Sort l) = replicate l '^'   subst :: Subst -> Term n -> NF subst f t = case t of@@ -74,15 +88,47 @@    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 o x -> param o (s x)-  Destr f x -> destroy f (s x)+  Param x -> param (s x)  where s' = subst (var 0 : map 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)@@ -101,34 +147,33 @@      Hole x -> Hole x   V s x -> shift s (fst $ f !! x)-  Param o (V s x) -> shift s (snd $ f !! x)-  Param o x -> Param o (s x)-  Destr f x -> Destr f (s x)- where s' o = subst' (p o f)+  Param (V s x) -> shift s (snd $ f !! x)+  Param x -> Param (s x)+ where s' o = subst' (p f)        s  = subst' f-       p o xs = (V zero 0, Param o $ V zero 0) : map (both $ wkv 1) xs-       +       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@(Sort _ r) t = case t of+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 +. d) i (s ty) (s' bo)-  (Pair o i x y) -> Pair (o +. d) i (s x) (s y)-  Pi o i a b -> Pi (o +. d) i (s a) (s' b)-  Sigma o i a b -> Sigma (o +. d) i (s a) (s' b)-  (App o a b) -> App (o +. d) (s a) (s b)-  (Proj o x k f) -> Proj (o +. d) (s x) k f+  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 i (s x)+  OfParam i x -> OfParam (modId (++showShift d) i) (s x)    Hole x -> Hole x-  Param o x -> Param (o +. d) (s x)-  Destr f x -> Destr (f + r) (s 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@@ -151,19 +196,29 @@  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 (Destr d x) = Destr d (wkv n x)-wkv n (Param o x) = Param o (wkv n x)+wkv n (Param x) = Param (wkv n x) wkv n (V s x) = V s (x + n) wkv n (Hole x) = Hole x -param :: Relevance -> NF -> NF-param o t = transNF 0 t o+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++ ----------------------------------- -- Display @@ -171,6 +226,7 @@  freeVars :: Term n -> [Int] freeVars (Var x) = freeVars x+freeVars (Destr _ 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)@@ -181,38 +237,37 @@ freeVars (Hole _) = mempty freeVars (Pair _ _ x y) = freeVars x <> freeVars y freeVars (Proj _ x _ _) = freeVars x-freeVars (Param _ x) = freeVars x+freeVars (Param x) = freeVars x freeVars (OfParam _ x) = freeVars x-freeVars (Destr _ x) = freeVars x  iOccursIn :: Int -> Term n -> Bool iOccursIn x t = x `elem` (freeVars t) -prettyRel' = prettySortNam- 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 (Destr i x) = cPrint p ii x <> "%" <> pretty i-cPrint p ii (Param o x) = cPrint p ii x <> sss (pretty o) <> "!"+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 (-1) ii x <> "⌋" cPrint p ii (Hole x) = text x cPrint p ii (Star i) = pretty i-cPrint p ii (V s k) +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 | s == Sort 0 0 = mempty-             | otherwise = "⇧" <> prettySortNam s-cPrint p ii (Proj o x k (Irr f))     = cPrint p ii x <> sss (pretty o) <> (if k then "#" else "/") <> text f+  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 t@(Pi _ _ _ _)    = parensIf (p > 1) (printBinders "→" ii mempty $ nestedPis t)-cPrint p ii t@(Sigma _ _ _ _) = parensIf (p > 1) (printBinders "×" ii mempty $ nestedSigmas t)-cPrint p ii (t@(Lam _ _ _ _))   = parensIf (p > 1) (nestedLams ii mempty 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 (-1) ii y]) +cross Ir = "⤬" -- ⚔⤬⤫⨯+cross Re = "×" -- ×⨯+ nestedPis  :: NF -> ([(Ident,Bool,NF,Relevance)], NF) nestedPis (Pi o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedPis b) nestedPis x = ([],x)@@ -221,23 +276,24 @@ nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedSigmas b) nestedSigmas x = ([],x) -printBinders :: 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 <+> sep)) (pis,b)+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 _ 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 <+> ":" <+> cPrint 0 ii ty)) c+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 t         = (text "\\ " <> (sep $ toList $ (xs |> "->")) <+> nest 3 (cPrint 0 ii t)) -printBind' ii name occurs d o = case not (isDummyId name) ||  occurs of-                  True -> parens (sss (pretty o) <> pretty name <+> text ":" <+> cPrint 0 ii d)+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-+                   nestedApp :: Neutral -> (Neutral,[(Relevance, 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)@@ -259,16 +315,22 @@                       in (v, Hole "does not appear!")                           -- Param evil v) -evil = Sort 0 666+-- 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)) -renam :: Int -> Int -> NF -> NF-renam d idx = subst [var $ mv d $ x | x <- [0..]] . shift' d oneRel -renam' d = subst' (map (mv' d) [0..])+-- renam :: Int -> Int -> NF -> NF+-- renam d idx = id -- subst [var $ mv d $ x | x <- [0..]]  +-- renam' d = subst' (map (mv' d) [0..])+ re :: Ident -> Ident-re (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,x++"₁")))+re (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,x++"°")))  arity, idx :: Int arity = 1@@ -276,66 +338,58 @@   -- | Transform a term to its relational interpretation--- NOTE: the level of the sort is incorrect! In fact only the rel. ever matters. (Destroy)-transV :: Int -> Variable -> Relevance -> Variable--transV d (V o x) o' | x < d =                V o $ (arity + 1) * x-                    | otherwise = Param o' $ V o $ (x - d) + (arity + 1) * d-transV d (Param o' x) o = Param o' $ transV d x o-transV d (Destr n x) o = destroy n (transV d x o)-transV d (Hole s) _ = Hole (s ++ "!")+transV    :: Int -> Variable -> Variable -transNe :: Int -> Neutral -> Relevance -> NF-transNe d (Var v) o = Neu $ Var $ transV d v o-transNe d (App o f a) o' = app o (app (next o) (transNe d f o') (renam d idx a)) (transNF d a o) -transNe d (Proj o x k f) o' = proj o (transNe d x o) k f-transNe d (OfParam i t) o = app o (renam' d t) (renam d idx (Neu $ OfParam i t))+transV  d (V o x) = Param $ V o x+transV  d (Param x) = Param $ transV d x+transV  d (Hole s) = Hole (s ++ "!") -transNF :: Int -> NF -> Relevance -> NF-transNF d (Neu v) o = transNe d v o-transNF d (Lam o i ty bo) o' = transBind d Lam o i ty (transNF (d+1) bo o')-transNF d (Pair o i x y) o' = Pair o i (transNF d x o) (transNF d y o') -transNF d ty@(Star  _) o = trans' d ty o-transNF d ty@(Pi    _ _ _ _) o = trans' d  ty o-transNF d ty@(Sigma _ _ _ _) o = trans' d ty o+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) -trans' d ty o = Lam (next o) (synthId "z₁") (renam d idx ty) (zerInRel d ty o)+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 --- | Build a relation witnessing x ∈ ⟦ty⟧. (where 'x' is Bound 0 in 'ty'.)+trans'  d ty = Lam Ir (synthId "z") ty (zerInRel d ty) --- In the translated context, 'z1', ... 'zn' are bound, but not--- 'zR'. (we are going to bind it soon).  However, 'inTrans' assumes--- it has "full" translated context.  So we weaken 'ty' (putting 'z' in scope) and apply the--- translation as normal.  But the translation is well behaved, so it--- does not use 'zR'. We substitute it with nothing when the job is--- done.-zerInRel d ty o = str $ inTrans (d + 1) (wk ty) o (var 0)+-- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)+zerInRel d ty = inTrans (d + 1) (wk ty) (var 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 :: Int -> NF -> Relevance -- ^ sort of the 1st argument-           -> NF -> NF-inTrans d (Star  s)       o z = (Pi (next o) dummyId (renam d idx z) (Star s))-inTrans d (Pi    o i a b) o' z = transBind d Pi o i a (inTrans (d + 1) b o' (app o (wk z) (var 0)))-inTrans d (Sigma o i a b) o' z = Sigma o i (inTrans d a o (proj o z True f)) -                             (subst (var 0:wk (renam d idx (proj o z True f)):map var [1..]) $-                              inTrans (1 + d) b o' (proj o (wk z) False f)) -- TEST: is depth ok?++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 o z = app (next o) (transNF d t o) (renam d idx z) +inTrans d t z = app Ir (transNF d t) z   -- | 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 o i a rest = binder (next o) (re i) (renam d idx a) $-                                binder o            i  (zerInRel d a o) $ -                                rest+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 +transBind d binder Ir i a rest = binder Ir i a rest  -- Invariant: the whole term is not destroyed.-destroy :: Relevance -> Term n -> Term n+destroy :: Int -> Term n -> Term n destroy d t = case t of   Var x -> Var $ pr x   Neu x -> Neu $ pr x@@ -343,8 +397,8 @@   V o x -> V o x   Hole x -> Hole x   Destr d' t -> destroy (min d d') t -- coalesce-  Param r x | r+1 == d -> x-            | otherwise -> Destr d $ Param r x +  Param x | d == 0 -> x+          | otherwise -> Destr d $ Param x     (Star o) -> Star o   (Pi o i a b)    -> mb Pi    o i a b @@ -352,24 +406,24 @@   (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 a) (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 b)+                   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+    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 `destroys` o+   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 a) (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 -r `destroys` r' = r' >= r
Options.hs view
@@ -13,6 +13,7 @@   Args {verb :: Int,         typeSystem :: TypeSystem,         showSorts :: Bool,+        collapseRelevance :: Bool,         files :: [String]         }    deriving (Show, Data, Typeable)@@ -23,6 +24,7 @@                                    CCω &= name "I" &= help "CCω (Impredicative)"]                                , -- &= opt (0 :: Int),                 showSorts = False &= help "display sort annotations in normal forms",+                collapseRelevance  = False &= help "! (param) does not generate new relevance levels.",                 files = [] &= args &= typFile               }
RawSyntax.hs view
@@ -15,9 +15,9 @@ ESet.    Exp6 ::= Sort ; EParam.  Exp4 ::= Exp4 "!"; EUp.     Exp4 ::= Exp4 "^";-ELeft.   Exp4 ::= Exp4 "<";+-- ELeft.   Exp4 ::= Exp4 "<"; EDestr.  Exp4 ::= Exp4 "%" Natural ;-EProj.   Exp4 ::= Exp4 "#" AIdent ;+EProj.   Exp4 ::= Exp4 "." AIdent ; EExtr.   Exp4 ::= Exp4 "/" AIdent ; EApp.    Exp3 ::= Exp3 Exp4 ; EPi.     Exp2  ::= Exp3 Arrow Exp2 ;@@ -33,7 +33,7 @@ terminator AIdent "" ; terminator Decl ";" ; -token Arrow  '-' '>' ;+token Arrow  ('-' '>') | ('=' '>') ;  NoBind. Bind   ::= AIdent ;  Bind.   Bind   ::= "(" AIdent ":" Exp ")" ;@@ -46,6 +46,6 @@  position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ; -position token Sort '*' (digit*) ('@' digit+)?;+position token Sort ('#' | '*' (digit*));  |]
Terms.hs view
@@ -21,7 +21,7 @@      Hole :: Irr Position -> String -> Term -- placeholder      Star :: Irr Position -> Sort -> Term -- sort      Bound :: Irr Position -> Int -> Term -- variable-     Pi :: Ident -> Term -> Term -> Term +     Pi :: Relevance -> Ident -> Term -> Term -> Term       Sigma :: Ident -> Term -> Term -> Term      Lam :: Ident -> Term -> Term -> Term       Pair :: Ident -> Term -> Term -> Term @@ -43,13 +43,13 @@      -- relational interpretations and world destruction.  In normal      -- form, arguments to these are either themselves or a variable.      Param :: Term -> Term -     Destroy :: Relevance -> Term -> Term+     Destroy :: Int -> Term -> Term  termPosition :: Term -> Irr Position  termPosition (Hole p _) = p termPosition (Star p _) = p termPosition (Bound p _) = p-termPosition (Pi i _ _) = identPosition i+termPosition (Pi _ i _ _) = identPosition i termPosition (Sigma i _ _) = identPosition i termPosition (Lam i _ _) = identPosition i termPosition (Pair i _ _) = identPosition i@@ -147,7 +147,7 @@  freeVars :: Term -> [Int] freeVars (Ann a b) = freeVars a <> freeVars b-freeVars (Pi _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b) freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b) freeVars (Bound _ x) = [x] freeVars (a :$: b) = freeVars a <> freeVars b@@ -170,7 +170,8 @@  cPrint :: Int -> DisplayContext -> Term -> Doc cPrint p ii (Destroy i x) = cPrint p ii x <> "%" <> pretty i-cPrint p ii (Shift o x) = cPrint 6 ii x <> "⇧" <> 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 (OfParam i x) = pretty i                              -- "⌊" <> cPrint (-1) ii x <> "⌋"@@ -183,7 +184,8 @@ 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))-cPrint p ii (Pi name d r)    = parensIf (p > 1) (sep [printBind ii name d r <+> text "→", cPrint 1 (name <| ii) r])+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 (Ann c ty)      = parensIf (p > 0) (cPrint 1 ii c <+> text ":" <+> cPrint 0 ii ty)
TypeCheckerNF.hs view
@@ -67,59 +67,62 @@ dispContext ctx = case viewl ctx of   EmptyL -> mempty   Bind x val typ o :< ctx' -> let di = display ctx' in (case val of-    Abstract   ->             pretty x <+>                             ":" <+> di typ <+> ":" <+> pretty o+    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), ":" <+> di typ <+> ":" <+> pretty o]+    Direct   v ->             pretty x <+> sep ["=" <+> parens (di v), colon o <+> di typ]     ) $$ dispContext ctx' -instance Lattice Sort where -  s1@(Sort l1 r1) ⊔ s2@(Sort l2 r2) -    | r1 /= r2 = s2-    | otherwise = case typeSystem options of-      CCω | l2 == 0 -> s2 -- The impredicative rule of CCω-      _ -> Sort (max l1 l2) r2+-- FIXME: flag an error if impredicativity disabled and we use it anyway.  hole = Neu . Var . Hole -iType :: Context -> Term -> Result (Value,Type,Relevance)+todo = Re++resurrect :: Relevance -> Context -> Context+resurrect Re = id+resurrect Ir = fmap (\e -> e {entryRelevance = Re})++iType :: Context -> Term -> Result (Value,Type) iType g (Ann e tyt)   =     do  (ty,o) <- iSort g tyt              v <- cType g e ty-            return (v,ty,sortRelevance o) -- annotations are removed+            return (v,ty) -- annotations are removed iType g t@(Terms.Star p s)-   =  return (Star s,Star $ above s, sortRelevance s)  -iType g (Terms.Pi ident tyt tyt')  -   =  do  (ty ,s1) <- iSort g tyt -          let r1 = sortRelevance s1+   =  return (Star s,Star $ above s)  +iType g (Terms.Pi r1 ident tyt tyt')  +   =  do  (ty ,s1) <- iSort (resurrect r1 g) tyt            (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'           let o = s1 ⊔ s2-          return (Pi r1 ident ty ty', Star o, sortRelevance o)+          return (Pi r1 ident ty ty', Star o) iType g (Terms.Sigma ident tyt tyt')  -   =  do  (ty,s1)  <- iSort g tyt -          let r1 = sortRelevance s1+   =  do  let r1 = todo+          (ty,s1)  <- iSort (resurrect r1 g) tyt            (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'           let o = s1 ⊔ s2-          return (Sigma r1 ident ty ty', Star o, sortRelevance o)-iType g e@(Terms.Bound _ x) = return $ (val $ entryValue e, wkn (x+1) $ entryType e,entryRelevance e)+          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)   where val (Direct v) = wkn (x+1) v-        val _ = var x-        e = g `index` x+        val _ = var x -- etaExpand o (var' x) typ+        Bind _ value typ 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), 0)+  return (hole x, hole ("type of " ++ x)) iType g (e1 Terms.:$: e2)-  =     do  (v1,si,o') <- iType g e1+  =     do  (v1,si) <- iType g e1             case si of               Pi o _ ty ty' -> do -                   v2 <- cType g e2 ty-                   return (app o v1 v2, subst0 v2 ty',o') +                   v2 <- cType (resurrect o g) e2 ty+                   return (app o v1 v2, subst0 v2 ty')                _             ->  throwError (e1,"invalid application") iType g (Terms.Proj e f) = do-  (v,t,o') <- iType g e+  (v,t) <- iType g e   search v t- where search :: NF -> NF -> Result (Value,Type,Relevance)+ where search :: NF -> NF -> Result (Value,Type)        search v (Sigma o (Irr (Identifier (_,f'))) ty ty') -              | f == f' = return (π1,ty,o)+              | f == f' = return (π1,ty)               | otherwise = search π2 (subst0 π1 ty')            where                   (π1,π2) = (case v of@@ -129,39 +132,39 @@        search _ _ = throwError (e,"field not found")  iType g (Terms.Pair ident e1 e2) = do-  (v1,t1,o) <- iType g e1-  (v2,t2,o') <- iType (Bind ident (Direct v1) t1 o <| g) e2-  return $ (Pair o ident v1 (str v2),Sigma o ident t1 t2,o ⊔ o')+  (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) -- 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 _ o) <- iSort g ty-    (ve,t,o') <- iType (Bind x Abstract vty o <| g) e-    return $ (Lam o x vty ve, Pi o x vty t, o')+    (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 (Terms.Param e) = do-  (v,t,o) <- iType g e-  return (param o v, app (next o) (param o t) (shift oneRel v), o)+  (v,t) <- iType g e+  return (param v, app Ir (param t) v)  iType g (Terms.Shift f e) = do-  (v,t,o) <- iType g e-  return (shift f v, shift f t, o + sortRelevance f)+  (v,t) <- iType g e+  return (shift f v, shift f t)  iType g x@(Terms.Destroy d e) = do-  (v,t,o) <- iType g e  -  case d `destroys` o of-    True -> throwError (x,"total destruction is forbidden. destroyed term:" <+> display g v)-    False -> return (destroy d v,destroy d t, d-1) +  (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 0)+         return $ (hole h, Sort 1)     _ -> throwError (e,displayT g e <+> "is not a type")  unify :: Context -> Term -> Type -> Type -> Result ()@@ -207,11 +210,7 @@   -- Γ ⊢ A ⌊A⌋ : ⟦B⟧ ⌊A⌋   -- Γ ⊢ A x   : ⟦B⟧ x   -- Γ ⊢ A     : (x : ⌊B⌋) → ⟦B⟧ x-  -- FIXME: here I just assume the relevance of t is the following.-  let theRelevance = 0 -      theType = Pi (next theRelevance) i (shift oneRel $ t) -                   (zerInRel 0 t theRelevance)-  e' <- cType g e theType       +  e' <- cType g e $ Pi Ir i t (zerInRel 0 t)   return (Neu $ OfParam i e')  cType g (Terms.Shift f e) t = do@@ -222,7 +221,7 @@   -- sort.  cType g e v -  =     do (e',v',_o) <- iType g e+  =     do (e',v') <- iType g e            unify g e v v'            return e'
tutorial/01-Module.ua view
@@ -49,12 +49,12 @@ -- Dependent pairs can also be declared depPair  = (A = Nat, suc) : ((A : *1) ; A -> A), --- fields named in the type can be extracted using #:-extract = depPair # A,+-- fields named in the type can be extracted using .:+extract = depPair.A,  -- Finally we must give the last component of the tuple, which is NOT -- named.  Since we have nothing special in mind, let's just give a--- trival (meaningless) term:+-- random simple term:  *
tutorial/02.1-Relevance.ua view
@@ -1,61 +1,60 @@--- Relevance levels and erasure----------------------------------+-- Relevance and erasure+------------------------- --- In uAgda, each term can exist at a specific relevance. --- --- For example * is the most relevant level, *< is less relevant, etc.--- --- The idea is that a term less relevant worlds can be erased, and the--- terms remains meaningful.+-- 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. --- For example, we can use a more precise type of the Leibniz equality--- that says that the actual type used is irrelevant for the predicate:+-- 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 =>. -Eq = \ A a b -> (P : A -> *) -> P a -> P b-     : (A : *<) -> (a b : A) -> *1,+-- 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:+-- follows... --- We assume an (abstract) representation N of naturals, in a less--- relevant world, as well as constructors for successor and zero. -Nat = \(N : *<) (s : N -> N) (z : N) ->+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 as normal (the predicate is in *)-\(n : N) -> (P : N -> *) -> P z -> ((m : N) -> P m -> P (s m)) -> P 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 first world of relevance to erase (all less relevant worlds--- will be erased as well).+-- is the depth of irrelevancy to erase.  -Nat-representation = Nat % 1,+Nat-representation = Nat % 0,  -- The normal form of the above term reveals that the result is the -- usual Church encoding for naturals.----- Each term can be copied to a less relevant world:--shiftType = \A -> A<-          : * -> *<,--shiftValue -  = \ A a -> a<-  : (A : *) -> (a : A) -> A<,----- In summary, occurences of the < operator can be understood as--- relevance annotations. They can be used mark types, terms and their--- usage as irrelevant. They are useful for erasure, but may be safely--- ignored otherwise.   *
tutorial/03-Parametricity.ua view
@@ -6,27 +6,18 @@ \(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),----- Note that the "x" an irrelevant argument to f!. We say that it lies--- in another relevance world. This is indicated by the postfix <--- after its type.---- that is ok, because we can always convert a term into a copy of it at --- a less relevant level (using that operator).-+fparam = f! : (x : A) => A! x -> B! (f x),  -- 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): -eraseType = ((x : A<) -> A! x -> B! (f< x)) % 1,+eraseType = ((x : A) => A! x -> B! (f x)) % 0,  --- Indeed, f!%1 = f.-fAgain = fparam %1,+-- Indeed, f!%0 = f.+fAgain = fparam %0,   -- We can get binary parametricity by combination of unary@@ -35,9 +26,7 @@  -- http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466 -fparam2 = f!!%2 : (x y : A<) -> A!!%2 x y -> B!!%2 (f< x) (f< y),--+fparam2 = f!!%1, -- : (x y : A) => A!!%2 x y => B!!%2 (f x) (f y),   *)
tutorial/03.1-Parametricity-Use.ua view
@@ -1,26 +1,23 @@ -- let's use parametricity in a useful way: prove that any--- function of type (X : *) -> X -> X is the identity.+-- function of type (X : #) -> X -> X is the identity. --- To simplify the example we use impredicativity here, use--- the -I flag to enable it.+-- To simplify the example we use impredicativity here. -Eq = \A a b -> (P : A -> *) -> P a -> P b-   : (A : *<) -> A -> A -> *+Eq = \A a b -> (P : A => #) -> P a -> P b+   : (A : #) -> A => A => #    ,  Theorem = -  (f : (A : *) -> A -> A) ->-  (A : *) ->+  (f : (A : #) -> A -> A) ->+  (A : #) ->   (x : A) ->-  Eq A< x< (f A x)<,+  Eq A x (f A x),  -proof = \(f : (A : *) -> (a : A) -> A) ->-        \(A : *) ->-        \(x : A) -> f! A< (Eq A< x<) x< (\_ p -> p)+proof = \(f : (A : #) -> (a : A) -> A) ->+        \(A : #) ->+        \(x : A) -> f! A (\y -> Eq A x y) x (\_ p -> p)       : Theorem-- ,-* +#
tutorial/04-Data.ua view
@@ -29,7 +29,7 @@  param Q = \ q -> ( -Nat = \n -> (P : q#Nat -> *) -> ((n : q#Nat) -> P n -> P (q#suc n)) -> (P q#zer) -> P n,+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), \ _ -> *)@@ -45,15 +45,15 @@   -- From there we can do simple computations:-one = Q#suc Q#zer : Q#Nat,-two = Q#suc one,+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<,+         : (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,@@ -62,11 +62,11 @@ -- That's fine, because we also have an operator for that: postfix ^.  lift = \n -> n^-     : Q#Nat -> Q#Nat^,+     : Q.Nat -> Q.Nat^,  plus - = \m n -> n^! (\_ -> Q#Nat) (\_ r -> Q#suc r) m - : Q#Nat -> Q#Nat -> Q#Nat,+ = \m n -> n^! (\_ -> Q.Nat) (\_ r -> Q.suc r) m + : Q.Nat -> Q.Nat -> Q.Nat,   four = plus two two,
uAgda.cabal view
@@ -1,5 +1,5 @@ name:           uAgda-version:        1.0.0.2+version:        1.1.0.0 category:       Dependent Types synopsis:       A simplistic dependently-typed language with parametricity. description: