Use record types for signature declarations (#249)

* Remove unused function `Support.List.for_each`

* Use record type for `Syn{ext,int}.Sgn.decl.Comp{Const,Dest}` and add documentation

* Use record type for `Syn{ext,int}.Sgn.decl.Comp{Typ,Cotyp}` and add documentation

* Use record type for `Syn{ext,int}.Sgn.decl.Query` and add documentation

* Fix some documentation references

* Use record type for `Syn{ext,int}.Sgn.decl.MRecTyp` and add documentation

* Implement `Support.Nonempty.destructure`

This allows for operations that act simultaneously on the head and tail of a non-empty list.

* Implement `Support.Nonempty.map2`

This is analogous to `Stdlib.List.map2`.

* Use `Nonempty.t` type for declarations in `MRecType`

The parser internally uses the `Nonempty.t` type for representing these mutually recursive LF type family declarations because at least one such declaration is required.
This also solves the non-exhaustive pattern-matching in `Prettyext.fmt_ppr_mrecs`.

* Use record type for `Syn{ext,int}.Sgn.decl.Val` and add documentation

* Use record type for `Syn{ext,int}.Sgn.decl.Module` and add documentation

* Use record type for `Syn{ext,int}.Sgn.decl.CompTypAbbrev` and add documentation

* Use record type for `Syn{ext,int}.Sgn.decl.Pragma` and add documentation

* Use record type for `Synext.Sgn.decl.GlobalPragma` and add documentation

* Remove unused constructor `Synint.decl.Proof`

* Add spacing and documentation

* Add changes lost in cherry-picking

* Use record labels in patterns

* Use `List.filter_map` instead of `Option.filter_map`

* Implement `List.split` tail-recursively

* implement `List.combine` tail-recursively

* Add missing documentation for raised exception `Invalid_argument` for `List.ap`

* Implement `Nonempty.singleton`

* Implement `Nonempty.filter_map`

* Implement `Nonempty.split`

* Implement `Nonempty.combine`

* Implement `Nonempty.partition`

* Implement `Nonempty.{ap,ap_one}`

* Use non-empty list type for theorem declarations

* Fix typo `"fucntion" -> "function"`

* Enforce in-order evalution of `f` in `Nonempty.map f l`

The evaluation order of tuple expressions is apparently unspecified.
`Nonempty.map f l` is being used with an effectful `f` that relies on its evaluation order on the list.

src/core/check.ml

@@ -169,7 +169,7 @@ module Comp = struct
          Id.print name
 
     | NotRecursiveDst name ->
-       fprintf ppf "A recursive call to nonrecursive fucntion %a is forbidden."
+       fprintf ppf "A recursive call to nonrecursive function %a is forbidden."
          Id.print name
 
     | IllegalParamTyp (cD, cPsi, tA) ->

src/core/check.mli

@@ -2,6 +2,7 @@
    @author Brigitte Pientka
    modified: Joshua Dunfield
 *)
+open Support
 
 module LF : sig
 
@@ -25,15 +26,15 @@ module LF : sig
       of mctx
          * dctx (* expected *)
          * dctx_hat (* found *)
-         * (Loc.t * mfront)
+         * (Location.t * mfront)
     | IllTypedMetaObj of mctx * clobj * dctx * cltyp
     | TermWhenVar of mctx * dctx * normal
     | SubWhenRen of mctx * dctx * sub
     | MissingType of string
 
-  exception Error of Loc.t * error
+  exception Error of Location.t * error
 
-  val throw : Loc.t -> error -> 'a
+  val throw : Location.t -> error -> 'a
 
   val check : mctx -> dctx -> nclo -> tclo -> unit
 
@@ -43,7 +44,7 @@ module LF : sig
   val checkDCtx : mctx -> dctx -> unit
 
   val checkSchemaWf : schema -> unit
-  val checkSchema : Loc.t -> mctx -> dctx -> Id.name -> schema -> unit
+  val checkSchema : Location.t -> mctx -> dctx -> Id.name -> schema -> unit
   val subsumes : mctx -> ctx_var -> ctx_var -> bool
 
   (** Checks that a type exists within a given schema.
@@ -54,12 +55,12 @@ module LF : sig
       The input name will be a part of the error message, and should
       be the declared name of the schema.
    *)
