From 9fe6ee3cce9831f72a40f81666cec09d215cca9a Mon Sep 17 00:00:00 2001 From: krangelov Date: Tue, 14 Sep 2021 19:54:38 +0200 Subject: [PATCH] bugfixes for showContext & showType --- src/runtime/c/pgf/pgf.cxx | 2 +- src/runtime/c/pgf/printer.cxx | 13 +++++++------ src/runtime/c/pgf/printer.h | 2 +- src/runtime/haskell/tests/basic.hs | 3 +++ 4 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/runtime/c/pgf/pgf.cxx b/src/runtime/c/pgf/pgf.cxx index 4b56a6547..50cabdc23 100644 --- a/src/runtime/c/pgf/pgf.cxx +++ b/src/runtime/c/pgf/pgf.cxx @@ -476,7 +476,7 @@ PgfText *pgf_print_context(size_t n_hypos, PgfTypeHypo *hypos, for (size_t i = 0; i < n_hypos; i++) { if (i > 0) printer.puts(" "); - printer.hypo(&hypos[i]); + printer.hypo(&hypos[i],4); } return printer.get_text(); } diff --git a/src/runtime/c/pgf/printer.cxx b/src/runtime/c/pgf/printer.cxx index 7c68abcd4..fefee4717 100644 --- a/src/runtime/c/pgf/printer.cxx +++ b/src/runtime/c/pgf/printer.cxx @@ -380,23 +380,24 @@ PgfLiteral PgfPrinter::lstr(PgfText *v) return 0; } -void PgfPrinter::hypo(PgfTypeHypo *hypo) +void PgfPrinter::hypo(PgfTypeHypo *hypo, int prio) { if (textcmp(hypo->cid, &wildcard) == 0) { - prio = 1; + this->prio = prio; m->match_type(this, hypo->type); } else { - push_variable(hypo->cid); - puts("("); if (hypo->bind_type == PGF_BIND_TYPE_IMPLICIT) puts("{"); - puts(&ctxt->name); + puts(hypo->cid); if (hypo->bind_type == PGF_BIND_TYPE_IMPLICIT) puts("}"); puts(" : "); + this->prio = 0; m->match_type(this, hypo->type); puts(")"); + + push_variable(hypo->cid); } } @@ -411,7 +412,7 @@ PgfType PgfPrinter::dtyp(size_t n_hypos, PgfTypeHypo *hypos, PgfPrintContext *save_ctxt = ctxt; for (int i = 0; i < n_hypos; i++) { - hypo(&hypos[i]); + hypo(&hypos[i],1); puts(" -> "); } diff --git a/src/runtime/c/pgf/printer.h b/src/runtime/c/pgf/printer.h index 12b26f0da..a640eb9d9 100644 --- a/src/runtime/c/pgf/printer.h +++ b/src/runtime/c/pgf/printer.h @@ -50,7 +50,7 @@ public: PgfText *get_text(); - void hypo(PgfTypeHypo *hypo); + void hypo(PgfTypeHypo *hypo, int prio); virtual PgfExpr eabs(PgfBindType btype, PgfText *name, PgfExpr body); virtual PgfExpr eapp(PgfExpr fun, PgfExpr arg); diff --git a/src/runtime/haskell/tests/basic.hs b/src/runtime/haskell/tests/basic.hs index e7e977520..b6eca2d5a 100644 --- a/src/runtime/haskell/tests/basic.hs +++ b/src/runtime/haskell/tests/basic.hs @@ -59,6 +59,9 @@ main = do ,TestCase (assertEqual "show type 5" "(f : N -> N) -> P (f z)" (showType [] (DTyp [(Explicit,"f",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "P" [EApp (EVar 0) (EFun "z")]))) ,TestCase (assertEqual "show type 6" "(f : N -> N) -> P (f n)" (showType ["n"] (DTyp [(Explicit,"f",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "P" [EApp (EVar 0) (EVar 1)]))) ,TestCase (assertEqual "show type 7" "({f} : N -> N) -> P (f n)" (showType ["n"] (DTyp [(Implicit,"f",DTyp [(Explicit,"_",DTyp [] "N" [])] "N" [])] "P" [EApp (EVar 0) (EVar 1)]))) + ,TestCase (assertEqual "show type 8" "(x : N) -> P x -> S" (showType [] (DTyp [(Explicit,"x",DTyp [] "N" []),(Explicit,"_",DTyp [] "P" [EVar 0])] "S" []))) + ,TestCase (assertEqual "show type 9" "(x : N) -> (y : P x) -> S" (showType [] (DTyp [(Explicit,"x",DTyp [] "N" []),(Explicit,"y",DTyp [] "P" [EVar 0])] "S" []))) + ,TestCase (assertEqual "show context" "(x : N) (P x)" (showContext [] [(Explicit,"x",DTyp [] "N" []),(Explicit,"_",DTyp [] "P" [EVar 0])])) ,TestCase (assertEqual "fresh variables 1" "\\v,v1->v1" (showExpr [] (EAbs Explicit "v" (EAbs Explicit "v" (EVar 0))))) ,TestCase (assertEqual "fresh variables 2" "\\v,v1->v" (showExpr [] (EAbs Explicit "v" (EAbs Explicit "v" (EVar 1))))) ,TestCase (assertEqual "fresh variables 3" "\\v,v1,v2->v1" (showExpr [] (EAbs Explicit "v" (EAbs Explicit "v" (EAbs Explicit "v" (EVar 1))))))