Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
tree: 203a4359a7
Fetching contributors…

Cannot retrieve contributors at this time

129 lines (103 sloc) 5.134 kb
> module Ivor.MakeData where
> import Ivor.TTCore
> import Ivor.Datatype
> import Debug.Trace
Transform a raw data declaration (just parameters and constructors)
into a full data definition with iota schemes.
FIXME: Throughout all this, need to ensure that the elimination operator name,
the target, methods and the motives are unique.
> type Params = [(Name,Raw)]
> type Constructors = [(Name,Raw)]
> mkRawData :: Monad m =>
> Name -> Params -> Raw -> Constructors -> m RawDatatype
> mkRawData name params contype cons =
> let ecasetype = mkCaseType True name params contype cons
> motiveName methNames
> ccasetype = mkCaseType False name params contype cons
> motiveName methNames
> datacons = mkDatacons params cons
> eischemes = mkSchemes True name (ruleName name "Elim")
> params datacons motiveName methNames
> cischemes = mkSchemes False name (ruleName name "Case")
> params datacons motiveName methNames
> tycontype = mkCon params contype in
> return $ RData (name,tycontype) datacons (length params)
> (ruleName name "Elim", ecasetype) -- elim rule
> (ruleName name "Case", ccasetype) -- case rule
> eischemes -- elim rule iota schemes
> cischemes -- case rule iota schemes
> where ruleName (UN n) suff = (UN (n++suff)) -- TMP HACK!
> motiveName = (UN "Phi")
> methName (UN n) = (UN ("meth_"++n))
> methNames = map (methName.fst) cons
> mkSchemes :: Bool -> Name -> Name -> Params -> Constructors -> Name ->
> [Name] -> [RawScheme]
> mkSchemes rec n ername ps cs motive mns = mks cs mns mns
> where mks [] [] mns = []
> mks ((c,cty):cs) (m:ms) mns
> = (mkScheme rec n ername ps c cty motive mns m):(mks cs ms mns)
> mkScheme rec n ername ps c cty motive mns meth
> = RSch (mkIArgs ps c cty motive mns)
> (RWRet (mkIRet rec n ername meth motive mns ps cty))
> mkIArgs ps c cty motive mns = getappargs (getrettype cty) ++
> [mkapp (Var c) (map Var (getargnames cty))] ++
> (map Var (motive:mns))
> mkIRet rec tyname ername meth motive mns ps cty =
> mkapp (Var meth) (drop (length ps) (mkArgs cty))
> where mkArgs (RBind n (B Pi ty) sc)
> | isrec ty tyname && rec
> = (Var n):(mkRecApp ername ty n motive mns):(mkArgs sc)
> | otherwise = (Var n):(mkArgs sc)
> mkArgs (RFileLoc f l t) = mkArgs t
> mkArgs _ = []
> mkRecApp en ty n motive mns =
> mkapp (Var en) $ (getappargs ty)++(map Var (n:motive:mns))
> mkCon :: Params -> Raw -> Raw
> mkCon [] ty = ty
> mkCon ((x,xty):xs) ty = RBind x (B Pi xty) (mkCon xs ty)
> mkDatacons :: Params -> Constructors -> Constructors
> mkDatacons _ [] = []
> mkDatacons ps ((x,xty):xs) = (x,(mkCon ps xty)):(mkDatacons ps xs)
> mkCaseType :: Bool -> Name -> Params -> Raw -> Constructors -> Name ->
> [Name] -> Raw
> mkCaseType rec n ps ty cs motiveName mns
> = bindParams ps $
> bindIndices ty $
> bindTarget targetName n ps ty $
> bindMotive motiveName targetName n ps ty $
> bindMethods rec n motiveName ps cs mns $
> applyMethod motiveName targetName ty
> where targetName = UN "target" -- TMP HACK!
> bindParams [] rest = rest
> bindParams ((n,ty):xs) rest = RBind n (B Pi ty) (bindParams xs rest)
> bindIndices (RBind n (B Pi ty) sc) rest
> = (RBind n (B Pi ty) (bindIndices sc rest))
> bindIndices (RFileLoc f l t) rest = bindIndices t rest
> bindIndices sc rest = rest
> bindTarget x n ps ty rest
> = RBind x
> (B Pi (mkapp (Var n) (map Var ((map fst ps)++(getargnames ty)))))
> rest
> bindMotive p x n ps ty rest
> = RBind p
> (B Pi (bindIndices ty $
> bindTarget x n ps ty $
> RStar)) rest
> bindMethods rec tyname p ps [] [] rest = rest
> bindMethods rec tyname p ps ((n,ty):cs) (mn:mns) rest
> = RBind mn (B Pi (methtype ty)) (bindMethods rec tyname p ps cs mns rest)
> where methtype (RBind a (B Pi argtype) sc)
> | isrec argtype tyname && rec
> = (RBind a (B Pi argtype) (mkrec a argtype sc))
> | otherwise = (RBind a (B Pi argtype) (methtype sc))
> methtype (RFileLoc _ _ t) = methtype t
> methtype sc = mkapp (Var p) $ (getindices sc)++
> [mkapp (Var n) (map Var ((map fst ps)++(getargnames ty)))]
> mkrec a argtype sc = (RBind (ih a) (B Pi (rectype a argtype p))
> (methtype sc))
> getindices x = drop (length ps) (getappargs x)
> ih (UN a) = UN (a++"_IH")
> rectype a aty p = mkapp (Var p) ((drop (length ps) (getappargs aty)++[Var a]))
> applyMethod p x ty = mkapp (Var p) ((map Var (getargnames ty)) ++ [Var x])
> isrec t tyname = (Var tyname) == getappfun t
> placeholder = Var (UN "Waitforit")
Jump to Line
Something went wrong with that request. Please try again.