bootstrap HOTT at build time, close #90

bin/dune

@@ -9,7 +9,7 @@
         (system "date +'%Y-%m-%d'")))))
 
 (executable
-  (libraries core parser top react lwt lambda-term)
+  (libraries core parser top hott react lwt lambda-term)
   (name narya)
   (public_name narya)
   (preprocess (pps ppx_blob))

bin/narya.ml

@@ -240,7 +240,7 @@ let rec interact_pg () : unit =
 
 let () =
   try
-    run_top @@ fun () ->
+    run_top ~install_hott:Hott.install @@ fun () ->
     (* Note: run_top executes the input files, so here we only have to do the interaction. *)
     Mbwd.miter
       (fun [ file ] ->

js/jsnarya.ml

@@ -39,7 +39,7 @@ let _ =
          discreteness := disc;
          inputs := Snoc (Emp, `String (Js.to_string startup));
          try
-           let _ = Pauser.init ~use_ansi:true (fun () -> "") in
+           let _ = Pauser.init ~use_ansi:true ~install_hott:(fun () -> ()) (fun () -> "") in
            Js.null
          with Top.Exit ->
            (* If executing the extra startup code raises an error, we catch that error in the error buffer and return it. *)

lib/core/check.ml

@@ -268,8 +268,8 @@ type (_, _, _) meta_tel =
       string option * ('a, 'b, potential) Meta.t * (('b, D.zero) snoc, 'c, 'bc) meta_tel
       -> ('b, 'c Fwn.suc, 'bc) meta_tel
 
-(* In HOTT mode, the user isn't allowed to define gel-types, so we bail out at typechecking time if we detect one.  However, we do want to allow *ourselves* to define glue as a Gel-type later on, so we start out this flag as true and then set it (permanently) to false later. *)
-let gel_ok = ref true
+(* In HOTT mode, the user isn't allowed to define gel-types, so we bail out at typechecking time if we detect one.  But in parametricity mode, and when bootstrapping the definition of glue, we set this flag to true. *)
+let gel_ok = ref false
 
 (* Check a term or case tree (depending on the energy: terms are kinetic, case trees are potential).  The ?discrete parameter is supplied if the term we are currently checking might be a discrete datatype, in which case it is a set of all the currently-being-defined mutual constants.  Most term-formers are nondiscrete, so they can just ignore this argument and make their recursive calls without it. *)
 let rec check : type a b s.

lib/core/constant.ml

@@ -1,5 +1,6 @@
 (* This module should not be opened, but be used qualified. *)
 
+open Util
 open Origin
 
 (* A constant is identified by an autonumber, scoped by an Origin. *)
@@ -44,7 +45,7 @@ module Table = struct
 
   (* Get or set all the data associated to a single file. *)
 
-  type 'a file_entry = 'a IntMap.t option
+  type 'a origin_entry = 'a IntMap.t option
 
   let find_file file tbl = Versioned.get_at tbl (File file)
 
@@ -53,17 +54,16 @@ module Table = struct
     | Some x -> Versioned.set_file tbl file x
     | None -> ()
 
-  (* Marshal the objects associated to a specific file only. *)
-  let to_channel_file chan file (tbl : 'a t) flags =
-    Marshal.to_channel chan (Versioned.get_at tbl (File file)) flags
+  (* Marshal the objects associated to a specific origin only. *)
+  let to_channel_origin chan origin (tbl : 'a t) flags =
+    Marshal.to_channel chan (Versioned.get_at tbl origin) flags
 
-  (* Unmarshal the objects associated to a specific file only, applying f to their elements before adding them to the current map, and returning the new file data. *)
-  let from_channel_file chan f file tbl =
-    match (Marshal.from_channel chan : 'a IntMap.t option) with
+  (* Unmarshal the objects associated to a specific origin only, applying f to their elements before adding them to the current map, and returning the new origin data. *)
+  let from_istream_origin chan f origin tbl =
+    match (Istream.unmarshal chan : 'a IntMap.t option) with
     | Some x ->
         let fx = IntMap.map f x in
-        Versioned.set_file tbl file fx;
-        Some fx
+        Option.bind (Versioned.set_at tbl origin fx) @@ fun () -> Some fx
     | None -> None
 end
 

lib/core/constant.mli

@@ -1,3 +1,4 @@
+open Util
 open Origin
 
 module Constant : sig
@@ -18,12 +19,12 @@ module Table : sig
   val find_opt : Constant.t -> 'a t -> 'a option
   val add : Constant.t -> 'a -> 'a t -> unit
 
-  type 'a file_entry
+  type 'a origin_entry
 
-  val find_file : File.t -> 'a t -> 'a file_entry
-  val add_file : File.t -> 'a file_entry -> 'a t -> unit
-  val to_channel_file : out_channel -> File.t -> 'a t -> Marshal.extern_flags list -> unit
-  val from_channel_file : in_channel -> ('a -> 'b) -> File.t -> 'b t -> 'b file_entry
+  val find_file : File.t -> 'a t -> 'a origin_entry
+  val add_file : File.t -> 'a origin_entry -> 'a t -> unit
+  val to_channel_origin : out_channel -> Origin.t -> 'a t -> Marshal.extern_flags list -> unit
+  val from_istream_origin : Istream.t -> ('a -> 'b) -> Origin.t -> 'b t -> 'b origin_entry
 end
 
 module Map : module type of Map.Make (Constant)

lib/core/global.ml

@@ -101,18 +101,18 @@ let all_holes () =
 
 (* Marshal and unmarshal the constants and metavariables pertaining to a single file.  We ignore the "current" data because that is only relevant during typechecking commands, whereas this comes at the end of typechecking a whole file.  We do NOT marshal the "holes" table because compiled files can't contain holes, and holedata potentially contains functional values. *)
 
-let to_channel_file chan file flags =
-  Constant.Table.to_channel_file chan file constants flags;
-  Metatable.to_channel_file chan file metas flags
+let to_channel_origin chan origin flags =
+  Constant.Table.to_channel_origin chan origin constants flags;
+  Metatable.to_channel_origin chan origin metas flags
 
 let link_definition f df =
   match df with
   | `Axiom, p -> (`Axiom, p)
   | `Defined tm, p -> (`Defined (Link.term f tm), p)
 
-type file_entry =
-  ((emp, kinetic) term * definition, Code.t) Result.t Constant.Table.file_entry
-  * unit Metatable.file_entry
+type origin_entry =
+  ((emp, kinetic) term * definition, Code.t) Result.t Constant.Table.origin_entry
+  * unit Metatable.origin_entry
 
 let find_file i = (Constant.Table.find_file i constants, Metatable.find_file i metas)
 
@@ -121,14 +121,14 @@ let add_file i (c, m) =
   Metatable.add_file i m metas
 
 (* Returns the new file data for constants and metas. *)
-let from_channel_file f chan i =
+let from_istream_origin f chan i =
   (* NB in a tuple (a,b), OCaml executes b before a!  But we have to unmarshal the constants before the metas, because that's the order we marshaled them in, so we control the order of execution with let.  *)
   let cs =
-    Constant.Table.from_channel_file chan
+    Constant.Table.from_istream_origin chan
       (Result.map (fun (tm, df) -> (Link.term f tm, link_definition f df)))
       i constants in
   let ms =
-    Metatable.from_channel_file chan
+    Metatable.from_istream_origin chan
       {
         map =
           (fun _ df ->
@@ -139,10 +139,10 @@ let from_channel_file f chan i =
       i metas in
   (cs, ms)
 
-(* Add a new constant. *)
+(* Add a new constant.  Only works on the current origin. *)
 let add c ty df = Constant.Table.add c (Ok (ty, df)) constants
 
-(* Set the definition of an already-defined constant.  Only works for the current origin. *)
+(* Set the definition of an already-defined constant.  Only works on the current origin. *)
 let set c df =
   match Constant.Table.find_opt c constants with
   | Some (Ok (ty, _)) -> Constant.Table.add c (Ok (ty, df)) constants

lib/core/global.mli

@@ -27,13 +27,13 @@ type find_hole =
 
 val find_hole : int -> find_hole
 val all_holes : unit -> find_hole Bwd.t
-val to_channel_file : Out_channel.t -> File.t -> Marshal.extern_flags list -> unit
+val to_channel_origin : Out_channel.t -> Origin.t -> Marshal.extern_flags list -> unit
 
-type file_entry
+type origin_entry
 
-val find_file : File.t -> file_entry
-val add_file : File.t -> file_entry -> unit
-val from_channel_file : (File.t -> File.t) -> In_channel.t -> File.t -> file_entry
+val find_file : File.t -> origin_entry
+val add_file : File.t -> origin_entry -> unit
+val from_istream_origin : (File.t -> File.t) -> Istream.t -> Origin.t -> origin_entry
 val add : Constant.t -> (emp, kinetic) term -> definition -> unit
 val set : Constant.t -> definition -> unit
 val add_error : Constant.t -> Reporter.Code.t -> unit

lib/core/meta.ml

@@ -177,30 +177,29 @@ module Table = struct
      fun f m acc ->
       IdMap.fold (fun _ (Entry (key, value)) acc -> f.fold key value acc) (Versioned.get m) acc
 
-    type 'x file_entry = 'x entry IdMap.t option
+    type 'x origin_entry = 'x entry IdMap.t option
 
-    let find_file (file : File.t) (m : 'a t) : 'a file_entry = Versioned.get_at m (File file)
+    let find_file (file : File.t) (m : 'a t) = Versioned.get_at m (File file)
 
     let add_file file x m =
       match x with
       | Some x -> Versioned.set_file m file x
       | None -> ()
 
-    let to_channel_file : type x.
-        Out_channel.t -> File.t -> x t -> Marshal.extern_flags list -> unit =
-     fun chan file m flags -> Marshal.to_channel chan (find_file file m) flags
+    let to_channel_origin : type x.
+        Out_channel.t -> Origin.t -> x t -> Marshal.extern_flags list -> unit =
+     fun chan origin m flags -> Marshal.to_channel chan (Versioned.get_at m origin) flags
 
     type 'x mapper = {
       map : 'a 'b 's. ('a, 'b, 's) key -> ('x, 'a, 'b, 's) F.t -> ('x, 'a, 'b, 's) F.t;
     }
 
-    let from_channel_file : type x. In_channel.t -> x mapper -> File.t -> x t -> x file_entry =
-     fun chan f file m ->
-      match (Marshal.from_channel chan : x file_entry) with
+    let from_istream_origin : type x. Istream.t -> x mapper -> Origin.t -> x t -> x origin_entry =
+     fun chan f origin m ->
+      match (Istream.unmarshal chan : x origin_entry) with
       | Some n ->
           let fn = IdMap.map (fun (Entry (key, value)) -> Entry (key, f.map key value)) n in
-          add_file file (Some fn) m;
-          Some fn
+          Option.bind (Versioned.set_at m origin fn) @@ fun () -> Some fn
       | None -> None
   end
 end

lib/core/meta.mli

@@ -53,16 +53,16 @@ module Table : sig
     val fold : ('x, 'acc) folder -> 'x t -> 'acc -> 'acc
     val fold_current : ('x, 'acc) folder -> 'x t -> 'acc -> 'acc
 
-    type 'x file_entry
+    type 'x origin_entry
 
-    val find_file : File.t -> 'x t -> 'x file_entry
-    val add_file : File.t -> 'a file_entry -> 'a t -> unit
-    val to_channel_file : Out_channel.t -> File.t -> 'x t -> Marshal.extern_flags list -> unit
+    val find_file : File.t -> 'x t -> 'x origin_entry
+    val add_file : File.t -> 'a origin_entry -> 'a t -> unit
+    val to_channel_origin : Out_channel.t -> Origin.t -> 'x t -> Marshal.extern_flags list -> unit
 
     type 'x mapper = {
       map : 'a 'b 's. ('a, 'b, 's) key -> ('x, 'a, 'b, 's) F.t -> ('x, 'a, 'b, 's) F.t;
     }
 
-    val from_channel_file : In_channel.t -> 'x mapper -> File.t -> 'x t -> 'x file_entry
+    val from_istream_origin : Istream.t -> 'x mapper -> Origin.t -> 'x t -> 'x origin_entry
   end
 end

lib/core/origin.ml

@@ -266,6 +266,18 @@ module Versioned = struct
     grow_files x file;
     Dynarray.set x.files file v
 
+  (* Set the value of the object associated to a given origin.  If we are in the past, only instants before the current time are accessible. *)
+  let set_at (x : 'a t) (i : Origin.t) (v : 'a) : unit option =
+    try
+      match i with
+      | Top -> Some (x.top := v)
+      | File file -> Some (set_file x file v)
+      | Instant instant -> (
+          match Origin.S.get () with
+          | Past now when instant > now -> None
+          | _ -> Some (Dynarray.set x.instants instant v))
+    with Invalid_argument _ -> None
+
   (* Fold over all the entries. *)
   let fold (x : 'a t) (f : 'acc -> 'a -> 'acc) (acc : 'acc) : 'acc =
     let acc = f acc !(x.top) in

lib/core/origin.mli

@@ -38,5 +38,6 @@ module Versioned : sig
   val set : 'a t -> 'a -> unit
   val modify : 'a t -> ('a -> 'a) -> unit
   val set_file : 'a t -> File.t -> 'a -> unit
+  val set_at : 'a t -> Origin.t -> 'a -> unit option
   val fold : 'a t -> ('acc -> 'a -> 'acc) -> 'acc -> 'acc
 end