about summary refs log tree commit diff
path: root/src/elaborator
diff options
context:
space:
mode:
Diffstat (limited to 'src/elaborator')
-rw-r--r--src/elaborator/Elaborator.ml16
-rw-r--r--src/elaborator/dune2
2 files changed, 9 insertions, 9 deletions
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))