fixes related to bounding of declarees in quantification and function definitions

src/backend/fingerprints.ml

@@ -405,6 +405,11 @@ let rec fp_expr counthyp countvar stack buf e =
         fp_expr counthyp countvar stack buf e
     | Bang _ ->
         Errors.bug ~at:e "Expr.Fingerprint: Bang"
+    | QuantTuply _
+    | ChooseTuply _
+    | SetStTuply _
+    | SetOfTuply _
+    | FcnTuply _ -> assert false
 
 
 and fp_sequent stack buf sq =
@@ -503,6 +508,8 @@ and fp_sequent stack buf sq =
               *)
               bprintf buf "$Fact(%a,%s)" (fp_expr counthyp countvar stack) e
                       (time_to_string tm)
+          | FreshTuply _ ->
+             assert false  (* unexpected case *)
   in
   spin stack sq.context
 

src/backend/isabelle.ml

@@ -459,6 +459,11 @@ and fmt_expr sd cx e = match e.core with
       Errors.bug ~at:e "Backend.Isabelle: @"
   | Parens (e, _) ->
       fmt_expr sd cx e
+  | QuantTuply _
+  | ChooseTuply _
+  | SetStTuply _
+  | SetOfTuply _
+  | FcnTuply _ -> assert false
 
 and extend_bound cx (v, kn, dom) =
   let (cx, v) = adj cx v in
@@ -537,6 +542,7 @@ and pp_print_sequent_outer cx ff sq = match Deque.front sq.context with
                *     failwith "Backend.Isabelle.pp_print_sequent"
                *)
         | Defn ({ core = Bpragma _ } , _, _, _) -> cx
+        | FreshTuply _ -> assert false  (* unexpected case *)
     end
 
 and pp_print_sequent_inner cx ff sq = match Deque.front sq.context with
@@ -575,6 +581,7 @@ and pp_print_sequent_inner cx ff sq = match Deque.front sq.context with
             let ncx = Ctx.bump cx in
             pp_print_sequent_inner ncx ff { sq with context = hs }
         | Defn (df, _, _, _) -> raise (Unsupported "Inner definition")
+        | FreshTuply _ -> assert false  (* unexpected case *)
     end
 
 type obx = obligation * string list * int * int

src/backend/ls4.ml

