[Git][monnier/typer][master] 2 commits: Apply the instantiated metavariable substs when displaying lexps
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... -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2e00884b0d84ec33ca9cacc643ca9ecdd... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Jean-Alexandre Barszcz