-  val checkTypeAgainstSchema: Syntax.Loc.t -> mctx -> dctx -> typ -> Id.name -> sch_elem list
+  val checkTypeAgainstSchema: Location.t -> mctx -> dctx -> typ -> Id.name -> sch_elem list
                               -> typ_rec * sub
   val instanceOfSchElem : mctx -> dctx -> tclo -> sch_elem -> (typ_rec * sub)
   val instanceOfSchElemProj : mctx -> dctx -> tclo -> (head * int) -> sch_elem -> (typ_rec * sub)
 
-  val checkMSub : Loc.t -> mctx -> msub -> mctx -> unit
+  val checkMSub : Location.t -> mctx -> msub -> mctx -> unit
 
 end
 
@@ -120,10 +121,10 @@ module Comp : sig
          * int (* premise index *)
          * suffices_typ (* given type annotation *)
 
-  exception Error of Loc.t * error
+  exception Error of Location.t * error
 
   (** Raises an error from this module. *)
-  val throw : Loc.t -> error -> 'a
+  val throw : Location.t -> error -> 'a
 
   (** Appends two sets of hypotheses.
       Appropriately MShifts the left contexts and applies an
@@ -153,7 +154,7 @@ module Comp : sig
       plicity and type information from the context on the left, but
       the entry name from the context on the right.
    *)
-  val validate_contexts : Loc.t -> LF.mctx * LF.mctx -> gctx * gctx -> LF.mctx * gctx
+  val validate_contexts : Location.t -> LF.mctx * LF.mctx -> gctx * gctx -> LF.mctx * gctx
 
   (** Checks a theorem in the given contexts against the given type.
       The given list of total declarations is used for totality checking.
@@ -249,7 +250,7 @@ module Comp : sig
       else, raises a synthesis mismatch error for the expression i
       saying that the type of i is expected to be a box-type.
    *)
-  val require_syn_typbox : LF.mctx -> gctx -> Loc.t -> exp_syn -> tclo -> meta_typ * LF.msub
+  val require_syn_typbox : LF.mctx -> gctx -> Location.t -> exp_syn -> tclo -> meta_typ * LF.msub
 
 
   (** Processes all leading PiBoxes to replace them with unification
@@ -296,7 +297,7 @@ module Comp : sig
 
       The provided location is used when raising errors.
    *)
-  val unify_suffices : Loc.t -> LF.mctx
+  val unify_suffices : Location.t -> LF.mctx
                        -> typ (* scrutinee type; to be decomposed *)
                        -> suffices_typ list (* type annotations *)
                        -> typ (* goal type; to match against
@@ -309,5 +310,5 @@ module Comp : sig
       the type (together with a delayed meta-substitution) of the
       produced expression.
    *)
-  val genMApp : Loc.t -> (LF.ctyp_decl -> bool) -> LF.mctx -> exp_syn * tclo -> int * (exp_syn * tclo)
+  val genMApp : Location.t -> (LF.ctyp_decl -> bool) -> LF.mctx -> exp_syn * tclo -> int * (exp_syn * tclo)
 end

src/core/command.ml

@@ -450,7 +450,11 @@ let printfun =
                ; thm_loc = Syntax.Loc.ghost
                }
              in
-             P.fmt_ppr_sgn_decl ppf (Synint.Sgn.Theorem [d])
+             P.fmt_ppr_sgn_decl ppf
+              (Synint.Sgn.Theorem
+                { location=Syntax.Loc.ghost
+                ; theorems=Nonempty.singleton d
+                })
           | _  -> fprintf ppf "- %s is not a function.;\n@?" arg
         with
         | Not_found ->
@@ -475,7 +479,7 @@ let query =
       begin fun ppf arglist ->
       try
         begin
-          let [Synext.Sgn.Query (_, name, extT, expected, tries)] =
+          let [Synext.Sgn.Query { name; typ=extT; expected_solutions=expected; maximum_tries=tries; _ }] =
             let expected = List.hd arglist in
             let tries = List.hd (List.tl arglist) in
             let str = String.concat " " (List.tl (List.tl arglist)) in

src/core/coverage.ml

