linearization for HOAS expressions

This commit is contained in:
krangelov
2021-12-09 08:45:53 +01:00
parent d1b1cd6e8c
commit 0069946f42
10 changed files with 80 additions and 32 deletions

View File

@@ -81,9 +81,10 @@ data Value s
| VPattType (Value s)
| VAlts (Value s) [(Value s, Value s)]
| VStrs [Value s]
-- This last constructor is only generated internally
-- These last constructors are only generated internally
-- in the PMCFG generator.
| VSymCat Int LIndex [(LIndex, Thunk s)]
| VSymVar Int Int
showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")"
@@ -226,6 +227,7 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,pv) ->
Just tnk -> return (i,tnk)
Nothing -> evalError ("Variable" <+> pp pv <+> "is not in scope")
return (VSymCat d r rs)
eval env (TSymVar d r) [] = do return (VSymVar d r)
eval env t vs = evalError ("Cannot reduce term" <+> pp t)
apply (VMeta m env vs0) vs = return (VMeta m env (vs0++vs))

View File

@@ -96,8 +96,10 @@ type2metaTerm :: SourceGrammar -> Int -> Map.Map MetaId Type -> LIndex -> [(LInd
type2metaTerm gr d ms r rs (Sort s) | s == cStr =
(ms,r+1,TSymCat d r rs)
type2metaTerm gr d ms r rs (RecType lbls) =
let ((ms',r'),ass) = mapAccumL (\(ms,r) (lbl,ty) -> let (ms',r',t) = type2metaTerm gr d ms r rs ty
in ((ms',r'),(lbl,(Just ty,t))))
let ((ms',r'),ass) = mapAccumL (\(ms,r) (lbl,ty) -> case lbl of
LVar j -> ((ms,r),(lbl,(Just ty,TSymVar d j)))
lbl -> let (ms',r',t) = type2metaTerm gr d ms r rs ty
in ((ms',r'),(lbl,(Just ty,t))))
(ms,r) lbls
in (ms',r',R ass)
type2metaTerm gr d ms r rs (Table p q) =
@@ -158,6 +160,7 @@ str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs
(r, rs,_) <- force tnk >>= param2int
(r',rs' ) <- compute r' tnks
return (r*cnt'+r',combine cnt' rs rs')
str2lin (VSymVar d r) = return [SymVar d r]
str2lin (VC vs) = fmap concat (mapM str2lin vs)
str2lin (VAlts def alts) = do def <- str2lin def
alts <- forM alts $ \(v,VStrs vs) -> do

View File

@@ -392,6 +392,7 @@ data Term =
| Alts Term [(Term, Term)] -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
| Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@
| TSymCat Int LIndex [(LIndex,Ident)]
| TSymVar Int Int
deriving (Show, Eq, Ord)
-- | Patterns

View File

@@ -249,6 +249,7 @@ ppTerm q d (ImplArg e) = braces (ppTerm q 0 e)
ppTerm q d (ELincat cat t) = prec d 4 ("lincat" <+> cat <+> ppTerm q 5 t)
ppTerm q d (ELin cat t) = prec d 4 ("lin" <+> cat <+> ppTerm q 5 t)
ppTerm q d (TSymCat i r rs) = pp '<' <> pp i <> pp ',' <> ppLinFun pp r rs <> pp '>'
ppTerm q d (TSymVar i r) = pp '<' <> pp i <> pp ',' <> pp '$' <> pp r <> pp '>'
ppEquation q (ps,e) = hcat (map (ppPatt q 2) ps) <+> "->" <+> ppTerm q 0 e