From 66cf5d3c5fff84a1cac333c1aa81a8e1f21ee6f4 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 8 Jul 2024 22:10:12 +0200 Subject: rename Ident -> Name --- src/ast/Ast.ml | 10 +++++----- src/ast/dune | 2 +- src/elaborator/Elaborator.ml | 16 ++++++++-------- src/elaborator/dune | 2 +- src/error/Error.ml | 4 ++-- src/error/dune | 2 +- src/ident/Ident.ml | 9 --------- src/ident/dune | 4 ---- src/name/Name.ml | 9 +++++++++ src/name/dune | 4 ++++ src/nbe/Data.ml | 20 ++++++++++---------- src/nbe/Domain.ml | 10 +++++----- src/nbe/Syntax.ml | 10 +++++----- src/nbe/dune | 2 +- src/pretty/Pretty.ml | 6 +++--- src/pretty/dune | 2 +- src/toplevel/dune | 2 +- 17 files changed, 57 insertions(+), 57 deletions(-) delete mode 100644 src/ident/Ident.ml delete mode 100644 src/ident/dune create mode 100644 src/name/Name.ml create mode 100644 src/name/dune diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml index 974409f..5952977 100644 --- a/src/ast/Ast.ml +++ b/src/ast/Ast.ml @@ -1,10 +1,10 @@ -type ident = Ident.t Asai.Range.located -type local_name = Ident.local Asai.Range.located +type ident = Name.t Asai.Range.located +type local_name = Name.local Asai.Range.located type arg = local_name * expr and raw_expr = - | Var of Ident.t + | Var of Name.t | Check of expr * expr | Pi of arg * expr | Fun of expr * expr @@ -38,7 +38,7 @@ type item = type file = item List.t -let dump_ident fmt ({ value; _ } : ident) = Ident.pp fmt value +let dump_ident fmt ({ value; _ } : ident) = Name.pp fmt value let dump_local_name fmt ({ value; _ } : local_name) = match value with | Some name -> Format.pp_print_string fmt name @@ -48,7 +48,7 @@ let rec dump_arg fmt ((name, tp) : arg) = Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_local_name name dump_expr tp and dump_raw_expr fmt = function - | Var id -> Format.fprintf fmt "Var @[%a@]" Ident.pp id + | Var name -> Format.fprintf fmt "Var @[%a@]" Name.pp name | Check (tm, tp) -> Format.fprintf fmt "@[%a@] : @[%a@]" dump_expr tm dump_expr tp | Bool -> Format.pp_print_string fmt "Bool" | True -> Format.pp_print_string fmt "True" diff --git a/src/ast/dune b/src/ast/dune index 072fe89..e3761bb 100644 --- a/src/ast/dune +++ b/src/ast/dune @@ -1,4 +1,4 @@ (library (name Ast) (public_name toytt.ast) - (libraries asai toytt.ident)) + (libraries asai toytt.name)) diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index c366ff3..d15a7f3 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -10,7 +10,7 @@ type env = { (* invariant: `tps`, `tms` and `names` all have length `size` *) tps : D.env; tms : D.env; - names : Ident.local bwd; + names : Name.local bwd; size : int; (* top-level context *) @@ -21,23 +21,23 @@ module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) (* general helpers *) -let lookup (id : Ident.t) : D.t * S.t = +let lookup (name : Name.t) : D.t * S.t = let env = Eff.read() in (* search through local context *) match Option.bind - (Ident.to_local id) + (Name.to_local name) (fun name -> Bwd.find_index ((=) name) env.names) with | Some ix -> let tp = Bwd.nth env.tps ix in (tp, S.Var ix) | None -> (* look up in top-level context *) - match Yuujinchou.Trie.find_singleton id env.toplvl with + match Yuujinchou.Trie.find_singleton name env.toplvl with | Some (Def { tp; tm }, _) -> - (tp, S.Def (id, tm)) - | None -> Error.unbound_variable id + (tp, S.Def (name, tm)) + | None -> Error.unbound_variable name -let bind ~(name : Ident.local) ~(tp : D.t) f = +let bind ~(name : Name.local) ~(tp : D.t) f = let arg = D.var (Eff.read()).size in let update env = { env with @@ -117,7 +117,7 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = end; tm -and check_connective connective ~(name : Ident.local) ~(base : A.expr) ~(fam : A.expr) ~(tp : D.t) = +and check_connective connective ~(name : Name.local) ~(base : A.expr) ~(fam : A.expr) ~(tp : D.t) = match tp with | D.Type -> let base = check ~tm:base ~tp in diff --git a/src/elaborator/dune b/src/elaborator/dune index e4180fa..3e5a418 100644 --- a/src/elaborator/dune +++ b/src/elaborator/dune @@ -6,7 +6,7 @@ bwd toytt.ast toytt.error - toytt.ident + toytt.name toytt.nbe toytt.pretty toytt.toplevel)) diff --git a/src/error/Error.ml b/src/error/Error.ml index 9a5ea9e..7a6a681 100644 --- a/src/error/Error.ml +++ b/src/error/Error.ml @@ -42,8 +42,8 @@ let illegal_character ~loc char = fatalf ~loc IllegalCharacter "illegal character '%s'" (Char.escaped char) let syntax_error ~loc = fatalf ~loc SyntaxError "syntax error" -let unbound_variable id = fatalf UnboundVariable - "unbound variable '%a'" Ident.pp id +let unbound_variable name = fatalf UnboundVariable + "unbound variable '%a'" Name.pp name let type_mismatch ?loc fmt_expected expected fmt_found found = fatalf ?loc TypeMismatch "@[type mismatch:@,expected: @[%a@]@, found: @[%a@]@]" fmt_expected expected fmt_found found diff --git a/src/error/dune b/src/error/dune index 857f7bc..916be3c 100644 --- a/src/error/dune +++ b/src/error/dune @@ -1,4 +1,4 @@ (library (name Error) (public_name toytt.error) - (libraries asai toytt.ident)) + (libraries asai toytt.name)) diff --git a/src/ident/Ident.ml b/src/ident/Ident.ml deleted file mode 100644 index 81c6575..0000000 --- a/src/ident/Ident.ml +++ /dev/null @@ -1,9 +0,0 @@ -type t = Yuujinchou.Trie.path - -type local = string option - -let to_local : t -> local option = function - | name :: [] -> Some (Some name) - | _ -> None - -let pp = Fmt.list ~sep:(Fmt.const Fmt.char '.') Fmt.string diff --git a/src/ident/dune b/src/ident/dune deleted file mode 100644 index 732a2c7..0000000 --- a/src/ident/dune +++ /dev/null @@ -1,4 +0,0 @@ -(library - (name Ident) - (public_name toytt.ident) - (libraries fmt yuujinchou)) diff --git a/src/name/Name.ml b/src/name/Name.ml new file mode 100644 index 0000000..81c6575 --- /dev/null +++ b/src/name/Name.ml @@ -0,0 +1,9 @@ +type t = Yuujinchou.Trie.path + +type local = string option + +let to_local : t -> local option = function + | name :: [] -> Some (Some name) + | _ -> None + +let pp = Fmt.list ~sep:(Fmt.const Fmt.char '.') Fmt.string diff --git a/src/name/dune b/src/name/dune new file mode 100644 index 0000000..5a4e44c --- /dev/null +++ b/src/name/dune @@ -0,0 +1,4 @@ +(library + (name Name) + (public_name toytt.name) + (libraries fmt yuujinchou)) diff --git a/src/nbe/Data.ml b/src/nbe/Data.ml index 8589ea5..38739b3 100644 --- a/src/nbe/Data.ml +++ b/src/nbe/Data.ml @@ -2,11 +2,11 @@ open Bwd type syn = | Var of int - | Def of Ident.t * value Lazy.t - | Pi of Ident.local * syn * (* BINDS *) syn - | Lam of Ident.local * (* BINDS *) syn + | Def of Name.t * value Lazy.t + | Pi of Name.local * syn * (* BINDS *) syn + | Lam of Name.local * (* BINDS *) syn | App of syn * syn - | Sg of Ident.local * syn * (* BINDS *) syn + | Sg of Name.local * syn * (* BINDS *) syn | Pair of syn * syn | Fst of syn | Snd of syn @@ -15,7 +15,7 @@ type syn = | True | False | BoolElim of { - motive_var : Ident.local; + motive_var : Name.local; motive : (* BINDS *) syn; true_case : syn; false_case : syn; @@ -25,9 +25,9 @@ type syn = and value = | Neutral of ne | Unfold of unfold - | Pi of Ident.local * value * clo - | Lam of Ident.local * clo - | Sg of Ident.local * value * clo + | Pi of Name.local * value * clo + | Lam of Name.local * clo + | Sg of Name.local * value * clo | Pair of value * value | Type | Bool @@ -40,14 +40,14 @@ and ne_head = and unfold = unfold_head * frm bwd * value Lazy.t and unfold_head = - | Def of Ident.t * value Lazy.t + | Def of Name.t * value Lazy.t and frm = | App of value | Fst | Snd | BoolElim of { - motive_var : Ident.local; + motive_var : Name.local; motive: clo; true_case: value; false_case: value; diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml index bf5ed90..f0922e8 100644 --- a/src/nbe/Domain.ml +++ b/src/nbe/Domain.ml @@ -3,9 +3,9 @@ open Bwd type t = Data.value = | Neutral of ne | Unfold of unfold - | Pi of Ident.local * t * clo - | Lam of Ident.local * clo - | Sg of Ident.local * t * clo + | Pi of Name.local * t * clo + | Lam of Name.local * clo + | Sg of Name.local * t * clo | Pair of t * t | Type | Bool @@ -18,14 +18,14 @@ and ne_head = Data.ne_head = and unfold = Data.unfold and unfold_head = Data.unfold_head = - | Def of Ident.t * t Lazy.t + | Def of Name.t * t Lazy.t and frm = Data.frm = | App of t | Fst | Snd | BoolElim of { - motive_var : Ident.local; + motive_var : Name.local; motive : clo; true_case : t; false_case: t; diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml index 5de5281..859102a 100644 --- a/src/nbe/Syntax.ml +++ b/src/nbe/Syntax.ml @@ -1,10 +1,10 @@ type t = Data.syn = | Var of int - | Def of Ident.t * Data.value Lazy.t - | Pi of Ident.local * t * (* BINDS *) t - | Lam of Ident.local * (* BINDS *) t + | Def of Name.t * Data.value Lazy.t + | Pi of Name.local * t * (* BINDS *) t + | Lam of Name.local * (* BINDS *) t | App of t * t - | Sg of Ident.local * t * (* BINDS *) t + | Sg of Name.local * t * (* BINDS *) t | Pair of t * t | Fst of t | Snd of t @@ -13,7 +13,7 @@ type t = Data.syn = | True | False | BoolElim of { - motive_var : Ident.local; + motive_var : Name.local; motive : (* BINDS *) t; true_case : t; false_case : t; diff --git a/src/nbe/dune b/src/nbe/dune index 3e62347..184d44f 100644 --- a/src/nbe/dune +++ b/src/nbe/dune @@ -1,4 +1,4 @@ (library (name NbE) (public_name toytt.nbe) - (libraries algaeff bwd toytt.ident toytt.error)) + (libraries algaeff bwd toytt.error toytt.name)) diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml index fa25a40..2f0a40b 100644 --- a/src/pretty/Pretty.ml +++ b/src/pretty/Pretty.ml @@ -6,13 +6,13 @@ module S = NbE.Syntax module Internal = struct type env = { - names : Ident.local bwd; + names : Name.local bwd; prec : int; } module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) - let bind (name : Ident.local) f fmt x = + let bind (name : Name.local) f fmt x = let update env = { env with names = env.names <: name } in Eff.scope update (fun () -> f fmt x) @@ -74,7 +74,7 @@ struct (* TODO: improve indentation *) and pp fmt = function | S.Var ix -> pp_var fmt ix - | S.Def (p, _) -> Ident.pp fmt p + | S.Def (p, _) -> Name.pp fmt p | S.Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam) | S.Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body | S.Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam) diff --git a/src/pretty/dune b/src/pretty/dune index 708b5b1..ea47845 100644 --- a/src/pretty/dune +++ b/src/pretty/dune @@ -5,5 +5,5 @@ bwd fmt toytt.error - toytt.ident + toytt.name toytt.nbe)) diff --git a/src/toplevel/dune b/src/toplevel/dune index 720635c..5840fd7 100644 --- a/src/toplevel/dune +++ b/src/toplevel/dune @@ -3,5 +3,5 @@ (public_name toytt.toplevel) (libraries yuujinchou - toytt.ident + toytt.name toytt.nbe)) -- cgit 1.4.1