@@ -490,6 +490,8 @@ let visitor = object (self : 'self)
             fprintf ff  "%s" (if (not is_first) then " & " else "");
             self#expr scxp e;
             true
+        | FreshTuply _ ->
+            assert false  (* unexpected case *)
       in
       (ret, Expr.Visit.adj scxp h)
   method myhyps ((ff,scx) as scxp) hs had_first = match Deque.front hs with
@@ -519,6 +521,7 @@ let visitor = object (self : 'self)
               self#expr scxp { e with core = Opaque name.core }
           | Some({core=Defn ({core=Operator (name, _)}, _, _, _)}) ->
                 self#expr scxp (Opaque name.core @@ name)
+          | Some {core=FreshTuply _}
           | Some({core=Fact _}) -> assert false
                 (* super#expr *)
           | Some({core=Defn _}) -> assert false

src/backend/zenon.ml

@@ -437,6 +437,11 @@ and fmt_expr sd cx e =
         Errors.bug ~at:e "Backend.Zenon.fmt_exp: encountered @"
     | Parens (e, _) ->
         fmt_expr sd cx e
+    | QuantTuply _
+    | ChooseTuply _
+    | SetStTuply _
+    | SetOfTuply _
+    | FcnTuply _ -> assert false
 
 and pp_print_boundvar cx ff (v, _, _) = pp_print_string ff v
 
@@ -488,6 +493,9 @@ and pp_print_sequent cx ff sq =
   | Some ({core = Fact (_, Hidden, _)}, hs) ->
      let ncx = bump cx in
      pp_print_sequent ncx ff {sq with context = hs}
+  | Some ({core=FreshTuply _}, _) ->
+      assert false  (* unexpected case *)
+
 
 let pp_print_obligation ff ob =
   fprintf ff ";; obligation #%d@\n" (Option.get ob.id);

src/expr.mli

@@ -48,14 +48,22 @@ module T: sig
     | List of bullet * expr list
     | Let of defn list * expr
     | Quant of quantifier * bounds * expr
+    | QuantTuply of
+          quantifier * tuply_bounds * expr
     | Tquant of quantifier * hints * expr
     | Choose of hint * expr option * expr
+    | ChooseTuply of
+          hints * expr option * expr
     | SetSt of hint * expr * expr
+    | SetStTuply of
+          hints * expr * expr
     | SetOf of expr * bounds
+    | SetOfTuply of expr * tuply_bounds
     | SetEnum of expr list
     | Product of expr list
     | Tuple of expr list
     | Fcn of bounds * expr
+    | FcnTuply of tuply_bounds * expr
     | FcnApp of expr * expr list
     | Arrow of expr * expr
     | Rect of (string * expr) list
@@ -100,6 +108,13 @@ module T: sig
   and bounds = bound list
   and bound =
       hint * kind * bound_domain
+  (* tuply bounds *)
+  and tuply_bounds = tuply_bound list
+  and tuply_bound =
+      tuply_name * bound_domain
+  and tuply_name =
+    | Bound_name of hint
+    | Bound_names of hints
   and bound_domain =
     | No_domain
     | Domain of expr
@@ -154,6 +169,7 @@ module T: sig
   and hyp = hyp_ wrapped
   and hyp_ =
     | Fresh of hint * shape * kind * hdom
+    | FreshTuply of hints * hdom
     | Flex of hint
     | Defn of defn * wheredef * visibility * export
     | Fact of expr * visibility * time
@@ -169,7 +185,9 @@ module T: sig
   and time = Now | Always | NotSet
 
   val unditto: bounds -> bounds
+  val unditto_tuply: tuply_bounds -> tuply_bounds
 
+  val name_of_tuply: tuply_name -> hint
   val name_of_bound: bound -> hint
   val names_of_bounds: bounds -> hints
   val string_of_bound: bound -> string
@@ -233,6 +251,12 @@ module T: sig
           bounds -> expr -> expr
       val make_forall:
           bounds -> expr -> expr
+      val make_tuply_exists:
+          tuply_bounds -> expr ->
+          expr
+      val make_tuply_forall:
+          tuply_bounds -> expr ->
+          expr
       val make_temporal_exists:
           t list -> expr -> expr
       val make_temporal_forall:
@@ -241,10 +265,21 @@ module T: sig
           t -> expr -> expr
       val make_bounded_choose:
           t -> expr -> expr -> expr
+      val make_tuply_choose:
+          t list -> expr -> expr
+      val make_bounded_tuply_choose:
+          t list -> expr ->
+          expr -> expr
       val make_setst:
           t -> expr -> expr -> expr
+      val make_tuply_setst:
+          t list -> expr ->
+          expr -> expr
       val make_setof:
           expr -> bounds -> expr
+      val make_tuply_setof:
+          expr -> tuply_bounds ->
+          expr
       val make_setenum:
           expr list -> expr
       val make_product:
@@ -253,6 +288,9 @@ module T: sig
           expr list -> expr
       val make_fcn:
           bounds -> expr -> expr
+      val make_tuply_fcn:
+          tuply_bounds -> expr ->
+          expr
       val make_fcn_domain:
           expr -> expr
       val make_fcn_app:
@@ -310,12 +348,25 @@ module T: sig
       val make_bounded:
           t -> kind ->
           expr -> bound
+      val make_unbounded_name_decl:
+          t -> tuply_bound
+      val make_bounded_name_decl:
+          t -> expr -> tuply_bound
+      val make_tuply_decl:
+          t list -> tuply_bound
+      val make_bounded_tuply_decl:
+          t list -> expr ->
+          tuply_bound
       val make_fresh:
           t -> kind -> hyp
       val make_bounded_fresh:
           t -> expr -> hyp
       val make_fresh_with_arity:
           t -> kind -> int -> hyp
+      val make_tuply_fresh:
+          t list -> hyp
+      val make_bounded_tuply_fresh:
+          t list -> expr -> hyp
   end
 
 
@@ -571,6 +622,21 @@ module Visit: sig
     method hyp      : 's scx -> hyp -> 's scx
     method hyps     : 's scx -> hyp Deque.dq -> 's scx
   end
+  class virtual ['s] map_concrete: object
+      inherit ['s] map
+      method tuply_bounds:
+          's scx -> tuply_bounds ->
+          's scx * tuply_bounds
+      method tuply_bound:
+          's scx -> tuply_bound -> tuply_bound
+  end
+  class virtual ['s] iter_concrete: object
+      inherit ['s] iter
+      method tuply_bounds:
+          's scx -> tuply_bounds -> 's scx
+      method tuply_bound:
+          's scx -> tuply_bound -> unit
+  end
   class virtual ['s] map_visible_hyp : ['s] map
   class virtual ['s] iter_visible_hyp : ['s] iter
 

src/expr/e_action.ml

@@ -371,6 +371,7 @@ class auto_expansion_of_defs =
                     begin
                     assert (e_level <= 2);
                     match hyp.core with
+                        | FreshTuply _
                         | Fact _ -> assert false
                         | Flex _  -> assert (e.core = Ix n); e
                         | Fresh (op_name, shape, kind, _) ->

src/expr/e_anon.ml

@@ -27,6 +27,8 @@ let hyp_is_named what h = match h.core with
             _, _, _) ->
         nm.core = what
     | Fact (_, _, _) -> false
+    | FreshTuply _ -> assert false  (* unexpected
+        case *)
 
 
 let anon_apply index op args =
@@ -221,8 +223,9 @@ class anon_sg = object (self: 'self)
                         let index = depth + 1 in
                         let op = e $$ decl in
                         Ix index @@ op
-                    (* fact: unexpected *)
-                    | Some (_, {core=Fact _}) -> assert false
+                    (* unexpected cases *)
+                    | Some (_, {core=Fact _ | FreshTuply _}) ->
+                        assert false
                     | None ->
                          (* TODO? allow builtin operators here ?
                          possibly passing a context with builtin operators

src/expr/e_constness.ml

@@ -54,6 +54,12 @@ class virtual const_visitor = object (self : 'self)
             end
         in
         assign e isconst (sq_const sq.context)
+    | QuantTuply _
+    | ChooseTuply _
+    | SetStTuply _
+    | SetOfTuply _
+    | FcnTuply _ ->
+        assert false
     | _ ->
         let e = super#expr scx e in
         let cx = snd scx in
@@ -178,6 +184,12 @@ class virtual const_visitor = object (self : 'self)
                   | None -> true
                   | Some e -> is_const e
               end
+          | QuantTuply _
+          | ChooseTuply _
+          | SetStTuply _
+          | SetOfTuply _
+          | FcnTuply _ ->
+              assert false  (* not implemented *)
         in
         assign e isconst const
 

src/expr/e_fmt.ml

@@ -349,6 +349,11 @@ let rec fmt_expr ?(temp=false) cx ew = match ew.core with
       fmt_expr ~temp:temp cx (Parens (e, Nlabel (l, xs) @@ e) @@ e)
   | Parens (e, {core = Syntax}) ->
       fmt_expr ~temp:temp cx e
+  | QuantTuply _
+  | ChooseTuply _
+  | SetStTuply _
+  | SetOfTuply _
+  | FcnTuply _ -> assert false
 
 and pp_print_bang ff () =
   if Params.debugging "garish" then
@@ -642,6 +647,8 @@ and pp_print_sequent  ?(temp=false) cx ff sq = match Deque.null sq.context with
                   fst (adj cx nm)
               | Fact (_, _,_) ->
                   bump cx
+              | FreshTuply _ ->
+                  assert false  (* not implemented *)
             in (cx, ch :: chs)
         end (cx, []) sq.context in
       let chs = List.filter (fun (cx, h) -> not (elide h)) (List.rev chs) in
@@ -679,6 +686,7 @@ and pp_print_hyp ?(temp=false) cx ff h =
            | Bounded (_, Hidden) -> ()
            | Bounded (b, _) -> fprintf ff " \\in %a" (pp_print_expr ~temp:temp cx) b) ;
         ncx
+    | FreshTuply _ -> assert false  (* not implemented *)
     | Flex nm ->
         let (ncx, nm) = adj cx nm in
         fprintf ff "NEW VARIABLE %s" nm ;

src/expr/e_level_comparison.ml

@@ -484,6 +484,13 @@ class level_comparison = object (self : 'self)
             && j = l
         | At b,
           At c -> b = c
+        | (QuantTuply _ | ChooseTuply _ |
+           SetStTuply _ | SetOfTuply _ |
+           FcnTuply _), _
+        | _, (QuantTuply _ | ChooseTuply _ |
+              SetStTuply _ | SetOfTuply _ |
+              FcnTuply _) ->
+            assert false
         | _, _ -> false
 
     method exprs cx1 cx2 es fs = match es, fs with

src/expr/e_levels.ml

@@ -262,6 +262,8 @@ class virtual ['s] level_computation = object (self : 'self)
                     let hyp_scx = E_t.scx_front scx n in
                     let (_, e_) = self#hyp hyp_scx hyp in
                     get_level_info e_
+                | FreshTuply _ ->
+                    assert false  (* not implemented *)
                 | Fact (e_, _, _) ->
                     (*
                     E_t.print_cx cx;
@@ -908,6 +910,12 @@ class virtual ['s] level_computation = object (self : 'self)
             let new_parens = Parens (e_, pf_) in
             let new_e = new_parens @@ e in
             assign new_e exprlevel e_level_info
+        | QuantTuply _
+        | ChooseTuply _
+        | SetStTuply _
+        | SetOfTuply _
+        | FcnTuply _ ->
+            assert false  (* not implemented *)
         in
         e_
         end
@@ -986,6 +994,8 @@ class virtual ['s] level_computation = object (self : 'self)
                 let level_args = StringSet.singleton name.core in
                 LevelInfo (level, weights, level_args)
                 end
+            | FreshTuply _ ->
+                assert false  (* not implemented *)
             (* defined operator of any arity *)
             | Defn (df, _, _, _) ->
                 let df_ = self#defn scx df in
@@ -1013,6 +1023,8 @@ class virtual ['s] level_computation = object (self : 'self)
                 in
                 let h = Fresh (nm, shp, lc, dom) @@ h in
                 (adj scx h, h)
+            | FreshTuply _ ->
+                assert false  (* not implemented *)
             | Flex s ->
                 let h = Flex s @@ h in
                 (adj scx h, h)