Fix why3 tactic (WIP)

src/common/debug.ml

@@ -26,7 +26,7 @@ module D = struct
     | Some x -> out ppf "Some(%a)" elt x
 
   let pair : 'a pp -> 'b pp -> ('a * 'b) pp = fun elt1 elt2 ppf (x1,x2) ->
-    out ppf "%a,%a" elt1 x1 elt2 x2
+    out ppf "(%a,%a)" elt1 x1 elt2 x2
 
   let list : 'a pp -> 'a list pp = fun elt ppf l ->
     match l with

src/handle/fol.ml

@@ -1,15 +1,18 @@
 (** Configuration for tactics based on first-order logic. *)
 
-open Common
+open Common open Error
 open Core open Term
 
 (** Builtin configuration for propositional logic. *)
 type config =
-  { symb_P   : sym (** Encoding of propositions. *)
+  { symb_Prop: sym (** Type of propositions. *)
+  ; symb_P   : sym (** Encoding of propositions. *)
+  ; symb_Set : sym (** Type of sets. *)
   ; symb_T   : sym (** Encoding of types. *)
   ; symb_or  : sym (** Disjunction(∨) symbol. *)
   ; symb_and : sym (** Conjunction(∧) symbol. *)
   ; symb_imp : sym (** Implication(⇒) symbol. *)
+  ; symb_eqv : sym (** Equivalence(⇔) symbol. *)
   ; symb_bot : sym (** Bot(⊥) symbol. *)
   ; symb_top : sym (** Top(⊤) symbol. *)
   ; symb_not : sym (** Not(¬) symbol. *)
@@ -19,11 +22,38 @@ type config =
 (** [get_config ss pos] build the configuration using [ss]. *)
 let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos ->
   let builtin = Builtin.get ss pos in
-  { symb_P   = builtin "P"
-  ; symb_T   = builtin "T"
+  let symb_P = builtin "P" and symb_T = builtin "T" in
+  let symb_Prop =
+    match unfold Timed.(!(symb_P.sym_type)) with
+    | Prod(a,_) ->
+        begin
+          match unfold a with
+          | Symb s -> s
+          | _ ->
+              fatal pos "The type of %a is not of the form Prop → _ \
+                         with Prop a symbol." Print.sym symb_P
+        end
+    | _ -> fatal pos "The type of %a is not a product" Print.sym symb_P
+  and symb_Set =
+    match unfold Timed.(!(symb_T.sym_type)) with
+    | Prod(a,_) ->
+        begin
+          match unfold a with
+          | Symb s -> s
+          | _ ->
+              fatal pos "The type of %a is not of the form Prop → _ \
+                         with Prop a symbol." Print.sym symb_T
+        end
+    | _ -> fatal pos "The type of %a is not a product" Print.sym symb_T
+  in
+  { symb_Prop
+  ; symb_P
+  ; symb_Set
+  ; symb_T
   ; symb_or  = builtin "or"
   ; symb_and = builtin "and"
   ; symb_imp = builtin "imp"
+  ; symb_eqv = builtin "eqv"
   ; symb_bot = builtin "bot"
   ; symb_top = builtin "top"
   ; symb_not = builtin "not"

src/handle/rewrite.ml

@@ -30,7 +30,7 @@ let get_eq_config : Sig_state.t -> popt -> eq_config = fun ss pos ->
 
 (* Register checks for the builtin symbols related to rewriting. *)
 let _ =
-  let check_t_or_p _ss pos sym =
+  let check_codomain_is_Type _ss pos sym =
     let valid =
       match Eval.whnf [] !(sym.sym_type) with
       | Prod(_, b) -> Eval.eq_modulo [] (snd (Bindlib.unbind b)) mk_Type
@@ -40,9 +40,9 @@ let _ =
       fatal pos "The type of [%s] is not of the form [_ → TYPE]." sym.sym_name
   in
   (* The type of the builtin ["T"] should be [U → TYPE]. *)
-  Builtin.register "T" check_t_or_p;
+  Builtin.register "T" check_codomain_is_Type;
   (* The type of the builtin ["P"] should be [Prop → TYPE]. *)
-  Builtin.register "P" check_t_or_p;
+  Builtin.register "P" check_codomain_is_Type;
   let get_domain_of_type s =
     match Eval.whnf [] !(s.sym_type) with
     | Prod(a,_) -> a
@@ -109,7 +109,7 @@ let _ =
 (** [get_eq_data pos cfg a] returns [((a,l,r),[v1;..;vn])] if [a ≡ Π v1:A1,
    .., Π vn:An, P (eq a l r)] and fails otherwise. *)
 let get_eq_data :
-  eq_config -> popt -> term -> (term * term * term) * tvar array = fun cfg ->
+  eq_config -> popt -> term -> (term * term * term) * tvar list = fun cfg ->
   let exception Not_eq of term in
   let get_eq_args u =
     if Logger.log_enabled () then log_rewr "get_eq_args %a" term u;
@@ -118,14 +118,14 @@ let get_eq_data :
     | _ -> raise (Not_eq u)
   in
   let exception Not_P of term in
-  let return vs r = r, Array.of_list (List.rev vs) in
+  let return vs r = r, List.rev vs in
   let rec get_eq vs t notin_whnf =
     if Logger.log_enabled () then log_rewr "get_eq %a" term t;
     match get_args t with
     | Prod(_,t), _ -> let v,t = Bindlib.unbind t in get_eq (v::vs) t true
     | p, [u] when is_symb cfg.symb_P p ->
       begin
-        let u = Eval.whnf ~tags:[`NoRw; `NoExpand] [] u in
+        let u = Eval.whnf ~tags:[`NoRw;`NoExpand] [] u in
         try return vs (get_eq_args u)
         with Not_eq _ ->
           (try return vs (get_eq_args (Eval.whnf [] u))
@@ -327,7 +327,8 @@ let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool ->
   let (t, t_type) = Query.infer pos p g_ctxt t in
 
   (* Check that [t_type ≡ Π x1:a1, ..., Π xn:an, P (eq a l r)]. *)
-  let (a, l, r), vars  = get_eq_data cfg pos t_type in
+  let (a, l, r), vars = get_eq_data cfg pos t_type in
+  let vars = Array.of_list vars in
 
   (* Apply [t] to the variables of [vars] to get a witness of the equality. *)
   let t = Array.fold_left (fun t x -> mk_Appl(t, mk_Vari x)) t vars in

src/handle/tactic.ml

@@ -185,6 +185,33 @@ let count_products : ctxt -> term -> int = fun c ->
     | _ -> acc
   in count 0
 
+(** [get_prod_ids env do_whnf t] returns the list [v1;..;vn] if [do_whnf] is
+    true and [whnf t] is of the form [Π v1:A1, .., Π vn:An, u] with [u] not a
+    product, or if [do_whnf] is false and [t] is of the form [Π v1:A1, .., Π
+    vn:An, u] with [u] not a product. *)
+let get_prod_ids env =
+  let rec aux acc do_whnf t =
+    match get_args t with
+    | Prod(_,b), _ ->
+        let x,b = Bindlib.unbind b in
+        aux (Bindlib.name_of x::acc) do_whnf b
+    | _ ->
+        if do_whnf then aux acc false (Eval.whnf (Env.to_ctxt env) t)
+        else List.rev acc
+  in aux []
+
+(** [gen_valid_idopts env ids] generates a list of pairwise distinct
+    identifiers distinct from those of [env] to replace [ids]. *)
+let gen_valid_idopts env ids =
+  let add_decl ids (s,_) = Extra.StrSet.add s ids in
+  let idset = ref (List.fold_left add_decl Extra.StrSet.empty env) in
+  let f id idopts =
+    let id = Extra.get_safe_prefix id !idset in
+    idset := Extra.StrSet.add id !idset;
+    Some(Pos.none id)::idopts
+  in
+  List.fold_right f ids []
+
 (** [handle ss sym_pos prv ps tac] applies tactic [tac] in the proof state
    [ps] and returns the new proof state. *)
 let rec handle :
@@ -209,26 +236,17 @@ let rec handle :
   | Unif _ -> fatal pos "Not a typing goal."
   | Typ ({goal_hyps=env;_} as gt) ->
   let scope t = Scope.scope_term ~mok:(Proof.meta_of_key ps) prv ss env t in
+  (* Function to apply the assume tactic several times without checking the
+     validity of identifiers. *)
+  let assume idopts =
+    match idopts with
+    | [] -> ps
+    | _ -> tac_refine pos ps gt gs (new_problem())
+             (scope (P.abst_list idopts P.wild))
+  in
   (* Function for checking that an identifier is not already in use. *)
   let check id =
     if Env.mem id.elt env then fatal id.pos "Identifier already in use." in
-  (* Function to apply [n] times the assume tactic. *)
-  let assume n =
-    if n <= 0 then ps
-    else
-      let add_decl strings (s,_) = Extra.StrSet.add s strings in
-      let strings = List.fold_left add_decl Extra.StrSet.empty env in
-      let h = Extra.get_safe_prefix "h" strings in
-      let rec mk_idopts acc k =
-        if k <= 0 then acc
-        else
-          let idopt = Some (Pos.make pos (h ^ string_of_int k)) in
-          mk_idopts (idopt::acc) (k-1)
-      in
-      let t = P.abst_list (mk_idopts [] n) P.wild in
-      let p = new_problem() in
-      tac_refine pos ps gt gs p (scope t)
-  in
   match elt with
   | P_tac_fail
   | P_tac_query _
@@ -257,8 +275,7 @@ let rec handle :
       List.iter (Option.iter check) idopts;
       (* Check that the given identifiers are pairwise distinct. *)
       Syntax.check_distinct_idopts idopts;
-      let p = new_problem() in
-      tac_refine pos ps gt gs p (scope (P.abst_list idopts P.wild))
+      assume idopts
   | P_tac_generalize {elt=id; pos=idpos} ->
       (* From a goal [e1,id:a,e2 ⊢ ?[e1,id,e2] : u], generate a new goal [e1 ⊢
          ?m[e1] : Π id:a, Π e2, u], and refine [?[e]] with [?m[e1] id e2]. *)
@@ -330,20 +347,19 @@ let rec handle :
   | P_tac_induction -> tac_induction pos ps gt gs
   | P_tac_refine t -> tac_refine pos ps gt gs (new_problem()) (scope t)
   | P_tac_refl ->
-      let cfg = Rewrite.get_eq_config ss pos in
-      let (a,l,_), vs = Rewrite.get_eq_data cfg pos gt.goal_type in
-      (* We first do [n] times the [assume] tactic. *)
-      let ps = assume (Array.length vs) in
-      (* We then apply reflexivity. *)
-      begin match ps.proof_goals with
-      | Typ gt::gs ->
-        let a,l =
-          if Array.length vs = 0 then a,l
-          else let (a,l,_),_ = Rewrite.get_eq_data cfg pos gt.goal_type in a,l
-        in
-        let prf = add_args (mk_Symb cfg.symb_refl) [a; l] in
-        tac_refine pos ps gt gs (new_problem()) prf
-      | _ -> assert false
+      begin
+        let cfg = Rewrite.get_eq_config ss pos in
+        let _,vs = Rewrite.get_eq_data cfg pos gt.goal_type in
+        let idopts = gen_valid_idopts env (List.map Bindlib.name_of vs) in
+        let ps = assume idopts in
+        match ps.proof_goals with
+        | [] -> assert false
+        | Unif _::_ -> assert false
+        | Typ gt::gs ->
+            let cfg = Rewrite.get_eq_config ss pos in
+            let (a,l,_),_ = Rewrite.get_eq_data cfg pos gt.goal_type in
+            let prf = add_args (mk_Symb cfg.symb_refl) [a; l] in
+            tac_refine pos ps gt gs (new_problem()) prf
       end
   | P_tac_remove ids ->
       (* Remove hypothesis [id] in goal [g]. *)
@@ -389,27 +405,26 @@ let rec handle :
         (Rewrite.rewrite ss p pos gt l2r pat (scope eq))
   | P_tac_sym ->
       let cfg = Rewrite.get_eq_config ss pos in
-      let (a,l,r), vs = Rewrite.get_eq_data cfg pos gt.goal_type in
-      let a,l,r =
-        if Array.length vs = 0 then a,l,r
-        else fst (Rewrite.get_eq_data cfg pos gt.goal_type)
-      in
+      let (a,l,r),_ = Rewrite.get_eq_data cfg pos gt.goal_type in
       let p = new_problem() in
       let prf =
-        let mt =
-          mk_Appl(mk_Symb cfg.symb_P,
-                  add_args (mk_Symb cfg.symb_eq) [a; r; l]) in
+        let mt = mk_Appl(mk_Symb cfg.symb_P,
+                         add_args (mk_Symb cfg.symb_eq) [a;r;l]) in
         let meta_term = LibMeta.make p (Env.to_ctxt env) mt in
         (* The proofterm is [eqind a r l M (λx,eq a l x) (refl a l)]. *)
         Rewrite.swap cfg a r l meta_term
       in
       tac_refine pos ps gt gs p prf
   | P_tac_why3 cfg ->
-      let ps = assume (count_products (Env.to_ctxt env) gt.goal_type) in
-      (match ps.proof_goals with
-       | Typ gt::_ ->
-         Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
-       | _ -> assert false)
+      begin
+        let ids = get_prod_ids env false gt.goal_type in
+        let idopts = gen_valid_idopts env ids in
+        let ps = assume idopts in
+        match ps.proof_goals with
+        | Typ gt::_ ->
+            Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
+        | _ -> assert false
+      end
   | P_tac_try tactic ->
     try handle ss sym_pos prv ps tactic
     with Fatal(_, _s) -> ps