Fixing bug in elim* when a bound is given.

When a bound is given to elim*, do not try to destruct internal
existentials.

Author: strub

src/ecCoreFol.ml

@@ -147,6 +147,12 @@ let hoarecmp_opp cmp =
   | FHeq -> FHeq
   | FHge -> FHle
 
+(* -------------------------------------------------------------------- *)
+let string_of_quant = function
+  | Lforall -> "forall"
+  | Lexists -> "exists"
+  | Llambda -> "fun"
+
 (* -------------------------------------------------------------------- *)
 let mk_form = EcAst.mk_form
 let f_node { f_node = form } = form
@@ -601,41 +607,63 @@ exception DestrError of string
 let destr_error e = raise (DestrError e)
 
 (* -------------------------------------------------------------------- *)
-let destr_forall1 f =
-  match f.f_node with
-  | Fquant(Lforall,(x,t)::bd,p) -> x,t,f_forall bd p
-  | _ -> destr_error "forall"
-
-let destr_forall f =
+let decompose_binder ?(bound : int option) ~(quantif : quantif) (f : form) =
   match f.f_node with
-  | Fquant(Lforall,bd,p) -> bd, p
-  | _ -> destr_error "forall"
-
-let decompose_forall f =
-  match f.f_node with
-  | Fquant(Lforall,bd,p) -> bd, p
-  | _ -> [], f
+  | Fquant (q, bds, f) when q = quantif -> begin
+    match bound with
+    | None ->
+      bds, f
+    | Some bound ->
+      let bound = min bound (List.length bds) in
+      let bd1, bd2 = List.takedrop bound bds in
+      (bd1, f_quant quantif bd2 f)
+  end
 
-let destr_lambda f =
-  match f.f_node with
-  | Fquant(Llambda,bd,p) -> bd, p
-  | _ -> destr_error "lambda"
+  | _ ->
+    ([], f)
 
-let decompose_lambda f =
-  match f.f_node with
-  | Fquant(Llambda,bd,p) -> bd, p
-  | _ -> [], f
+let decompose_forall ?(bound : int option) (f : form) =
+  decompose_binder ?bound ~quantif:Lforall f
 
-let destr_exists1 f =
-  match f.f_node with
-  | Fquant(Lexists,(x,t)::bd,p) -> x,t,f_exists bd p
-  | _ -> destr_error "exists"
+let decompose_exists ?(bound : int option) (f : form) =
+  decompose_binder ?bound ~quantif:Lexists f
 
-let destr_exists f =
-  match f.f_node with
-  | Fquant(Lexists,bd,p) -> bd, p
-  | _ -> destr_error "exists"
+let decompose_lambda ?(bound : int option) (f : form) =
+  decompose_binder ?bound ~quantif:Llambda f    
+  
+(* -------------------------------------------------------------------- *)
+let destr_binder ?(bound : int option) ~quantif:quantif (f : form) =
+  let bds, f = decompose_binder ?bound ~quantif f in
+
+  if 0 < Option.value ~default:1 bound && List.is_empty bds then
+    destr_error (string_of_quant quantif);
+  bds, f
+
+let destr_forall ?(bound : int option) (f : form) =
+  destr_binder ?bound ~quantif:Lforall f
+  
+let destr_exists ?(bound : int option) (f : form) =
+  destr_binder ?bound ~quantif:Lexists f
+  
+let destr_lambda ?(bound : int option) (f : form) =
+  destr_binder ?bound ~quantif:Llambda f
 
+(* -------------------------------------------------------------------- *)
+let destr_binder1 ~quantif:quantif (f : form) =
+  let (x, t), f =
+    fst_map as_seq1 (destr_binder ~bound:1 ~quantif f)
+  in (x, t, f)
+
+let destr_forall1 (f : form) =
+  destr_binder1 ~quantif:Lforall f
+
+let destr_exists1 (f : form) =
+  destr_binder1 ~quantif:Lexists f
+  
+let destr_lambda1 (f : form) =
+  destr_binder1 ~quantif:Llambda f
+  
+(* -------------------------------------------------------------------- *)
 let destr_let f =
   match f.f_node with
   | Flet(lp, e1,e2) -> lp,e1,e2

