uAgda 1.2.0.0 → 1.2.0.1
raw patch · 4 files changed
+42/−26 lines, 4 files
Files
- Normal.hs +17/−19
- TypeCheckerNF.hs +5/−6
- tutorial/03.2-Nested-Parametricity.ua +18/−0
- uAgda.cabal +2/−1
Normal.hs view
@@ -50,7 +50,7 @@ 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+ Hole :: Irr String -> Variable type Subst = [Cube NF] @@ -69,7 +69,7 @@ subst0 :: Cube NF -> NF -> NF subst0 u = subst (u:map (unit . var) [0..]) -hole = Neu . Var . Hole+hole = Neu . Var . Hole . Irr subst :: Subst -> Term n -> NF subst f t = case t of@@ -88,7 +88,7 @@ -- OfParam i x -> Neu (OfParam i (s x)) -- Destr d x -> destroy d (s x)- Hole x -> hole x+ Hole (Irr 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@@ -126,7 +126,7 @@ wk = wkn 1 str = strn 1-strn n = subst (replicate n (unit $ Neu $ Var $ Hole "str: oops!") ++ map (unit . var) [0..])+strn n = subst (replicate n (unit $ hole "str: oops!") ++ map (unit . var) [0..]) wkv :: Int -> Variable -> Variable wkv n (Param r x) = Param r (wkv n x)@@ -185,7 +185,7 @@ -- 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 (Hole (Irr x)) = text x cPrint p ii (Star i) = pretty i 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 "/")@@ -262,19 +262,16 @@ swapV q (V bv x) = Swap q $ V bv 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 v@(Param _ _) | isIdentity q' = v+ | otherwise = Swap (simplifyPerm n q) v+ where n = countParam v+ q' = simplifyPerm n q+swapV q (Hole (Irr s)) = Hole $ Irr (s ++ "#") swapV q x = Swap q x -power 0 f = id-power n f = f . power (n-1) f--(f *** g) (x,y) = (f x, g y) - -- 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)+countParam (Param Thing x) = 1 + countParam x+countParam x = 0 fullVarCube x = full (\i -> Neu $ Var $ V i x) @@ -328,7 +325,7 @@ maybeParam = if r == Thing then Param r else id -- keep only "proper" parametricity n = getDepth x -transV r d (Hole s) = Neu $ Var $ Hole (s ++ showRole r)+transV r d (Hole (Irr s)) = hole (s ++ showRole r) transNe :: Role -> Action -> Neutral -> NF transNe r d (Var v) = transV r d v@@ -357,7 +354,7 @@ 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)+trans' Thing d ty = Lam Pred (synthId "z") (unit1 (transNF Index d ty)) (zerInRel d ty) -- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.) zerInRel :: Action -> NF -> NF@@ -370,10 +367,11 @@ 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 (Star (Sort l δ)) z = (Pi Pred dummyId (unit1 z) (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 "⊘"))+inTrans d ty z = app Pred (transNF Thing d ty) (unit1 z) +unit1 z = (pair z (hole "⊘"))
TypeCheckerNF.hs view
@@ -73,11 +73,10 @@ dispContext :: Context -> Doc dispContext ctx0 = case viewl ctx0 of EmptyL -> mempty- Bind x val typ o :< ctx0' -> (let ctx = fmap entryIdent ctx0 - ctx' = fmap entryIdent ctx0'+ Bind x val typ o :< ctx0' -> (let 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]+ 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' todo = Regu -- for now sigma types are always of the "complete" cube kind.@@ -112,7 +111,7 @@ where val (Direct v) = wkn (x+1) v val _ = Neu $ Var $ V bv x typ = cubeAccess "iType var" typ0 bv- arg = updateCube (ones da) (hole "⊘") arg0+ arg = updateCube (ones da) (hole "⊘") arg0 arg0 = subCubeAt bv $ fullVarCube x (dim typ0) finalTyp = app Pred (wkn (x+1) typ) arg da = dim arg0@@ -176,7 +175,7 @@ (val,v,_) <- iType g e case v of Star i -> return (val,i)- (Neu (Var (Hole h))) -> do + (Neu (Var (Hole (Irr h)))) -> do report $ text h <+> "must be a type" return $ (hole h, Sort 1 0) _ -> throwError (e,displayT g e <+> "is not a type. Instead: " <+> display g v)
+ tutorial/03.2-Nested-Parametricity.ua view
@@ -0,0 +1,18 @@+-- nested parametricity example from the paper.+++\(A : *) ->++( + parametricity = \(x:A) -> x!+ : (x:A) -> A! @ {x},++ nested = parametricity!+ : (x : {A; A!}) -> A!! @ {x 0;x 1;x 0!},+ + nestedNF = \ (x : {A; A!}) -> x 1 ! #10+ : (x : {A; A!}) -> A!! @ {x 0;x 1;x 0!},+ ++*+)
uAgda.cabal view
@@ -1,5 +1,5 @@ name: uAgda-version: 1.2.0.0+version: 1.2.0.1 category: Dependent Types synopsis: A simplistic dependently-typed language with parametricity. description:@@ -24,6 +24,7 @@ tutorial/02-Holes.ua tutorial/03-Parametricity.ua tutorial/03.1-Parametricity-Use.ua+ tutorial/03.2-Nested-Parametricity.ua executable uAgda