Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Tree: 30d87904d3
Fetching contributors…

Cannot retrieve contributors at this time

982 lines (839 sloc) 36.574 kB
> {-# OPTIONS_GHC -fglasgow-exts -XIncoherentInstances #-}
> module Ivor.TTCore where
> import Ivor.Gadgets
> import Ivor.Constant
> import Data.List
> import Data.Char
> import Control.Monad.State
> import Data.Typeable
> import Data.Binary hiding (get,put)
> import Debug.Trace
Raw terms are those read in directly from the user, and may be badly typed.
(Need to add marked up terms for optimisation).
> data Raw
> = Var Name
> | ROpts [Name]
> | RApp Raw Raw
> | RBind Name (Binder Raw) Raw
> | forall c.(Constant c) => RConst !c
> | RStar
> | RInfer -- Term to be inferred by the typechecker
> | RMeta Name -- a metavariable, to be implemented separately
> | RLabel Raw RComputation
> | RCall RComputation Raw
> | RReturn Raw
> | RAnnot String -- Debugging hack
> | RFileLoc FilePath Int Raw -- For more helpful type error messages
> | RStage RStage
> data RComputation = RComp Name [Raw]
> deriving Eq
> data RStage = RQuote Raw
> | RCode Raw
> | REval Raw
> | REscape Raw
> deriving Eq
TT represents terms in the core type theory, parametrised by the
representation of the names
> data TT n
> = P n
> | V Int
> | Con Int n Int -- Tag, name and arity
> | TyCon n Int -- Name and arity
> | Meta n (TT n) -- Metavariable and its type
> | Elim n
> | App (TT n) (TT n)
> | Bind n (Binder (TT n)) (Scope (TT n))
> | Proj n Int (TT n) -- Projection in iota schemes (carries type name)
> | Label (TT n) (Computation n)
> | Call (Computation n) (TT n)
> | Return (TT n)
> | forall c. Constant c => Const !c
> | Star
> | Stage (Stage n)
> data Computation n = Comp n [TT n]
Stage gives staging annotations
> data Stage n = Quote (TT n)
> | Code (TT n)
> | Eval (TT n) (TT n) -- term, type
> | Escape (TT n) (TT n) -- term, type
> deriving Show
Constants
> class (Typeable c, Show c, Eq c) => Constant c where
> constType :: c -> TT Name
> newtype Scope n = Sc n
> deriving (Show, Eq)
> data Binder n = B (Bind n) n
> deriving (Show, Eq)
> data Bind n
> = Lambda
> | Pi
> | Let n
> | Hole
> | Guess n
> | Pattern n
> | MatchAny
> deriving (Show, Eq)
Local environments
> type Env n = [(n,Binder (TT n))]
Separate types for de Bruijn indexed terms and de Bruijn levelled terms
> newtype Levelled n = Lev (TT n) deriving Eq
> newtype Indexed n = Ind (TT n) deriving Eq
Pattern represents the patterns used to define iota schemes.
> data Pattern n =
> PVar n -- Variable
> | PCon Int n n [Pattern n] -- Constructor, with tag and type
> | forall c.(Constant c) => PConst !c
> | PMarkCon n [Pattern n] -- Detagged constructor
> | PTerm -- Presupposed term (don't care what it is)
> | PMark n -- Marked variable
> instance Show n => Show (Pattern n) where
> show (PVar n) = show n
> show (PCon t n ty ts) = show n ++ show ts
> show (PConst c) = show c
> show (PMarkCon n ts) = show n ++ show ts
> show PTerm = "_"
> show (PMark n) = "[" ++ show n ++ "]"
> instance Eq n => Eq (Pattern n) where
> (==) (PVar x) (PVar y) = x == y
> (==) (PCon t1 n1 ty1 ts1) (PCon t2 n2 ty2 ts2) = t1 == t2 &&
> n1 == n2 &&
> ty1 == ty2 &&
> ts1 == ts2
> (==) (PConst x) (PConst y) = case cast x of
> Just x' -> x' == y
> _ -> False
> (==) (PMarkCon n1 ts1) (PMarkCon n2 ts2) = n1 == n2 && ts1 == ts2
> (==) PTerm PTerm = True
> (==) (PMark x) (PMark y) = x == y
> (==) _ _ = False
{- | forall c. Constant c => PConst c -- Constant (don't think it makes sense) -}
> instance Eq n => Ord (Pattern n) where
> compare (PCon x _ _ _) (PCon y _ _ _) = compare x y
> compare _ _ = EQ -- Don't care!
UN covers names defined by users, MN covers names invented by the system.
This keeps both namespaces separate.
> data Name
> = UN String
> | MN (String,Int)
> deriving (Ord, Eq)
> instance Typeable Name where
> typeOf n = mkTyConApp (mkTyCon "Name") []
Data declarations and pattern matching
> data RawWith = RWith Bool Raw [RawScheme] -- match with an extra arg, add new schemes
> | RWRet Raw -- if Bool is true, add an equality proof
> deriving Show
data With = With [Indexed n]
| WPatt [Pattern n]
| WNone
deriving Show
> data RawScheme = RSch [Raw] RawWith
> deriving Show
> data Scheme n = Sch [Pattern n] (Env n) (Indexed n)
> deriving Show
> type PMRaw = RawScheme
For equality of patterns, we're only interested in whether the LHS are
equal. This is so that we can easily filter out overlapping cases when
generating cases for coverage/type checking. Checking for overlapping
is dealt with later.
> instance Eq PMRaw where
> (==) (RSch ps r) (RSch ps' r') = ps == ps'
> type PMDef n = Scheme n
> data PMFun n = PMFun Int -- arity
> [PMDef n] -- patterns
> deriving Show
====================== Functors ===============================
> instance Functor Scope where
> fmap f (Sc x) = Sc (f x)
> instance Functor Binder where
> fmap f (B b x) = B (fmap f b) (f x)
> instance Functor Bind where
> fmap f Lambda = Lambda
> fmap f Pi = Pi
> fmap f (Let x) = Let (f x)
> fmap f Hole = Hole
> fmap f (Guess x) = Guess (f x)
> fmap f (Pattern x) = Pattern (f x)
> fmap f MatchAny = MatchAny
> instance Functor TT where
> fmap f (P x) = P (f x)
> fmap f (V i) = V i
> fmap f (Con t x i) = Con t (f x) i
> fmap f (TyCon x i) = TyCon (f x) i
> fmap f (Meta x t) = Meta (f x) (fmap f t)
> fmap f (Elim x) = Elim (f x)
> fmap f (App tf a) = App (fmap f tf) (fmap f a)
> fmap f (Bind n b sc) = Bind (f n) (fmap (fmap f) b) (fmap (fmap f) sc)
> fmap f (Proj n i x) = Proj (f n) i (fmap f x)
> fmap f (Const x) = Const x
> fmap f (Label t c) = Label (fmap f t) (fmap f c)
> fmap f (Call c t) = Call (fmap f c) (fmap f t)
> fmap f (Return t) = Return (fmap f t)
> fmap f (Stage t) = Stage (fmap f t)
> fmap f Star = Star
> instance Functor Stage where
> fmap f (Quote t) = Quote (fmap f t)
> fmap f (Code t) = Code (fmap f t)
> fmap f (Eval t ty) = Eval (fmap f t) (fmap f ty)
> fmap f (Escape t ty) = Escape (fmap f t) (fmap f ty)
> sLift :: (TT a -> TT b) -> Stage a -> Stage b
> sLift f (Quote t) = Quote (f t)
> sLift f (Code t) = Code (f t)
> sLift f (Eval t ty) = Eval (f t) (f ty)
> sLift f (Escape t ty) = Escape (f t) (f ty)
> sLiftf :: (TT a -> b) -> Stage a -> b
> sLiftf f (Quote t) = f t
> sLiftf f (Code t) = f t
> sLiftf f (Eval t ty) = f t
> sLiftf f (Escape t ty) = f t
> sLiftM :: Monad m => (TT a -> m (TT b)) -> Stage a -> m (Stage b)
> sLiftM f (Quote t) = do x <- f t
> return $ Quote x
> sLiftM f (Code t) = do x <- f t
> return $ Code x
> sLiftM f (Eval t ty) = do x <- f t
> xty <- f ty
> return $ Eval x xty
> sLiftM f (Escape t ty) = do x <- f t
> xty <- f ty
> return $ Escape x xty
> instance Functor Computation where
> fmap f (Comp n ts) = Comp (f n) (fmap (fmap f) ts)
> instance Functor Indexed where
> fmap f (Ind t) = Ind $ fmap f t
> instance Functor Levelled where
> fmap f (Lev t) = Lev $ fmap f t
====================== Gadgets for TT =============================
Do something hairy to all the Vs in a TT term. Kind of like fmap, only on
the variable numbers rather than the names.
Each V is processed with a function taking the context and the index.
> vapp :: (([n],Int) -> (TT n)) -> TT n -> TT n
> vapp f t = v' [] t
> where
> v' ctx (V i) = f (ctx,i)
> v' ctx (App f' a) = (App (v' ctx f') (v' ctx a))
> v' ctx (Bind n b (Sc sc)) = (Bind n (fmap (v' ctx) b)
> (Sc (v' (n:ctx) sc)))
> v' ctx (Proj n i x) = Proj n i (v' ctx x)
> v' ctx (Label t (Comp n cs))
> = Label (v' ctx t) (Comp n (fmap (v' ctx) cs))
> v' ctx (Call (Comp n cs) t)
> = Call (Comp n (fmap (v' ctx) cs)) (v' ctx t)
> v' ctx (Return t) = Return (v' ctx t)
> v' ctx (Stage t) = Stage (sLift (v' ctx) t)
> v' ctx x = x
> indexise :: Levelled n -> Indexed n
> indexise (Lev t) = Ind $ vapp (\ (ctx,i) -> V (i-((length ctx)-1))) t
> levelise :: Indexed n -> Levelled n
> levelise (Ind t) = Lev $ vapp (\ (ctx,i) -> V ((length ctx)-i-1)) t
Same, but for Ps
> papp :: (n -> (TT n)) -> TT n -> TT n
> papp f t = v' t
> where
> v' (P n) = f n
> v' (V i) = V i
> v' (Meta n t) = Meta n (v' t)
> v' (App f' a) = (App (v' f') (v' a))
> v' (Bind n b (Sc sc)) = (Bind n (fmap (v') b)
> (Sc (v' sc)))
> v' (Proj n i x) = Proj n i (v' x)
> v' (Label t (Comp n cs))
> = Label (v' t) (Comp n (fmap (v') cs))
> v' (Call (Comp n cs) t)
> = Call (Comp n (fmap (v') cs)) (v' t)
> v' (Return t) = Return (v' t)
> v' (Stage t) = Stage (sLift (v') t)
> v' x = x
FIXME: This needs to rename all duplicated binder names first, otherwise
we get a duff term when we go back to the indexed version.
> makePs :: TT Name -> TT Name
> makePs t = let t' = evalState (uniqifyAllState t) [] in
> vapp (\ (ctx,i) -> P (traceIndex ctx i ("makePs " ++
> debugTT t))) t'
> --if (i<length ctx) then P (ctx!!i)
> -- else V i) t'
> makePsUniq :: TT Name -> TT Name
> makePsUniq t = vapp (\ (ctx,i) -> P (traceIndex ctx i ("makePs " ++
> debugTT t))) t
> --if (i<length ctx) then P (ctx!!i)
> -- else V i) t'
> makePsEnv env t = let t' = evalState (uniqifyAllState t) env in
> vapp (\ (ctx,i) -> P (traceIndex ctx i
> ("makePsEnv" ++ debugTT t))) t'
> uniqifyAllState :: TT Name -> State [Name] (TT Name)
> uniqifyAllState (Bind n b (Sc sc)) =
> do names <- get
> let n' = uniqify n names
> put $ nub (n':names)
> b' <- uniqifyAllStateB b
> sc' <- uniqifyAllState sc
> return (Bind n' b' (Sc sc'))
> uniqifyAllState (App f a) =
> do f' <- uniqifyAllState f
> a' <- uniqifyAllState a
> return (App f' a')
> uniqifyAllState (Proj n i t) =
> do t' <- uniqifyAllState t
> return (Proj n i t')
> uniqifyAllState (Label t c) =
> do t' <- uniqifyAllState t
> c' <- uniqifyAllStateC c
> return (Label t' c')
> uniqifyAllState (Call c t) =
> do t' <- uniqifyAllState t
> c' <- uniqifyAllStateC c
> return (Call c' t')
> uniqifyAllState (Return t) =
> do t' <- uniqifyAllState t
> return (Return t')
> uniqifyAllState (Stage t) =
> do t' <- sLiftM uniqifyAllState t
> return (Stage t')
> uniqifyAllState x = return $ x
> uniqifyAllStateB (B Lambda ty) =
> do ty' <- uniqifyAllState ty
> return (B Lambda ty')
> uniqifyAllStateB (B Pi ty) =
> do ty' <- uniqifyAllState ty
> return (B Pi ty')
> uniqifyAllStateB (B Hole ty) =
> do ty' <- uniqifyAllState ty
> return (B Hole ty')
> uniqifyAllStateB (B (Let v) ty) =
> do ty' <- uniqifyAllState ty
> v' <- uniqifyAllState v
> return (B (Let v') ty')
> uniqifyAllStateB (B (Guess v) ty) =
> do ty' <- uniqifyAllState ty
> v' <- uniqifyAllState v
> return (B (Guess v') ty')
> uniqifyAllStateB (B (Pattern v) ty) =
> do ty' <- uniqifyAllState ty
> v' <- uniqifyAllState v
> return (B (Pattern v') ty')
> uniqifyAllStateB (B MatchAny ty) =
> do ty' <- uniqifyAllState ty
> return (B MatchAny ty')
> uniqifyAllStateC (Comp n cs) =
> do cs' <- mapM uniqifyAllState cs
> return (Comp n cs')
Take a term with explicit names and convert it to a term with
de Bruijn indices
> finalise :: Eq n => Indexed n -> Indexed n
> finalise (Ind tm) = Ind (pv [] tm)
> where
> pv env (P n) | Just i <- lookupidx 0 n env = V i
> | otherwise = P n
> pv env (App f a) = App (pv env f) (pv env a)
> pv env (Proj n i t) = Proj n i (pv env t)
> pv env (Bind n b@(B _ ty) (Sc t))
> = Bind n (fmap (pv env) b) (Sc (pv ((n,(pv env ty)):env) t))
> pv env (Label t (Comp n cs))
> = Label (pv env t) (Comp n (fmap (pv env) cs))
> pv env (Call (Comp n cs) t)
> = Call (Comp n (fmap (pv env) cs)) (pv env t)
> pv env (Return t) = Return (pv env t)
> pv env (Stage t) = Stage (sLift (pv env) t)
> pv env x = x
>
> lookupidx i n ((x,_):xs) | n==x = Just i
> | otherwise = lookupidx (i+1) n xs
> lookupidx i n [] = Nothing
Check the purity of a term; a term is pure iff it has no holes.
> pure :: TT Name -> Bool
> pure (Bind _ (B b ty) (Sc sc)) = purebind b && pure ty && pure sc
> pure (App f a) = pure f && pure a
> pure (Proj _ _ t) = pure t
> pure (Label t (Comp n cs)) = pure t && and (map pure cs)
> pure (Call (Comp n cs) t) = pure t && and (map pure cs)
> pure (Return t) = pure t
> pure (Stage t) = sLiftf pure t
> pure _ = True
>
> purebind Hole = False -- Seems a bit OTT to use a type class just for this...
> purebind (Guess _) = False
> purebind (Let t) = pure t
> purebind _ = True
Map a function across all binders in a term
> binderMap :: (Name -> Bind (TT Name) -> TT Name -> a) -> TT Name -> [a]
> binderMap f (Bind n (B b@(Let v) ty) (Sc sc))
> = (f n b ty):(binderMap f v) ++ (binderMap f ty) ++ (binderMap f sc)
> binderMap f (Bind n (B b@(Guess v) ty) (Sc sc))
> = (f n b ty):(binderMap f v) ++ (binderMap f ty) ++ (binderMap f sc)
> binderMap f (Bind n (B b@(Pattern v) ty) (Sc sc))
> = (f n b ty):(binderMap f v) ++ (binderMap f ty) ++ (binderMap f sc)
> binderMap f (Bind n (B b ty) (Sc sc))
> = (f n b ty):(binderMap f ty) ++ (binderMap f sc)
> binderMap bf (App f a) = binderMap bf f ++ binderMap bf a
> binderMap f (Proj _ _ t) = binderMap f t
> binderMap f (Label t (Comp n cs)) = binderMap f t ++
> concat (fmap (binderMap f) cs)
> binderMap f (Call (Comp n cs) t) = concat (fmap (binderMap f) cs) ++
> binderMap f t
> binderMap f (Return t) = binderMap f t
> binderMap f (Stage t) = sLiftf (binderMap f) t
> binderMap f _ = []
Substitute a term into V 0 in the scope (and weaken other indices)
I think this works! But de Bruijn index mangling breaks my brain, so
maybe find a better way, or think carefully about why this is okay...
> subst :: TT n -> Scope (TT n) -> TT n
> subst tm (Sc x) = vapp weakenv $ vapp subv x
> where subv (xs,i) | i == length xs = (vinc tm)
> | otherwise = V i
> weakenv (xs,i) | i > length xs = V (i-1)
> | otherwise = V i
> vinc (V n) = V (n+1) -- So that we weakenv it correctly
> vinc x = x
Traverse a term looking for metavariables. Replace them with concrete
names and return all the new names we need to define for it to be
a complete definition.
> updateMetas :: TT n -> (TT n, [(n, TT n)])
> updateMetas tm = runState (ums tm) []
> where ums (App f a) = do f' <- ums f
> a' <- ums a
> return (App f' a')
> ums (Meta n ty) = do ty' <- ums ty
> mvs <- get
> put ((n,ty'):mvs)
> return (P n)
> ums (Bind n (B b ty) (Sc sc))
> = do b' <- umsB b
> ty' <- ums ty
> sc' <- ums sc
> return (Bind n (B b' ty') (Sc sc'))
> ums x = return x
> umsB (Let v) = do v' <- ums v
> return (Let v')
> umsB (Guess v) = do v' <- ums v
> return (Guess v')
> umsB (Pattern v) = do v' <- ums v
> return (Pattern v')
> umsB x = return x
Return all the names used in a scope
> getNames :: (Show n, Eq n) => Scope (TT n) -> [n]
> getNames (Sc x) = nub $ p' x where
> p' (P x) = [x]
> p' (App f' a) = (p' f')++(p' a)
> p' (Bind n b (Sc sc))
> | scnames <- p' sc = ((nub scnames) \\ [n]) ++ pb' b
> p' (Proj _ i x) = p' x
> p' (Label t (Comp n cs)) = p' t ++ concat (map p' cs)
> p' (Call (Comp n cs) t) = concat (map p' cs) ++ p' t
> p' (Return t) = p' t
> p' (Stage t) = sLiftf p' t
> p' x = []
> pb' (B (Let v) ty) = p' v ++ p' ty
> pb' (B (Guess v) ty) = p' v ++ p' ty
> pb' (B (Pattern v) ty) = p' v ++ p' ty
> pb' (B _ ty) = p' ty
Return all the bound names used in a scope
> getBoundNames :: Eq n => Scope (TT n) -> [n]
> getBoundNames (Sc x) = nub $ p' x where
> p' (P x) = []
> p' (App f' a) = (p' f')++(p' a)
> p' (Bind n b (Sc sc)) = n:(p' sc) ++ pb' b
> p' (Proj _ i x) = p' x
> p' (Label t (Comp n cs)) = p' t ++ concat (map p' cs)
> p' (Call (Comp n cs) t) = concat (map p' cs) ++ p' t
> p' (Return t) = p' t
> p' (Stage t) = sLiftf p' t
> p' x = []
> pb' (B (Let v) ty) = p' v ++ p' ty
> pb' (B (Guess v) ty) = p' v ++ p' ty
> pb' (B (Pattern v) ty) = p' v ++ p' ty
> pb' (B _ ty) = p' ty
The following gadgets expect a fully explicitly named term, rather than
with de Bruijn indices or levels. We need a newtype Named n.
> substName :: (Show n, Eq n) => n -> TT n -> Scope (TT n) -> TT n
> substName p tm (Sc x) = p' x where
> p' (P x) | x == p = tm
> p' (App f' a) = (App (p' f') (p' a))
> p' (Bind n b (Sc sc)) = (Bind n (fmap p' b) (Sc (p' sc)))
> -- | n == p = (Bind n (fmap p' b) (Sc sc))
> -- | otherwise
> p' (Proj n i x) = Proj n i (p' x)
> p' (Label t (Comp n cs)) = Label (p' t) (Comp n (map p' cs))
> p' (Call (Comp n cs) t) = Call (Comp n (map p' cs)) (p' t)
> p' (Return t) = Return (p' t)
> p' (Stage t) = Stage (sLift p' t)
> p' x = x
Look for a specific term and replace it.
Probably hopelessly inefficient.
> substTerm :: (Show n, Eq n) => TT n -> TT n -> Scope (TT n) -> TT n
> substTerm p tm (Sc x) = p' x where
> p' x | x == p = tm
> p' (App f' a) = (App (p' f') (p' a))
> p' (Bind n b (Sc sc)) = (Bind n (fmap p' b) (Sc (p' sc)))
> -- | n == p = (Bind n (fmap p' b) (Sc sc))
> -- | otherwise
> p' (Proj n i x) = Proj n i (p' x)
> p' (Label t (Comp n cs)) = Label (p' t) (Comp n (map p' cs))
> p' (Call (Comp n cs) t) = Call (Comp n (map p' cs)) (p' t)
> p' (Return t) = Return (p' t)
> p' (Stage t) = Stage (sLift p' t)
> p' x = x
> getSc (Sc x) = x
Apply a function (non-recursively) to every sub term.
> mapSubTerm :: (TT Name -> TT Name) -> TT Name -> TT Name
> mapSubTerm f = mst where
> mst (App ff s) = App (f ff) (f s)
> mst (Bind x b (Sc sc)) = Bind x (fmap f b) (Sc (f sc))
> mst (Proj n i ty) = Proj n i (f ty)
> mst (Stage t) = Stage (sLift f t)
> mst x = x
Get the arguments of an application
> getArgs :: TT Name -> [TT Name]
> getArgs (App f a) = getArgs f ++ [a]
> getArgs _ = []
> getRawArgs :: Raw -> [Raw]
> getRawArgs (RApp f a) = getRawArgs f ++ [a]
> getRawArgs (RFileLoc f l t) = getRawArgs t
> getRawArgs _ = []
Get the function being applied in an application
> getFun :: TT Name -> TT Name
> getFun (App f a) = getFun f
> getFun x = x
Get the expected arguments of a function type
> getExpected :: TT Name -> [(Name,TT Name)]
> getExpected (Bind n (B Pi ty) (Sc sc)) = (n,ty):(getExpected sc)
> getExpected _ = []
Get the return type of a function type
> getReturnType :: TT Name -> TT Name
> getReturnType (Bind n (B Pi ty) (Sc sc)) = getReturnType sc
> getReturnType x = x
Make a name unique in the given environment
> uniqify :: Name -> [Name] -> Name
> uniqify x env | x `elem` env = uniqify (mangleName x) env
> | otherwise = x
x -> x0, x1 -> x2, etc. Increments an index at the end of a name, in order
to generate a new and hopefully unique name.
> mangleName :: Name -> Name
> mangleName (MN (n,i)) = MN (n,i+1)
> mangleName (UN n) = UN (incName n)
> where incName x | (num, name) <- span isDigit (reverse x)
> = (reverse name)++show (inc num)
>
> inc :: String -> Int
> inc "" = 0
> inc xs = (read (reverse xs)) + 1
Bind a list of things
> bind :: Bind (TT Name) -> [(Name,TT Name)] -> Scope (TT Name) -> TT Name
> bind binder [] sc = getSc sc
> bind binder ((n,ty):xs) sc = Bind n (B binder ty) (Sc (bind binder xs sc))
Apply a function to a list of arguments
> appArgs :: TT n -> [TT n] -> TT n
> appArgs f [] = f
> appArgs f (x:xs) = appArgs (App f x) xs
====================== Show instances =============================
> instance Show Name where
> show = forget
> instance Show n => Show (TT n) where
> show x = forget (forget x)
> instance Show Raw where
> show = forget
> instance Show n => (Show (Levelled n)) where
> show = show.indexise
> instance Show n => (Show (Indexed n)) where
> show (Ind t) = show t
===================== Eq instances ================================
> instance Eq Raw where
> (==) (Var x) (Var y) = x==y
> (==) (RApp f a) (RApp f' a') = f==f' && a==a'
> (==) (RBind n b sc) (RBind n' b' sc') = n==n' && b==b' && sc==sc'
> (==) (RConst x) (RConst y) = case cast x of
> Just x' -> x'==y
> Nothing -> False
> (==) RStar RStar = True
> (==) (RLabel t (RComp n cs)) (RLabel t' (RComp n' cs')) =
> t==t' && n==n' && cs == cs'
> (==) (RCall (RComp n cs) t) (RCall (RComp n' cs') t') =
> t==t' && n==n' && cs == cs'
> (==) (RReturn t) (RReturn t') = t == t'
> (==) (RStage t) (RStage t') = t == t'
> (==) RInfer RInfer = True
> (==) (RMeta x) (RMeta x') = x == x'
> (==) (RFileLoc f l t) (RFileLoc _ _ t') = t == t'
> (==) _ _ = False
> instance Eq n => Eq (TT n) where
> (==) (P x) (P y) = x==y
> (==) (V i) (V j) = i==j
> (==) (Con t x i) (Con t' y j) = x==y
> (==) (TyCon x i) (TyCon y j) = x==y
> (==) (Meta x t) (Meta y t') = x==y && t==t'
> (==) (Elim x) (Elim y) = x==y
> (==) (App f a) (App f' a') = f==f' && a==a'
> (==) (Bind _ b sc) (Bind _ b' sc') = b==b' && sc==sc'
Eta equality:
> (==) (Bind x (B Lambda ty) (Sc (App t (V 0)))) t' = t == t'
> (==) t' (Bind x (B Lambda ty) (Sc (App t (V 0)))) = t == t'
> (==) (Proj _ i x) (Proj _ j y) = i==j && x==y
> (==) (Const x) (Const y) = case cast x of
> Just x' -> x'==y
> Nothing -> False
> (==) Star Star = True
> (==) (Label t (Comp n cs)) (Label t' (Comp n' cs')) =
> t==t' -- && n==n' && cs == cs'
> (==) (Call (Comp n cs) t) (Call (Comp n' cs') t') =
> t==t' -- && n==n' && cs == cs'
> (==) (Return t) (Return t') = t == t'
> (==) (Stage t) (Stage t') = t == t'
> (==) _ _ = False
> instance Eq n => Eq (Stage n) where
> (==) (Quote t) (Quote t') = t == t'
> (==) (Code t) (Code t') = t == t'
> (==) (Eval t _) (Eval t' _) = t == t'
> (==) (Escape t _) (Escape t' _) = t == t'
> (==) _ _ = False
===================== Forgetful maps ==============================
> instance Forget Name String where
> forget (UN n) = n
> forget (MN ("INFER",i)) = "y"++show i
> forget (MN ("T",i)) = "z"++show i
> forget (MN (x,i)) = x ++ "[" ++ show i ++ "]"
> instance Forget Raw String where
> forget x = fPrec 10 x where
> fPrec :: Int -> Raw -> String
> fPrec _ (Var n) = forget n
> fPrec _ (ROpts n) = show n
> fPrec x (RApp f a) = bracket x 1 $ fPrec 1 f ++ " " ++ fPrec 0 a
> fPrec x (RBind n (B Lambda t) sc) = bracket x 2 $
> "["++forget n ++":"++fPrec 10 t++"]" ++ fPrec 10 sc
> fPrec x (RBind n (B Pi t) sc)
> | nameOccurs n sc = bracket x 2 $
> "("++forget n ++":"++fPrec 10 t++") -> " ++ fPrec 10 sc
> | otherwise = bracket x 2 $
> (fPrec 1 t) ++" -> " ++ fPrec 10 sc
> fPrec x (RBind n (B (Let v) t) sc) = bracket x 2 $
> "let "++forget n ++":"++ fPrec 10 t
> ++"=" ++ fPrec 10 v ++ " in " ++ fPrec 10 sc
> fPrec x (RBind n (B Hole t) sc) = bracket x 2 $
> "?"++forget n ++":"++fPrec 10 t++"." ++ fPrec 10 sc
> fPrec x (RBind n (B (Guess v) t) sc) = bracket x 2 $
> "try "++forget n ++":"++fPrec 10 t
> ++"=" ++ fPrec 10 v ++ " in " ++ fPrec 10 sc
> fPrec x (RBind n (B (Pattern v) t) sc) = bracket x 2 $
> "patt "++forget n ++":"++fPrec 10 t
> ++"=" ++ fPrec 10 v ++ " in " ++ fPrec 10 sc
> fPrec x (RBind n (B MatchAny t) sc) = bracket x 2 $
> "patt "++forget n ++":"++fPrec 10 t ++ " in " ++ fPrec 10 sc
> fPrec _ (RLabel t c) =
> "< "++fPrec 10 t++" : "++fcomp c++" >"
> fPrec x (RCall c t) = bracket x 3 $
> "call < " ++ fcomp c ++ " > "++ fPrec 0 t
> fPrec _ (RReturn t) = "return " ++ fPrec 0 t
> fPrec _ (RStage (RQuote t)) = "{'" ++ fPrec 10 t ++ "}"
> fPrec _ (RStage (RCode t)) = "{{" ++ fPrec 10 t ++ "}}"
> fPrec _ (RStage (REval t)) = "!" ++ fPrec 0 t
> fPrec _ (RStage (REscape t)) = "~" ++ fPrec 0 t
> fPrec _ (RConst x) = show x
> fPrec _ (RStar) = "*"
> fPrec _ (RInfer) = "_"
> fPrec _ (RMeta n) = "?"++forget n
> fPrec p (RFileLoc f l t) = fPrec p t
> fPrec p (RAnnot s) = "[" ++ s ++ "]"
> bracket outer inner str | inner>outer = "("++str++")"
> | otherwise = str
> fcomp (RComp n cs) = forget n ++ showargs cs
> where showargs [] = ""
> showargs (x:xs) = " " ++ fPrec 0 x ++ showargs xs
> instance Forget RStage String where
> forget (RQuote x) = "{'" ++ forget x ++ "}"
> forget (RCode x) = "{{" ++ forget x ++ "}}"
> forget (REval x) = "{!" ++ forget x ++ "}"
> forget (REscape x) = "{~" ++ forget x ++ "}"
> instance Show n => Forget (Indexed n) Raw where
> forget (Ind t) = forget t
> instance Show n => Forget (Levelled n) Raw where
> forget (Lev t) = forget t
> instance (Show Name) => Forget (TT Name) Raw where
> forget t = forgetTT (vapp showV t)
> where
> showV (ctx,i) | i < length ctx = P (ctx!!i)
> | otherwise = V i
> forgetTT (P x) = case (cast x) of
> Just (MN ("INFER",i)) -> RInfer
> _ -> Var $ UN (show x)
> forgetTT (V i) = RAnnot $ "v" ++ (show i)
> forgetTT (Con t x i) = Var $ UN (show x)
> forgetTT (TyCon x i) = Var $ UN (show x)
> forgetTT (Meta n i) = RMeta (UN (show n ++ " : " ++ show i))
> forgetTT (Elim x) = Var $ UN (show x)
> forgetTT (App f a) = RApp (forgetTT f) (forgetTT a)
> forgetTT (Bind n (B Lambda t) (Sc sc)) =
> (RBind (UN (show n)) (B Lambda (forget t)) (forget sc))
> forgetTT (Bind n (B Pi t) (Sc sc)) =
> (RBind (UN (show n)) (B Pi (forget t)) (forget sc))
> forgetTT (Bind n (B MatchAny t) (Sc sc)) =
> (RBind (UN (show n)) (B MatchAny (forget t)) (forget sc))
> forgetTT (Bind n (B (Let v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Let (forget v)) (forget t))
> (forget sc))
> forgetTT (Bind n (B Hole t) (Sc sc)) =
> (RBind (UN (show n)) (B Hole (forget t)) (forget sc))
> forgetTT (Bind n (B (Guess v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Guess (forget v)) (forget t))
> (forget sc))
> forgetTT (Bind n (B (Pattern v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Pattern (forget v)) (forget t))
> (forget sc))
> forgetTT (Proj n i t) = RAnnot $ (show t)++"!"++(show i)++":"++show n
> forgetTT (Label t (Comp n cs)) = RLabel (forgetTT t)
> (RComp (UN $ show n)
> (map forgetTT cs))
> forgetTT (Call (Comp n cs) t) = RCall (RComp (UN $ show n)
> (map forgetTT cs))
> (forgetTT t)
> forgetTT (Return t) = RReturn (forgetTT t)
> forgetTT (Stage t) = RStage (forget t)
> forgetTT (Const x) = RConst x
> forgetTT Star = RStar
> instance (Show n) => Forget (TT n) Raw where
> forget t = forgetTT (vapp showV t)
> where
> showV (ctx,i) | i < length ctx = P (ctx!!i)
> | otherwise = V i
> forgetTT (P x) = Var $ UN (show x)
> forgetTT (V i) = RAnnot $ "v" ++ (show i)
> forgetTT (Con t x i) = Var $ UN (show x)
> forgetTT (TyCon x i) = Var $ UN (show x)
> forgetTT (Meta n i) = RMeta (UN (show n ++ " : " ++ show i))
> forgetTT (Elim x) = Var $ UN (show x)
> forgetTT (App f a) = RApp (forgetTT f) (forgetTT a)
> forgetTT (Bind n (B Lambda t) (Sc sc)) =
> (RBind (UN (show n)) (B Lambda (forget t)) (forget sc))
> forgetTT (Bind n (B Pi t) (Sc sc)) =
> (RBind (UN (show n)) (B Pi (forget t)) (forget sc))
> forgetTT (Bind n (B MatchAny t) (Sc sc)) =
> (RBind (UN (show n)) (B MatchAny (forget t)) (forget sc))
> forgetTT (Bind n (B (Let v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Let (forget v)) (forget t))
> (forget sc))
> forgetTT (Bind n (B Hole t) (Sc sc)) =
> (RBind (UN (show n)) (B Hole (forget t)) (forget sc))
> forgetTT (Bind n (B (Guess v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Guess (forget v)) (forget t))
> (forget sc))
> forgetTT (Bind n (B (Pattern v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Pattern (forget v)) (forget t))
> (forget sc))
> forgetTT (Proj n i t) = RAnnot $ (show t)++"!"++(show i)++":"++show n
> forgetTT (Label t (Comp n cs)) = RLabel (forgetTT t)
> (RComp (UN $ show n)
> (map forgetTT cs))
> forgetTT (Call (Comp n cs) t) = RCall (RComp (UN $ show n)
> (map forgetTT cs))
> (forgetTT t)
> forgetTT (Return t) = RReturn (forgetTT t)
> forgetTT (Stage t) = RStage (forget t)
> forgetTT (Const x) = RConst x
> forgetTT Star = RStar
> instance Show n => Forget (Stage n) RStage where
> forget (Code x) = RCode (forget x)
> forget (Quote x) = RQuote (forget x)
> forget (Eval x _) = REval (forget x)
> forget (Escape x _) = REscape (forget x)
> testid = (Bind (UN "x") (B Lambda Star) (Sc (V 0)))
> testterm = (App testid Star)
Some handy gadgets for Raw terms
> mkapp f [] = f
> mkapp f (x:xs) = mkapp (RApp f x) xs
> getargnames (RBind n _ sc) = n:(getargnames sc)
> getargnames (RFileLoc _ _ t) = getargnames t
> getargnames _ = []
> getappargs (RApp f a) = getappargs f ++ [a]
> getappargs (RFileLoc _ _ t) = getappargs t
> getappargs _ = []
> getappfun (RApp f a) = getappfun f
> getappfun (RFileLoc _ _ t) = getappfun t
> getappfun x = x
> getrettype (RBind n (B Pi _) sc) = getrettype sc
> getrettype (RFileLoc _ _ t) = getrettype t
> getrettype x = x
> nameOccurs x (Var n) | x == n = True
> | otherwise = False
> nameOccurs x (RApp f a) = nameOccurs x f || nameOccurs x a
> nameOccurs x (RBind n b sc)
> | x == n = False
> | otherwise = occBind x b || nameOccurs x sc
> nameOccurs x (RLabel r comp) = nameOccurs x r || occComp x comp
> nameOccurs x (RCall comp r) = nameOccurs x r || occComp x comp
> nameOccurs x (RReturn r) = nameOccurs x r
> nameOccurs x (RStage s) = occStage x s
> nameOccurs x (RFileLoc f l t) = nameOccurs x t
> nameOccurs x _ = False
> occComp x (RComp _ rs) = or $ map (nameOccurs x) rs
> occBind x (B (Let v) t) = nameOccurs x v || nameOccurs x t
> occBind x (B _ t) = nameOccurs x t
> occStage x (RQuote r) = nameOccurs x r
> occStage x (RCode r) = nameOccurs x r
> occStage x (REval r) = nameOccurs x r
> occStage x (REscape r) = nameOccurs x r
> fileLine (RFileLoc f l t) = Just (f,l)
> fileLine (RBind n b sc) = fileLine sc
> fileLine _ = Nothing
> debugTT t = show (forgetTT (vapp showV t))
> where
> showV (ctx,i) | i < length ctx = P (UN ("{v}"++show i))
> | otherwise = V i
> forgetTT (P x) = Var $ UN (show x)
> forgetTT (V i) = RAnnot $ "v" ++ (show i)
> forgetTT (Con t x i) = Var $ UN (show x)
> forgetTT (TyCon x i) = Var $ UN (show x)
> forgetTT (Meta x i) = RMeta (UN (show x))
> forgetTT (Elim x) = Var $ UN (show x)
> forgetTT (App f a) = RApp (forgetTT f) (forgetTT a)
> forgetTT (Bind n (B Lambda t) (Sc sc)) =
> (RBind (UN (show n)) (B Lambda (forget t)) (forget sc))
> forgetTT (Bind n (B Pi t) (Sc sc)) =
> (RBind (UN (show n)) (B Pi (forget t)) (forget sc))
> forgetTT (Bind n (B (Let v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Let (forget v)) (forget t))
> (forget sc))
> forgetTT (Bind n (B Hole t) (Sc sc)) =
> (RBind (UN (show n)) (B Hole (forget t)) (forget sc))
> forgetTT (Bind n (B (Guess v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Guess (forget v)) (forget t))
> (forget sc))
> forgetTT (Bind n (B (Pattern v) t) (Sc sc)) =
> (RBind (UN (show n)) (B (Pattern (forget v)) (forget t))
> (forget sc))
> forgetTT (Proj n i t) = RAnnot $ (show t)++"!"++(show i)++":"++show n
> forgetTT (Label t (Comp n cs)) = RLabel (forgetTT t)
> (RComp (UN $ show n)
> (map forgetTT cs))
> forgetTT (Call (Comp n cs) t) = RCall (RComp (UN $ show n)
> (map forgetTT cs))
> (forgetTT t)
> forgetTT (Return t) = RReturn (forgetTT t)
> forgetTT (Stage (Quote t)) = RStage (RQuote (forgetTT t))
> forgetTT (Stage (Code t)) = RStage (RCode (forgetTT t))
> forgetTT (Stage (Eval t _)) = RStage (REval (forgetTT t))
> forgetTT (Stage (Escape t _)) = RStage (REscape (forgetTT t))
> forgetTT (Const x) = RConst x
> forgetTT Star = RStar
> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))
> pToV = pToV2 0
> pToV2 v p (P n) | p==n = Sc (V v)
> | otherwise = Sc (P n)
> pToV2 v p (V w) = Sc (V w)
> pToV2 v p (Con t n i) = Sc (Con t n i)
> pToV2 v p (TyCon n i) = Sc (TyCon n i)
> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))
> where getSc (Sc a) = a
> pToV2 v p (Elim n) = Sc (Elim n)
> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)
> (pToV2 (v+1) p sc))
> where getSc (Sc a) = a
> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))
> (getSc (pToV2 v p a))
> where getSc (Sc a) = a
> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))
> (Comp n (map (getSc.(pToV2 v p)) ts))
> pToV2 v p (Call (Comp n ts) t) = Sc $ Call
> (Comp n (map (getSc.(pToV2 v p)) ts))
> (getSc (pToV2 v p t))
> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))
> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))
> where getSc (Sc a) = a
> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
> pToV2 v p (Const x) = Sc (Const x)
> pToV2 v p Star = Sc Star
Jump to Line
Something went wrong with that request. Please try again.