let typecheck_obj =
let profiler = HExtlib.profile "add_obj.typecheck_obj" in
- fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
+ fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri)
+ (Unshare.fresh_types obj)
let index_obj =
let profiler = HExtlib.profile "add_obj.index_obj" in
(* EXPERIMENTAL: pretty print the object in natural language *)
(try !object_declaration_hook uri obj
with exc ->
- prerr_endline "Error: object_declaration_hook failed");
+ prerr_endline ("Error: object_declaration_hook failed"^
+ Printexc.to_string exc));
try
HLog.message
(Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
List.iter remove_single_obj !uris;
raise exn
in
- let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+ let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
match obj with
| Cic.InductiveDefinition (indTypes, _, _, _) ->
let counter = ref 0 in
UriManager.UriHashtbl.clear coercion_hashtbl;
CoercDb.remove_coercion (fun (_,_,_,_) -> true)
+let stack = ref [];;
+
+let h2l h =
+ UriManager.UriHashtbl.fold
+ (fun k v acc -> (k,v) :: acc) h []
+;;
+
+let push () =
+ stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
+ remove_all_coercions ()
+;;
+
+let pop () =
+ match !stack with
+ | [] -> raise (Failure "Unable to POP from librarySync.ml")
+ | (db,h) :: tl ->
+ stack := tl;
+ remove_all_coercions ();
+ CoercDb.restore db;
+ List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
+ h
+;;
+
let add_coercion ~add_composites refinement_toolkit uri arity saturations
baseuri
=
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
- CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph
in
(* we have to get the source and the tgt type uri
* in Coq syntax we have already their names, but
(fun (uri, name, bo) (_name, coercion, arity) ->
let saturations = 0 in
try
- let ty, ugraph =
- CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
add_single_obj uri obj refinement_toolkit;
generate_sibling_mutual_definitions refinement_toolkit uri attrs
name bo
| Cic.Constant _ -> ()
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- uris := !uris @
- generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit uri obj;
- let rec get_record_attrs =
- function
- | [] -> None
- | (`Class (`Record fields))::_ -> Some fields
- | _::tl -> get_record_attrs tl
- in
- (match get_record_attrs attrs with
- | None -> () (* not a record *)
- | Some fields ->
- uris := !uris @
- (generate_projections refinement_toolkit uri fields))
+ | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
+ let _,inductive,_,_ = List.hd inductivefuns in
+ if inductive then
+ begin
+ uris := !uris @
+ generate_elimination_principles uri refinement_toolkit;
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
+ end ;
+ let rec get_record_attrs =
+ function
+ | [] -> None
+ | (`Class (`Record fields))::_ -> Some fields
+ | _::tl -> get_record_attrs tl
+ in
+ (match get_record_attrs attrs with
+ | None -> () (* not a record *)
+ | Some fields ->
+ uris := !uris @
+ (generate_projections refinement_toolkit uri fields))
| Cic.CurrentProof _
| Cic.Variable _ -> assert false
end;