| 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 =
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
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) =
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
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
*)
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"
| 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
| _ ->
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;;