Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
195 lines (164 sloc) 7.51 KB
> module Ivor.Datatype where
> import Ivor.TTCore
> import Ivor.Gadgets
> import Ivor.Typecheck
> import Ivor.Nobby
> import Ivor.PatternDefs
> import Ivor.Errors
> import Ivor.Values
> import Debug.Trace
> data Datadecl = Datadecl {
> datatycon :: Name,
> params :: [(Name,Raw)],
> tycontype :: Raw,
> constructors :: [(Name,Raw)]
> }
Elaborated version with elimination rule and iota schemes.
> data RawDatatype =
> RData { rtycon :: (Name,Raw),
> rdatacons :: [(Name,Raw)],
> rnum_params :: Int,
> rerule :: (Name,Raw),
> rcrule :: (Name,Raw),
> re_ischemes :: [RawScheme],
> rc_ischemes :: [RawScheme]
> }
> deriving Show
> data Datatype n =
> Data { tycon :: (n, Gval n),
> datacons :: [(n, Gval n)],
> num_params :: Int,
> erule :: (n, Indexed n),
> crule :: (n, Indexed n),
> e_ischemes :: Maybe (PMFun Name),
> c_ischemes :: Maybe (PMFun Name),
> e_rawschemes :: [RawScheme],
> c_rawschemes :: [RawScheme]
> }
> deriving Show
> getPat (Sch p i) = p
> getRed (Sch p i) = i
> getArity [] = 2 -- empty data type should have elim rule of arity 2!
> -- (actually not if they're dependent. Fix this.)
> getArity ss = length (getPat (ss!!0))
checkType checks a raw data type, with its elimination rule and iota
schemes, and returns a DataType, ready for compilation to entries in
the context and an executable elimination rule.
> checkType :: Gamma Name -> RawDatatype -> IvorM (Datatype Name)
> checkType gamma (RData (ty,kind) cons numps (er,erty) (cr,crty) eschemes cschemes) =
> do (kv, _) <- typecheck gamma kind
> let erdata = Elims er cr (map fst cons)
> let gamma' = extend gamma (ty,G (TCon (arity gamma kv) erdata) kv defplicit)
> (consv,gamma'') <- checkCons gamma' 0 cons
> (ev, _) <- typecheck gamma'' erty
> (cv, _) <- typecheck gamma'' crty
> -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)
> ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False
> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False
> return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
> (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)
> checkTypeNoElim :: Gamma Name -> RawDatatype -> IvorM (Datatype Name)
> checkTypeNoElim gamma (RData (ty,kind) cons numps (er,erty) (cr,crty) eschemes cschemes) =
> do (kv, _) <- typecheck gamma kind
> let erdata = Elims er cr (map fst cons)
> let gamma' = extend gamma (ty,G (TCon (arity gamma kv) erdata) kv defplicit)
> (consv,gamma'') <- checkCons gamma' 0 cons
> (ev, _) <- typecheck gamma'' erty
> (cv, _) <- typecheck gamma'' crty
> -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)
> return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
> (er,ev) (cr,cv) Nothing Nothing [] [])
> checkCons gamma t [] = return ([], gamma)
> checkCons gamma t ((cn,cty):cs) =
> do (cv,_) <- typecheck gamma cty
> let ccon = G (DCon t (arity gamma cv)) cv defplicit
> let gamma' = extend gamma (cn,ccon)
> (rest,gamma'') <- checkCons gamma' (t+1) cs
> return (((cn,ccon):rest), gamma'')
checkScheme takes a raw iota scheme and returns a scheme with a well-typed
RHS (or fails if there is a type error).
For a scheme of the form
foo p0 p1 ... pn = t
we get V 0 = pn ... V n = p0
then pattern variables are retrieved by projection with Proj in typechecked t.
> checkScheme :: Gamma Name -> Name -> RawScheme -> IvorM (Scheme Name)
> checkScheme gamma n (RSch pats (RWRet ret)) =
> do let ps = map (mkPat gamma) pats
> let rhsvars = getPatVars gamma ps
> let rhs = substVars gamma n rhsvars ret
> return (Sch (reverse ps) (Ind rhs))
Make a pattern from a raw term. Anything weird, just make it a "PTerm".
> mkPat :: Gamma Name -> Raw -> Pattern Name
> mkPat gam (Var n) = mkPatV n (lookupval n gam)
> where mkPatV n (Just (DCon t x)) = PCon t n tyname []
> mkPatV n (Just (TCon x _)) = PCon 0 n (UN "Type") []
> mkPatV n _ = PVar n
> tyname = case (getTyName gam n) of
> Just x -> x
> mkPat gam (RApp f a) = pat' (unwind f a)
> where unwind (RApp f s) a = let (f',as) = unwind f s in
> (f',(mkPat gam a):as)
> unwind (RFileLoc _ _ t) a = unwind t a
> unwind t a = (t, [mkPat gam a])
> pat' (Var n, as) = mkPatV n (lookupval n gam) (reverse as)
> pat' (RFileLoc _ _ t, as) = pat' (t, as)
> pat' _ = PTerm
> mkPatV n (Just (DCon t x)) as = PCon t n tyname as
> mkPatV n (Just (TCon x _)) as = PCon 0 n (UN "Type") as
> mkPatV _ _ _ = PTerm
> tyname = case (getTyName gam (getname (getappfun f))) of
> Just x -> x
> getname (Var n) = n
> getname (RFileLoc _ _ t) = getname t
> mkPat gam _ {-(RBind _ _ _)-} = PTerm
> {-
> TODO: If a datatype has a placeholder in its indices, the value should
> be inferred (i.e. it should be checked) otherwise we can't make a pattern
> properly (and we'll certainly need this for optimisation)
> mkPat gam x = error $ "Can't make a pattern from " ++ show x
> -}
Get the pattern variables from the patterns, and work out what the projection
function for each name is.
> getPatVars :: Gamma Name ->[Pattern Name] -> [(Name, TT Name)]
> getPatVars gam xs = pv' 0 (reverse xs)
> where pv' i [] = []
> pv' i (x:xs) = (project gam i x) ++ (pv' (i+1) xs)
indexify (n,t) = (n,Ind t)
Projection.
> project :: Gamma Name -> Int -> Pattern Name -> [(Name, TT Name)]
> project gam n x = project' n (\i -> V i) x
> where project' n f (PVar x) = [(x,f n)]
> project' n f (PCon _ fn ty es) = projargs n f 0 es ty
> project' n f (PMarkCon fn es) = projargs n f 0 es (UN "FOO")
> project' n f _ = [] -- Can't project from terms or marked vars.
> projargs n f i [] _ = []
> projargs n f i (PMark _:xs) ty = projargs n f i xs ty
> projargs n f i (x:xs) ty
> = (project' n ((\a -> (Proj ty i a)).f) x)
> ++ projargs n f (i+1) xs ty
-- > argtypes ty = case lookuptype ty gam of
-- > (Just (Ind ty)) -> map (getFnName.snd)
-- > $ getExpected ty
-- > getFnName (TyCon x _) = x
-- > getFnName (App f x) = getFnName f
-- > getFnName (Bind _ _ (Sc x)) = getFnName x
-- > getFnName x = MN ("Dunno: "++show x, 0)
Make a RHS of an iota scheme, substituting names with projection operations.
ASSUMPTION: No bindings on the RHS. This should be true of all iota schemes.
Takes the name of the elimination rule and assumes any reference to an
elimination rule is a reference to this
> substVars :: Gamma Name -> Name -> [(Name,TT Name)] -> Raw -> TT Name
> substVars gam er ns r = sv' r
> where sv' (Var x) = case (lookup x ns) of
> Nothing -> mkGood x
> (Just i) -> i
> sv' (RApp f a) = App (sv' f) (sv' a)
> sv' (RConst c) = Const c
> sv' (RFileLoc _ _ t) = sv' t
> mkGood x = case (lookupval x gam) of
> (Just (DCon t i)) -> Con t x i
> (Just (TCon i _)) -> TyCon x i
> (Just (ElimRule _)) -> Elim er
> _ -> P x
> dummyRule :: ElimRule
> dummyRule _ = Nothing
Something went wrong with that request. Please try again.