Generation of inductive and inversion principles for mutual

[helm.git] / components / tactics / inversion_principle.ml

diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml
index 8031e7bbd26b77c027c43fcd3a5e438813010770..1d56cab728770bd9eac6707080dde1b863599d30 100644 (file)
--- a/components/tactics/inversion_principle.ml
+++ b/components/tactics/inversion_principle.ml
@@ -132,70 +132,81 @@ let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*)
 let build_inversion uri obj =
  (*uri e obj of InductiveDefinition *)
  let module PET = ProofEngineTypes in
- let typeno = 0 in
- let name,nleft,arity,cons_list =
-  match obj with
-   Cic.InductiveDefinition (tys,_,nleft,_) ->
-    let (name,_,arity,cons_list) = List.nth tys typeno in 
-    (*we suppose there is only one inductiveType, so typeno=0 identically *)
-    (name,nleft,arity,cons_list)
-  |_ -> assert false
+ let build_one typeno name nleft arity cons_list =
+     (*check if there are right parameters, else return void*)
+     if List.length (list_of_prod arity) = (nleft + 1) then
+       None
+     else
+       try
+        let arity_l = cut_last (list_of_prod arity) in
+        let rightparam_tys = cut_first nleft arity_l in
+        let theorem = build_theorem rightparam_tys arity_l arity cons_list 
+          [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in
+          debug_print 
+            (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
+          let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem  
+            CicUniv.empty_ugraph in
+            (*DEBUG*) debug_print 
+            (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
+            let buri = UriManager.buri_of_uri uri in
+            let inversor_uri = 
+              UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
+            let goal = CicMkImplicit.new_meta metasenv [] in
+            let metasenv' = (goal,[],ref_theorem)::metasenv in
+            let proof= 
+              (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in 
+            let _,applies =
+              List.fold_right
+                (fun _ (i,applies) ->
+                   i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) 
+                cons_list (2,[])
+            in
+            let proof1,gl1 = 
+              PET.apply_tactic
+                (Tacticals.then_
+                   ~start:(PrimitiveTactics.intros_tac ())
+                   (*if the number of applies is 1, we cannot use 
+                     thens, but then_*)
+                   ~continuation:
+                   (match (List.length applies) with
+                        0 -> (Inversion.private_inversion_tac (Cic.Rel 1))
+                      | 1 -> (Tacticals.then_
+                                ~start:(Inversion.private_inversion_tac 
+                                          (Cic.Rel 1))
+                                ~continuation:(PrimitiveTactics.apply_tac 
+                                                 (Cic.Rel 2))
+                             )
+                      | _ -> (Tacticals.thens
+                                ~start:(Inversion.private_inversion_tac 
+                                          (Cic.Rel 1))
+                                ~continuations:applies
+                             )
+                   ))
+                (proof,goal) 
+            in
+            let metasenv,bo,ty =
+              match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty
+            in
+              assert (metasenv = []);
+              Some
+                (inversor_uri,
+                 Cic.Constant 
+                   (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
+       with
+          Inversion.EqualityNotDefinedYet -> None
  in
- (*check if there are right parameters, else return void*)
- if List.length (list_of_prod arity) = (nleft + 1) then
-  None
- else
-  try
-   let arity_l = cut_last (list_of_prod arity) in
-   let rightparam_tys = cut_first nleft arity_l in
-   let theorem = build_theorem rightparam_tys arity_l arity cons_list 
-   [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in
-   (*DEBUG*) debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm 
-    theorem)));
-   let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem  
-   CicUniv.empty_ugraph in
-   (*DEBUG*) debug_print (lazy ("theorem dopo refine: " ^ (CicPp.ppterm 
-    ref_theorem)));
-   let buri = UriManager.buri_of_uri uri in
-   let inversor_uri = 
-    UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
-   let goal = CicMkImplicit.new_meta metasenv [] in
-   let metasenv' = (goal,[],ref_theorem)::metasenv in
-   let proof= (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in 
-   let _,applies =
-    List.fold_right
-     (fun _ (i,applies) ->
-      i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) 
-     cons_list (2,[])
-   in
-   let proof1,gl1 = 
-    PET.apply_tactic
-     (Tacticals.then_
-      ~start:(PrimitiveTactics.intros_tac ())
-      (*if the number of applies is 1, we cannot use thens, but then_*)
-      ~continuation:
-       (match (List.length applies) with
-        0 -> (Inversion.private_inversion_tac (Cic.Rel 1))
-      | 1 -> (Tacticals.then_
-        ~start:(Inversion.private_inversion_tac (Cic.Rel 1))
-        ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
-        )
-      | _ -> (Tacticals.thens
-         ~start:(Inversion.private_inversion_tac (Cic.Rel 1))
-         ~continuations:applies
-        )
-   ))
-   (proof,goal) 
-   in
-   let metasenv,bo,ty =
-    match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty
-   in
-   assert (metasenv = []);
-   Some
-    (inversor_uri,
-    Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
-  with
-   Inversion.EqualityNotDefinedYet -> None
+   match obj with
+     | Cic.InductiveDefinition (tys,_,nleft,_) ->
+         let counter = ref (List.length tys) in
+        List.fold_right 
+          (fun (name,_,arity,cons_list) res ->
+              counter := !counter-1;
+             match build_one !counter name nleft arity cons_list with
+               | None -> res 
+               | Some inv -> inv::res) 
+          tys []
+     |_ -> assert false
+         
 ;;
 
 let init () = ();;