bugfixes for showContext & showType

This commit is contained in:
krangelov
2021-09-14 19:54:38 +02:00
parent a7bf47cb87
commit 9fe6ee3cce
4 changed files with 12 additions and 8 deletions

View File

@@ -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();
}

View File

@@ -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(" -> ");
}

View File

@@ -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);

View File

@@ -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))))))