Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer

Commits: ac4cc3a5 by Jean-Alexandre Barszcz at 2020-08-20T15:01:14-04:00 Apply the instantiated metavariable substs when displaying lexps

- - - - - f0b33b28 by Jean-Alexandre Barszcz at 2020-08-20T15:01:36-04:00 Replace instantiated metavars when checking syntactic equality

- - - - -

1 changed file:

- src/lexp.ml

Changes:

===================================== src/lexp.ml ===================================== @@ -805,7 +805,7 @@ and lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx e + | MVal e -> lexp_str ctx (push_susp e subst) | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> @@ -993,7 +993,19 @@ let rec eq e1 e2 = | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) - -> i1 = i2 && subst_eq s1 s2 + -> if i1 == i2 then subst_eq s1 s2 else + (match (metavar_lookup i1, metavar_lookup i2) with + | (MVal l, _) -> eq (push_susp l s1) e2 + | (_, MVal l) -> eq e1 (push_susp l s2) + | _ -> false) + | (Metavar (i1, s1, _), _) + -> (match metavar_lookup i1 with + | MVal l -> eq (push_susp l s1) e2 + | _ -> false) + | (_, Metavar (i2, s2, _)) + -> (match metavar_lookup i2 with + | MVal l -> eq e1 (push_susp l s2) + | _ -> false) | _ -> false

and subst_eq s1 s2 =

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2e00884b0d84ec33ca9cacc643ca9ecdd...