From 0069946f4222134aeabf8f9db2b6e3c1eef965d5 Mon Sep 17 00:00:00 2001 From: krangelov Date: Thu, 9 Dec 2021 08:45:53 +0100 Subject: [PATCH] linearization for HOAS expressions --- src/compiler/GF/Compile/Compute/Concrete.hs | 4 +- src/compiler/GF/Compile/GeneratePMCFG.hs | 7 ++- src/compiler/GF/Grammar/Grammar.hs | 1 + src/compiler/GF/Grammar/Printer.hs | 1 + src/runtime/c/pgf/linearizer.cxx | 52 ++++++++++++++++----- src/runtime/c/pgf/linearizer.h | 11 ++++- src/runtime/c/pgf/pgf.cxx | 15 +++--- src/runtime/c/pgf/pgf.h | 9 ++-- src/runtime/haskell/PGF2.hsc | 6 +-- src/runtime/haskell/PGF2/FFI.hsc | 6 +-- 10 files changed, 80 insertions(+), 32 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 4dce08580..1fb1e0f5e 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -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)) diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs index 467e191f7..d0a54e947 100644 --- a/src/compiler/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/GF/Compile/GeneratePMCFG.hs @@ -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 diff --git a/src/compiler/GF/Grammar/Grammar.hs b/src/compiler/GF/Grammar/Grammar.hs index 57a513178..cdbdfea8a 100644 --- a/src/compiler/GF/Grammar/Grammar.hs +++ b/src/compiler/GF/Grammar/Grammar.hs @@ -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 diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs index 0d90968b1..0ee9037db 100644 --- a/src/compiler/GF/Grammar/Printer.hs +++ b/src/compiler/GF/Grammar/Printer.hs @@ -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 diff --git a/src/runtime/c/pgf/linearizer.cxx b/src/runtime/c/pgf/linearizer.cxx index 0efa4dc03..0e68cad08 100644 --- a/src/runtime/c/pgf/linearizer.cxx +++ b/src/runtime/c/pgf/linearizer.cxx @@ -14,6 +14,9 @@ PgfLinearizer::TreeNode::TreeNode(PgfLinearizer *linearizer) this->var_count = 0; this->var_values= NULL; + this->n_hoas_vars = 0; + this->hoas_vars = NULL; + linearizer->root= this; } @@ -32,6 +35,23 @@ void PgfLinearizer::TreeNode::linearize_arg(PgfLinearizationOutputIface *out, Pg arg->linearize(out, linearizer, lindex); } +void PgfLinearizer::TreeNode::linearize_var(PgfLinearizationOutputIface *out, PgfLinearizer *linearizer, size_t d, size_t r) +{ + TreeNode *arg = args; + while (d > 0) { + arg = arg->next_arg; + if (arg == 0) + break; + d--; + } + if (arg == 0) + throw pgf_error("Missing argument"); + if (r >= arg->n_hoas_vars) + throw pgf_error("Missing lambda variable"); + linearizer->printer.efun(arg->hoas_vars[r]); + out->symbol_token(linearizer->printer.get_text()); +} + void PgfLinearizer::TreeNode::linearize_syms(PgfLinearizationOutputIface *out, PgfLinearizer *linearizer, ref> syms) { for (size_t i = 0; i < syms->len; i++) { @@ -50,6 +70,7 @@ void PgfLinearizer::TreeNode::linearize_syms(PgfLinearizationOutputIface *out, P } case PgfSymbolVar::tag: { auto sym_var = ref::untagged(sym); + linearize_var(out, linearizer, sym_var->d, sym_var->r); break; } case PgfSymbolKS::tag: { @@ -448,7 +469,9 @@ ref PgfLinearizer::TreeLitNode::get_lincat(PgfLinearizer *linear return lincat; } -PgfLinearizer::PgfLinearizer(ref concr, PgfMarshaller *m) { +PgfLinearizer::PgfLinearizer(PgfPrintContext *ctxt, ref concr, PgfMarshaller *m) + : printer(ctxt,0,m) +{ this->concr = concr; this->m = m; this->root = NULL; @@ -460,7 +483,6 @@ PgfLinearizer::PgfLinearizer(ref concr, PgfMarshaller *m) { this->wild->size = 1; this->wild->text[0] = '_'; this->wild->text[1] = 0; - }; PgfLinearizer::~PgfLinearizer() @@ -565,7 +587,19 @@ void PgfLinearizer::BracketStack::flush(PgfLinearizationOutputIface *out) PgfExpr PgfLinearizer::eabs(PgfBindType btype, PgfText *name, PgfExpr body) { - return 0; + printer.push_variable(name); + + TreeNode *node = (TreeNode *) m->match_expr(this, body); + + PgfText** hoas_vars = (PgfText**) malloc((node->n_hoas_vars+1)*sizeof(PgfText*)); + hoas_vars[0] = textdup(name); + memcpy(hoas_vars+1, node->hoas_vars, node->n_hoas_vars*sizeof(PgfText*)); + free(node->hoas_vars); + node->n_hoas_vars++; + node->hoas_vars = hoas_vars; + + printer.pop_variable(); + return (PgfExpr) node; } PgfExpr PgfLinearizer::eapp(PgfExpr fun, PgfExpr arg) @@ -586,11 +620,7 @@ PgfExpr PgfLinearizer::elit(PgfLiteral lit) PgfExpr PgfLinearizer::emeta(PgfMetaId meta) { - PgfPrinter printer(NULL,0,NULL); - if (meta == 0) - printer.puts("?"); - else - printer.nprintf(32,"?%d",meta); + printer.emeta(meta); return (PgfExpr) new TreeLindefNode(this, printer.get_text()); } @@ -600,7 +630,6 @@ PgfExpr PgfLinearizer::efun(PgfText *name) if (lin != 0) return (PgfExpr) new TreeLinNode(this, lin); else { - PgfPrinter printer(NULL,0,NULL); printer.puts("["); printer.efun(name); printer.puts("]"); @@ -610,7 +639,8 @@ PgfExpr PgfLinearizer::efun(PgfText *name) PgfExpr PgfLinearizer::evar(int index) { - return 0; + printer.evar(index); + return (PgfExpr) new TreeLindefNode(this, printer.get_text()); } PgfExpr PgfLinearizer::etyped(PgfExpr expr, PgfType ty) @@ -630,7 +660,6 @@ PgfLiteral PgfLinearizer::lint(size_t size, uintmax_t *v) strcpy(cat->text, "Int"); ref lincat = namespace_lookup(concr->lincats, cat); - PgfPrinter printer(NULL,0,NULL); printer.lint(size,v); return (PgfExpr) new TreeLitNode(this, lincat, printer.get_text()); @@ -643,7 +672,6 @@ PgfLiteral PgfLinearizer::lflt(double v) strcpy(cat->text, "Float"); ref lincat = namespace_lookup(concr->lincats, cat); - PgfPrinter printer(NULL,0,NULL); printer.lflt(v); return (PgfExpr) new TreeLitNode(this, lincat, printer.get_text()); diff --git a/src/runtime/c/pgf/linearizer.h b/src/runtime/c/pgf/linearizer.h index 7df80cac8..eef86f5b0 100644 --- a/src/runtime/c/pgf/linearizer.h +++ b/src/runtime/c/pgf/linearizer.h @@ -20,6 +20,9 @@ public: }; class PGF_INTERNAL_DECL PgfLinearizer : public PgfUnmarshaller { + // List of free variables in order reverse to the order of binding + PgfPrinter printer; + ref concr; PgfMarshaller *m; @@ -34,15 +37,19 @@ class PGF_INTERNAL_DECL PgfLinearizer : public PgfUnmarshaller { size_t var_count; size_t *var_values; + size_t n_hoas_vars; + PgfText **hoas_vars; + TreeNode(PgfLinearizer *linearizer); virtual bool resolve(PgfLinearizer *linearizer) { return true; }; virtual void check_category(PgfLinearizer *linearizer, PgfText *cat)=0; virtual void linearize_arg(PgfLinearizationOutputIface *out, PgfLinearizer *linearizer, size_t d, PgfLParam *r); + virtual void linearize_var(PgfLinearizationOutputIface *out, PgfLinearizer *linearizer, size_t d, size_t r); virtual void linearize_syms(PgfLinearizationOutputIface *out, PgfLinearizer *linearizer, ref> syms); virtual void linearize(PgfLinearizationOutputIface *out, PgfLinearizer *linearizer, size_t lindex)=0; size_t eval_param(PgfLParam *param); virtual ref get_lincat(PgfLinearizer *linearizer)=0; - virtual ~TreeNode() { free(var_values); }; + virtual ~TreeNode() { free(var_values); free(hoas_vars); }; }; struct TreeLinNode : public TreeNode { @@ -125,7 +132,7 @@ class PGF_INTERNAL_DECL PgfLinearizer : public PgfUnmarshaller { PgfText *wild; public: - PgfLinearizer(ref concr, PgfMarshaller *m); + PgfLinearizer(PgfPrintContext *ctxt, ref concr, PgfMarshaller *m); bool resolve(); void reverse_and_label(); diff --git a/src/runtime/c/pgf/pgf.cxx b/src/runtime/c/pgf/pgf.cxx index a5c4ebb17..b976ef492 100644 --- a/src/runtime/c/pgf/pgf.cxx +++ b/src/runtime/c/pgf/pgf.cxx @@ -1994,7 +1994,8 @@ int pgf_has_linearization(PgfDB *db, PgfConcrRevision revision, PGF_API PgfText *pgf_linearize(PgfDB *db, PgfConcrRevision revision, - PgfExpr expr, PgfMarshaller *m, + PgfExpr expr, PgfPrintContext *ctxt, + PgfMarshaller *m, PgfExn* err) { PGF_API_BEGIN { @@ -2002,7 +2003,7 @@ PgfText *pgf_linearize(PgfDB *db, PgfConcrRevision revision, ref concr = PgfDB::revision2concr(revision); PgfLinearizationOutput out; - PgfLinearizer linearizer(concr, m); + PgfLinearizer linearizer(ctxt, concr, m); m->match_expr(&linearizer, expr); linearizer.reverse_and_label(); if (linearizer.resolve()) { @@ -2016,7 +2017,8 @@ PgfText *pgf_linearize(PgfDB *db, PgfConcrRevision revision, PGF_API_DECL void pgf_bracketed_linearize(PgfDB *db, PgfConcrRevision revision, - PgfExpr expr, PgfMarshaller *m, + PgfExpr expr, PgfPrintContext *ctxt, + PgfMarshaller *m, PgfLinearizationOutputIface *out, PgfExn* err) { @@ -2024,7 +2026,7 @@ void pgf_bracketed_linearize(PgfDB *db, PgfConcrRevision revision, DB_scope scope(db, READER_SCOPE); ref concr = PgfDB::revision2concr(revision); - PgfLinearizer linearizer(concr, m); + PgfLinearizer linearizer(ctxt, concr, m); m->match_expr(&linearizer, expr); linearizer.reverse_and_label(); if (linearizer.resolve()) { @@ -2230,7 +2232,8 @@ pgf_graphviz_abstract_tree(PgfDB *db, PgfRevision revision, PGF_API PgfText * pgf_graphviz_parse_tree(PgfDB *db, PgfConcrRevision revision, - PgfExpr expr, PgfMarshaller *m, + PgfExpr expr, PgfPrintContext *ctxt, + PgfMarshaller *m, PgfGraphvizOptions* opts, PgfExn *err) { @@ -2240,7 +2243,7 @@ pgf_graphviz_parse_tree(PgfDB *db, PgfConcrRevision revision, ref concr = PgfDB::revision2concr(revision); PgfLinearizationGraphvizOutput out; - PgfLinearizer linearizer(concr, m); + PgfLinearizer linearizer(ctxt, concr, m); m->match_expr(&linearizer, expr); linearizer.reverse_and_label(); if (linearizer.resolve()) { diff --git a/src/runtime/c/pgf/pgf.h b/src/runtime/c/pgf/pgf.h index fa3cfb6b5..f949abb3d 100644 --- a/src/runtime/c/pgf/pgf.h +++ b/src/runtime/c/pgf/pgf.h @@ -634,12 +634,14 @@ struct PgfLinearizationOutputIface PGF_API_DECL PgfText *pgf_linearize(PgfDB *db, PgfConcrRevision revision, - PgfExpr expr, PgfMarshaller *m, + PgfExpr expr, PgfPrintContext *ctxt, + PgfMarshaller *m, PgfExn* err); PGF_API_DECL void pgf_bracketed_linearize(PgfDB *db, PgfConcrRevision revision, - PgfExpr expr, PgfMarshaller *m, + PgfExpr expr, PgfPrintContext *ctxt, + PgfMarshaller *m, PgfLinearizationOutputIface *out, PgfExn* err); @@ -700,7 +702,8 @@ typedef struct { PGF_API PgfText * pgf_graphviz_parse_tree(PgfDB *db, PgfConcrRevision revision, - PgfExpr expr, PgfMarshaller *m, + PgfExpr expr, PgfPrintContext *ctxt, + PgfMarshaller *m, PgfGraphvizOptions* opts, PgfExn *err); diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc index fa28034e5..24c187dd4 100644 --- a/src/runtime/haskell/PGF2.hsc +++ b/src/runtime/haskell/PGF2.hsc @@ -615,7 +615,7 @@ linearize c e = withForeignPtr (c_revision c) $ \c_revision -> bracket (newStablePtr e) freeStablePtr $ \c_e -> withForeignPtr marshaller $ \m -> - bracket (withPgfExn "linearize" (pgf_linearize (c_db c) c_revision c_e m)) free $ \c_text -> + bracket (withPgfExn "linearize" (pgf_linearize (c_db c) c_revision c_e nullPtr m)) free $ \c_text -> if c_text == nullPtr then return "" else peekText c_text @@ -694,7 +694,7 @@ bracketedLinearize c e = unsafePerformIO $ do (#poke PgfLinearizationOutputIfaceVtbl, symbol_ne) vtbl c_symbol_ne (#poke PgfLinearizationOutputIfaceVtbl, symbol_meta) vtbl c_symbol_meta (#poke PgfLinearizationOutputIface, vtbl) c_out vtbl - withPgfExn "bracketedLinearize" (pgf_bracketed_linearize (c_db c) c_revision c_e m c_out)) + withPgfExn "bracketedLinearize" (pgf_bracketed_linearize (c_db c) c_revision c_e nullPtr m c_out)) (ne,_,bs) <- readIORef ref (if ne then return [] @@ -922,7 +922,7 @@ graphvizParseTree c opts e = bracket (newStablePtr e) freeStablePtr $ \c_e -> withForeignPtr marshaller $ \m -> withGraphvizOptions opts $ \c_opts -> - bracket (withPgfExn "graphvizParseTree" (pgf_graphviz_parse_tree (c_db c) c_revision c_e m c_opts)) free $ \c_text -> + bracket (withPgfExn "graphvizParseTree" (pgf_graphviz_parse_tree (c_db c) c_revision c_e nullPtr m c_opts)) free $ \c_text -> peekText c_text graphvizWordAlignment :: [Concr] -> GraphvizOptions -> Expr -> String diff --git a/src/runtime/haskell/PGF2/FFI.hsc b/src/runtime/haskell/PGF2/FFI.hsc index 8017616ac..79a30ca49 100644 --- a/src/runtime/haskell/PGF2/FFI.hsc +++ b/src/runtime/haskell/PGF2/FFI.hsc @@ -207,9 +207,9 @@ foreign import ccall pgf_drop_lin :: Ptr PgfDB -> Ptr Concr -> Ptr PgfText -> Pt foreign import ccall pgf_has_linearization :: Ptr PgfDB -> Ptr Concr -> Ptr PgfText -> Ptr PgfExn -> IO CInt -foreign import ccall pgf_linearize :: Ptr PgfDB -> Ptr Concr -> StablePtr Expr -> Ptr PgfMarshaller -> Ptr PgfExn -> IO (Ptr PgfText) +foreign import ccall pgf_linearize :: Ptr PgfDB -> Ptr Concr -> StablePtr Expr -> Ptr PgfPrintContext -> Ptr PgfMarshaller -> Ptr PgfExn -> IO (Ptr PgfText) -foreign import ccall pgf_bracketed_linearize :: Ptr PgfDB -> Ptr Concr -> StablePtr Expr -> Ptr PgfMarshaller -> Ptr PgfLinearizationOutputIface -> Ptr PgfExn -> IO () +foreign import ccall pgf_bracketed_linearize :: Ptr PgfDB -> Ptr Concr -> StablePtr Expr -> Ptr PgfPrintContext -> Ptr PgfMarshaller -> Ptr PgfLinearizationOutputIface -> Ptr PgfExn -> IO () foreign import ccall "wrapper" wrapSymbol0 :: Wrapper (Ptr PgfLinearizationOutputIface -> IO ()) @@ -237,7 +237,7 @@ foreign import ccall pgf_set_concrete_flag :: Ptr PgfDB -> Ptr Concr -> Ptr PgfT foreign import ccall pgf_graphviz_abstract_tree :: Ptr PgfDB -> Ptr PGF -> StablePtr Expr -> Ptr PgfMarshaller -> Ptr PgfGraphvizOptions -> Ptr PgfExn -> IO (Ptr PgfText) -foreign import ccall pgf_graphviz_parse_tree :: Ptr PgfDB -> Ptr Concr -> StablePtr Expr -> Ptr PgfMarshaller -> Ptr PgfGraphvizOptions -> Ptr PgfExn -> IO (Ptr PgfText) +foreign import ccall pgf_graphviz_parse_tree :: Ptr PgfDB -> Ptr Concr -> StablePtr Expr -> Ptr PgfPrintContext -> Ptr PgfMarshaller -> Ptr PgfGraphvizOptions -> Ptr PgfExn -> IO (Ptr PgfText) -----------------------------------------------------------------------