👹 Worship Yuujinchou 5.0

.github/workflows/ocaml.yml

@@ -9,7 +9,7 @@ jobs:
     strategy:
       matrix:
         include:
-          - ocaml-compiler: "4.13"
+          - ocaml-compiler: "5.0"
             with-doc: true
     runs-on: ubuntu-latest
     steps:

README.md

@@ -1,6 +1,6 @@
 ## cooltt
 
-A cool implementation of normalization by evaluation (nbe) & elaboration for
+A cool implementation of normalization by evaluation (NbE) & elaboration for
 Cartesian cubical type theory.
 
 For examples, see the `test/` directory.
@@ -16,14 +16,14 @@ See `test/README.md` for a brief description of each program's purpose.
 
 ## Building
 
-cooltt has been built with OCaml 4.13.0 with [opam
-2.0.8](https://opam.ocaml.org/). 
+cooltt has been built with OCaml 5.0 with [opam 2.0.8](https://opam.ocaml.org/).
 
 ### With OPAM
+
 If you are running an older version of OCaml, try executing the following command:
 
 ```
-$ opam switch create 4.13.0
+$ opam switch create 5.0
 ```
 
 Once these dependencies are installed cooltt can be built with the following set of commands.
@@ -46,22 +46,27 @@ $ dune exec cooltt                      # from the `cooltt` top-level directory
 ```
 
 ### With Nix
+
 First, you'll need the [Nix package manager](https://nixos.org/download.html), and then
 you'll need to [install or enable flakes](https://nixos.wiki/wiki/Flakes).
 
 Then, cooltt can be built with the command
+
 ```
 nix build --impure
 ```
+
 to put a binary `cooltt` in `result/bin/cooltt`. This is good for if you just want to build
 and play around with cooltt.
 
 If you're working on cooltt, you can enter a development shell with an OCaml compiler, dune,
 and other tools with
+
 ```
 nix develop --impure
 ```
-and then build as in the [with OPAM](https://github.com/RedPRL/cooltt/#with-opam=) section 
+
+and then build as in the [with OPAM](https://github.com/RedPRL/cooltt/#with-opam=) section
 above.
 
 ## Acknowledgments

cooltt.opam

@@ -10,7 +10,7 @@ synopsis: "Experimental implementation of Cartesian cubical type theory"
 license: "Apache-2.0"
 depends: [
   "dune" {>= "2.0"}
-  "ocaml" {>= "4.10.0"}
+  "ocaml" {>= "5.0"}
   "ppx_deriving" {>= "4.4.1"}
   "bantorra" {>= "0.1" & < "0.2"}
   "bwd" {>= "2.1"}
@@ -20,7 +20,7 @@ depends: [
   "menhir" {>= "20180703"}
   "uuseg" {>= "12.0.0"}
   "uutf" {>= "1.0.2"}
-  "yuujinchou" {>= "2.0.0" & < "3"}
+  "yuujinchou" {>= "5.0"}
   "odoc" {with-doc}
   "kado"
 ]

src/core/Namespace.ml

@@ -1,51 +1,67 @@
+open Bwd
 open Yuujinchou
 
-type path = Pattern.path
+type path = Yuujinchou.Trie.path
 
-type 'a t = 'a Trie.t
-type 'a pattern = ([< `Print of string option] as 'a) Pattern.t
+module Param = struct
+  type data = CodeUnit.Global.t
+  type tag = unit
+  type hook = [`Print of string option]
+  type context = |
+end
+module M = Modifier.Make(Param)
+
+type t = CodeUnit.Global.t Trie.Untagged.t
+type pattern = [`Print of string option ] Yuujinchou.Language.t
+
+exception BindingNotFound of path
+exception Shadowing of path
 type ('a, 'error) result = ('a, [> `BindingNotFound of path | `Shadowing of path ] as 'error) Stdlib.result
 
 let empty = Trie.empty
 
 let prefix = Trie.prefix
 
-let merge ~shadowing ~rev_path _ x =
-  if shadowing
-  then Result.ok x
-  else Result.error (`Shadowing (List.rev rev_path))
+let merge ~shadowing path _ x =
+  if shadowing then x else raise @@ Shadowing (Bwd.to_list path)
 
 let transform ~shadowing ~pp pat ns =
-  let hooks (`Print lbl) ~rev_prefix t =
+  let not_found _ path = raise @@ BindingNotFound (Bwd.to_list path) in
+  let hook _ path (`Print lbl) t =
     let lbl = Option.fold ~none:"?" ~some:(fun lbl -> "?" ^ lbl) lbl in
     Format.printf "@[<v2>Emitted namespace under %a@,%s = @[{ "
-      Ident.pp (`User (List.rev rev_prefix)) lbl;
+      Ident.pp (`User (Bwd.to_list path)) lbl;
     let first = ref true in (* XXX NON-functional programming! *)
-    Trie.iteri (fun ~rev_path sym ->
+    Trie.Untagged.iter (fun path sym ->
         if not !first then Format.printf "@,; ";
         first := false; (* XXX there are 100 ways to avoid references *)
-        Format.printf "@[<hov>%a =>@ %a@]" Ident.pp (`User (List.rev rev_path)) pp sym) t;
+        Format.printf "@[<hov>%a =>@ %a@]" Ident.pp (`User (Bwd.to_list path)) pp sym) t;
     Format.printf "@ }@]@]@.@.";
-    Result.ok t
+    t
   in
-  Action.run_with_hooks ~hooks ~union:(merge ~shadowing) pat ns
+  try Result.ok @@ M.run ~not_found ~shadow:(fun _ctx -> merge ~shadowing) ~hook @@ fun () -> M.modify pat ns with
+  | BindingNotFound p -> Result.error @@ `BindingNotFound p
+  | Shadowing p -> Result.error @@ `Shadowing p
 
 let union ~shadowing ns1 ns2 =
-  Trie.Result.union (merge ~shadowing) ns1 ns2
+  try Result.ok @@ Trie.Untagged.union (merge ~shadowing) ns1 ns2 with
+  | Shadowing p -> Result.error @@ `Shadowing p
 
-let merge1 ~shadowing ~path x old_x =
+let merge1 ~shadowing path x old_x =
   if Option.is_none old_x || shadowing
-  then Result.ok (Some x)
-  else Result.error (`Shadowing (List.rev path))
+  then Some x
+  else raise @@ Shadowing (Bwd.to_list path)
 
 let add ~shadowing ident sym ns =
   match ident with
   | `User path ->
-    Trie.Result.update_singleton path (merge1 ~shadowing ~path sym) ns
-  | _ ->
-    Result.ok ns
+    begin
+      try Result.ok @@ Trie.Untagged.update_singleton path (merge1 ~shadowing (Bwd.of_list path) sym) ns with
+      | Shadowing p -> Result.error @@ `Shadowing p
+    end
+  | _ -> Result.ok ns
 
 let find (ident : Ident.t) ns =
   match ident with
-  | `User path -> Trie.find_singleton path ns
+  | `User path -> Trie.Untagged.find_singleton path ns
   | _ -> None

src/core/Namespace.mli

@@ -1,17 +1,21 @@
-type path = Yuujinchou.Pattern.path
+type path = Yuujinchou.Trie.path
 
-type +'a t
-type 'a pattern = ([< `Print of string option ] as 'a) Yuujinchou.Pattern.t
+type t
+type pattern = [`Print of string option ] Yuujinchou.Language.t
 type ('a, 'error) result = ('a, [> `BindingNotFound of path | `Shadowing of path ] as 'error) Stdlib.result
 
-val empty : 'a t
+val empty : t
 
-val prefix : path -> 'a t -> 'a t
+val prefix : path -> t -> t
 
-val transform : shadowing:bool -> pp:(Format.formatter -> 'a -> unit) -> _ pattern -> 'a t -> ('a t, 'error) result
+val transform : shadowing:bool
+  -> pp:(Format.formatter -> CodeUnit.Global.t -> unit)
+  -> pattern
+  -> t
+  -> (t, 'error) result
 
-val union : shadowing:bool -> 'a t -> 'a t -> ('a t, 'error) result
+val union : shadowing:bool -> t -> t -> (t, 'error) result
 
-val add : shadowing:bool -> Ident.t -> 'a -> 'a t -> ('a t, 'error) result
+val add : shadowing:bool -> Ident.t -> CodeUnit.Global.t -> t -> (t, 'error) result
 
-val find : Ident.t -> 'a t -> 'a option
+val find : Ident.t -> t -> CodeUnit.Global.t option

src/core/RefineMonad.mli

@@ -27,12 +27,12 @@ val get_local : int -> D.con m
 val get_lib : Bantorra.Manager.library m
 val with_unit : Bantorra.Manager.library -> id -> 'a m -> 'a m
 
-val import : shadowing:bool -> _ Namespace.pattern -> id -> unit m
+val import : shadowing:bool -> Namespace.pattern -> id -> unit m
 val loading_status : CodeUnitID.t -> [ `Loaded | `Loading | `Unloaded ] m
 
-val view : shadowing:bool -> _ Namespace.pattern -> unit m
-val export : shadowing:bool -> _ Namespace.pattern -> unit m
-val repack : shadowing:bool -> _ Namespace.pattern -> unit m
+val view : shadowing:bool -> Namespace.pattern -> unit m
+val export : shadowing:bool -> Namespace.pattern -> unit m
+val repack : shadowing:bool -> Namespace.pattern -> unit m
 val with_section : shadowing:bool -> prefix:Namespace.path option -> 'a m -> 'a m
 
 val eval : S.t -> D.con m

src/core/RefineState.ml

@@ -11,7 +11,7 @@ type t =
     (** current unit ID *)
     unit_id : CodeUnitID.t;
     (** current nested scopes *)
-    scopes : Global.t Scopes.t;
+    scopes : Scopes.t;
     (** numbers of holes in the current unit *)
     holes : (D.tp * D.cof * D.tm_clo) list;
 
@@ -21,7 +21,7 @@ type t =
     (** all known units (including the ones that are being processed), which keep the data associated with global symbols *)
     units : CodeUnit.t IDMap.t;
     (** all global cofibrations and namespaces exported by processed units (not including the ones in proccessing) *)
-    exports : (Global.t Namespace.t * CofThy.Disj.t) IDMap.t;
+    exports : (Namespace.t * CofThy.Disj.t) IDMap.t;
   }
 
 let init lib =

