diff options
| author | Malte Voos <git@mal.tc> | 2024-06-23 01:36:48 +0200 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-06-23 01:36:48 +0200 |
| commit | 8d40541003736d5319ec981278338e8c8c66daf6 (patch) | |
| tree | e595d0055af42b6a9d84e504befbe114a8cef5e2 /lib/Quote.ml | |
| parent | 36762e83887b6f917df46c5e40a11d53b697209d (diff) | |
| download | toytt-8d40541003736d5319ec981278338e8c8c66daf6.tar.gz toytt-8d40541003736d5319ec981278338e8c8c66daf6.zip | |
keep track of bound names everywhere to be able to output names instead of de bruijn indices
Diffstat (limited to 'lib/Quote.ml')
| -rw-r--r-- | lib/Quote.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/lib/Quote.ml b/lib/Quote.ml index 611843a..4b88e91 100644 --- a/lib/Quote.ml +++ b/lib/Quote.ml @@ -15,9 +15,9 @@ struct let rec quote = function | D.Neutral ne -> quote_ne ne - | D.Pi (base, fam) -> S.Pi (quote base, quote_clo fam) - | D.Lam clo -> S.Lam (quote_clo clo) - | D.Sg (base, fam) -> S.Sg (quote base, quote_clo fam) + | D.Pi (name, base, fam) -> S.Pi (name, quote base, quote_clo fam) + | D.Lam (name, clo) -> S.Lam (name, quote_clo clo) + | D.Sg (name, base, fam) -> S.Sg (name, quote base, quote_clo fam) | D.Pair (v, w) -> S.Pair (quote v, quote w) | D.Type -> S.Type | D.Bool -> S.Bool @@ -34,11 +34,12 @@ struct | D.App v -> S.App (hd, quote v) | D.Fst -> S.Fst hd | D.Snd -> S.Snd hd - | D.BoolElim { cmot; vtrue; vfalse } -> + | D.BoolElim { motive_var; motive; true_case; false_case } -> S.BoolElim { - motive = quote_clo cmot; - true_case = quote vtrue; - false_case = quote vfalse; + motive_var; + motive = quote_clo motive; + true_case = quote true_case; + false_case = quote false_case; scrut = hd; } end |