REF: factor out common code, thus improving interfaces

and reducing code duplication. The common code was
operating on the syntax tree, and has been added as
new functions to the modules `Expr.T` and `Expr.Visit`.

API: This commit adds functions for creating syntax-tree nodes,
to the module `Expr.T`. These functions reduce the repetition
of code (for example, code used to wrap nodes
as `'a Property.wrapped`).

The new functions also define an interface for node creation
that is less dependent on the exact representation of the
syntax tree. Thus, code that uses the new functions is
more independent of changes to the syntax tree.

These changes are motivated by and in anticipation of
an upcoming change to the types of syntax tree nodes.

DEV: This commit changes the order of OCaml modules in
the `EXPR_PACK` inside `src/Makefile`.
The reason for this change is that the newly-added
function `E_visit.hyps_of_bounds_unditto`
calls the functions `E_subst.app_expr` and
`E_subst.shift`.

So the module `expr/e_subst` has to appear before
`expr/e_visit`. `expr/e_subst` depends on `expr/e_fmt`,
so `expr/e_fmt` has to appear before `expr/e_subst`.
`expr/e_levels` depends on `expr/e_visit`,
so `expr/e_visit` has to appear before `expr/e_levels`.
The other modules appear in the same order as earlier.

- REF: write subclass signatures in a way that the super
  signature does not need to be repeated

src/Makefile

@@ -63,12 +63,12 @@ PARS_PACK = \
 
 EXPR_PACK = \
   expr/e_t \
-  expr/e_visit \
   expr/e_fmt \
+  expr/e_subst \
+  expr/e_visit \
   expr/e_levels \
   expr/e_constness \
   expr/e_substitutive \
-  expr/e_subst \
   expr/e_eq \
   expr/e_deref \
   expr/e_leibniz \

src/backend/fingerprints.ml

@@ -291,7 +291,7 @@ let rec fp_expr counthyp countvar stack buf e =
         fp_let counthyp countvar stack buf ds e
     | Quant (q, bs, e) ->
         let n = List.length bs in
-        let l = List.map (fun (a,_,_) -> a.core) bs in
+        let l = strings_of_bounds bs in
         (*let bounds = (fp_bounds count stack) bs in*)
          let bu = Buffer.create 17 in
            pushlvars stack l;
@@ -345,7 +345,7 @@ let rec fp_expr counthyp countvar stack buf e =
            (Buffer.contents bu)
     | SetOf (e, bs) ->
         let n = List.length bs in
-        let l = List.map (fun (a,_,_) -> a.core) bs in
+        let l = strings_of_bounds bs in
         (*let vars = String.concat "." l in*)
          let bu = Buffer.create 17 in
            pushlvars stack l;
@@ -361,7 +361,7 @@ let rec fp_expr counthyp countvar stack buf e =
         bprintf buf "$Prod(%a)" (list fps) es
     | Fcn (bs, e) ->
         let n = List.length bs in
-        let l = List.map (fun (a,_,_) -> a.core) bs in
+        let l = strings_of_bounds bs in
          let bu = Buffer.create 17 in
            pushlvars stack l;
            bprintf bu "%a" (fp_expr counthyp countvar stack) e;

src/backend/isabelle.ml

@@ -30,7 +30,7 @@ let cook x = "is" ^ pickle x
 
 let adj cx v =
   let cx = Ctx.push cx (pickle v.core) in
-  (cx, Ctx.string_of_ident (fst (Ctx.top cx)))
+  (cx, Ctx.string_of_ident (Ctx.front cx))
 
 let rec adjs cx = function
   | [] -> (cx, [])

src/backend/isabelle.mli

@@ -14,6 +14,9 @@ val adjs:
 val cook: string -> string
 val lookup_id: ctx -> int -> string
 val crypthash: ctx -> Expr.T.expr -> string
+val extend_bound:
+    ctx -> Expr.T.bound ->
+    ctx * (string * Expr.T.kind * Expr.T.bound_domain)
 
 (* backend/prep.ml *)
 val thy_temp:

src/backend/smt.ml

