Options to make function and type boundaries partly implicit

bin/narya.ml

@@ -33,6 +33,18 @@ let speclist =
     ("-compact", Arg.Set compact, "Reformat code compactly");
     ("-unicode", Arg.Set unicode, "Display and reformat code using Unicode for built-ins (default)");
     ("-ascii", Arg.Clear unicode, "Display and reformat code using ASCII for built-ins");
+    ( "-hide-function-boundaries",
+      Arg.Clear show_function_boundaries,
+      "Hide implicit boundaries of higher-dimensional applications (default)" );
+    ( "-show-function-boundaries",
+      Arg.Set show_function_boundaries,
+      "Display implicit boundaries of higher-dimensional applications" );
+    ( "-hide-type-boundaries",
+      Arg.Clear show_type_boundaries,
+      "Hide implicit boundaries of instantiations of higher-dimensional types (default)" );
+    ( "-show-type-boundaries",
+      Arg.Set show_type_boundaries,
+      "Display implicit boundaries of instantiations of higher-dimensional types" );
     ("-arity", Arg.Set_int arity, "Arity of parametricity (default = 2)");
     ( "-direction",
       Arg.String set_refls,

lib/core/dump.ml

@@ -183,7 +183,10 @@ and synth : type a. formatter -> a synth -> unit =
   | Const c -> fprintf ppf "Const(%a)" pp_printed (print (PConstant c))
   | Field (tm, fld) -> fprintf ppf "Field(%a, %s)" synth tm.value (Field.to_string_ori fld)
   | Pi (_, _, _) -> fprintf ppf "Pi(?)"
-  | App (fn, arg) -> fprintf ppf "App(%a, %a)" synth fn.value check arg.value
+  | App (fn, arg, { value = `Explicit; _ }) ->
+      fprintf ppf "App(%a, %a)" synth fn.value check arg.value
+  | App (fn, arg, { value = `Implicit; _ }) ->
+      fprintf ppf "App(%a, {%a})" synth fn.value check arg.value
   | Asc (tm, ty) -> fprintf ppf "Asc(%a, %a)" check tm.value check ty.value
   | Let (_, _, _) -> fprintf ppf "Let(?)"
   | Letrec (_, _, _) -> fprintf ppf "LetRec(?)"

lib/core/implicitboundaries.ml

@@ -0,0 +1,10 @@
+open Reporter
+
+let forward_functions : (unit -> [ `Implicit | `Explicit ]) ref =
+  ref (fun () -> fatal (Anomaly "Implicitboundaries.functions not set"))
+
+let forward_types : (unit -> [ `Implicit | `Explicit ]) ref =
+  ref (fun () -> fatal (Anomaly "Implicitboundaries.functions not set"))
+
+let functions () = !forward_functions ()
+let types () = !forward_types ()

lib/core/norm.ml

@@ -35,7 +35,7 @@ let rec take_args :
   | arg :: args, Suc plus -> take_args (Ext (env, mn, Ok arg)) mn args plus
   | _ -> fatal (Anomaly "wrong number of arguments in argument list")
 
-(* A "view" is the aspect of a type or term that we match against to determine its behavior.  A view of a term is just another term, but in WHNF.  A view of a type is either a universe, a pi-type, another canonical type (data or codata), or a neutral.  The non-neutral sorts come with their instantiations that have been checked to have the correct dimension. *)
+(* A "view" is the aspect of a type or term that we match against to determine its behavior.  A view of a term is just another term, but in WHNF.  A view of a type is either a universe, a pi-type, another canonical type (data or codata), or a neutral.  All come with their instantiations that have been checked to have the correct dimension. *)
 
 type view_type =
   | UU : (D.zero, 'k, 'k, normal) TubeOf.t -> view_type
@@ -46,7 +46,7 @@ type view_type =
       * (D.zero, 'k, 'k, normal) TubeOf.t
       -> view_type
   | Canonical : head * 'k canonical * (D.zero, 'k, 'k, normal) TubeOf.t -> view_type
-  | Neutral : head -> view_type
+  | Neutral : head * (D.zero, 'k, 'k, normal) TubeOf.t -> view_type
 
 let rec view_term : type s. s value -> s value =
  fun tm ->
@@ -121,7 +121,7 @@ and view_type ?(severity = Asai.Diagnostic.Bug) (ty : kinetic value) (err : stri
               (* Always a bug *)
               fatal (Dimension_mismatch ("view canonical", dim_canonical c, TubeOf.inst tyargs)))
       | Realize v -> view_type ~severity (inst v tyargs) err
-      | _ -> Neutral head)
+      | _ -> Neutral (head, tyargs))
 
 (* Evaluation of terms and evaluation of case trees are technically separate things.  In particular, evaluating a kinetic (standard) term always produces just a value, whereas evaluating a potential term (a function case tree) can either
 
@@ -1008,6 +1008,15 @@ let rec tyof_inst :
       } in
   inst (universe m) margs
 
