* *)
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
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 ~basedir =
+ 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
(*** GENERATION OF AUXILIARY LEMMAS ***)
-let generate_elimination_principles ~basedir uri =
+let generate_elimination_principles ~basedir 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 ~basedir;
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 ~basedir ~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 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 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
+ 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
(* 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);
+ 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 ~basedir uri obj;
+ add_single_obj ~basedir uri obj refinement_toolkit;
uri::acc)
composite_uris 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 ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composite_uris;
+ (*
+ 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 []);
lemmas
Not_found -> () (* mhh..... *)
-let generate_projections ~basedir uri fields =
+let generate_projections ~basedir 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 ~basedir uri obj refinement_toolkit;
let composites =
if coercion then
- add_coercion ~basedir ~add_composites:true uri
+ add_coercion ~basedir ~add_composites:true refinement_toolkit uri
else
[]
in
raise exn
-let add_obj uri obj ~basedir =
- add_single_obj uri obj ~basedir;
+let add_obj refinement_toolkit uri obj ~basedir =
+ add_single_obj uri obj refinement_toolkit ~basedir;
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 ~basedir uri refinement_toolkit;
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 ~basedir refinement_toolkit uri fields))
| Cic.CurrentProof _
| Cic.Variable _ -> assert false
end;
projects / helm.git / blobdiff