* *)
let coercion_hashtbl = UriManager.UriHashtbl.create 3
-let rec merge_coercions =
- let module C = Cic in
- let aux = (fun (u,t) -> u,merge_coercions t) in
- function
- C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
- | C.Meta (n,subst) ->
- let subst' =
- List.map
- (function None -> None | Some t -> Some (merge_coercions t)) subst
- in
- C.Meta (n,subst')
- | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty)
- | C.Prod (name,so,dest) ->
- C.Prod (name, merge_coercions so, merge_coercions dest)
- | C.Lambda (name,so,dest) ->
- C.Lambda (name, merge_coercions so, merge_coercions dest)
- | C.LetIn (name,so,dest) ->
- C.LetIn (name, merge_coercions so, merge_coercions dest)
- | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when
- CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CoercGraph.target_of c1 in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
- | _ -> assert false) (* the composite coercion must exist *)
- | C.Appl l -> C.Appl (List.map merge_coercions l)
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Var (uri, exp_named_subst)
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Const (uri, exp_named_subst)
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutInd (uri,tyno,exp_named_subst)
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutConstruct (uri,tyno,consno,exp_named_subst)
- | C.MutCase (uri,tyno,out,te,pl) ->
- let pl = List.map merge_coercions pl in
- C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl)
- | C.Fix (fno, fl) ->
- let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in
- C.Fix (fno, fl)
- | C.CoFix (fno, fl) ->
- let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in
- C.CoFix (fno, fl)
-
-let merge_coercions_in_obj obj =
- let module C = Cic in
- match obj with
- | C.Constant (id, body, ty, params, attrs) ->
- let body =
- match body with
- | None -> None
- | Some body -> Some (merge_coercions body)
- in
- let ty = merge_coercions ty in
- C.Constant (id, body, ty, params, attrs)
- | C.Variable (name, body, ty, params, attrs) ->
- let body =
- match body with
- | None -> None
- | Some body -> Some (merge_coercions body)
- in
- let ty = merge_coercions ty in
- C.Variable (name, body, ty, params, attrs)
- | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
- assert false
- | C.InductiveDefinition (indtys, params, leftno, attrs) ->
- let indtys =
- List.map
- (fun (name, ind, arity, cl) ->
- let arity = merge_coercions arity in
- let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in
- (name, ind, arity, cl))
- indtys
- in
- C.InductiveDefinition (indtys, params, leftno, attrs)
-
let uris_of_obj uri =
let innertypesuri = UriManager.innertypesuri_of_uri uri in
let bodyuri = UriManager.bodyuri_of_uri uri in
let univgraphuri = UriManager.univgraphuri_of_uri uri in
innertypesuri,bodyuri,univgraphuri
-let paths_and_uris_of_obj uri ~basedir =
- let basedir = basedir ^ "/xml" in
+let paths_and_uris_of_obj uri =
+ let resolved = Http_getter.filename' ~writable:true uri in
+ let basepath = Filename.dirname resolved in
let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
- let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
- (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
- let innertypespath = basedir ^ "/" ^ innertypesfilename in
- let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri uri) ^ ".xml.gz" in
- let xmlpath = basedir ^ "/" ^ xmlfilename in
- let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
- let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
- let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
- let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
+ let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
+ let innertypespath = basepath ^ "/" ^ innertypesfilename in
+ let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
+ let xmlpath = basepath ^ "/" ^ xmlfilename in
+ let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
+ let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in
+ let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
+ let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri
-let save_object_to_disk ~basedir uri obj ugraph univlist =
+let save_object_to_disk uri obj ugraph univlist =
let ensure_path_exists path =
let dir = Filename.dirname path in
HExtlib.mkdir dir
in
let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri =
- paths_and_uris_of_obj uri basedir
+ paths_and_uris_of_obj uri
in
List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
(* now write to disk *)
(univgraphuri,xmlunivgraphpath) ::
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
- None,None -> []
+ None,_ -> []
| Some bodyxml,Some bodyuri->
ensure_path_exists xmlbodypath;
Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
fun ~dbd ~uri ->
profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-let add_single_obj uri obj ~basedir =
+let add_single_obj uri obj refinement_toolkit =
+ let module RT = RefinementTool in
let obj =
if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
then
- merge_coercions_in_obj obj
+ refinement_toolkit.RT.pack_coercion_obj obj
else
obj
in
index_obj ~dbd ~uri; (* 2 must be in the env *)
try
(*3*)
- let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in
+ let new_stuff = save_object_to_disk uri obj ugraph univlist in
try
HLog.message
(Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
List.iter
(fun uri ->
(try
- let file = Http_getter.resolve' uri in
+ let file = Http_getter.resolve' ~writable:true uri in
HExtlib.safe_remove file;
HExtlib.rmdir_descend (Filename.dirname file)
with Http_getter_types.Key_not_found _ -> ());
(*** GENERATION OF AUXILIARY LEMMAS ***)
-let generate_elimination_principles ~basedir 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 ~basedir;
+ add_single_obj uri obj refinement_toolkit;
uris := uri :: !uris
with CicElim.Can_t_eliminate -> ()
in
UriManager.UriHashtbl.clear coercion_hashtbl;
CoercDb.remove_coercion (fun (_,_,u1) -> true)
-let add_coercion ~basedir ~add_composites uri =
+let add_coercion ~add_composites refinement_toolkit uri =
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
*)
let extract_last_two_p ty =
let rec aux = function
- | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) ->
- assert false
- (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
+ | Cic.Prod( _, _, ((Cic.Prod _) as t)) ->
+ aux t
| Cic.Prod( _, src, tgt) -> src, tgt
| _ -> assert false
in
aux ty
in
+ let already_in =
+ List.exists
+ (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+ (CoercDb.to_list ())
+ in
let ty_src, ty_tgt = extract_last_two_p coer_ty in
- let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
- let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
- let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
- let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
- (* update the DB *)
- List.iter
- (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
- new_coercions;
- CoercDb.add_coercion (src_uri, tgt_uri, uri);
- (* add the composites obj and they eventual lemmas *)
- let lemmas =
- if add_composites then
- List.fold_left
- (fun acc (_,_,uri,obj) ->
- add_single_obj ~basedir uri obj;
- uri::acc)
- composite_uris new_coercions
+ let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
+ let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
+ if not add_composites then
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
+ else
+ let new_coercions =
+ CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ in
+ let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+ if already_in then
+ (* this if starts here just to be sure the closure function works fine *)
+ begin
+ assert (new_coercions = []);
+ HLog.warn
+ (UriManager.string_of_uri uri ^
+ " is already declared as a coercion! skipping...");
+ []
+ end
else
- []
- in
- (* store that composite_uris are related to uri. the first component is the
- * stuff in the DB while the second is stuff for remove_obj *)
- prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composite_uris;
- UriManager.UriHashtbl.add coercion_hashtbl uri
- (composite_uris,if add_composites then composite_uris else []);
- lemmas
+ begin
+ (* update the DB *)
+ List.iter
+ (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
+ new_coercions;
+ CoercDb.add_coercion (src_carr, tgt_carr, uri);
+ (* add the composites obj and they eventual lemmas *)
+ let lemmas =
+ if add_composites then
+ List.fold_left
+ (fun acc (_,_,uri,obj) ->
+ add_single_obj uri obj refinement_toolkit;
+ uri::acc)
+ [] new_coercions
+ else
+ []
+ in
+ (* store that composite_uris are related to uri. the first component is
+ * the stuff in the DB while the second is stuff for remove_obj *)
+ (*
+ prerr_endline ("adding: " ^
+ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composite_uris;
+ *)
+ UriManager.UriHashtbl.add coercion_hashtbl uri
+ (composite_uris,if add_composites then composite_uris else []);
+ (*
+ prerr_endline ("lemmas:");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ lemmas;
+ prerr_endline ("lemmas END");*)
+ lemmas
+ end
+;;
let remove_coercion uri =
try
let (composites_in_db, composites_in_lib) =
UriManager.UriHashtbl.find coercion_hashtbl uri
in
- prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+ (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composites_in_db;
+ composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
(* remove from the DB *)
Not_found -> () (* mhh..... *)
-let generate_projections ~basedir uri fields =
+let generate_projections refinement_toolkit uri fields =
let uris = ref [] in
let projections = CicRecord.projections_of uri (List.map fst fields) in
try
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- add_single_obj ~basedir uri obj;
+ add_single_obj uri obj refinement_toolkit;
let composites =
if coercion then
- add_coercion ~basedir ~add_composites:true uri
+ begin
+ prerr_endline ("composite for " ^ UriManager.string_of_uri uri);
+ let x = add_coercion ~add_composites:true refinement_toolkit uri
+ in
+ prerr_endline ("are: ");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+ prerr_endline "---";
+ x
+ end
else
[]
in
List.iter remove_single_obj !uris;
raise exn
+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]
-let add_obj uri obj ~basedir =
- add_single_obj uri obj ~basedir;
+let add_obj refinement_toolkit uri obj =
+ add_single_obj uri obj refinement_toolkit;
let uris = ref [] in
try
begin
match obj with
| Cic.Constant _ -> ()
| Cic.InductiveDefinition (_,_,_,attrs) ->
- uris := !uris @ generate_elimination_principles ~basedir uri;
+ uris := !uris @
+ generate_elimination_principles uri refinement_toolkit;
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
let rec get_record_attrs =
function
| [] -> None
(match get_record_attrs attrs with
| None -> () (* not a record *)
| Some fields ->
- uris := !uris @ (generate_projections ~basedir uri fields))
+ uris := !uris @
+ (generate_projections refinement_toolkit uri fields))
| Cic.CurrentProof _
| Cic.Variable _ -> assert false
end;
projects / helm.git / blobdiff