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/elaborator/Elaborator.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/elaborator/Elaborator.ml') 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 -- cgit 1.4.1