aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/ast/Ast.ml10
-rw-r--r--src/ast/dune2
-rw-r--r--src/elaborator/Elaborator.ml16
-rw-r--r--src/elaborator/dune2
-rw-r--r--src/error/Error.ml4
-rw-r--r--src/error/dune2
-rw-r--r--src/ident/dune4
-rw-r--r--src/name/Name.ml (renamed from src/ident/Ident.ml)0
-rw-r--r--src/name/dune4
-rw-r--r--src/nbe/Data.ml20
-rw-r--r--src/nbe/Domain.ml10
-rw-r--r--src/nbe/Syntax.ml10
-rw-r--r--src/nbe/dune2
-rw-r--r--src/pretty/Pretty.ml6
-rw-r--r--src/pretty/dune2
-rw-r--r--src/toplevel/dune2
16 files changed, 48 insertions, 48 deletions
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
"@[<v>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/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/ident/Ident.ml b/src/name/Name.ml
index 81c6575..81c6575 100644
--- a/src/ident/Ident.ml
+++ b/src/name/Name.ml
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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 10:47:54 +0000