forked from GitHub/gf-core
gfcc generation with HOAS: var fields appended to records
This commit is contained in:
@@ -134,6 +134,7 @@ mkContext hyps = [C.Hyp (i2i x) (mkType ty) | (x,ty) <- hyps]
|
|||||||
mkTerm :: Term -> C.Term
|
mkTerm :: Term -> C.Term
|
||||||
mkTerm tr = case tr of
|
mkTerm tr = case tr of
|
||||||
Vr (IA (_,i)) -> C.V i
|
Vr (IA (_,i)) -> C.V i
|
||||||
|
Vr (IAV (_,_,i)) -> C.V i
|
||||||
Vr (IC s) | isDigit (last s) ->
|
Vr (IC s) | isDigit (last s) ->
|
||||||
C.V (read (reverse (takeWhile (/='_') (reverse s))))
|
C.V (read (reverse (takeWhile (/='_') (reverse s))))
|
||||||
---- from gf parser of gfc
|
---- from gf parser of gfc
|
||||||
@@ -362,10 +363,11 @@ paramValues cgr = (labels,untyps,typs) where
|
|||||||
[(cat,(unlockTyp ls)) | (_,(cat,CncCat (Yes (RecType ls)) _ _)) <- jments]
|
[(cat,(unlockTyp ls)) | (_,(cat,CncCat (Yes (RecType ls)) _ _)) <- jments]
|
||||||
labels = Map.fromList $ concat
|
labels = Map.fromList $ concat
|
||||||
[((cat,[lab]),(typ,i)):
|
[((cat,[lab]),(typ,i)):
|
||||||
|
[((cat,[LVar v]),(typ,toInteger (mx + v))) | v <- [0,1]] ++ ---- 1 or 2 vars
|
||||||
[((cat,[lab,lab2]),(ty,j)) |
|
[((cat,[lab,lab2]),(ty,j)) |
|
||||||
rs <- getRec typ, ((lab2, ty),j) <- zip rs [0..]]
|
rs <- getRec typ, ((lab2, ty),j) <- zip rs [0..]]
|
||||||
|
|
|
|
||||||
(cat,ls) <- lincats, ((lab, typ),i) <- zip ls [0..]]
|
(cat,ls) <- lincats, ((lab, typ),i) <- zip ls [0..], let mx = length ls]
|
||||||
-- go to tables recursively
|
-- go to tables recursively
|
||||||
---- TODO: even go to deeper records
|
---- TODO: even go to deeper records
|
||||||
where
|
where
|
||||||
@@ -447,13 +449,15 @@ term2term cgr env@(labels,untyps,typs) tr = case tr of
|
|||||||
r2r tr@(P (S (V ty ts) v) l) = t2t $ S (V ty [comp (P t l) | t <- ts]) v
|
r2r tr@(P (S (V ty ts) v) l) = t2t $ S (V ty [comp (P t l) | t <- ts]) v
|
||||||
|
|
||||||
r2r tr@(P p _) = case getLab tr of
|
r2r tr@(P p _) = case getLab tr of
|
||||||
Ok (cat,labs) -> P (t2t p) . mkLab $ maybe (prtTrace tr $ 66664) snd $
|
Ok (cat,labs) -> P (t2t p) . mkLab $
|
||||||
Map.lookup (cat,labs) labels
|
maybe (prtTrace tr $ 66664) snd $
|
||||||
|
Map.lookup (cat,labs) labels
|
||||||
_ -> K ((A.prt tr +++ prtTrace tr "66665"))
|
_ -> K ((A.prt tr +++ prtTrace tr "66665"))
|
||||||
|
|
||||||
-- this goes recursively into tables (ignored) and records (accumulated)
|
-- this goes recursively into tables (ignored) and records (accumulated)
|
||||||
getLab tr = case tr of
|
getLab tr = case tr of
|
||||||
Vr (IA (cat, _)) -> return (identC cat,[])
|
Vr (IA (cat, _)) -> return (identC cat,[])
|
||||||
|
Vr (IAV (cat,_,_)) -> return (identC cat,[])
|
||||||
Vr (IC s) -> return (identC cat,[]) where
|
Vr (IC s) -> return (identC cat,[]) where
|
||||||
cat = init (reverse (dropWhile (/='_') (reverse s))) ---- from gf parser
|
cat = init (reverse (dropWhile (/='_') (reverse s))) ---- from gf parser
|
||||||
---- Vr _ -> error $ "getLab " ++ show tr
|
---- Vr _ -> error $ "getLab " ++ show tr
|
||||||
|
|||||||
@@ -138,10 +138,13 @@ str :: CType
|
|||||||
str = S []
|
str = S []
|
||||||
|
|
||||||
lintype :: GFCC -> CId -> CId -> LinType
|
lintype :: GFCC -> CId -> CId -> LinType
|
||||||
lintype gfcc lang fun = case catSkeleton (lookType gfcc fun) of
|
lintype gfcc lang fun = case typeSkeleton (lookType gfcc fun) of
|
||||||
(cs,c) -> (map linc cs, linc c) ---- HOAS
|
(cs,c) -> (map vlinc cs, linc c) ---- HOAS
|
||||||
where
|
where
|
||||||
linc = lookLincat gfcc lang
|
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 -> CId -> Term -> Term
|
||||||
inline gfcc lang t = case t of
|
inline gfcc lang t = case t of
|
||||||
|
|||||||
@@ -27,19 +27,24 @@ realize trm = case trm of
|
|||||||
_ -> "ERROR " ++ show trm ---- debug
|
_ -> "ERROR " ++ show trm ---- debug
|
||||||
|
|
||||||
linExp :: GFCC -> CId -> Exp -> Term
|
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
|
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
|
AS s -> R [kks (show s)] -- quoted
|
||||||
AI i -> R [kks (show i)]
|
AI i -> R [kks (show i)]
|
||||||
--- [C lst, kks (show i), C size] where
|
--- [C lst, kks (show i), C size] where
|
||||||
--- lst = mod (fromInteger i) 10 ; size = if i < 10 then 0 else 1
|
--- lst = mod (fromInteger i) 10 ; size = if i < 10 then 0 else 1
|
||||||
AF d -> R [kks (show d)]
|
AF d -> R [kks (show d)]
|
||||||
|
AV x -> addB $ R [kks (prCId x)] ---- lindef of cat
|
||||||
AM _ -> TM
|
AM _ -> TM
|
||||||
where
|
where
|
||||||
lin = linExp mcfg lang
|
lin = linExp mcfg lang
|
||||||
comp = compute mcfg lang
|
comp = compute mcfg lang
|
||||||
look = lookLin 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 :: GFCC -> CId -> [Term] -> Term -> Term
|
||||||
compute mcfg lang args = comp where
|
compute mcfg lang args = comp where
|
||||||
|
|||||||
@@ -69,10 +69,18 @@ catSkeleton :: Type -> ([CId],CId)
|
|||||||
catSkeleton ty = case ty of
|
catSkeleton ty = case ty of
|
||||||
DTyp hyps val _ -> ([valCat ty | Hyp _ ty <- hyps],val)
|
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 :: Type -> CId
|
||||||
valCat ty = case ty of
|
valCat ty = case ty of
|
||||||
DTyp _ val _ -> val
|
DTyp _ val _ -> val
|
||||||
|
|
||||||
|
contextLength :: Type -> Int
|
||||||
|
contextLength ty = case ty of
|
||||||
|
DTyp hyps _ _ -> length hyps
|
||||||
|
|
||||||
cid :: String -> CId
|
cid :: String -> CId
|
||||||
cid = CId
|
cid = CId
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user