src/ecCoreFol.mli

@@ -224,6 +224,9 @@ val f_xadd_simpl  : form -> form -> form
 val f_xmul_simpl  : form -> form -> form
 val f_xmuli_simpl : form -> form -> form
 
+(* -------------------------------------------------------------------- *)
+val string_of_quant : quantif -> string
+
 (* -------------------------------------------------------------------- *)
 exception DestrError of string
 
@@ -236,6 +239,21 @@ val destr_app2 : name:string -> (path -> bool) -> form -> form * form
 val destr_app1_eq : name:string -> path -> form -> form
 val destr_app2_eq : name:string -> path -> form -> form * form
 
+val decompose_binder  : ?bound:int -> quantif:quantif -> form -> bindings * form
+val decompose_forall  : ?bound:int -> form -> bindings * form
+val decompose_exists  : ?bound:int -> form -> bindings * form
+val decompose_lambda  : ?bound:int -> form -> bindings * form
+
+val destr_binder  : ?bound:int -> quantif:quantif -> form -> bindings * form
+val destr_forall  : ?bound:int -> form -> bindings * form
+val destr_exists  : ?bound:int -> form -> bindings * form
+val destr_lambda  : ?bound:int -> form -> bindings * form
+
+val destr_binder1  : quantif:quantif -> form -> ident * gty * form
+val destr_forall1  : form -> ident * gty * form
+val destr_exists1  : form -> ident * gty * form
+val destr_lambda1  : form -> ident * gty * form
+
 val destr_op        : form -> EcPath.path * ty list
 val destr_local     : form -> EcIdent.t
 val destr_pvar      : form -> prog_var * memory
@@ -256,14 +274,6 @@ val destr_eq        : form -> form * form
 val destr_eq_or_iff : form -> form * form
 val destr_let       : form -> lpattern * form * form
 val destr_let1      : form -> EcIdent.t * ty * form * form
-val destr_forall1   : form -> EcIdent.t * gty * form
-val destr_forall    : form -> bindings * form
-val decompose_forall: form -> bindings * form
-val decompose_lambda: form -> bindings * form
-val destr_lambda    : form -> bindings * form
-
-val destr_exists1   : form -> EcIdent.t * gty * form
-val destr_exists    : form -> bindings * form
 val destr_equivF    : form -> equivF
 val destr_equivS    : form -> equivS
 val destr_eagerF    : form -> eagerF

src/ecFol.ml

@@ -984,44 +984,48 @@ let f_dlet_simpl tya tyb d f =
  * - p1 => E x p2 -> [x] (p1 => p2)
  * - E x p1 => p2 -> [] (E x p1 => p2)
  *)
-let destr_exists_prenex f =
-  let rec prenex_exists bds p =
-    match sform_of_form p with
-    | SFand (`Sym, (f1, f2)) ->
-      let (bds, f2) = prenex_exists bds f2 in
-      let (bds, f1) = prenex_exists bds f1 in
+let destr_exists_prenex ?(bound : int option) (f : form) =
+  let rec prenex_exists ~bound bds p =
+    match bound, sform_of_form p with
+    | Some bound, _ when bound <= 0 ->
+      (bds, p)
+
+    | None, SFand (`Sym, (f1, f2)) ->
+      let (bds, f2) = prenex_exists ~bound:None bds f2 in
+      let (bds, f1) = prenex_exists ~bound:None bds f1 in
       (bds, f_and f1 f2)
 
-    | SFor (`Sym, (f1, f2)) ->
-      let (bds, f2) = prenex_exists bds f2 in
-      let (bds, f1) = prenex_exists bds f1 in
+    | None, SFor (`Sym, (f1, f2)) ->
+      let (bds, f2) = prenex_exists ~bound:None bds f2 in
+      let (bds, f1) = prenex_exists ~bound:None bds f1 in
       (bds, f_or f1 f2)
 
