forked from GitHub/gf-core
gfcc generation with HOAS: var fields appended to records
This commit is contained in:
@@ -138,10 +138,13 @@ str :: CType
|
||||
str = S []
|
||||
|
||||
lintype :: GFCC -> CId -> CId -> LinType
|
||||
lintype gfcc lang fun = case catSkeleton (lookType gfcc fun) of
|
||||
(cs,c) -> (map linc cs, linc c) ---- HOAS
|
||||
lintype gfcc lang fun = case typeSkeleton (lookType gfcc fun) of
|
||||
(cs,c) -> (map vlinc cs, linc c) ---- HOAS
|
||||
where
|
||||
linc = lookLincat gfcc lang
|
||||
vlinc (0,c) = linc c
|
||||
vlinc (i,c) = case linc c of
|
||||
R ts -> R (ts ++ replicate i str)
|
||||
|
||||
inline :: GFCC -> CId -> Term -> Term
|
||||
inline gfcc lang t = case t of
|
||||
|
||||
@@ -27,19 +27,24 @@ realize trm = case trm of
|
||||
_ -> "ERROR " ++ show trm ---- debug
|
||||
|
||||
linExp :: GFCC -> CId -> Exp -> Term
|
||||
linExp mcfg lang tree@(DTr _ at trees) = ---- bindings TODO
|
||||
linExp mcfg lang tree@(DTr xs at trees) = ---- bindings TODO
|
||||
case at of
|
||||
AC fun -> comp (lmap lin trees) $ look fun
|
||||
AC fun -> addB $ comp (lmap lin trees) $ look fun
|
||||
AS s -> R [kks (show s)] -- quoted
|
||||
AI i -> R [kks (show i)]
|
||||
--- [C lst, kks (show i), C size] where
|
||||
--- lst = mod (fromInteger i) 10 ; size = if i < 10 then 0 else 1
|
||||
AF d -> R [kks (show d)]
|
||||
AV x -> addB $ R [kks (prCId x)] ---- lindef of cat
|
||||
AM _ -> TM
|
||||
where
|
||||
lin = linExp mcfg lang
|
||||
comp = compute mcfg lang
|
||||
look = lookLin mcfg lang
|
||||
addB t
|
||||
| Data.List.null xs = t
|
||||
| otherwise = case t of
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . prCId) xs)
|
||||
|
||||
compute :: GFCC -> CId -> [Term] -> Term -> Term
|
||||
compute mcfg lang args = comp where
|
||||
|
||||
@@ -69,10 +69,18 @@ catSkeleton :: Type -> ([CId],CId)
|
||||
catSkeleton ty = case ty of
|
||||
DTyp hyps val _ -> ([valCat ty | Hyp _ ty <- hyps],val)
|
||||
|
||||
typeSkeleton :: Type -> ([(Int,CId)],CId)
|
||||
typeSkeleton ty = case ty of
|
||||
DTyp hyps val _ -> ([(contextLength ty, valCat ty) | Hyp _ ty <- hyps],val)
|
||||
|
||||
valCat :: Type -> CId
|
||||
valCat ty = case ty of
|
||||
DTyp _ val _ -> val
|
||||
|
||||
contextLength :: Type -> Int
|
||||
contextLength ty = case ty of
|
||||
DTyp hyps _ _ -> length hyps
|
||||
|
||||
cid :: String -> CId
|
||||
cid = CId
|
||||
|
||||
|
||||
Reference in New Issue
Block a user