ENH: parse and expand bound tuples

lsp/lib/docs/proof_step.ml

@@ -272,6 +272,11 @@ and of_step (step : Tlapm_lib.Proof.T.step) acc : t option * Acc.t =
         (of_proof
            (Range.of_wrapped_must step)
            (Range.of_wrapped expr) proof acc)
+  | Proof.T.PickTuply (_, expr, proof) ->
+      Acc.some
+        (of_proof
+           (Range.of_wrapped_must step)
+           (Range.of_wrapped expr) proof acc)
   | Proof.T.Use (_, _) -> (None, acc)
   | Proof.T.Have expr ->
       let suppl_locs = List.filter_map Range.of_wrapped [ expr ] in
@@ -283,6 +288,18 @@ and of_step (step : Tlapm_lib.Proof.T.step) acc : t option * Acc.t =
       in
       Acc.some
         (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
+  | Proof.T.TakeTuply tuply_bounds ->
+      let suppl_locs =
+        List.concat (List.map (fun (tuply_name, _) ->
+          begin match tuply_name with
+          | Expr.T.Bound_name hint ->
+            List.filter_map Range.of_wrapped [ hint ]
+          | Expr.T.Bound_names hints ->
+            List.filter_map Range.of_wrapped hints
+          end) tuply_bounds)
+      in
+      Acc.some
+        (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
   | Proof.T.Witness exprs ->
       let suppl_locs = List.filter_map Range.of_wrapped exprs in
       Acc.some

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
@@ -539,6 +544,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
@@ -577,6 +583,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/smtlib.ml

@@ -650,6 +650,8 @@ let pp_print_obligation ?(solver="SMT") ff ob =
           fprintf ff "; omitted declaration of '%s' (missing type)@." nm.core;
           pp_print_newline ff ();
           spin ncx hs
+    | Some ({core=FreshTuply (_, _); _ }, _) ->
+        failwith "unexpected case"
   in
 
   pp_print_newline ff ();
@@ -670,4 +672,3 @@ let pp_print_obligation ?(solver="SMT") ff ob =
 
   fprintf ff "(check-sat)@.";
   fprintf ff "(exit)@."
-

src/backend/thf.ml

@@ -564,6 +564,8 @@ let pp_print_obligation ?(solver="Zipper") ff ob =
         pp_print_thf cx ff ("defn_" ^ nm) Type (Opr v);
         pp_print_newline ff ();
         spin ncx hs
+    | Some ({core=FreshTuply (_, _); _ }, _) ->
+        failwith "unexpected case"
   in
 
   let cx =
@@ -580,4 +582,3 @@ let pp_print_obligation ?(solver="Zipper") ff ob =
   fprintf ff "%%---- Goal@.";
   pp_print_thf cx ff "goal" Conjecture (Form sq.active);
   pp_print_newline ff ();
-

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.ml

@@ -3,10 +3,12 @@
 Copyright (C) 2011-2019  INRIA and Microsoft Corporation
 *)
 module T = E_t
+module Namespaces = E_namespaces
 module Fmt = E_fmt
 module Subst = E_subst
 module Visit = E_visit
 module Collect = E_collect
+module Tuply_declarations = E_tuply_declarations
 module Eq = E_eq
 module Deref = E_deref
 module Leibniz = E_leibniz

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
@@ -254,6 +272,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:
@@ -262,10 +286,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:
@@ -274,6 +309,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:
@@ -331,12 +369,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
 
 
@@ -373,6 +424,20 @@ module T: sig
 end
 
 
+module Namespaces: sig
+    open Util
+
+
+    val mint_from_hint:
+        hint -> hint
+    val mint_by_min_free:
+        string -> int -> string list ->
+            string
+    val mint_by_count:
+        string -> int -> int * string
+end
+
+
 module Fmt: sig
     open T
     open Ctx
@@ -599,6 +664,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, 'a] foldmap : object
     method expr     : 's scx -> 'a -> expr -> 'a * expr
     method pform    : 's scx -> 'a -> pform -> 'a * pform
@@ -636,6 +716,8 @@ module Visit: sig
       method rename : ctx -> hyp -> Util.hint -> hyp * Util.hint
       method renames : ctx -> hyp list -> Util.hints -> hyp list * Util.hints
   end
+
+  val name_operators: ctx -> expr -> expr
 end
 
 
@@ -659,6 +741,15 @@ module Collect : sig
 end
 
 
+module Tuply_declarations: sig
+    open T
+    val expand_tuply_declarations:
+        expr -> expr
+    val tuplify_functions:
+        expr -> expr
+end
+
+
 module Eq: sig
     open T
     val expr:
@@ -671,7 +762,12 @@ end
 
 
 module Deref: sig
-    val badexp: T.expr
+    open T
+    val resolve_bang:
+        hyp Deque.dq -> expr ->
+        expr list -> sel list -> expr
+    val badexp: expr
+    val is_badexp: expr -> bool
 end
 
 
@@ -743,6 +839,17 @@ end
 module Parser: sig
     open Tla_parser
     open T
+    type boundeds
+    val has_tuply_bounded:
+        boundeds -> bool
+    val tuply_bounds_of_boundeds:
+        boundeds -> tuply_bounds
+    val bounds_of_boundeds:
+        boundeds -> bounds
+    val quantifier_boundeds:
+        bool -> (pcx, boundeds) P.prs
+    val colon_expr:
+        bool -> (pcx, expr) P.prs
     val expr: bool -> T.expr lprs
     val bounds: bool -> T.bound list lprs
     val defn: bool -> T.defn lprs

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, _) ->