fix #22 Add arguments to induction_pr_arg

Also fix induction_pr_arg so that it adds the right attribute inside the
goal.

CHANGES.md

@@ -25,6 +25,8 @@ Transformations
   * Fix crash of eliminate_unknown_types
   * Giving too many arguments to a transformation do not display a popup anymore
   * Fix behavior of induction_arg_ty_lex (now equivalent to induction_ty_lex)
+  * Add optional arguments to induction_arg_pr (containing what is to be
+  generalized in the induction). Also, fixing its behavior.
 
 Counterexamples
   * Improved display of counterexamples in Task view

src/transform/args_wrapper.ml

@@ -512,6 +512,11 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
             let list =
               List.map (fun id -> id.Ptree.id_str) (parse_list_ident s') in
             wrap_to_store t' (f (Some list)) tail env tables task
+        | Tlist t' ->
+            let pr_list = parse_list_qualid s' in
+            let pr_list =
+              List.map (fun id -> find_symbol id tables) pr_list in
+            wrap_to_store t' (f (Some pr_list)) tail env tables task
         | _ -> raise (Arg_expected (string_of_trans_typ t', s'))
        end
     | Topt (_, t'), _ ->

src/transform/ind_itp.ml

@@ -76,22 +76,30 @@ let revert ?tr g d : Term.term =
   | Ddata _ -> raise (Arg_trans "revert: cannot revert type")
   | Dparam ls ->
     (try
-       let attrs = match tr with
+       let attrs = Opt.map (fun x -> Ident.Sattr.add x Ident.Sattr.empty) (match tr with
          | None -> None
-         | Some tr -> Some (tr ls) in
+         | Some tr -> tr (Tslsymbol ls)) in
        let new_ident = Ident.id_fresh ?attrs ls.ls_name.Ident.id_string in
        let new_var = Term.create_vsymbol new_ident (Opt.get ls.Term.ls_value) in
        let g = t_replace (t_app_infer ls []) (t_var new_var) g in
        t_forall_close [new_var] [] g
      with
-     | e -> raise (Arg_trans ("revert: cannot revert:" ^ ls.ls_name.Ident.id_string)))
+     | _ -> raise (Arg_trans ("revert: cannot revert:" ^ ls.ls_name.Ident.id_string)))
   (* TODO extend this *)
   | Dlogic _ ->
     raise (Arg_trans "revert: cannot revert logic decls")
   | Dind _ ->
     raise (Arg_trans "revert: cannot revert induction decls")
-  | Dprop (k, _pr, t) when k <> Pgoal ->
-    Term.t_implies t g
+  | Dprop (k, pr, t) when k <> Pgoal ->
+      let t = match tr with
+      | None -> t
+      | Some tr ->
+          begin match tr (Tsprsymbol pr) with
+          | None -> t
+          | Some attr -> t_attr_add attr t
+          end
+      in
+      Term.t_implies t g
   | Dprop (Pgoal, _, _) -> raise (Arg_trans "revert: cannot revert goal")
   | _ -> raise (Arg_trans "revert: please report")
 

src/transform/ind_itp.mli

@@ -9,10 +9,10 @@
 (*                                                                  *)
 (********************************************************************)
 
-(* [tr] gives a function that gives a set of attributes to the fresh elements
-   generated during the revert. It allows in particular to add [@induction] for
-   induction_ty_lex.
+(* [tr] is a function that associates a symbol of the task with an attribute.
+   This is used to add new attributes (such as @induction) on some quantified
+   variables (see induction_arg_pr).
 *)
 val revert_tr_symbol:
-  ?tr:(Term.lsymbol -> Ident.Sattr.t) ->
+  ?tr:(Args_wrapper.symbol -> Ident.attribute option) ->
     Args_wrapper.symbol list -> Task.task Trans.trans

src/transform/induction.ml

@@ -349,13 +349,13 @@ let () =
 
 let induction_on_hyp ls =
   (* We add the induction attribute on the reverted symbol *)
-  let tr = Some
-      (fun s -> (* Add induction attribute *only* on ls *)
-         if ls_equal s ls then
-           Ident.Sattr.singleton (create_attribute "induction")
-         else Ident.Sattr.empty)
+  let tr s = (* Add induction attribute *only* on ls *)
+    match s with
+    | Tslsymbol s when ls_equal s ls ->
+        Some attr_ind
+    | _ -> None
   in
-  Trans.compose (Ind_itp.revert_tr_symbol ?tr [Tslsymbol ls])
+  Trans.compose (Ind_itp.revert_tr_symbol ~tr [Tslsymbol ls])
     (Trans.store induction_ty_lex)
 
 let () = wrap_and_register

src/transform/induction_pr.ml

@@ -224,21 +224,31 @@ let induction_l attr induct task = match task with
     with Ind_not_found -> [task] end
   | _ -> assert false
 
-let induction_on_hyp attr b h =
-  Trans.compose (Ind_itp.revert_tr_symbol [Tsprsymbol h])
+let induction_on_hyp attr b h list_hyp_opt =
+  let l = match list_hyp_opt with
+  | None -> [Tsprsymbol h]
+  | Some l -> Tsprsymbol h :: l in
+  let tr x = match x with
+  | Tsprsymbol pr when Decl.pr_equal pr h -> Some attr
+  | _ -> None in
+  Trans.compose (Ind_itp.revert_tr_symbol ~tr l)
     (Trans.store (induction_l attr b))
 
 let () = wrap_and_register
     ~desc:"induction_arg_pr <name>@ \
-      performs@ 'induction_pr'@ on@ the@ given@ premise."
+      performs@ 'induction_pr'@ on@ the@ given@ premise. Optional@ <with_gen>@ \
+      arguments@ are@ the@ elements@ to@ be@ generalized@."
     "induction_arg_pr"
-    (Tprsymbol Ttrans_l) (induction_on_hyp attr_ind true)
+    (Tprsymbol (Topt ("with_gen", Tlist Ttrans_l)))
+    (induction_on_hyp attr_ind true)
 
 let () = wrap_and_register
     ~desc:"inversion_arg_pr <name>@ \
-      performs@ 'inversion_pr'@ on@ the@ given@ premise."
+      performs@ 'inversion_pr'@ on@ the@ given@ premise. Optional@ <with_gen>@ \
+      arguments@ are@ the@ elements@ to@ be@ generalized@."
     "inversion_arg_pr"
-    (Tprsymbol Ttrans_l) (induction_on_hyp attr_inv false)
+    (Tprsymbol (Topt ("with_gen", Tlist Ttrans_l)))
+    (induction_on_hyp attr_inv false)
 
 let () =
   Trans.register_transform_l "induction_pr"