let typecheck_obj =
let profiler = HExtlib.profile "add_obj.typecheck_obj" in
- fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri)
- (Unshare.fresh_types obj)
+ fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
let index_obj =
let profiler = HExtlib.profile "add_obj.index_obj" in
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 (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
- then
- refinement_toolkit.RT.pack_coercion_obj obj
- else
- obj
+ if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
+ then refinement_toolkit.RT.pack_coercion_obj obj
+ else obj
in
let dbd = LibraryDb.instance () in
if CicEnvironment.in_library uri then
(Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n"
(univ_time *. 100. /. total_time) (total_time) (univ_time)
(UriManager.name_of_uri uri));*)
- let _, ugraph, univlist =
- CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+ let obj, ugraph, univlist =
+ try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri
+ with CicEnvironment.Object_not_found _ -> assert false
+ in
try
index_obj ~dbd ~uri; (* 2 must be in the env *)
try
let remove_all_coercions () =
UriManager.UriHashtbl.clear coercion_hashtbl;
- CoercDb.remove_coercion (fun (_,_,_,_) -> true)
+ CoercDb.remove_coercion (fun _ -> true)
let stack = ref [];;
in
aux ty
in
- let src_carr, tgt_carr =
+ let src_carr, tgt_carr, no_args =
let get_classes arity saturations l =
(* this is the ackerman's function revisited *)
let rec aux = function
in
let types = spine2list coer_ty in
let src,tgt = get_classes arity saturations types in
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- match tgt with
- None -> assert false
- | Some `Funclass -> CoercDb.Fun arity
- | Some (`Class tgt) ->
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
+ (match tgt with
+ | None -> assert false
+ | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
+ | Some (`Class tgt) ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
+ List.length types - 1
in
let already_in_obj src_carr tgt_carr uri obj =
List.exists
(fun (s,t,ul) ->
List.exists
- (fun u,_ ->
+ (fun u,_,_ ->
let bo =
match obj with
| Cic.Constant (_, Some bo, _, _, _) -> bo
ul)
(CoercDb.to_list ())
in
+ let cpos = no_args - arity - saturations - 1 in
if not add_composites then
- (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
[])
else
baseuri
in
let new_coercions =
- List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
+ List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
new_coercions
in
- let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
+ let composite_uris =
+ List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions
+ in
(* update the DB *)
List.iter
- (fun (src,tgt,uri,saturations,_,_) ->
- CoercDb.add_coercion (src,tgt,uri,saturations))
+ (fun (src,tgt,uri,saturations,_,_,cpos) ->
+ CoercDb.add_coercion (src,tgt,uri,saturations,cpos))
new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
(* add the composites obj and they eventual lemmas *)
let lemmas =
List.fold_left
- (fun acc (_,tgt,uri,saturations,obj,arity) ->
+ (fun acc (_,tgt,uri,saturations,obj,arity,cpos) ->
add_single_obj uri obj refinement_toolkit;
- (uri,arity,saturations)::acc)
+ (uri,arity,saturations,cpos)::acc)
[] new_coercions
in
(* store that composite_uris are related to uri. the first component is
composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion
- (fun (_,_,u,_) -> UriManager.eq uri u);
+ (fun (_,_,u,_,_) -> UriManager.eq uri u);
(* remove from the DB *)
List.iter
- (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
+ (fun u ->
+ CoercDb.remove_coercion (fun (_,_,u1,_,_) -> UriManager.eq u u1))
composites_in_db;
(* remove composites from the lib *)
List.iter remove_single_obj composites_in_lib
prerr_endline "---";
*)
(*CSC: I throw the arity away. See comment above *)
- List.map (fun u,_,_ -> u) x
+ List.map (fun u,_,_,_ -> u) x
end
else
[]
List.fold_right
(fun (name,idx,ty,bo) (n,uris) ->
if name = name_to_avoid then
- (n+1,uris)
+ (n-1,uris)
else
let uri =
UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
- let bo = Cic.Fix (n,funs) in
+ let bo = Cic.Fix (n-1,funs) in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- add_single_obj uri obj refinement_toolkit;
- (n+1,uri::uris)
- ) funs (1,[]))
+ (add_single_obj uri obj refinement_toolkit;
+ (n-1,uri::uris)))
+ funs (List.length funs,[]))
| Cic.CoFix (_,funs) ->
snd (
List.fold_right
(fun (name,ty,bo) (n,uris) ->
if name = name_to_avoid then
- (n+1,uris)
+ (n-1,uris)
else
let uri =
UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
- let bo = Cic.CoFix (n,funs) in
+ let bo = Cic.CoFix (n-1,funs) in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
add_single_obj uri obj refinement_toolkit;
- (n+1,uri::uris)
- ) funs (1,[]))
+ (n-1,uri::uris)
+ ) funs (List.length funs,[]))
| _ -> assert false
let add_obj refinement_toolkit uri obj =
projects / helm.git / blobdiff