@@ -1274,7 +1274,7 @@ let genObj (cD, cPsi, tP) (tH, tA, k) =
        end;
      Some (cD', (cPsi', tR', (tP', S.LF.id)), ms')
 
-let genAllObj cg = Option.filter_map (genObj cg)
+let genAllObj cg = List.filter_map (genObj cg)
 
 let genConst (cD, cPsi, (a, tS)) =
   Types.freeze a;
@@ -2520,7 +2520,7 @@ let genPatt names mk_pat_var (cD_p, tau_v) (c, tau_c) =
      raise e
 
 let genAllPatt names mk_pat_var ((cD_v, tau_v) : LF.mctx * Comp.typ) =
-  Option.filter_map
+  List.filter_map
     begin fun (c, tau_c) ->
     genPatt names mk_pat_var (cD_v, tau_v) (c, tau_c)
     end

src/core/holes.mli

@@ -1,3 +1,4 @@
+open Support
 open Syntax.Int
 
 (* Define two opaque types to be used as indices for `hole_info`. *)
@@ -20,7 +21,7 @@ type _ hole_info =
 
 (** A hole with a known kind of information. *)
 type 'a hole =
-  { loc : Syntax.Loc.t
+  { loc : Location.t
   ; name : HoleId.name
     (** "Context Delta", for metavariables. *)
   ; cD : LF.mctx
@@ -41,11 +42,11 @@ val string_of_lookup_strategy : lookup_strategy -> string
 type error =
   | InvalidHoleIdentifier of string
   | NoSuchHole of lookup_strategy
-  | NameShadowing of string * Loc.t
+  | NameShadowing of string * Location.t
   | UnsolvedHole of HoleId.name * HoleId.t
 
 (** An error that arises when lookup by a given strategy fails. *)
-exception Error of Loc.t * error
+exception Error of Location.t * error
 
 (** Parses a lookup strategy.
  * An integer gives the `by_id` strategy, whereas a non-integer gives
@@ -56,7 +57,7 @@ val parse_lookup_strategy : string -> lookup_strategy option
 (** Parses a lookup strategy, throwing an exception on failure.
     The given location is used in the thrown exception.
  *)
-val unsafe_parse_lookup_strategy : Loc.t -> string -> lookup_strategy
+val unsafe_parse_lookup_strategy : Location.t -> string -> lookup_strategy
 
 (** Looks up a hole by its number.
   * Use strategies with `get`. *)
@@ -111,13 +112,13 @@ val unsafe_get : lookup_strategy -> HoleId.t * some_hole
 val lookup : string -> (HoleId.t * some_hole) option
 
 (** Decides whether a location is contained within a location. *)
-val loc_within : Syntax.Loc.t -> Syntax.Loc.t -> bool
+val loc_within : Location.t -> Location.t -> bool
 
 (** Counts the number of holes. *)
 val count : unit -> int
 
 (** Removes all holes contained in the given location. *)
-val destroy_holes_within : Syntax.Loc.t -> unit
+val destroy_holes_within : Location.t -> unit
 
 (** Allocates a new hole ID. *)
 val allocate : unit -> HoleId.t
@@ -135,7 +136,7 @@ val clear : unit -> unit
 val list : unit -> (HoleId.t * some_hole) list
 
 (** Adds a Harpoon subgoal to the internal list. *)
-val add_harpoon_subgoal : Loc.t * Comp.open_subgoal -> unit
+val add_harpoon_subgoal : Location.t * Comp.open_subgoal -> unit
 
 (** Gets the list of Harpoon subgoals. *)
-val get_harpoon_subgoals : unit -> (Loc.t * Comp.open_subgoal) list
+val get_harpoon_subgoals : unit -> (Location.t * Comp.open_subgoal) list

src/core/id.ml

@@ -95,12 +95,12 @@ let gen_fresh_name (ns : name list) (n : name) : name =
     else y
   in
   let cnts =
-    let open Option in
-    filter_map
+    List.filter_map
       begin fun n' ->
-      String.equal n'.hint_name n.hint_name
-      |> of_bool
-      $> Fun.const n'.hint_cnt
+        let open Option in
+        String.equal n'.hint_name n.hint_name
+        |> of_bool
+        $> Fun.const n'.hint_cnt
       end
       ns
   in