@@ -199,7 +199,7 @@ and fmt_expr (ecx:Ectx.t) e =
             when q = q' ->
         fmt_expr ecx (Quant (q, bs @ bs', ex) @@ e)
     | Quant (q, bs, ex) ->
-        (** Assumption: [ex] is [Smt.unditto]'ed and
+        (** Assumption: [ex] is [Expr.T.unditto]'ed and
         [bs] has [No_domain]s.
         *)
         let ecx, vss, _ = Ectx.adj_bs ecx bs in
@@ -446,10 +446,8 @@ let collect_data scx (hs, c) =
                         self#expr scx d
                     | _ -> ()
                 end bs ;
-            let hs = List.map begin
-                fun (v, k, _) -> Fresh (v, Shape_op 0, k, Unbounded) @@ v
-                    (** Hack to recognize bounded variables by [Shape_op 0] *)
-                end bs in
+            (* Hack to recognize bounded variables by [Shape_op 0] *)
+            let hs = Expr.Visit.hyps_of_bounds_as_arity_0 bs in
             Expr.Visit.adjs scx hs
     end in
     List.iter (visitor#expr scx) hs;

src/backend/zenon.ml

@@ -26,6 +26,9 @@ include (Isabelle : sig
            val cook : string -> string
            val lookup_id : ctx -> int -> string
            val crypthash : ctx -> expr -> string
+           val extend_bound:
+              ctx -> bound ->
+              ctx * (string * Expr.T.kind * Expr.T.bound_domain)
          end)
 
 exception Unsupported of string
@@ -435,10 +438,6 @@ and fmt_expr sd cx e =
     | Parens (e, _) ->
         fmt_expr sd cx e
 
-and extend_bound cx (v, kn, ran) =
-  let (cx, v) = adj cx v in
-    (cx, (v, kn, ran))
-
 and pp_print_boundvar cx ff (v, _, _) = pp_print_string ff v
 
 and pp_print_boundset sd cx ff b = match b.core with

src/expr.mli

@@ -168,7 +168,170 @@ module T: sig
 
   and time = Now | Always | NotSet
 
+  val unditto: bounds -> bounds
+
+  val name_of_bound: bound -> hint
+  val names_of_bounds: bounds -> hints
+  val string_of_bound: bound -> string
+  val strings_of_bounds:
+      bounds -> string list
+  val bounds_of_variables:
+      hints -> bounds
+  val bounds_of_parameters:
+      (hint * shape) list -> bounds
+
+
+  module type Node_factory_sig =
+  sig
+      type t
+
+      (* construction of
+      syntax-tree nodes *)
+      val make_ix:
+          int -> expr
+      val make_opaque:
+          t -> expr
+      val make_internal:
+          Builtin.builtin -> expr
+      val make_arg:
+          t -> (hint * shape)
+      val make_lambda:
+          t list -> expr -> expr
+      val make_def:
+          t -> expr -> defn
+      val make_def_with_args:
+          t -> t list ->
+          expr -> defn
+      val make_recursive_def:
+          t -> shape -> defn
+      val make_sequent:
+          ctx -> expr -> expr
+      val make_bang:
+          expr -> sel list ->
+          expr
+      val make_apply:
+          expr -> expr list ->
+          expr
+      val make_with:
+          expr -> Method.t -> expr
+      val make_if:
+          expr -> expr ->
+          expr -> expr
+      val make_junction:
+          bullet -> expr list ->
+          expr
+      val make_disjunction:
+          expr list -> expr
+      val make_conjunction:
+          expr list -> expr
+      val make_let:
+          defn list -> expr -> expr
+      val make_quantifier:
+          quantifier -> bounds ->
+          expr -> expr
+      val make_exists:
+          bounds -> expr -> expr
+      val make_forall:
+          bounds -> expr -> expr
+      val make_temporal_exists:
+          t list -> expr -> expr
+      val make_temporal_forall:
+          t list -> expr -> expr
+      val make_choose:
+          t -> expr -> expr
+      val make_bounded_choose:
+          t -> expr -> expr -> expr
+      val make_setst:
+          t -> expr -> expr -> expr
+      val make_setof:
+          expr -> bounds -> expr
+      val make_setenum:
+          expr list -> expr
+      val make_product:
+          expr list -> expr
+      val make_tuple:
+          expr list -> expr
+      val make_fcn:
+          bounds -> expr -> expr
+      val make_fcn_domain:
+          expr -> expr
+      val make_fcn_app:
+          expr -> expr -> expr
+      val make_fcn_app_commas:
+          expr -> expr list ->
+          expr
+      val make_fcn_set:
+          expr -> expr -> expr
+      val make_record_set:
+          (t * expr) list -> expr
+      val make_record:
+          (t * expr) list -> expr
+      val make_except:
+          expr -> exspec list ->
+          expr
+      val make_dot:
+          expr -> t -> expr
+      val make_square_action:
+          expr -> expr -> expr
+      val make_angle_action:
+          expr -> expr -> expr
+      val make_subscripted_always:
+          expr -> expr -> expr
+      val make_subscripted_eventually:
+          expr -> expr -> expr
+      val make_weak_fairness:
+          expr -> expr -> expr
+      val make_strong_fairness:
+          expr -> expr -> expr
+      val make_case:
+          (expr * expr) list ->
+          expr option -> expr
+      val make_string:
+          t -> expr
+      val make_number:
+          t -> t -> expr
+      val make_at: bool -> expr
+      val make_parens:
+          expr -> pform -> expr
+      val make_const_decl:
+          t -> bound
+      val make_const_decls:
+          t list -> bounds
+      val make_bounded_const_decl:
+          t -> expr -> bound
+      val make_bounded_const_decls:
+          (t * expr) list -> bounds
+      val make_param_decl:
+          t -> bound
+      val make_param_decls:
+          t list -> bounds
+      val make_unbounded:
+          t -> kind -> bound
+      val make_bounded:
+          t -> kind ->
+          expr -> bound
+      val make_fresh:
+          t -> kind -> hyp
+      val make_bounded_fresh:
+          t -> expr -> hyp
+      val make_fresh_with_arity:
+          t -> kind -> int -> hyp
+  end
+
+
+  module From_string:
+      Node_factory_sig with
+      type t = string
+
+
+  module From_hint:
+      Node_factory_sig with
+      type t = hint
+
+
   val get_val_from_id: 'hyp Deque.dq -> int -> 'hyp
+  val name_of_ix:
+      int -> ctx -> hint
   val hyp_name: hyp -> string
 
   val print_cx: ctx -> unit
@@ -363,9 +526,21 @@ end
 
 module Visit: sig
   open T
+  val hyp_of_bound_full: bound -> hyp
+  val hyps_of_bounds: bounds -> hyp list
+  val hyps_of_bounds_full: bounds -> hyp list
+  val hyps_of_bounds_unditto: bounds -> hyp list
+  val hyps_of_bounds_as_arity_0: bounds -> hyp list
+  val map_bound_domains:
+      (expr -> expr) -> bounds -> bounds
+  val map_bounds:
+      (Util.hint -> Util.hint) -> (expr -> expr) -> bounds -> bounds
+  val rename_bound: bound -> Util.hint -> bound
+  val rename_bounds: bounds -> Util.hints -> bounds
   type 's scx = 's * hyp Deque.dq
   val adj  : 's scx -> hyp -> 's scx
   val adjs : 's scx -> hyp list -> 's scx
+  val adj_unboundeds_unchecked: 's scx -> bounds -> 's scx
   class virtual ['s] map : object
     method expr     : 's scx -> expr -> expr
     method pform    : 's scx -> pform -> pform
@@ -400,20 +575,7 @@ module Visit: sig
   class virtual ['s] iter_visible_hyp : ['s] iter
 
   class virtual ['s] map_rename : object
-    method expr     : 's scx -> expr -> expr
-    method pform    : 's scx -> pform -> pform
-    method sel      : 's scx -> sel -> sel
-    method sequent  : 's scx -> sequent -> 's scx * sequent
-    method defn     : 's scx -> defn -> defn
-    method defns    : 's scx -> defn list -> 's scx * defn list
-    method bounds   : 's scx -> bound list -> 's scx * bound list
-    method bound    : 's scx -> bound -> 's scx * bound
-    method exspec   : 's scx -> exspec -> exspec
-    method instance : 's scx -> instance -> instance
-    method hyp      : 's scx -> hyp -> 's scx * hyp
-    method hyps     : 's scx -> hyp Deque.dq -> 's scx * hyp Deque.dq
-    method adj      : 's scx -> hyp -> 's scx
-    method adjs     : 's scx -> hyp list -> 's scx
+      inherit ['s] map
       method rename : ctx -> hyp -> Util.hint -> hyp * Util.hint
       method renames : ctx -> hyp list -> Util.hints -> hyp list * Util.hints
   end
@@ -442,53 +604,7 @@ module Leibniz: sig
             bool
 
     class virtual leibniz_visitor:
-        object
-        inherit [unit] Visit.map
-        method expr:
-            unit Visit.scx -> expr ->
-                expr
-        method pform:
-            unit Visit.scx -> pform ->
-                pform
-        method sel:
-            unit Visit.scx -> sel ->
-                sel
-        method sequent:
-            unit Visit.scx ->
-            sequent ->
-                unit Visit.scx * sequent
-        method defn:
-            unit Visit.scx -> defn ->
-                defn
-        method defns:
-            unit Visit.scx ->
-            defn list ->
-                unit Visit.scx * defn list
-        method bounds:
-            unit Visit.scx ->
-            bound list ->
-                unit Visit.scx * bound list
-        method bound:
-            unit Visit.scx ->
-            bound ->
-                unit Visit.scx * bound
-        method exspec:
-            unit Visit.scx ->
-            exspec ->
-                exspec
-        method instance:
-            unit Visit.scx ->
-            instance ->
-                instance
-        method hyp:
-            unit Visit.scx ->
-            hyp ->
-                unit Visit.scx * hyp
-        method hyps:
-            unit Visit.scx ->
-            hyp Deque.dq ->
-                unit Visit.scx * hyp Deque.dq
-    end
+        [unit] Visit.map
 end