Generation of inductive and inversion principles for mutual

inductive types (before only single types were allowed).

diff --git a/components/library/cicElim.ml b/components/library/cicElim.ml
index fb3c0655cf49c1450449a250c7095fa50094d2e6..f919d2875e2d7674ff4b4d13facae24a47ffd1c9 100644 (file)
--- a/components/library/cicElim.ml
+++ b/components/library/cicElim.ml
@@ -409,7 +409,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
         | Cic.Type _ -> "_rect"
         | _ -> assert false
       in
-      let name = UriManager.name_of_uri uri ^ suffix in
+      (* let name = UriManager.name_of_uri uri ^ suffix in *)
+      let name = name ^ suffix in
       let buri = UriManager.buri_of_uri uri in
       let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
       let obj_attrs = [`Class (`Elim sort); `Generated] in

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index e1b73821bc6176014ca5c55bb30474858b126f30..1db8f0cfc2c7b8374b79ae334ef068da0cab6c83 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -178,19 +178,30 @@ let remove_single_obj uri =
 
 let generate_elimination_principles uri refinement_toolkit =
   let uris = ref [] in
-  let elim sort =
-    try
-      let uri,obj = CicElim.elim_of ~sort uri 0 in
-       add_single_obj uri obj refinement_toolkit;
-       uris := uri :: !uris
-    with CicElim.Can_t_eliminate -> ()
+  let elim i =
+    let elim sort =
+      try
+       let uri,obj = CicElim.elim_of ~sort uri i in
+         add_single_obj uri obj refinement_toolkit;
+         uris := uri :: !uris
+      with CicElim.Can_t_eliminate -> ()
+    in
+      try
+       List.iter 
+         elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+      with exn ->
+       List.iter remove_single_obj !uris;
+       raise exn 
   in
-  try
-    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
-    !uris
-  with exn ->
-   List.iter remove_single_obj !uris;
-   raise exn
+  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+    match obj with
+      | Cic.InductiveDefinition (indTypes, _, _, _) ->
+         let counter = ref 0 in
+           List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
+           !uris
+      | _  -> 
+         failwith (Printf.sprintf "not an inductive definition (%s)"
+                     (UriManager.string_of_uri uri))
 
 (* COERCIONS ***********************************************************)
   
@@ -350,11 +361,10 @@ let generate_projections refinement_toolkit uri fields =
 let build_inversion_principle = ref (fun a b -> assert false);;
 
 let generate_inversion refinement_toolkit uri obj =
- match !build_inversion_principle uri obj with
-    None -> []
-  | Some (ind_uri,ind_obj) ->
-     add_single_obj ind_uri ind_obj refinement_toolkit;
-     [ind_uri]
+  List.map 
+    (fun (ind_uri,ind_obj) -> 
+       add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
+    (!build_inversion_principle uri obj)
 
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;

diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli
index b29a0aa0342b33442b57272f144556029cc24d46..61e2b2515ae9ba36837b142427cfd508b12014a5 100644 (file)
--- a/components/library/librarySync.mli
+++ b/components/library/librarySync.mli
@@ -26,7 +26,7 @@
 exception AlreadyDefined of UriManager.uri
 
 (* this is a pointer to the function which builds the inversion principle *)
-val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) option) ref
+val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref
 
 (* adds an object to the library together with all auxiliary lemmas on it *)
 (* (e.g. elimination principles, projections, etc.)                       *)

diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index 74117f7109dd596602e0d1ee26a23c7a1cd132da..e381b3003d7b4940eba1b0886c007922066211d0 100644 (file)
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -306,14 +306,17 @@ let inversion_tac ~term =
   let (_,metasenv,_,_) = proof in
   let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
   let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-  let uri = baseuri_of_term termty in  
+  let uri, typeno = 
+    match termty with
+      | Cic.MutInd (uri,typeno,_) 
+      | Cic.Appl(Cic.MutInd (uri,typeno,_)::_) -> uri,typeno
+      | _ -> assert false
+  in
+  (* let uri = baseuri_of_term termty in *)
   let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   let name,nleft,arity,cons_list =
    match obj with
     Cic.InductiveDefinition (tys,_,nleft,_) ->
-     (*we suppose there is only one inductiveType in the definition, 
-     so typeno=0 identically *)
-     let typeno = 0 in
      let (name,_,arity,cons_list) = List.nth tys typeno in 
         (name,nleft,arity,cons_list)
    |_ -> assert false

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 () = ();;