-    | SFimp (f1, f2) ->
-      let (bds, f2) = prenex_exists bds f2 in
+    | None, SFimp (f1, f2) ->
+      let (bds, f2) = prenex_exists ~bound:None bds f2 in
       (bds, f_imp f1 f2)
 
-    | SFquant (Lexists, bd, lazy p) ->
-      let bd, p   =
+    | None, SFif (f, f1, f2) ->
+      let (bds, f2) = prenex_exists ~bound:None bds f2 in
+      let (bds, f1) = prenex_exists ~bound:None bds f1 in
+      (bds, f_if f f1 f2)
+  
+    | bound, SFquant (Lexists, bd, lazy p) ->
+      let bound = Option.map (fun x -> x - 1) bound in
+      let bd, p =
         let s = Fsubst.f_subst_init ~freshen:true () in
         let s, bd = Fsubst.add_binding s bd in
         bd, Fsubst.f_subst s p in
       let bds = bd::bds in
-      prenex_exists bds p
-
-    | SFif (f, f1, f2) ->
-      let (bds, f2) = prenex_exists bds f2 in
-      let (bds, f1) = prenex_exists bds f1 in
-      (bds, f_if f f1 f2)
+      prenex_exists ~bound bds p
 
-    | SFop (op, [f1; f2]) when is_interp_ehoare_form_op op ->
-      let (bds, f1) = prenex_exists bds f1 in
+    | bound, SFop (op, [f1; f2]) when is_interp_ehoare_form_op op ->
+      let (bds, f1) = prenex_exists ~bound bds f1 in
       (bds, f_interp_ehoare_form f1 f2)
 
     | _ -> (bds, p)
   in
     (* Make it fail as with destr_exists *)
-    match prenex_exists [] f with
+    match prenex_exists ~bound [] f with
     | [] , _ -> destr_error "exists"
     | bds, f -> (List.rev bds, f)
 

src/ecFol.mli

@@ -149,7 +149,7 @@ val f_real_div_simpl : form -> form -> form
 val f_real_inv_simpl : form -> form
 
 (* -------------------------------------------------------------------- *)
-val destr_exists_prenex : form -> bindings * form
+val destr_exists_prenex : ?bound:int -> form -> bindings * form
 val destr_ands : deep:bool -> form -> form list
 
 (* -------------------------------------------------------------------- *)

src/ecPrinting.ml

@@ -1268,12 +1268,6 @@ let pp_locbinds ppe ?fv vs =
 
   pp_locbinds_blocks ppe ?fv (merge vs)
 
-(* -------------------------------------------------------------------- *)
-let string_of_quant = function
-  | Lforall -> "forall"
-  | Lexists -> "exists"
-  | Llambda -> "fun"
-
 (* -------------------------------------------------------------------- *)
 let string_of_hcmp = function
   | FHle -> "<="

src/phl/ecPhlExists.ml

@@ -24,20 +24,11 @@ let get_to_gens fs =
   List.map do_id fs
 
 (* -------------------------------------------------------------------- *)
-let t_hr_exists_elim_r ?bound tc =
+let t_hr_exists_elim_r ?(bound : int option) (tc : tcenv1) =
   let pre = tc1_get_pre tc in
   let bd, pre =
-    try  destr_exists_prenex pre
+    try  destr_exists_prenex ?bound pre
     with DestrError _ -> [], pre in
-  let bd, pre =
-    bound
-      |> omap (fun bound ->
-             let bound = min bound (List.length bd) in
-             let bd1, bd2 = List.takedrop bound bd in
-
-             (bd1, f_exists bd2 pre))
-      |? (bd, pre) in
-
   let concl = f_forall bd (set_pre ~pre (FApi.tc1_goal tc)) in
   FApi.xmutate1 tc `HlExists [concl]