+(* Get the instantiation arguments of a type, of any sort. *)
+let get_tyargs ?(severity = Asai.Diagnostic.Bug) (ty : kinetic value) (err : string) :
+    normal full_tube =
+  match view_type ~severity ty err with
+  | UU tyargs -> Full_tube tyargs
+  | Pi (_, _, _, tyargs) -> Full_tube tyargs
+  | Canonical (_, _, tyargs) -> Full_tube tyargs
+  | Neutral (_, tyargs) -> Full_tube tyargs
+
 (* Check whether a given type is discrete, or has one of the the supplied constant heads (since for testing whether a newly defined datatype can be discrete, it and members of its mutual families can appear in its own parameters and arguments). *)
 let is_discrete : ?discrete:unit Constant.Map.t -> kinetic value -> bool =
  fun ?discrete ty ->
@@ -1016,7 +1025,7 @@ let is_discrete : ?discrete:unit Constant.Map.t -> kinetic value -> bool =
   (* The currently-being-defined types may not be canonical yet: if they don't have definitions yet they are neutral. *)
   | Canonical (Const { name; ins }, _, _), Some consts ->
       Option.is_some (is_id_ins ins) && Constant.Map.mem name consts
-  | Neutral (Const { name; ins }), Some consts ->
+  | Neutral (Const { name; ins }, _), Some consts ->
       Option.is_some (is_id_ins ins) && Constant.Map.mem name consts
       (* In theory, pi-types with discrete codomain, and record types with discrete fields, could also be discrete.  But that would be trickier to check as it would require evaluating their codomain and fields under binders, and eta-conversion for those types should implement direct discreteness automatically.  So the only thing we're missing is that they can't appear as arguments to a constructor of some other discrete datatype. *)
   | _ -> false

lib/core/raw.ml

@@ -107,7 +107,8 @@ module Make (I : Indices) = struct
     | Const : Constant.t -> 'a synth
     | Field : 'a synth located * Field.or_index -> 'a synth
     | Pi : I.name * 'a check located * 'a I.suc check located -> 'a synth
-    | App : 'a synth located * 'a check located -> 'a synth
+    (* The location of the implicitness flag is, in the implicit case, the location of the braces surrounding the implicit argument. *)
+    | App : 'a synth located * 'a check located * [ `Implicit | `Explicit ] located -> 'a synth
     | Asc : 'a check located * 'a check located -> 'a synth
     | UU : 'a synth
     (* A Let can either synthesize or (sometimes) check.  It synthesizes only if its body also synthesizes, but we wait until typechecking type to look for that, so that if it occurs in a checking context the body can also be checking.  Thus, we make it a "synthesizing term".  The term being bound must also synthesize; the shorthand notation "let x : A := M" is expanded during parsing to "let x := M : A". *)
@@ -247,7 +248,7 @@ module Resolve (R : Resolver) = struct
       | Const c -> Const c
       | Field (tm, fld) -> Field (synth ctx tm, fld)
       | Pi (x, dom, cod) -> Pi (R.rename ctx x, check ctx dom, check (R.snoc ctx x) cod)
-      | App (fn, arg) -> App (synth ctx fn, check ctx arg)
+      | App (fn, arg, impl) -> App (synth ctx fn, check ctx arg, impl)
       | Asc (tm, ty) -> Asc (check ctx tm, check ctx ty)
       | UU -> UU
       | Let (x, tm, body) -> Let (R.rename ctx x, synth ctx tm, (check (R.snoc ctx x)) body)

lib/core/reporter.ml

@@ -91,6 +91,7 @@ module Code = struct
     | Low_dimensional_argument_of_degeneracy : (string * 'a D.t) -> t
     | Missing_argument_of_degeneracy : string -> t
     | Applying_nonfunction_nontype : printable * printable -> t
+    | Unexpected_implicitness : [ `Implicit | `Explicit ] * string -> t
     | Unimplemented : string -> t
     | Matching_datatype_has_degeneracy : printable -> t
     | Wrong_number_of_arguments_to_pattern : Constr.t * int -> t
@@ -164,6 +165,7 @@ module Code = struct
     | Section_closed : string list -> t
     | No_such_section : t
     | Display_set : string * string -> t
+    | Option_set : string * string -> t
     | Break : t
     | Accumulated : t Asai.Diagnostic.t Bwd.t -> t
     | No_holes_allowed : string -> t
@@ -214,6 +216,7 @@ module Code = struct
     | Invalid_variable_face _ -> Error
     | Not_enough_arguments_to_instantiation -> Error
     | Applying_nonfunction_nontype _ -> Error
+    | Unexpected_implicitness _ -> Error
     | Wrong_number_of_arguments_to_constructor _ -> Error
     | Unimplemented _ -> Error
     | Matching_datatype_has_degeneracy _ -> Error
@@ -287,6 +290,7 @@ module Code = struct
     | Section_closed _ -> Info
     | No_such_section -> Error
     | Display_set _ -> Info
+    | Option_set _ -> Info
     | Break -> Error
     | Accumulated _ -> Error
     | No_holes_allowed _ -> Error
@@ -341,6 +345,7 @@ module Code = struct
     (* Function-types *)
     | Checking_lambda_at_nonfunction _ -> "E0700"
     | Applying_nonfunction_nontype _ -> "E0701"
+    | Unexpected_implicitness _ -> "E0702"
     (* Record fields *)
     | No_such_field _ -> "E0800"
     (* Tuples *)
@@ -436,7 +441,8 @@ module Code = struct
     | Commands_undone _ -> "I0006"
     | Section_opened _ -> "I0007"
     | Section_closed _ -> "I0008"
-    | Display_set _ -> "I0100"
+    | Option_set _ -> "I0100"
+    | Display_set _ -> "I0101"
     (* Control of execution *)
     | Quit _ -> "I0200"
     | Break -> "E0201"
@@ -579,6 +585,12 @@ module Code = struct
         textf
           "@[<hv 0>attempt to apply/instantiate@;<1 2>%a@ of type@;<1 2>%a@ which is not a function-type or universe@]"
           pp_printed (print tm) pp_printed (print ty)
+    | Unexpected_implicitness (i, str) ->
+        textf "unexpected %s argument: %s"
+          (match i with
+          | `Implicit -> "implicit"
+          | `Explicit -> "explicit")
+          str
     | Unimplemented str -> textf "%s not yet implemented" str
     | Matching_datatype_has_degeneracy ty ->
         textf "@[<hv 0>can't match on element of datatype@;<1 2>%a@ that has a degeneracy applied@]"
@@ -733,6 +745,7 @@ module Code = struct
     | Section_opened prefix -> textf "section %s opened" (String.concat "." prefix)
     | Section_closed prefix -> textf "section %s closed" (String.concat "." prefix)
     | Display_set (setting, str) -> textf "display set %s to %s" setting str
+    | Option_set (setting, str) -> textf "option set %s to %s" setting str
     | No_such_section -> text "no section here to end"
     | Break -> text "user interrupt"
     | No_holes_allowed cmd -> textf "command '%s' cannot contain holes" cmd

lib/dim/dim.ml

@@ -9,6 +9,7 @@ let is_pos : type n. n D.t -> bool = function
 
 module Endpoints = Endpoints
 include Arith
+include Singleton
 include Deg
 include Perm
 include Sface
@@ -32,19 +33,12 @@ let string_of_dim : type n. n D.t -> string = fun n -> string_of_deg (deg_zero n
 
 (* ********** Special generators ********** *)
 
-type one = D.one
-
-let one = D.one
 let refl : (one, D.zero) deg = Zero D.one
 
 type two = D.two
 
 let sym : (two, two) deg = Suc (Suc (Zero D.zero, Now), Later Now)
 
-type _ is_suc = Is_suc : 'n D.t * ('n, one, 'm) D.plus -> 'm is_suc
-
-let suc_pos : type n. n D.pos -> n is_suc = fun (Pos n) -> Is_suc (n, Suc Zero)
-
 let deg_of_name : string -> any_deg option =
  fun str ->
   if List.exists (fun s -> s = str) (Endpoints.refl_names ()) then Some (Any refl)

lib/dim/dim.mli

@@ -16,10 +16,17 @@ module Endpoints : sig
   val run :
     arity:int -> refl_char:char -> refl_names:string list -> internal:bool -> (unit -> 'a) -> 'a
 
+  val uniq : 'l1 len -> 'l2 len -> ('l1, 'l2) Eq.t
+  val len : 'l len -> 'l N.t
   val wrapped : unit -> wrapped
   val internal : unit -> bool
 end
 
+type _ is_singleton
+type _ is_suc = Is_suc : 'n D.t * ('n, 'one, 'm) D.plus * 'one is_singleton -> 'm is_suc
+
+val suc_pos : 'n D.pos -> 'n is_suc
+
 type any_dim = Any : 'n D.t -> any_dim
 
 val dim_of_string : string -> any_dim option
@@ -216,6 +223,7 @@ val tface_plus :
 type ('m, 'n) pface = ('m, D.zero, 'n, 'n) tface
 
 val pface_of_sface : ('m, 'n) sface -> [ `Proper of ('m, 'n) pface | `Id of ('m, 'n) Eq.t ]
+val pface_plus : ('k, 'm) pface -> ('m, 'n, 'mn) D.plus -> ('k, 'n, 'kn) D.plus -> ('kn, 'mn) pface
 
 val sface_plus_tface :
   ('k, 'm) sface ->
@@ -247,6 +255,15 @@ type (_, _, _) pface_of_plus =
 
 val pface_of_plus : ('m, 'n, 'k, 'nk) tface -> ('m, 'n, 'k) pface_of_plus
 
+val singleton_tface :
+  ('m, 'n, 'k, 'nk) tface -> 'k is_singleton -> 'l Endpoints.len -> ('m, 'n) sface * 'l N.index
+
+val is_codim1 : ('m, 'n, 'k, 'nk) tface -> unit option
+
+type (_, _, _) tface_of = Tface_of : ('m, 'n, 'k, 'nk) tface -> ('n, 'k, 'nk) tface_of
+
+val codim1_envelope : ('m, 'n, 'k, 'nk) tface -> ('n, 'k, 'nk) tface_of
+
 module Tube (F : Fam2) : sig
   module C : module type of Cube (F)
 
@@ -259,6 +276,21 @@ module Tube (F : Fam2) : sig
   val pboundary :
     ('m, 'k, 'mk) D.plus -> ('k, 'l, 'kl) D.plus -> ('m, 'kl, 'mkl, 'b) t -> ('mk, 'l, 'mkl, 'b) t
 
+  val of_cube_bwv :
+    'n D.t ->
+    'k is_singleton ->
+    ('n, 'k, 'nk) D.plus ->
+    'l Endpoints.len ->
+    (('n, 'b) C.t, 'l) Bwv.t ->
+    ('n, 'k, 'nk, 'b) t
+
+  val to_cube_bwv :
+    'k is_singleton ->
+    ('n, 'k, 'nk) D.plus ->
+    'l Endpoints.len ->
+    ('n, 'k, 'nk, 'b) t ->
+    (('n, 'b) C.t, 'l) Bwv.t
+
   val plus : ('m, 'k, 'mk, 'b) t -> ('m, 'k, 'mk) D.plus
   val inst : ('m, 'k, 'mk, 'b) t -> 'k D.t
   val uninst : ('m, 'k, 'mk, 'b) t -> 'm D.t
@@ -554,13 +586,6 @@ module Plusmap : sig
   end
 
 (*  *)
-type one
-
-val one : one D.t
-
-type _ is_suc = Is_suc : 'n D.t * ('n, one, 'm) D.plus -> 'm is_suc
-
-val suc_pos : 'n D.pos -> 'n is_suc
 val deg_of_name : string -> any_deg option
 val name_of_deg : ('a, 'b) deg -> string option
 

lib/dim/singleton.ml

@@ -0,0 +1,5 @@
+type one = D.one
+type _ is_singleton = One : one is_singleton
+type _ is_suc = Is_suc : 'n D.t * ('n, 'one, 'm) D.plus * 'one is_singleton -> 'm is_suc
+
+let suc_pos : type n. n D.pos -> n is_suc = fun (Pos n) -> Is_suc (n, Suc Zero, One)

lib/dim/tface.ml

@@ -1,4 +1,5 @@
 open Util
+open Singleton
 open Sface
 
 (* "Tube faces" are strict faces that are constrained to lie in a particular tube. *)
@@ -70,6 +71,10 @@ let rec pface_of_sface : type m n. (m, n) sface -> [ `Proper of (m, n) pface | `
       | `Proper fb -> `Proper (Mid fb)
       | `Id Eq -> `Id Eq)
 
+let pface_plus :
+    type m n mn k kn. (k, m) pface -> (m, n, mn) D.plus -> (k, n, kn) D.plus -> (kn, mn) pface =
+ fun d mn kn -> tface_plus d mn mn kn
+
 (* Any strict face can be added to a tube face on the left to get another tube face. *)
 
 let rec sface_plus_tface :
@@ -124,3 +129,31 @@ let pface_of_plus : type m n k nk. (m, n, k, nk) tface -> (m, n, k) pface_of_plu
   let (TFace_of_plus (pq, s, d)) = tface_of_plus Zero d in
   let Eq = D.plus_uniq (cod_plus_of_tface d) (D.zero_plus (codr_tface d)) in
   PFace_of_plus (pq, s, d)
+
+(* A tube face with exactly one instantiated dimension can be decomposed into an endpoint and a strict face. *)
+
+let singleton_tface :
+    type m n k nk l.
+    (m, n, k, nk) tface -> k is_singleton -> l Endpoints.len -> (m, n) sface * l N.index =
+ fun d k l ->
+  let One = k in
+  match d with
+  | End (s, n0, (l', i)) ->
+      let Zero = n0 in
+      let Eq = Endpoints.uniq l l' in
+      (s, i)
+
+(* A tface is codimension-1 if it has exactly one endpoint. *)
+
+let rec is_codim1 : type m n k nk. (m, n, k, nk) tface -> unit option = function
+  | End (fa, _, _) -> Option.map (fun _ -> ()) (is_id_sface fa)
+  | Mid s -> is_codim1 s
+
+type (_, _, _) tface_of = Tface_of : ('m, 'n, 'k, 'nk) tface -> ('n, 'k, 'nk) tface_of
+
+(* Every tface belongs to a unique codimension-1 tface. *)
+let rec codim1_envelope : type m n k nk. (m, n, k, nk) tface -> (n, k, nk) tface_of = function
+  | End (fa, nk, l) -> Tface_of (End (id_sface (cod_sface fa), nk, l))
+  | Mid s ->
+      let (Tface_of s1) = codim1_envelope s in
+      Tface_of (Mid s1)