From 2a81986e024706c6af2ea89dc57b7020d97fa8d6 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sun, 18 Jul 2021 01:09:20 +0200 Subject: [PATCH 1/4] API: change syntax tree to represent also tuply declarations and update the code throughout `tlapm`, because this commit changes the existing types in the module `Expr.T`. --- src/backend/fingerprints.ml | 7 + src/backend/isabelle.ml | 7 + src/backend/ls4.ml | 3 + src/backend/zenon.ml | 8 + src/expr.mli | 66 +++++++ src/expr/e_action.ml | 1 + src/expr/e_anon.ml | 7 +- src/expr/e_constness.ml | 12 ++ src/expr/e_fmt.ml | 8 + src/expr/e_level_comparison.ml | 7 + src/expr/e_levels.ml | 12 ++ src/expr/e_subst.ml | 13 ++ src/expr/e_t.ml | 311 +++++++++++++++++++++++++++++++++ src/expr/e_t.mli | 54 ++++++ src/expr/e_visit.ml | 200 +++++++++++++++++++++ src/expr/e_visit.mli | 17 ++ src/frontend/coalesce.ml | 7 +- src/proof.mli | 2 + src/proof/p_fmt.ml | 3 + src/proof/p_gen.ml | 3 + src/proof/p_simplify.ml | 9 + src/proof/p_subst.ml | 3 + src/proof/p_t.ml | 2 + src/proof/p_t.mli | 2 + src/proof/p_visit.ml | 94 ++++++++++ src/proof/p_visit.mli | 10 ++ src/smt/ectx.ml | 2 + src/smt/smtcommons.ml | 8 + src/typesystem/typ_e.ml | 11 ++ 29 files changed, 885 insertions(+), 4 deletions(-) diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index 90d9fd0e..053144d5 100644 --- a/src/backend/fingerprints.ml +++ b/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 diff --git a/src/backend/isabelle.ml b/src/backend/isabelle.ml index c9504d7d..dee692d5 100644 --- a/src/backend/isabelle.ml +++ b/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 diff --git a/src/backend/ls4.ml b/src/backend/ls4.ml index 04423cfd..8d581bf8 100644 --- a/src/backend/ls4.ml +++ b/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 diff --git a/src/backend/zenon.ml b/src/backend/zenon.ml index 3bde495d..db78b969 100644 --- a/src/backend/zenon.ml +++ b/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); diff --git a/src/expr.mli b/src/expr.mli index 0c5809ec..3058c559 100644 --- a/src/expr.mli +++ b/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 diff --git a/src/expr/e_action.ml b/src/expr/e_action.ml index 408b0192..7e1f5968 100644 --- a/src/expr/e_action.ml +++ b/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, _) -> diff --git a/src/expr/e_anon.ml b/src/expr/e_anon.ml index 386b22e1..046a1fe5 100644 --- a/src/expr/e_anon.ml +++ b/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 diff --git a/src/expr/e_constness.ml b/src/expr/e_constness.ml index 76f010d0..c15d76ed 100644 --- a/src/expr/e_constness.ml +++ b/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 diff --git a/src/expr/e_fmt.ml b/src/expr/e_fmt.ml index 69da2e6f..f86704be 100644 --- a/src/expr/e_fmt.ml +++ b/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 ; diff --git a/src/expr/e_level_comparison.ml b/src/expr/e_level_comparison.ml index 49d4538d..f3df4bc0 100644 --- a/src/expr/e_level_comparison.ml +++ b/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 diff --git a/src/expr/e_levels.ml b/src/expr/e_levels.ml index 5109416c..afb0b5ca 100644 --- a/src/expr/e_levels.ml +++ b/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) diff --git a/src/expr/e_subst.ml b/src/expr/e_subst.ml index 66b5b307..b33c28ff 100644 --- a/src/expr/e_subst.ml +++ b/src/expr/e_subst.ml @@ -93,6 +93,11 @@ let rec app_expr s oe = match oe.core with Case (List.map (fun (e, f) -> (app_expr s e, app_expr s f)) arms, Option.map (app_expr s) oth) @@ oe | Parens (e, rig) -> Parens (app_expr s e, rig) @@ oe + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> assert false and app_exprs s es = List.map (fun e -> app_expr s e) es @@ -196,6 +201,7 @@ and app_hyps s cs = match Deque.front cs with and app_hyp s h = match h.core with | Fresh (x, shp, lv, b) -> Fresh (x, shp, lv, app_dom s b) @@ h + | FreshTuply _ -> assert false (* not implemented *) | Flex v -> Flex v @@ h | Defn (d, wd, us, ex) -> Defn (app_defn s d, wd, us, ex) @@ h | Fact (e, us,tm) -> Fact (app_expr s e, us,tm) @@ h @@ -346,6 +352,11 @@ class map = object (self : 'self) At b @@ oe | Parens (e, pf) -> Parens (self#expr s e, self#pform s pf) @@ oe + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> assert false (* not implemented *) method exprs s es = List.map (self#expr s) es @@ -421,6 +432,7 @@ class map = object (self : 'self) | Bounded (r, rvis) -> Bounded (self#expr s r, rvis) in Fresh (nm, shp, lc, dom) @@ h + | FreshTuply _ -> assert false (* not implemented *) | Flex v -> Flex v @@ h | Defn (df, wd, vis, ex) -> let (s, df) = self#defn s df in @@ -472,6 +484,7 @@ class map_visible_hyp = object (self: 'self) method hyp s h = begin match h.core with | Fresh _ | Flex _ -> super#hyp s h + | FreshTuply _ -> assert false (* not implemented *) | Defn (_, _, Hidden, _) | Fact (_, Hidden, _) -> (bump s, h) | Defn _ | Fact _ -> super#hyp s h diff --git a/src/expr/e_t.ml b/src/expr/e_t.ml index 620f3433..c9967217 100644 --- a/src/expr/e_t.ml +++ b/src/expr/e_t.ml @@ -73,6 +73,7 @@ and expr_ = | Let of defn list * expr (* rigid quantification `\E` or `\A` *) | Quant of quantifier * bounds * expr + | QuantTuply of quantifier * tuply_bounds * expr (* temporal quantification `\EE` or `\AA` *) | Tquant of quantifier * hints * expr (* Two cases (unbounded and bounded `CHOOSE`): @@ -90,6 +91,32 @@ and expr_ = ``` *) | Choose of hint * expr option * expr + (* Two cases (unbounded and bounded `CHOOSE` + with tuple declaration): + + - `CHOOSE <>: pred`, for example: + ```ocaml + let x = noprops "x" in + let y = noprops "y" in + let names = [x; y] in + Choose (names, None, pred) + ``` + + - `CHOOSE <> \in S: pred`, + for example: + ```ocaml + let x = noprops "x" in + let y = noprops "y" in + let names = [x; y] in + Choose (names, Some S, pred) + ``` + + Use this constructor *only* when + tuply declarations are present. + Otherwise, use the constructor `Choose`. + *) + | ChooseTuply of + hints * expr option * expr (* `{x \in S: P(x)}` axiom scheme of separation @@ -104,6 +131,16 @@ and expr_ = 3. predicate (`P(x)` above) *) | SetSt of hint * expr * expr + (* `{<> \in S: P(x)}` + + Elements: + 1. list of declared identifiers + (`x`, ..., `y` above), + 2. set (`S` above) that bounds the + values of the tuple of identifiers + 3. predicate (`P(x)` above) + *) + | SetStTuply of hints * expr * expr (* `{f(x): x \in S}` axiom scheme of replacement @@ -112,6 +149,7 @@ and expr_ = specifically page 301. *) | SetOf of expr * bounds + | SetOfTuply of expr * tuply_bounds (* `{1, 2}` set enumeration @@ -126,6 +164,7 @@ and expr_ = | Tuple of expr list (* Function constructor `[x \in S |-> e]` *) | Fcn of bounds * expr + | FcnTuply of tuply_bounds * expr (* `f[x]` *) | FcnApp of expr * expr list (* Set of functions `[A -> B]` *) @@ -181,6 +220,12 @@ and expoint = (** Bound variables *) and bounds = bound list and bound = hint * kind * bound_domain +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 @@ -300,6 +345,15 @@ and hyp_ = - domain bound `hdom` *) | Fresh of hint * shape * kind * hdom + (* "tuple" of declared identifiers + + <> \in S + + where: + - x, ..., y are stored in the `hints`, and + - S is stored in `hdom` + *) + | FreshTuply of hints * hdom (* declared variable named `hint.core` *) | Flex of hint (* operator definition in module or `LET` scope *) @@ -368,6 +422,32 @@ let unditto (bounds: bounds): bounds = unditto [] No_domain bounds +let unditto_tuply + (bounds: tuply_bounds): + tuply_bounds = + let rec unditto out prevdom bs = + let recurse b bs prevdom = + let out = b :: out in + unditto out prevdom bs in + match bs with + | (_, (Domain d as prevdom) as b) :: bs -> + recurse b bs prevdom + | (v, Ditto) :: bs -> + let b = (v, prevdom) in + recurse b bs prevdom + | (_, No_domain as b) :: bs -> + recurse b bs prevdom + | [] -> + List.rev out in + unditto [] No_domain bounds + + +let name_of_tuply (t: tuply_name): hint = + match t with + | Bound_name name -> name + | Bound_names _ -> assert false + + let name_of_bound ((name, _, _): bound): hint = name @@ -479,6 +559,12 @@ 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: @@ -488,11 +574,22 @@ sig 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: @@ -501,6 +598,9 @@ 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: @@ -559,12 +659,25 @@ 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 @@ -777,6 +890,34 @@ struct Forall bounds predicate + let make_tuply_quantifier + (quantifier: quantifier) + (bounds: tuply_bounds) + (predicate: expr): + expr = + let quant_ = QuantTuply ( + quantifier, + bounds, + predicate) in + noprops quant_ + + + let make_tuply_exists + (bounds: tuply_bounds) + (predicate: expr): + expr = + make_tuply_quantifier + Exists bounds predicate + + + let make_tuply_forall + (bounds: tuply_bounds) + (predicate: expr): + expr = + make_tuply_quantifier + Forall bounds predicate + + let make_temporal_quantifier (quantifier: quantifier) (names: t list) @@ -832,6 +973,33 @@ struct noprops choose_ + let make_tuply_choose + (names: t list) + (predicate: expr): + expr = + let names = List.map + hint_of names in + let choose_ = ChooseTuply ( + names, + None, + predicate) in + noprops choose_ + + + let make_bounded_tuply_choose + (names: t list) + (bound: expr) + (predicate: expr): + expr = + let names = List.map + hint_of names in + let choose_ = ChooseTuply ( + names, + Some bound, + predicate) in + noprops choose_ + + let make_setst (name: t) (bound: expr) @@ -845,6 +1013,20 @@ struct noprops setst_ + let make_tuply_setst + (names: t list) + (bound: expr) + (predicate: expr): + expr = + let names = List.map + hint_of names in + let setst_ = SetStTuply ( + names, + bound, + predicate) in + noprops setst_ + + let make_setof (expr: expr) (bounds: bounds): @@ -854,6 +1036,15 @@ struct noprops setof_ + let make_tuply_setof + (expr: expr) + (bounds: tuply_bounds): + expr = + let setof_ = SetOfTuply ( + expr, bounds) in + noprops setof_ + + let make_setenum (exprs: expr list): expr = @@ -884,6 +1075,15 @@ struct noprops func_ + let make_tuply_fcn + (bounds: tuply_bounds) + (value: expr): + expr = + let func_ = FcnTuply ( + bounds, value) in + noprops func_ + + let make_fcn_domain (func: expr): expr = @@ -1172,6 +1372,42 @@ struct (name, kind, Domain bound) + let make_unbounded_name_decl + (name: t): + tuply_bound = + let name = hint_of name in + (Bound_name name, + No_domain) + + + let make_bounded_name_decl + (name: t) + (domain: expr): + tuply_bound = + let name = hint_of name in + (Bound_name name, + Domain domain) + + + let make_tuply_decl + (names: t list): + tuply_bound = + let names = List.map + hint_of names in + (Bound_names names, + No_domain) + + + let make_bounded_tuply_decl + (names: t list) + (domain: expr): + tuply_bound = + let names = List.map + hint_of names in + (Bound_names names, + Domain domain) + + let make_fresh (name: t) (kind: kind): @@ -1248,6 +1484,59 @@ struct kind, Unbounded) in fresh @@ name + + + let make_tuply_fresh + (names: t list): + hyp = + (* Return tuply declaration. + + WARNING: The properties of the + *first* item of `names` are + copied to the returned + hypothesis. + *) + let names = List.map + hint_of names in + let fresh = FreshTuply ( + names, Unbounded) in + let h = List.hd names in + fresh @@ h + + + let make_bounded_tuply_fresh + (names: t list) + (domain: expr): + hyp = + (* Bounded declaration. + + The declaration is tuply, + in that multiple + identifiers are declared, + as a tuple, with the + meaning this has in + TLA+ syntax. + + The returned declaration + has visible domain-bound. + To create a declaration + with hidden domain-bound, + use the relevant + data constructors. + + WARNING: The properties + of the *first* item of + `names` are copied to + the returned hypothesis. + *) + let names = List.map + hint_of names in + let d = Bounded ( + domain, Visible) in + let fresh = FreshTuply ( + names, d) in + let h = List.hd names in + fresh @@ h end @@ -1307,12 +1596,27 @@ let name_of_ix failwith "`RECURSIVE`\ declaration found" end + | FreshTuply _ -> + failwith "Found \ + positional index \ + that refers to \ + tuply declaration." | Fact _ -> failwith "Found \ positional index \ that refers to Fact." +let pformat_tuply (names: hints): string = + (* String of `names` with TLA+ tuple syntax. *) + let accum = "<<" in + let step accum name = + accum ^ ", " ^ name.core in + let accum = List.fold_left + step accum names in + accum ^ ">>" + + let hyp_name h = match h.core with | Fresh (nm, _, _, _) | Flex nm @@ -1323,6 +1627,8 @@ let hyp_name h = match h.core with | Recursive (nm, _)}, _, _, _) -> nm.core + | FreshTuply (names, _) -> + pformat_tuply names | Fact (_, _,_) -> "??? FACT ???" @@ -1360,6 +1666,11 @@ let print_cx cx = let visible = describe_domain_bound dom in ("Constant operator `" ^ name.core ^ "` (" ^ visible ^ ")\n") + | FreshTuply (names, dom) -> + let tuply = pformat_tuply names in + let visible = describe_domain_bound dom in + ("Constant tuply declaration of " ^ + tuply ^ "` (" ^ visible ^ ")\n") | Defn (df, _, visibility, _) -> let visible = visibility_to_string visibility in diff --git a/src/expr/e_t.mli b/src/expr/e_t.mli index 5fb2b08c..d1a67046 100644 --- a/src/expr/e_t.mli +++ b/src/expr/e_t.mli @@ -59,16 +59,24 @@ and expr_ = | 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 @@ -117,6 +125,13 @@ and expoint = 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 @@ -175,6 +190,7 @@ 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 @@ -194,6 +210,11 @@ 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: @@ -260,6 +281,12 @@ 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: @@ -268,10 +295,21 @@ 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: @@ -280,6 +318,9 @@ 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: @@ -337,12 +378,25 @@ 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 diff --git a/src/expr/e_visit.ml b/src/expr/e_visit.ml index 04142526..cf4826e1 100644 --- a/src/expr/e_visit.ml +++ b/src/expr/e_visit.ml @@ -15,6 +15,8 @@ let hyp_rename v h = begin match h.core with | Fresh (_, shp, k, dom) -> Fresh (v, shp, k, dom) + | FreshTuply _ -> assert false (* renaming + is undefined for this case *) | Flex _ -> Flex v | Defn (df, wd, vis, ex) -> @@ -159,6 +161,41 @@ let hyps_of_bounds_as_arity_0 List.map make_fresh bs +let hyp_of_tuply_bound + (names: Util.hints) + (dom: bound_domain): + hyp = + match dom with + | Domain d -> + make_bounded_tuply_fresh names d + | No_domain -> + make_tuply_fresh names + | Ditto -> Errors.bug "\ + E_visit.hyp_of_tuply_bound: \ + Ditto not expected" + + +let hyps_of_tuply_bounds_unditto + (bs: tuply_bounds): hyp list = + let bs = unditto_tuply bs in + let mapper n (v, dom) = + let dom = + match dom with + | Domain d -> + let d = shifter n d in + Domain d + | No_domain -> dom + | Ditto -> assert false in + match v with + | Bound_name name -> + hyp_of_bound_full ( + name, Constant, dom) + | Bound_names names -> + hyp_of_tuply_bound names dom + in + List.mapi mapper bs + + let map_bound_domains (mapper: expr -> expr) (bs: bounds): @@ -326,6 +363,13 @@ class virtual ['s] map = object (self : 'self) At b @@ oe | Parens (e, pf) -> Parens (self#expr scx e, self#pform scx pf) @@ oe + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> + failwith "use instead the class \ + `E_visit.map_concrete`" method pform scx pf = pf @@ -398,6 +442,9 @@ class virtual ['s] map = object (self : 'self) in let h = Fresh (nm, shp, lc, dom) @@ h in (self#adj scx h, h) + | FreshTuply (names, dom) -> + failwith "use instead the class \ + `E_visit.map_concrete`" | Flex s -> let h = Flex s @@ h in (self#adj scx h, h) @@ -518,6 +565,13 @@ class virtual ['s] iter = object (self : 'self) | Parens (e, pf) -> self#expr scx e ; self#pform scx pf + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> + failwith "use instead the class\ + `E_visit.iter_concrete`" method pform scx pf = () @@ -591,6 +645,9 @@ class virtual ['s] iter = object (self : 'self) ignore (self#defn scx df) | Fact (e, _, _) -> self#expr scx e + | FreshTuply _ -> + failwith "use instead the class\ + `E_visit.iter_concrete`" end ; adj scx h method hyps scx hs = match Dq.front hs with @@ -602,6 +659,135 @@ class virtual ['s] iter = object (self : 'self) end + +class virtual ['s] map_concrete = + (* Mapping of a concrete syntax tree. + + Code related to use of `FreshTuply` + from the context is untested, + but implemented for completeness. + *) + object (self: 'self) + inherit ['s] map as super + + method expr scx oe = + match oe.core with + | QuantTuply (qfr, bs, pred) -> + let (scx, bs) = self#tuply_bounds scx bs in + let pred = self#expr scx pred in + QuantTuply (qfr, bs, pred) @@ oe + | ChooseTuply (names, optdom, pred) -> + let optdom = Option.map + (self#expr scx) optdom in + let h = match optdom with + | None -> make_tuply_fresh names + | Some dom -> + make_bounded_tuply_fresh + names dom in + let scx = self#adj scx h in + let pred = self#expr scx pred in + ChooseTuply (names, optdom, pred) @@ oe + | SetStTuply (names, dom, pred) -> + let dom = self#expr scx dom in + let fresh = make_bounded_tuply_fresh + names dom in + let scx = self#adj scx fresh in + let pred = self#expr scx pred in + SetStTuply (names, dom, pred) @@ oe + | SetOfTuply (elem, bs) -> + let (scx, bs) = self#tuply_bounds scx bs in + let elem = self#expr scx elem in + SetOfTuply (elem, bs) @@ oe + | FcnTuply (bs, value) -> + let (scx, bs) = self#tuply_bounds scx bs in + let value = self#expr scx value in + FcnTuply (bs, value) @@ oe + | _ -> super#expr scx oe + + method tuply_bounds scx bs = + let bs = List.map (self#tuply_bound scx) bs in + let hs = hyps_of_tuply_bounds_unditto bs in + let scx = self#adjs scx hs in + (scx, bs) + + method tuply_bound scx (tuply_name, dom) = + let dom = match dom with + | Domain d -> + let d = self#expr scx d in + Domain d + | _ -> dom in + (tuply_name, dom) + + method hyp scx h = + match h.core with + | FreshTuply (names, dom) -> + let dom = match dom with + | Unbounded -> Unbounded + | Bounded (r, rvis) -> + Bounded (self#expr scx r, rvis) in + let h = FreshTuply (names, dom) @@ h in + (self#adj scx h, h) + | _ -> super#hyp scx h +end + + +class virtual ['s] iter_concrete = + (* Iteration over a concrete syntax tree. + + Code related to use of `FreshTuply` + from the context is untested, + but implemented for completeness. + *) + object (self: 'self) + inherit ['s] iter as super + + method expr scx oe = + match oe.core with + | QuantTuply (_, bs, pred) -> + let scx = self#tuply_bounds scx bs in + self#expr scx pred + | ChooseTuply (names, optdom, pred) -> + let h = match optdom with + | None -> make_tuply_fresh names + | Some dom -> + self#expr scx dom; + make_bounded_tuply_fresh + names dom in + let scx = adj scx h in + self#expr scx pred + | SetStTuply (names, dom, pred) -> + self#expr scx dom; + let fresh = make_bounded_tuply_fresh + names dom in + let scx = adj scx fresh in + self#expr scx pred + | SetOfTuply (elem, bs) -> + let scx = self#tuply_bounds scx bs in + self#expr scx elem + | FcnTuply (bs, value) -> + let scx = self#tuply_bounds scx bs in + self#expr scx value + | _ -> super#expr scx oe + + method tuply_bounds scx bs = + List.iter (self#tuply_bound scx) bs; + let hs = hyps_of_tuply_bounds_unditto bs in + adjs scx hs + + method tuply_bound scx (_, dom) = + match dom with + | Domain d -> self#expr scx d + | _ -> () + + method hyp scx h = + match h.core with + | FreshTuply (_, Bounded (dom, _)) -> + self#expr scx dom; + adj scx h + | _ -> super#hyp scx h +end + + class virtual ['s] map_visible_hyp = object (self : 'self) (* Map expressions, visiting only visible hypotheses. *) inherit ['s] map as super @@ -627,6 +813,9 @@ class virtual ['s] map_visible_hyp = object (self : 'self) | Fact (e, Visible, tm) -> let h = Fact (self#expr scx e, Visible, tm) @@ h in (adj scx h, h) + | FreshTuply _ -> + failwith "use instead the class \ + `E_visit.iter_concrete`" end class virtual ['s] iter_visible_hyp = object (self : 'self) @@ -648,6 +837,9 @@ class virtual ['s] iter_visible_hyp = object (self : 'self) ignore (self#defn scx df) | Fact (e, Visible, _) -> self#expr scx e + | FreshTuply _ -> + failwith "use instead the class \ + `E_visit.iter_concrete`" end ; adj scx h end @@ -790,6 +982,12 @@ class virtual ['s] map_rename = object (self : 'self) let scx = self#adj scx hyp in let e = self#expr scx e in SetSt (v, dom, e) @@ oe + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> + failwith "unused pattern-case, so not implemented" | _ -> super#expr scx oe method defn scx df = @@ -854,6 +1052,8 @@ class virtual ['s] map_rename = object (self : 'self) let h = Fresh (nm, shp, lc, dom) @@ h in let (h, _) = self#rename cx h nm in (self#adj scx h, h) + | FreshTuply _ -> + failwith "unused pattern-case, so not implemented" | Flex s -> let h = Flex s @@ h in let (h, _) = self#rename cx h s in diff --git a/src/expr/e_visit.mli b/src/expr/e_visit.mli index 5e37fcd2..df0549ff 100644 --- a/src/expr/e_visit.mli +++ b/src/expr/e_visit.mli @@ -56,6 +56,23 @@ class virtual ['s] iter : object 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 diff --git a/src/frontend/coalesce.ml b/src/frontend/coalesce.ml index 53b25f94..cb50a46e 100644 --- a/src/frontend/coalesce.ml +++ b/src/frontend/coalesce.ml @@ -171,8 +171,9 @@ let rename_with_loc cx e = *) let h = Defn (df, wd, vis, ex) @@ hyp in (h, name) + | FreshTuply _ | Fact _ -> - assert false + assert false (* unexpected cases *) end in visitor#expr ((), cx) e @@ -364,7 +365,9 @@ let coalesce_modal_visitor = object (self) let op_ = (Operator (coalesced_op, expr)) @@ index in coalesce_operator cx op_ args end - | Fact _ -> (* unexpected `Fact` *) assert false + | FreshTuply _ + | Fact _ -> + assert false (* unexpected cases *) | Defn ({core=Recursive _}, _, _, _) -> (* not implemented case *) assert false | Defn ({core=Instance _}, _, _, _) -> diff --git a/src/proof.mli b/src/proof.mli index 95ae89b1..fb1c18ed 100644 --- a/src/proof.mli +++ b/src/proof.mli @@ -23,9 +23,11 @@ module T : sig | Suffices of sequent * proof | Pcase of expr * proof | Pick of bound list * expr * proof + | PickTuply of tuply_bounds * expr * proof | Use of usable * bool | Have of expr | Take of bound list + | TakeTuply of tuply_bounds | Witness of expr list | Forget of int and qed_step = qed_step_ wrapped diff --git a/src/proof/p_fmt.ml b/src/proof/p_fmt.ml index b71e6c43..210f5f0c 100644 --- a/src/proof/p_fmt.ml +++ b/src/proof/p_fmt.ml @@ -291,6 +291,9 @@ and pp_print_step cx ff stp = let cx = bump cx in (* conjunction of nondom facts in the SUFFICES *) bump cx + | TakeTuply _ + | PickTuply _ -> + assert false in cx and pp_print_qed_step cx ff q = diff --git a/src/proof/p_gen.ml b/src/proof/p_gen.ml index e0039964..29a48d92 100644 --- a/src/proof/p_gen.ml +++ b/src/proof/p_gen.ml @@ -352,6 +352,9 @@ and gen_step (sq, inits, time_flag) stp = | Witness _ | Pick _ -> Errors.bug ~at:stp "Proof.Gen.gen_step" + | TakeTuply _ + | PickTuply _ -> + assert false (* FIXME this function must split the list of facts into its elements and pass them one by one to gen_step *) diff --git a/src/proof/p_simplify.ml b/src/proof/p_simplify.ml index 0fa06e26..9e3c3756 100644 --- a/src/proof/p_simplify.ml +++ b/src/proof/p_simplify.ml @@ -273,6 +273,9 @@ and simplify_step cx goal st time_flag = (Quant (Forall, gbs, ge) @@ goal, shf + 1) in strip shf aux goal bs + | {core=QuantTuply (Forall, _, _)} -> + assert false (* tuple declarations + have been translated earlier *) | _ -> let msg = Util.sprintf "@.@[@[%s@ %s@]@,%a@]@." @@ -355,6 +358,9 @@ and simplify_step cx goal st time_flag = let e = Apply (Internal Builtin.Unprimable @@ e, [e]) @@ e in let goal = app_expr (scons e (shift 0)) goal in instantiate aux err goal es + | {core = QuantTuply (Exists, _, _)} -> + assert false (* tuple declarations + have been translated earlier *) | goal -> let msg = Util.sprintf "@.@[@[%s@ %s@]@,%a@]@." @@ -447,6 +453,9 @@ and simplify_step cx goal st time_flag = | _ -> Errors.bug ~at:st "Proof.Simplify.simplify_step/PICK" in (cx, goal, nsts, time_flag) + | TakeTuply _ + | PickTuply _ -> + assert false in Util.eprintf ~debug:"simpl" ~at:st "simplify_step (result)@\n@[%t@ --> %t@]@.@." diff --git a/src/proof/p_subst.ml b/src/proof/p_subst.ml index 9b044a12..15489911 100644 --- a/src/proof/p_subst.ml +++ b/src/proof/p_subst.ml @@ -74,6 +74,9 @@ and app_step s stp = match stp.core with | Witness es -> let es = List.map (app_expr s) es in (s, Witness es @@ stp) + | TakeTuply _ + | PickTuply _ -> + assert false and app_usable s us = let app_def dw = diff --git a/src/proof/p_t.ml b/src/proof/p_t.ml index 7a6b5a40..39d438a2 100644 --- a/src/proof/p_t.ml +++ b/src/proof/p_t.ml @@ -49,9 +49,11 @@ and step_ = | Suffices of sequent * proof | Pcase of expr * proof | Pick of bound list * expr * proof + | PickTuply of tuply_bounds * expr * proof | Use of usable * bool | Have of expr | Take of bound list + | TakeTuply of tuply_bounds | Witness of expr list | Forget of int (** Terminal proof-step **) diff --git a/src/proof/p_t.mli b/src/proof/p_t.mli index 0016fcc8..b1a82bd0 100644 --- a/src/proof/p_t.mli +++ b/src/proof/p_t.mli @@ -26,9 +26,11 @@ and step_ = | Suffices of sequent * proof | Pcase of expr * proof | Pick of bound list * expr * proof + | PickTuply of tuply_bounds * expr * proof | Use of usable * bool | Have of expr | Take of bound list + | TakeTuply of tuply_bounds | Witness of expr list | Forget of int (** Terminal proof-step **) diff --git a/src/proof/p_visit.ml b/src/proof/p_visit.ml index 974b6481..26fc3a34 100644 --- a/src/proof/p_visit.ml +++ b/src/proof/p_visit.ml @@ -161,6 +161,10 @@ class virtual ['hyp] map = object (self : 'self) let scx = bump scx 4 in (* finally, we are in the next step *) (scx, st) + | TakeTuply _ + | PickTuply _ -> + failwith "use instead the class \ + `P_visit.map_concrete`" method usable scx us = let usdef dw = @@ -266,6 +270,10 @@ class virtual ['hyp] iter = object (self : 'self) let scx = Expr.Visit.adj_unboundeds_unchecked scx bs in bump scx 4 + | TakeTuply _ + | PickTuply _ -> + failwith "use instead the class \ + `P_visit.iter_concrete`" method usable scx us = let usdef dw = match dw.core with @@ -278,3 +286,89 @@ class virtual ['hyp] iter = object (self : 'self) List.iter usdef us.defs end + + +class virtual ['s] map_concrete = + object (self: 'self) + inherit ['s] map as super + inherit ['s] Expr.Visit.map_concrete + + method step scx st = + let stepnm = string_of_stepno + (Property.get st Props.step) in + let adj_step scx = + Expr.Visit.adj + scx + (Defn ( + Operator ( + stepnm @@ st, + dummy) @@ st, + Proof Always, + Visible, + Local) @@ st) in + match st.core with + | TakeTuply bs -> + let (scx, bs) = self#tuply_bounds + scx bs in + let st = TakeTuply bs @@ st in + let scx = bump scx 1 in + let scx = adj_step scx in + let scx = bump scx 1 in + (scx, st) + | PickTuply (bs, e, prf) -> + let prf = self#proof + (bump scx 3) prf in + let (bs, e) = + let (scx, bs) = self#tuply_bounds + scx bs in + let e = self#expr scx e in + (bs, e) in + let st = PickTuply (bs, e, prf) @@ st in + let scx = adj_step scx in + let scx = bump scx 1 in + let scx, _ = self#tuply_bounds scx bs in + let scx = bump scx 4 in + (scx, st) + | _ -> + super#step scx st + end + + +class virtual ['s] iter_concrete = + object (self: 'self) + inherit ['s] iter as super + inherit ['s] Expr.Visit.iter_concrete + + method step scx st = + let stepnm = string_of_stepno + (Property.get st Props.step) in + let adj_step scx = + Expr.Visit.adj + scx + (Defn ( + Operator ( + stepnm @@ st, + dummy) @@ st, + Proof Always, + Visible, + Local) @@ st) in + match st.core with + | TakeTuply bs -> + let scx = self#tuply_bounds + scx bs in + let scx = bump scx 1 in + let scx = adj_step scx in + bump scx 1 + | PickTuply (bs, e, prf) -> + self#proof scx prf ; + let () = + let scx = self#tuply_bounds + scx bs in + self#expr scx e in + let scx = adj_step scx in + let scx = bump scx 1 in + let scx = self#tuply_bounds + scx bs in + bump scx 4 + | _ -> super#step scx st + end diff --git a/src/proof/p_visit.mli b/src/proof/p_visit.mli index fa7ecc81..43fca22c 100644 --- a/src/proof/p_visit.mli +++ b/src/proof/p_visit.mli @@ -26,3 +26,13 @@ class virtual ['s] iter: object method step: 's scx -> step -> 's scx method usable: 's scx -> usable -> unit end + +class virtual ['s] map_concrete: object + inherit ['s] map + inherit ['s] Expr.Visit.map_concrete +end + +class virtual ['s] iter_concrete: object + inherit ['s] iter + inherit ['s] Expr.Visit.iter_concrete +end diff --git a/src/smt/ectx.ml b/src/smt/ectx.ml index a7c05a4a..4927f6be 100644 --- a/src/smt/ectx.ml +++ b/src/smt/ectx.ml @@ -49,6 +49,7 @@ let update_hyp_name id h = | Fact _ -> (* Errors.bug "Backend.SMT.Ectx.adj: Fact not expected" *) h + | FreshTuply _ -> assert false (* unexpected case *) let adj (dx,cx) h = let id = hyp_name h in @@ -128,4 +129,5 @@ let rec from_hyps (ecx:t) (hs:hyp Deque.dq) : t = from_hyps ecx hs | Fact _ -> from_hyps (bump ecx) hs + | FreshTuply _ -> assert false (* unexpected case *) end diff --git a/src/smt/smtcommons.ml b/src/smt/smtcommons.ml index a10f8724..46bc0a34 100644 --- a/src/smt/smtcommons.ml +++ b/src/smt/smtcommons.ml @@ -831,6 +831,8 @@ let allids cx = _, _, _) -> SSet.add nm.core r | Fact (_, _, _) -> r + | FreshTuply _ -> + assert false (* unexpected case *) end SSet.empty cx let subtract xs x = fold_left (fun r a -> if x = a then r else r @ [a]) [] xs @@ -972,6 +974,12 @@ and fv_expr scx e : string list = @ (match oth with Some e -> fv_expr scx e | None -> []) | Parens (e, pf) -> fv_expr scx e + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> + assert false | _ -> [] and fv_sel scx = function | Sel_inst args -> diff --git a/src/typesystem/typ_e.ml b/src/typesystem/typ_e.ml index 07e5cf07..57170dfb 100644 --- a/src/typesystem/typ_e.ml +++ b/src/typesystem/typ_e.ml @@ -32,6 +32,8 @@ let hyp_optype h = optype nm | Fact (_, _, _) -> None + | FreshTuply _ -> + assert false (* unexpected case *) (* Equivalence classes of type variables *) @@ -783,6 +785,12 @@ let rec fmt_expr (cx: Expr.Fmt.ctx) ew = match ew.core with fmt_expr cx (Parens (e, Nlabel (l, xs) @@ e) @@ e) | Parens (e, {core=Syntax}) -> fmt_expr cx e + | QuantTuply _ + | ChooseTuply _ + | SetStTuply _ + | SetOfTuply _ + | FcnTuply _ -> + assert false and pp_print_bang ff () = if Params.debugging "garish" then @@ -1083,6 +1091,8 @@ and pp_print_sequent cx ff sq = match Deque.null sq.context with fst (Expr.Fmt.adj cx nm) | Fact (_, _, _) -> Expr.Fmt.bump cx + | FreshTuply _ -> + assert false (* not implemented *) in (cx, ch :: chs) end (cx, []) sq.context in let chs = List.filter @@ -1121,6 +1131,7 @@ and pp_print_hyp cx ff h = fprintf ff " \\in %a" (pp_print_expr cx) b); ncx + | FreshTuply _ -> assert false (* not implemented *) | Flex nm -> let t = optype nm in let (ncx, nm) = Expr.Fmt.adj cx nm in From 460c378a7461a4c1ae8224cdf32b60d630b96796 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 5 Jun 2021 02:17:35 +0200 Subject: [PATCH 2/4] BUG: do not allow unbounded declarations in function definitions The change in this commit corrects a bug with function definitions. Parsing of function definitions allowed using unbounded declarations (and also mixing bounded and unbounded declarations). For example, before this change, parsing allowed: ```tla f[x \in S, y] == TRUE ``` and even: ```tla f[x] == TRUE ``` These syntax errors are detected by SANY. In any case, this change ensures that `tlapm` does not parse such definitions. The error was due to calling the function `bounds` within the function `ophead`, instead of calling the function `boundeds` (which was called before commit 5958dfaca70b07613603baadff57926aff7eba66 in order to handle function constructors within the function `atomic_expr`). This commit also adds tests for this bug. --- src/expr/e_parser.ml | 13 +++++++++++-- test/fast/language/FunctionDefinitionBoundeds.tla | 9 +++++++++ .../language/FunctionDefinitionOnlyBoundeds_1.tla | 10 ++++++++++ .../language/FunctionDefinitionOnlyBoundeds_2.tla | 10 ++++++++++ 4 files changed, 40 insertions(+), 2 deletions(-) create mode 100644 test/fast/language/FunctionDefinitionBoundeds.tla create mode 100644 test/fast/language/FunctionDefinitionOnlyBoundeds_1.tla create mode 100644 test/fast/language/FunctionDefinitionOnlyBoundeds_2.tla diff --git a/src/expr/e_parser.ml b/src/expr/e_parser.ml index 2c70f472..d43f7a44 100644 --- a/src/expr/e_parser.ml +++ b/src/expr/e_parser.ml @@ -1063,9 +1063,18 @@ and ophead b = lazy begin `Op (op_name, params)); (* function definition + for example: + f[x \in S, y \in Q] == ... + + Only bounded declarations are allowed in function constructors. + Read 16.1.7 on pages 301--304 of the book "Specifying Systems", + in particular pages 303--304. + + This is why the function `boundeds` is called, + instead of the function `bounds`. *) - punct "[" >>> use (bounds b) <<< punct "]" - <$> (fun args -> `Fun (name_1, args)); + punct "[" >>> use (boundeds b) <<< punct "]" + <$> (fun boundeds -> `Fun (name_1, boundeds)); (* first-order-operator definition *) optional ( diff --git a/test/fast/language/FunctionDefinitionBoundeds.tla b/test/fast/language/FunctionDefinitionBoundeds.tla new file mode 100644 index 00000000..3d79b497 --- /dev/null +++ b/test/fast/language/FunctionDefinitionBoundeds.tla @@ -0,0 +1,9 @@ +---------------------- MODULE FunctionDefinitionBoundeds ----------------------- +(* Test that function definitions allow bounded declarations. + +Bounded declarations can include tuple declarations. +*) +f[x \in {TRUE}, y \in TRUE] == x + +g[x \in {TRUE}, <> \in TRUE \X FALSE] == x /\ (y \/ ~ z) +================================================================================ diff --git a/test/fast/language/FunctionDefinitionOnlyBoundeds_1.tla b/test/fast/language/FunctionDefinitionOnlyBoundeds_1.tla new file mode 100644 index 00000000..28240f9b --- /dev/null +++ b/test/fast/language/FunctionDefinitionOnlyBoundeds_1.tla @@ -0,0 +1,10 @@ +------------------- MODULE FunctionDefinitionOnlyBoundeds_1 -------------------- +(* Test that function definitions allow only bounded declarations. + +The below form is a syntax error in TLA+. +Previously, `tlapm` parsed this form. +The syntax error is detected by SANY. +*) +f[x] == TRUE +================================================================================ +stderr: Error: Could not parse diff --git a/test/fast/language/FunctionDefinitionOnlyBoundeds_2.tla b/test/fast/language/FunctionDefinitionOnlyBoundeds_2.tla new file mode 100644 index 00000000..236789e9 --- /dev/null +++ b/test/fast/language/FunctionDefinitionOnlyBoundeds_2.tla @@ -0,0 +1,10 @@ +------------------- MODULE FunctionDefinitionOnlyBoundeds_2 -------------------- +(* Test that function definitions allow only bounded declarations. + +The below form is a syntax error in TLA+. +Previously, `tlapm` parsed this form. +The syntax error is detected by SANY. +*) +f[x \in TRUE, y] == TRUE +================================================================================ +stderr: Error: Could not parse From 0667253f99561fcae5de855da4e7d060636a6f3b Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 5 Jun 2021 03:02:15 +0200 Subject: [PATCH 3/4] BUG: do not allow both bounded and unbounded declarations in \E, \A because TLA+ does not allow this kind of syntax. A single rigid quantifier can include either: - only unbounded declarations, for example `\E x, y, z: ...`, or - only bounded declarations, for example `\A x \in A, y \in B, z \in C: ...`. A single rigid quantifier cannot include both bounded and unbounded declarations. This syntax is caught by SANY. --- src/expr/e_parser.ml | 55 ++++++++++++++++++- .../language/ConstantQuantifierBoundeds.tla | 5 ++ .../language/ConstantQuantifierUnboundeds.tla | 5 ++ .../ExistsNotBothBoundedAndUnbounded.tla | 7 +++ .../ForallNotBothBoundedAndUnbounded.tla | 7 +++ 5 files changed, 78 insertions(+), 1 deletion(-) create mode 100644 test/fast/language/ConstantQuantifierBoundeds.tla create mode 100644 test/fast/language/ConstantQuantifierUnboundeds.tla create mode 100644 test/fast/language/ExistsNotBothBoundedAndUnbounded.tla create mode 100644 test/fast/language/ForallNotBothBoundedAndUnbounded.tla diff --git a/src/expr/e_parser.ml b/src/expr/e_parser.ml index d43f7a44..4440673d 100644 --- a/src/expr/e_parser.ml +++ b/src/expr/e_parser.ml @@ -18,6 +18,12 @@ module B = Builtin let tuple_of_names = angle names +let make_unboundeds (names: Util.hints): bounds = + let make_bound name = ( + name, Constant, No_domain) in + List.map make_bound names + + (*let b = ref false*) let fixities = @@ -298,12 +304,33 @@ and complex_expr b = lazy begin (* constant quantification for example: \E x, y, z: x = y + + Each constant quantifier can contain either: + + - only unbounded constant declarations, for example: + `\E x, y, z: x = y`, or + + - only bounded constant declarations: + `\E x \in S, y, z \in R: x = z`, + + but not both bounded and unbounded. + Bounded and unbounded declarations can be represented + using nested quantifiers, for example: + + `\E x \in S: \E y, z: x = z` + + Read Section 16.1.1 on pages 293--294 of the book "Specifying Systems", + in particular page 294. *) locate begin choice [ punct "\\A" Forall ; punct "\\E" Exists ; ] - <**> use (bounds b) + <**> alt [ + use (boundeds b); + names + <$> (fun names -> make_unboundeds names) + ] <**> (colon_expr b) end <$> begin fun ({core = ((q, bs), e)} as quant) -> @@ -677,6 +704,32 @@ and operator b = lazy begin ] end + +(* The function `bounds` is currently unused. + +The function `bounds` allows including both bounded and unbounded +declarations in a single constructor. + +Including both bounded and unbounded declarations in a single +quantifier constructor is not allowed in TLA+, +read Section 16.1.1 on pages 293--294 of the book "Specifying Systems", +in particular page 294. + +Including both bounded and unbounded declarations in a single +`CHOOSE` constructor is not allowed in TLA+, +read Section 16.1.2 on pages 294--296 of the book "Specifying Systems", +in particular page 294. + +Including unbounded declarations in a set constructor is +not allowed in TLA+, +read Section 16.1.6 on pages 299--301 of the book "Specifying Systems", +in particular page 301. + +Including unbounded declarations in a function constructor or +function definition is not allowed in TLA+, +read Section 16.1.7 on pages 301--304 of the book "Specifying Systems", +in particular pages 303--304. +*) and bounds b = lazy begin comma1 (names <*> optional (in_expr b)) <$> begin diff --git a/test/fast/language/ConstantQuantifierBoundeds.tla b/test/fast/language/ConstantQuantifierBoundeds.tla new file mode 100644 index 00000000..59e4547a --- /dev/null +++ b/test/fast/language/ConstantQuantifierBoundeds.tla @@ -0,0 +1,5 @@ +---------------------- MODULE ConstantQuantifierBoundeds ----------------------- +(* Test that \E and \A allow bounded declarations. *) +E == \E x \in TRUE, y, z \in TRUE, w \in TRUE: TRUE +A == \A x \in TRUE, y, z \in TRUE, w \in TRUE: TRUE +================================================================================ diff --git a/test/fast/language/ConstantQuantifierUnboundeds.tla b/test/fast/language/ConstantQuantifierUnboundeds.tla new file mode 100644 index 00000000..f7257bf0 --- /dev/null +++ b/test/fast/language/ConstantQuantifierUnboundeds.tla @@ -0,0 +1,5 @@ +--------------------- MODULE ConstantQuantifierUnboundeds ---------------------- +(* Test that \E and \A allow unbounded declarations. *) +E == \E x, y, z: TRUE +A == \A x, y, z: TRUE +================================================================================ diff --git a/test/fast/language/ExistsNotBothBoundedAndUnbounded.tla b/test/fast/language/ExistsNotBothBoundedAndUnbounded.tla new file mode 100644 index 00000000..0e573377 --- /dev/null +++ b/test/fast/language/ExistsNotBothBoundedAndUnbounded.tla @@ -0,0 +1,7 @@ +------------------- MODULE ExistsNotBothBoundedAndUnbounded -------------------- +(* Test that \E does not allow both bounded and unbounded declarations +within the same quantifier. +*) +E == \E x \in TRUE, y: TRUE +================================================================================ +stderr: Error: Could not parse diff --git a/test/fast/language/ForallNotBothBoundedAndUnbounded.tla b/test/fast/language/ForallNotBothBoundedAndUnbounded.tla new file mode 100644 index 00000000..f08b2480 --- /dev/null +++ b/test/fast/language/ForallNotBothBoundedAndUnbounded.tla @@ -0,0 +1,7 @@ +------------------- MODULE ForallNotBothBoundedAndUnbounded -------------------- +(* Test that \A does not allow both bounded and unbounded declarations +within the same quantifier. +*) +A == \A x \in TRUE, y: TRUE +================================================================================ +stderr: Error: Could not parse From 3845b04691d5601c6a4f142c116b098713e2b2a5 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 5 Jun 2021 02:31:27 +0200 Subject: [PATCH 4/4] TST: that function constructors allow only bounded declarations in other words, that the following expression is not allowed: ```tla [x \in S, y |-> TRUE] ``` and the following expression is allowed: ```tla [x \in S, y \in S |-> TRUE] ``` Also, add a reminder in a comment in the parser code. --- src/expr/e_parser.ml | 5 +++++ test/fast/language/FunctionConstructorBoundeds.tla | 4 ++++ test/fast/language/FunctionConstructorOnlyBoundeds.tla | 5 +++++ 3 files changed, 14 insertions(+) create mode 100644 test/fast/language/FunctionConstructorBoundeds.tla create mode 100644 test/fast/language/FunctionConstructorOnlyBoundeds.tla diff --git a/src/expr/e_parser.ml b/src/expr/e_parser.ml index 4440673d..58673942 100644 --- a/src/expr/e_parser.ml +++ b/src/expr/e_parser.ml @@ -483,6 +483,11 @@ and atomic_expr b = lazy begin [x \in S |-> e] [<> \in S \X R |-> e] [<> \in S \X R, z \in Q |-> e] + + Only bounded declarations are allowed in function constructors. + Read Section 16.1.7 on pages 301--304 of + the book "Specifying Systems", + in particular pages 303--304. *) attempt (use (func_boundeds b) <<< mapsto) <**> use (expr b) diff --git a/test/fast/language/FunctionConstructorBoundeds.tla b/test/fast/language/FunctionConstructorBoundeds.tla new file mode 100644 index 00000000..925c8c0d --- /dev/null +++ b/test/fast/language/FunctionConstructorBoundeds.tla @@ -0,0 +1,4 @@ +---------------------- MODULE FunctionConstructorBoundeds ---------------------- +(* Test that function constructors allow bounded declarations. *) +f == [x \in {TRUE}, y \in TRUE |-> x /\ y] +================================================================================ diff --git a/test/fast/language/FunctionConstructorOnlyBoundeds.tla b/test/fast/language/FunctionConstructorOnlyBoundeds.tla new file mode 100644 index 00000000..9c55a57a --- /dev/null +++ b/test/fast/language/FunctionConstructorOnlyBoundeds.tla @@ -0,0 +1,5 @@ +-------------------- MODULE FunctionConstructorOnlyBoundeds -------------------- +(* Test that function constructors allow only bounded declarations. *) +f == [x \in TRUE, y |-> TRUE] +================================================================================ +stderr: Error: Could not parse