From 8d40541003736d5319ec981278338e8c8c66daf6 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 23 Jun 2024 01:36:48 +0200 Subject: keep track of bound names everywhere to be able to output names instead of de bruijn indices --- lib/Conversion.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'lib/Conversion.ml') diff --git a/lib/Conversion.ml b/lib/Conversion.ml index b70a070..00bc942 100644 --- a/lib/Conversion.ml +++ b/lib/Conversion.ml @@ -18,11 +18,11 @@ struct let rec equate v1 v2 = match v1, v2 with | D.Neutral ne, v | v, D.Neutral ne -> equate_ne ne v - | D.Pi (base1, fam1), D.Pi (base2, fam2) -> + | D.Pi (_, base1, fam1), D.Pi (_, base2, fam2) -> equate base1 base2; equate_clo fam1 fam2 - | D.Lam clo1, D.Lam clo2 -> equate_clo clo1 clo2 - | D.Sg (base1, fam1), D.Sg (base2, fam2) -> + | D.Lam (_, clo1), D.Lam (_, clo2) -> equate_clo clo1 clo2 + | D.Sg (_, base1, fam1), D.Sg (_, base2, fam2) -> equate base1 base2; equate_clo fam1 fam2 | D.Pair (fst1, snd1), D.Pair (fst2, snd2) -> @@ -44,8 +44,8 @@ struct | D.App arg1, D.App arg2 -> equate arg1 arg2 | D.Fst, D.Fst -> () | D.Snd, D.Snd -> () - | D.BoolElim { cmot = mot1; vtrue = t1; vfalse = f1 }, - D.BoolElim { cmot = mot2; vtrue = t2; vfalse = f2 } -> + | D.BoolElim { motive = mot1; true_case = t1; false_case = f1; _ }, + D.BoolElim { motive = mot2; true_case = t2; false_case = f2; _ } -> equate_clo mot1 mot2; equate t1 t2; equate f1 f2; @@ -63,7 +63,7 @@ struct equate_ne_head hd hd2; equate_spine sp sp2 (* eta expansion *) - | D.Lam clo -> bind @@ fun arg -> + | D.Lam (_, clo) -> bind @@ fun arg -> equate_ne (hd, sp <: D.App arg) (Eval.inst_clo clo arg) | D.Pair (fst, snd) -> equate_ne (hd, sp <: D.Fst) fst; -- cgit 1.4.1