X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=9f3bda42304490f51701271d8f83e54c27aa675c;hb=5d917dca1e20e201ada174da2c36796f73a24623;hp=fb3c0655cf49c1450449a250c7095fa50094d2e6;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index fb3c0655c..9f3bda423 100644
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -150,14 +150,20 @@ let rec mk_rels consno = function
   | 0 -> []
   | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1)
 
-let rec strip_pi = function
-  | Cic.Prod (_, _, tgt) -> strip_pi tgt
+let rec strip_pi ctx t = 
+  match CicReduction.whd ~delta:true ctx t with
+  | Cic.Prod (n, s, tgt) -> strip_pi (Some (n,Cic.Decl s) :: ctx) tgt
   | t -> t
 
-let rec count_pi = function
-  | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
+let strip_pi t = strip_pi [] t
+
+let rec count_pi ctx t = 
+  match CicReduction.whd ~delta:true ctx t with
+  | Cic.Prod (n, s, tgt) -> count_pi (Some (n,Cic.Decl s)::ctx) tgt + 1
   | t -> 0
 
+let count_pi t = count_pi [] t
+
 let rec type_of_p sort dependent leftno indty = function
   | Cic.Prod (n, src, tgt) when leftno = 0 ->
       let n =
@@ -217,7 +223,7 @@ let rec branch (uri, typeno) insource paramsno t fix head args =
       if insource then
         (match args with
         | [arg] -> Cic.Appl (fix :: args)
-        | _ -> Cic.Appl (head :: [Cic.Appl args]))
+        | _ -> Cic.Appl (fix :: [Cic.Appl args]))
       else
         (match args with
         | [] -> head
@@ -259,7 +265,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
 
 let elim_of ~sort uri typeno =
   counter := ~-1;
-  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+  let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
   match obj with
   | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
       let (name, inductive, ty, constructors) =
@@ -267,6 +273,10 @@ let elim_of ~sort uri typeno =
           List.nth indTypes typeno
         with Failure _ -> assert false
       in
+      let ty = Unshare.unshare ~fresh_univs:true ty in
+      let constructors = 
+        List.map (fun (name,c)-> name,Unshare.unshare ~fresh_univs:true c) constructors 
+      in
       let paramsno = count_pi ty in (* number of (left or right) parameters *)
       let rightno = paramsno - leftno in
       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
@@ -357,7 +367,7 @@ let elim_of ~sort uri typeno =
             in
             (* rightno is the decreasing argument, i.e. the argument of
              * inductive type *)
-            Cic.Fix (0, ["f", rightno, final_ty, fixfun])
+            Cic.Fix (0, ["aux", rightno, final_ty, fixfun])
           else
             add_right_lambda dependent leftno (conslen + 1) 1 rightno indty
               mutcase ty
@@ -390,7 +400,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
 *)
       let (computed_type, ugraph) =
         try
-          CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
+          CicTypeChecker.type_of_aux' [] [] eliminator_body
+          CicUniv.oblivion_ugraph
         with CicTypeChecker.TypeCheckerFailure msg ->
           raise (Elim_failure (lazy (sprintf 
             "type checker failure while type checking:\n%s\nerror:\n%s"
@@ -409,7 +420,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
@@ -418,4 +430,32 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
   | _ ->
       failwith (sprintf "not an inductive definition (%s)"
         (UriManager.string_of_uri uri))
+;;
+
+let generate_elimination_principles ~add_obj ~add_coercion uri obj =
+ match obj with
+  | Cic.InductiveDefinition (indTypes,_,_,attrs) ->
+     let _,inductive,_,_ = List.hd indTypes in
+     if not inductive then []
+     else
+      let _,all_eliminators =
+        List.fold_left
+          (fun (i,res) _ ->
+            let elim sort =
+              try Some (elim_of ~sort uri i)
+              with Can_t_eliminate -> None
+            in
+             i+1,
+              HExtlib.filter_map 
+               elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] @ res
+          ) (0,[]) indTypes
+      in
+      List.fold_left
+        (fun lemmas (uri,obj) -> add_obj uri obj @ uri::lemmas) 
+        [] all_eliminators
+  | _ -> []
+;;
+
 
+let init () = 
+  LibrarySync.add_object_declaration_hook generate_elimination_principles;;