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/Syntax.ml | 82 ++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 44 insertions(+), 38 deletions(-) (limited to 'lib/Syntax.ml') diff --git a/lib/Syntax.ml b/lib/Syntax.ml index c4cf80d..fc58353 100644 --- a/lib/Syntax.ml +++ b/lib/Syntax.ml @@ -1,11 +1,12 @@ open Bwd +open Bwd.Infix type t = Data.syn = | Var of int - | Pi of t * (* BINDS *) t - | Lam of (* BINDS *) t + | Pi of Ident.local * t * (* BINDS *) t + | Lam of Ident.local * (* BINDS *) t | App of t * t - | Sg of t * (* BINDS *) t + | Sg of Ident.local * t * (* BINDS *) t | Pair of t * t | Fst of t | Snd of t @@ -14,6 +15,7 @@ type t = Data.syn = | True | False | BoolElim of { + motive_var : Ident.local; motive : (* BINDS *) t; true_case : t; false_case : t; @@ -22,23 +24,21 @@ type t = Data.syn = module Pretty = struct - type local_names = Yuujinchou.Trie.path option bwd - type tm_with_names = t * local_names - - let pp_name fmt (id : Yuujinchou.Trie.path) = Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.') - Format.pp_print_string fmt id - module Internal = struct type env = { + names : Ident.local bwd; prec : int; } module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) + let bind (name : Ident.local) f fmt x = + let update env = { env with names = env.names <: name } in + Eff.scope update (fun () -> f fmt x) + let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) = - Eff.scope (fun _ -> { prec; }) (fun () -> inner fmt v) + Eff.scope (fun env -> { env with prec; }) (fun () -> inner fmt v) let delimited inner = with_prec 0 inner @@ -49,49 +49,54 @@ struct Fun.id let lassoc (prec : int) - ?(pre = "") (pp_left : 'l Fmt.t) - ?(middle = " ") - (pp_right : 'r Fmt.t) - ?(post = "") : ('l * 'r) Fmt.t = + ?(sep = " ") + (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = parenthesize prec @@ fun fmt v -> - Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" - pre + Fmt.pf fmt "@[%a@]%s@[%a@]" (with_prec prec pp_left) (fst v) - middle + sep (with_prec (prec + 1) pp_right) (snd v) - post let rassoc (prec : int) - ?(pre = "") (pp_left : 'l Fmt.t) - ?(middle = " ") - (pp_right : 'r Fmt.t) - ?(post = "") : ('l * 'r) Fmt.t = + ?(sep = " ") + (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = parenthesize prec @@ fun fmt v -> - Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" - pre + Fmt.pf fmt "@[%a@]%s@[%a@]" (with_prec (prec + 1) pp_left) (fst v) - middle + sep (with_prec prec pp_right) (snd v) - post - let pp_var ix fmt = Fmt.pf fmt "%@%d" ix + let pp_local_name fmt name = + Fmt.string fmt @@ Option.value ~default:"_" name + + let pp_var fmt ix = + let names = (Eff.read()).names in + match Bwd.nth_opt names ix with + (* the variable has a bound name which has not been shadowed *) + | Some ((Some name) as id) when Bwd.find_index ((=) id) names = Some ix -> Fmt.string fmt name + (* the variable does not have a bound name or its bound name has been shadowed *) + | Some _ -> Fmt.pf fmt "%@%d" ix + | None -> Reporter.bug "index out of range in pp_var" let rec pp_pair fmt = (delimited @@ fun fmt (a, b) -> Fmt.pf fmt "@[(@[%a@], @[%a@])@]" pp a pp b) fmt and pp_bool_elim fmt = - (delimited @@ fun fmt (motive, true_case, false_case, scrut) -> Fmt.pf fmt - "@[bool-elim @[%a@] at _ -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]" - pp scrut pp motive pp true_case pp false_case + (delimited @@ fun fmt (motive_var, motive, true_case, false_case, scrut) -> Fmt.pf fmt + "@[bool-elim @[%a@] at @[%a@] -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]" + pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case ) fmt + and pp_arg fmt (name, tp) = + Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp + (* TODO: improve indentation *) and pp fmt = function - | Var ix -> pp_var ix fmt - | Pi (base, fam) -> rassoc 1 ~pre:"(_ : " pp ~middle:") -> " pp fmt (base, fam) - | Lam body -> Fmt.pf fmt "@[\\_ -> @[%a@]@]" pp body - | Sg (base, fam) -> rassoc 2 ~pre:"(_ : " pp ~middle:") * " pp fmt (base, fam) + | Var ix -> pp_var fmt ix + | Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam) + | Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body + | Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam) | App (a, b) -> lassoc 3 pp pp fmt (a, b) | Pair (a, b) -> pp_pair fmt (a, b) | Fst a -> lassoc 3 Fmt.string pp fmt ("fst", a) @@ -100,10 +105,11 @@ struct | Bool -> Fmt.string fmt "bool" | True -> Fmt.string fmt "true" | False -> Fmt.string fmt "false" - | BoolElim { motive; true_case; false_case; scrut } -> pp_bool_elim fmt (motive, true_case, false_case, scrut) + | BoolElim { motive_var; motive; true_case; false_case; scrut } + -> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut) end - let pp fmt tm = - let env : Internal.env = { prec = 0; } in + let pp fmt (tm, names) = + let env : Internal.env = { names; prec = 0; } in Internal.Eff.run ~env (fun () -> Internal.pp fmt tm) end -- cgit 1.4.1