packages feed

nanoAgda 0.1.0 → 0.1.1

raw patch · 6 files changed

+8/−261 lines, 6 files

Files

AbsSynToTerm.hs view
@@ -73,11 +73,7 @@                               (A.EAbs _ _ _) -> throwError "cannot use lambda for type"    _              -> Pi (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)-{-- where o = case arrow of                     -         A.Arrow "=>" -> Pr-         A.Arrow "->" -> Ty--}+ 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.EAnn e1 e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2
Main.hs view
@@ -64,25 +64,11 @@     Right (a,b) -> do         putStrV 0 $ "nf =" <+> pretty a        putStrV 0 $ "ty =" <+> pretty b-{--       case b of -         (Pi i s t) -> do-           putStrV v $ "s ∈ ⟦S⟧ =" <+> prettyTerm (S.singleton i) (zerInRel s)-           putStrV v $ "T =" <+> prettyTerm (S.singleton i) t-         _ -> putStrV v "not a function!"--}        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- = do-      putStrV 2 $ "\n[Abstract Syntax]\n\n" ++ show tree-      putStrV 2 $ "\n[Linearized tree]\n\n" ++ printTree tree--}- main :: IO () main = do    results <- mapM runFile (files options)
Normal.hs view
@@ -30,17 +30,12 @@            Sigma :: Ident -> NF -> NF -> NF      Pair  :: Ident -> NF -> NF -> NF  -- Pair does not bind any variable.-     Proj  :: -- ^ 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.+     Proj  :: Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.               Irr String -> Neutral       -           V :: Int -> Variable -- deBruijn index       Hole :: String -> Variable - type Subst = [NF]  deriving instance Eq (Term n)@@ -49,17 +44,12 @@ var :: Int -> NF var x = Neu $ var' x -var'' = V - var' x = Var $ V 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   Neu x -> s x@@ -80,10 +70,12 @@        s  = subst f  +-- | Hereditary application app :: NF -> NF -> NF  app (Lam i _ bo) u = subst0 u bo app (Neu n)      u = Neu (App n u) +-- | Hereditary projection proj :: NF -> Bool -> Irr String -> NF proj (Pair _ x y) True f = x proj (Pair _ x y) False f = y
Terms.hs view
@@ -47,84 +47,6 @@ termPosition (Extr x _) = termPosition x termPosition (Ann x _) = termPosition x -{--bound = Bound dummyPosition---- | Hereditary application--- invariant: preserves normal forms -app :: Term -> Term -> Term -app (Lam i _ bo) u = subst0 u bo-app neutral u = neutral :$: u--subst0 :: Term -> Term -> Term-subst0 u = subst (u:map bound [0..])  --type Subst = [Term]------ | Hereditary substitution-subst :: Subst -> Term -> Term-subst f t = case t of-  Bound _ x -> f !! x-  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)-  (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-  (Extr x f) -> extr (s x) f-  Hole p x -> Hole p x-  Star p x -> Star p x-  Param arity x -> param0 arity (s x)-  OfParam i x -> OfParam i (s x)-  Shift f x -> ssubst f (s x)-  Destroy i x -> Destroy i (s x) -- need to move to sort annotated terms to do this correctly. -  - where s' = subst (bound 0 : map wk f)-       s  = subst f---- | Non-hereditary substitution-subst' :: Subst -> Term -> Term-subst' f t = case t of-  Bound _ x -> f !! x-  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)-  (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-  (Extr x f) -> Extr (s x) f-  Hole p x -> Hole p x-  Star p x -> Star p x-  Param arity x -> Param arity (s x)-  OfParam i x -> OfParam i (s x)-  Shift f x -> Shift f (s x)-  Destroy i x -> Destroy i (s x)-  - where s' = subst (bound 0 : map wk f)-       s  = subst f---wkn n = subst' (map bound [n..])-wk = wkn 1-str = subst0 (Hole dummyPosition "oops!")---- | Hereditary projection-proj (Extr x f')   f | f /= f' = proj x f-proj (Pair (Irr (Identifier (_pos,f'))) x y) f -  | f == f' = x-   | f /= f' = proj (str y) f-proj x f = Proj x f---- | Hereditary extraction-extr (Pair (Irr (Identifier (_pos,f'))) x y) f | f == f' = str y-extr x f = Extr x f---}- deriving instance Show (Term) deriving instance Eq (Term) @@ -185,152 +107,3 @@ instance Pretty Term where     pretty = prettyTerm mempty -{-------------------------------------------------------------------- Sort substitution--ssubst :: Sort -> Term -> Term-ssubst f t = case t of-  Bound p x -> Shift f (Bound p x)-  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)-  (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-  (Extr x f) -> Extr (s x) f-  Hole p x -> Hole p x-  Star p x -> Star p (f + x)-  Param arity x -> Param arity (s x)-  OfParam i x -> OfParam (modId (++ show f) i) (s x)  -  Shift f' x -> ssubst (f + f') x-  Destroy f x -> Destroy f (s x)- where s = ssubst f-------------------------------------------------------------------- Hereditary parametricity transform--type Env = [Subst]--renam :: Env -> Int -> Term -> Term-renam g idx a = ssubst nextRel $ subst (g !! idx) a--re :: Int -> Ident -> Ident-re idx = modId (++ subscriptShow idx)--param0 arity = param arity (map (Param arity . bound) [0..] : replicate arity (map bound [0..]))---- | Transform a term to its relational interpretation-param :: Int -> Env -> Term -> Term-param arity = paramProg-  where-  extCtx gs = [bound idx:map (wkn (arity + 1)) g | (idx,g) <- zip (0:reverse [1..arity]) gs]-    -  paramProg :: Env -> Term -> Term-  paramProg g (Shift f x) = Shift f (paramProg g x) -  paramProg g (Destroy f x) = Param arity (Destroy f x)-  paramProg g (Hole p s) = Hole p ("[" ++ s ++ "]")-  paramProg g (Bound p x) = g !! 0 !! x-  paramProg g (Lam i ty bo) = paramBind g Lam  i ty $-                          paramProg (extCtx g) bo-    -  paramProg g (Pair i x y) = -     Pair i (paramProg g x) -            (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 (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"-  paramProg g (OfParam i x) = case arity of-      0 -> OfParam (modId (\x -> "⌈" ++ x ++ "⌉") i) (paramProg g x)                                -      1 -> x `app` ssubst nextRel (OfParam i x) -      _ -> error "mismatch in arity not yet supported"-  paramProg g x@(Param _ _) = Param arity x -- FIXME: here the renaming substitution should be applied;-                              -- but applying the current substitution has the effect of swapping the params.-  paramProg g ty = appl [Lam (synthId $ "z" ++ subscriptShow i) (wkn (i-1) $ renam g i ty) | i <- [1..arity] ] (zerInRel g ty)--  appl :: [a -> a] -> a -> a-  appl []     x = x-  appl (f:fs) x = f (appl fs x)--  -- | Build a relation witnessing x ∈ ⟦ty⟧. (where 'x' is not bound in 'ty'.)-  zerInRel :: Env -> Term -> Term-  zerInRel gs ty = inParam (map (map (wkn arity)) gs) ty (reverse $ map bound [0..arity-1])--  -- | Build a relation z ∈ ⟦ty⟧.  z is a term that, after renaming,-  -- gives the vector of terms member of the relation.  Note that-  -- 'param' is never applied to 'z', therefore 'zR' never occurs in the result.--  inParam :: Env -> Term -> [Term] -> Term-  inParam g (Star  p s)   zs = appl [Pi dummyId (wkn i z) | (i,z) <- zip [0..] zs] (Star p s)-  inParam g (Pi    i a b) zs = paramBind g Pi i a (inParam (extCtx g) b -                                                  [(wkn (arity + 1) z `app` bound i) | (i,z) <- zip (reverse [1..arity]) zs])--  inParam g@(g0:gs) (Sigma name@(Irr (Identifier (_,f))) a b) zs = -    Sigma name (inParam g a (map (`proj` f) zs))-    (inParam ((bound 0:map wk g0):[(proj (wk z) f):map wk g2 | (g2,z) <- zip gs zs]) b [(Extr (wk z) f) | z <- zs])-  -- z ∈ ⟦(x : A) × B(x)⟧ =   (x : π₁ z ∈ ⟦A⟧) × π₂ z ∈ ⟦B(x)⟧--  inParam g (Sigma _ _ _) z = error "Σ not implemented"-  inParam g t z = foldl app (paramProg g t) z--  -- | Translate a binding (x : A) into (x₁ : A₁) (⟦x⟧ : ⟦A⟧ x₁)-  paramBind :: Env -> (Ident -> Term -> Term -> Term) -> Ident -> Term -> Term -> Term-  paramBind g binder name a rest = -      appl -      [binder (re i name) (wkn (i-1) $ renam g i a) | i <- [1..arity]] $-      binder name         (zerInRel g a) $ -      rest --nextRel = Sort 0 1-nxt = ssubst nextRel------------------------------- destruction of worlds---destruction :: Int -> Seq Bool -> Term -> Maybe Term-destruction destroyed d t = case t of-  (Hole p x)  -> Just $ Hole p ("|" ++  x ++ "|")-  (Bound p x)  -    | x >= Data.Sequence.length d -> Just (Bound p x)  -    -- FIXME: this is incorrect; instead the callers of this function-    -- must give the correct value for variables of the environment.-    | otherwise -> if d `index` x then Just (Bound p x) else Nothing-  (Star p (Sort l w))  -      | w >= destroyed -> Nothing-  (Star p (Sort l r))  -> Just $ Star p (Sort l r)-  (Pi i a b)  -> mb d Pi i a b -  (Sigma i a b)  -> mb d Sigma i a b -  (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-                   Nothing -> pr a-                   Just b' -> (:$: b') <$> pr a -  (Proj x f) -> (\x -> Proj x f) <$> pr x  -  (Extr x f) -> (\x -> Extr x f) <$> pr x  -  -  -- FIXME: This should traverse the potential series of Param to find if the variable is removed.-  (Param arity (Bound p x)) | x < Data.Sequence.length d && not (d `index` x) -> Nothing-  -- Just a "renaming" on NFs: x should be a (renamed) variable.-  (Param arity x) -> Just (Destroy destroyed (Param arity x))-  (Shift f x)    ->  Just (Destroy destroyed (Shift f x))-   -  (OfParam n x) -> OfParam (modId (++ "%" ++ show destroyed) n) <$> pr x-  -- where mb d binder i a b = case pr a of-                             Nothing -> str <$> destruction destroyed (False <| d) b-                             Just a' -> binder i a' <$> destruction destroyed (True <| d) b-       pr x = destruction destroyed d x---- pr (Param x) d = Just x FIXME: there is a problem here: 1st--- order variables have been removed, so we cannot refer to them.---  --}
TypeCheckerNF.hs view
@@ -91,7 +91,7 @@ iType g e@(Terms.Bound _ x) = do   return $ (val $ value, wkn (x+1) $ typ)   where val (Direct v) = wkn (x+1) v-        val _ = var x -- etaExpand o (var' x) typ+        val _ = var x -- We could do eta-expansion here: etaExpand (var' x) typ         Bind _ value typ = g `index` x          iType g (Terms.Hole p x) = do@@ -140,7 +140,7 @@          return $ (hole h, Sort 1)     _ -> throwError (e,displayT g e <+> "is not a type") -+-- | Test if two types are equal. unify :: Context -> Term -> Type -> Type -> Result () unify g e q q' =          do let ii = length g
nanoAgda.cabal view
@@ -1,5 +1,5 @@ name:           nanoAgda-version:        0.1.0+version:        0.1.1 category:       Dependent Types synopsis:       A toy dependently-typed language description:@@ -16,7 +16,7 @@ author:         Jean-Philippe Bernardy maintainer:     jeanphilippe.bernardy@gmail.com Cabal-Version:  >= 1.8-tested-with:    GHC==6.12.3+tested-with:    GHC==7.2.2 build-type:     Simple  executable nanoAgda