src/core/RefineState.mli

@@ -11,10 +11,10 @@ val get_holes : t -> (D.tp * D.cof * D.tm_clo) list
 val add_hole : (D.tp * D.cof * D.tm_clo) -> t -> t
 
 (* Manipulate of scopes *)
-val transform_view : shadowing:bool -> _ Namespace.pattern -> t -> (t, 'error) Namespace.result
-val transform_export : shadowing:bool -> _ Namespace.pattern -> t -> (t, 'error) Namespace.result
-val export_view : shadowing:bool -> _ Namespace.pattern -> t -> (t, 'error) Namespace.result
-val import : shadowing:bool -> _ Namespace.pattern -> CodeUnitID.t -> t -> (t, 'error) Namespace.result
+val transform_view : shadowing:bool -> Namespace.pattern -> t -> (t, 'error) Namespace.result
+val transform_export : shadowing:bool -> Namespace.pattern -> t -> (t, 'error) Namespace.result
+val export_view : shadowing:bool -> Namespace.pattern -> t -> (t, 'error) Namespace.result
+val import : shadowing:bool -> Namespace.pattern -> CodeUnitID.t -> t -> (t, 'error) Namespace.result
 
 val begin_section : t -> t
 val end_section : shadowing:bool -> prefix:Namespace.path option -> t -> (t, 'error) Namespace.result

src/core/Scope.ml

@@ -1,6 +1,6 @@
-type 'a t =
-  { view : 'a Namespace.t
-  ; export : 'a Namespace.t
+type t =
+  { view : Namespace.t
+  ; export : Namespace.t
   }
 
 let empty = {view = Namespace.empty; export = Namespace.empty}

src/core/Scope.mli

@@ -1,30 +1,30 @@
-type +'a t
+type t
 
-val empty : 'a t
-val inherit_view : 'a t -> 'a t
-val get_export : prefix:Namespace.path option -> 'a t -> 'a Namespace.t
-val resolve : Ident.t -> 'a t -> 'a option
+val empty : t
+val inherit_view : t -> t
+val get_export : prefix:Namespace.path option -> t -> Namespace.t
+val resolve : Ident.t -> t -> CodeUnit.Global.t option
 
 val transform_view :
   shadowing:bool ->
-  pp:(Format.formatter -> 'a -> unit) ->
-  _ Namespace.pattern ->
-  'a t -> ('a t, 'error) Namespace.result
+  pp:(Format.formatter -> CodeUnit.Global.t -> unit) ->
+  Namespace.pattern ->
+  t -> (t, 'error) Namespace.result
 
 val transform_export :
   shadowing:bool ->
-  pp:(Format.formatter -> 'a -> unit) ->
-  _ Namespace.pattern ->
-  'a t -> ('a t, 'error) Namespace.result
+  pp:(Format.formatter -> CodeUnit.Global.t -> unit) ->
+  Namespace.pattern ->
+  t -> (t, 'error) Namespace.result
 
 val export_view :
   shadowing:bool ->
-  pp:(Format.formatter -> 'a -> unit) ->
-  _ Namespace.pattern ->
-  'a t -> ('a t, 'error) Namespace.result
+  pp:(Format.formatter -> CodeUnit.Global.t -> unit) ->
+  Namespace.pattern ->
+  t -> (t, 'error) Namespace.result
 
-val add : shadowing:bool -> Ident.t -> 'a -> 'a t -> ('a t, 'error) Namespace.result
+val add : shadowing:bool -> Ident.t -> CodeUnit.Global.t -> t -> (t, 'error) Namespace.result
 
-val include_ : shadowing:bool -> 'a Namespace.t -> 'a t -> ('a t, 'error) Namespace.result
+val include_ : shadowing:bool -> Namespace.t -> t -> (t, 'error) Namespace.result
 
-val import : shadowing:bool -> 'a Namespace.t -> 'a t -> ('a t, 'error) Namespace.result
+val import : shadowing:bool -> Namespace.t -> t -> (t, 'error) Namespace.result

src/core/Scopes.ml

@@ -1,6 +1,6 @@
 open Bwd
 
-type 'a t = 'a Scope.t bwd
+type t = Scope.t bwd
 
 let init s = Snoc (Emp, s)
 

src/core/Scopes.mli

@@ -1,30 +1,30 @@
-type +'a t
+type t
 
-val init : 'a Scope.t -> 'a t
+val init : Scope.t -> t
 
 val transform_view :
   shadowing:bool ->
-  pp:(Format.formatter -> 'a -> unit) ->
-  _ Namespace.pattern ->
-  'a t -> ('a t, 'error) Namespace.result
+  pp:(Format.formatter -> CodeUnit.Global.t -> unit) ->
+  Namespace.pattern ->
+  t -> (t, 'error) Namespace.result
 
 val transform_export :
   shadowing:bool ->
-  pp:(Format.formatter -> 'a -> unit) ->
-  _ Namespace.pattern ->
-  'a t -> ('a t, 'error) Namespace.result
+  pp:(Format.formatter -> CodeUnit.Global.t -> unit) ->
+  Namespace.pattern ->
+  t -> (t, 'error) Namespace.result
 
 val export_view :
   shadowing:bool ->
-  pp:(Format.formatter -> 'a -> unit) ->
-  _ Namespace.pattern ->
-  'a t -> ('a t, 'error) Namespace.result
+  pp:(Format.formatter -> CodeUnit.Global.t -> unit) ->
+  Namespace.pattern ->
+  t -> (t, 'error) Namespace.result
 
-val add : shadowing:bool -> Ident.t -> 'a -> 'a t -> ('a t, 'error) Namespace.result
-val import : shadowing:bool -> 'a Namespace.t -> 'a t -> ('a t, 'error) Namespace.result
+val add : shadowing:bool -> Ident.t -> CodeUnit.Global.t -> t -> (t, 'error) Namespace.result
+val import : shadowing:bool -> Namespace.t -> t -> (t, 'error) Namespace.result
 
-val begin_ : 'a t -> 'a t
-val end_ : shadowing:bool -> prefix:Namespace.path option -> 'a t -> ('a t, 'error) Namespace.result
+val begin_ : t -> t
+val end_ : shadowing:bool -> prefix:Namespace.path option -> t -> (t, 'error) Namespace.result
 
-val resolve : Ident.t -> 'a t -> 'a option
-val export_top : 'a t -> 'a Namespace.t
+val resolve : Ident.t -> t -> CodeUnit.Global.t option
+val export_top : t -> Namespace.t

src/frontend/ConcreteSyntaxData.ml

@@ -79,7 +79,7 @@ and con_ =
   | V of con * con * con * con
   | VProj of con
   | Cap of con
-  | ModAny
+  | ModAll
   | ModOnly of string list
   | ModRename of string list * string list
   | ModNone

src/frontend/Driver.ml

@@ -257,7 +257,7 @@ and execute_decl (decl : CS.decl) : command =
 
   | CS.Import {shadowing; unitpath; modifier} ->
     RM.update_span (Option.fold ~none:None ~some:CS.get_info modifier) @@
-    let* modifier = Option.fold ~none:(RM.ret Yuujinchou.Pattern.any) ~some:Elaborator.modifier modifier in
+    let* modifier = Option.fold ~none:(RM.ret Yuujinchou.Language.all) ~some:Elaborator.modifier modifier in
     import_unit ~shadowing unitpath modifier
   | CS.View {shadowing; modifier} ->
     RM.update_span (CS.get_info modifier) @@
@@ -280,7 +280,7 @@ and execute_decl (decl : CS.decl) : command =
       function
       | Ok () ->
         RM.update_span (Option.fold ~none:None ~some:CS.get_info modifier) @@
-        let* modifier = Option.fold ~none:(RM.ret @@ Yuujinchou.Pattern.seq []) ~some:Elaborator.modifier modifier in
+        let* modifier = Option.fold ~none:(RM.ret @@ Yuujinchou.Language.id) ~some:Elaborator.modifier modifier in
         let* () = RM.repack ~shadowing modifier in
         RM.ret Continue
       | Error () -> RM.refine_err ErrorsInSection