command_of_obj (G.Include (floc, value ^ ".ma"))
let coercion value =
- command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0))
+ command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
let inline (uri, prefix) =
command_of_macro (G.Inline (floc, G.Declarative, uri, prefix))
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
let saturate_coercion ul metasenv subst context =
- let cl = List.map CicUtil.term_of_uri ul in
+ let cl =
+ List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
let funclass_arityl =
- let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+ let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
in
let freshmeta = CicMkImplicit.new_meta metasenv subst in
List.map2
- (fun arity c ->
+ (fun arity (c,saturations) ->
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context c
CicUniv.empty_ugraph in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
- metasenv, Cic.Meta (lastmeta-1,irl),
+ metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
match args with
[] -> c
| _ -> Cic.Appl (c::args)
Pp.node (CoercDb.name_of_carr carr)
~attrs:["href", UriManager.string_of_uri uri] fmt in
List.iter
- (fun (src, tgt, cl) ->
+ (fun (src, tgt, ul) ->
let src_name = CoercDb.name_of_carr src in
let tgt_name = CoercDb.name_of_carr tgt in
pp_description src;
pp_description tgt;
List.iter
- (fun c ->
+ (fun (u,saturations) ->
Pp.edge src_name tgt_name
- ~attrs:[ "label", UriManager.name_of_uri c;
- "href", UriManager.string_of_uri c ]
+ ~attrs:[ "label",
+ (UriManager.name_of_uri u ^
+ if saturations = 0 then
+ ""
+ else
+ "(" ^ string_of_int saturations ^ ")");
+ "href", UriManager.string_of_uri u ]
fmt)
- cl)
+ ul)
l;
Pp.trailer fmt;
Buffer.contents buf
(************************* meet calculation stuff ********************)
let eq_uri_opt u1 u2 =
match u1,u2 with
- | Some u1, Some u2 -> UriManager.eq u1 u2
+ | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
| None,Some _ | Some _, None -> false
| None, None -> true
;;
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 11
+let magic = 12
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
- | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
+ | Coercion of loc * UriManager.uri * bool (* add_obj *) *
+ int (* arity *) * int (* saturations *)
| Default of loc * string * UriManager.uri list
| Drop of loc
| Include of loc * string
Printf.sprintf "default \"%s\" %s" what
(String.concat " " (List.map UriManager.string_of_uri uris))
-let pp_coercion uri do_composites arity =
- Printf.sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
- (if do_composites then "compounds" else "no compounds")
+let pp_coercion uri do_composites arity saturations=
+ Printf.sprintf "coercion %s %d %d (* %s *)"
+ (UriManager.string_of_uri uri) arity saturations
+ (if do_composites then "compounds" else "no compounds")
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
- | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
+ | Coercion (_, uri, do_composites, i, j) ->
+ pp_coercion uri do_composites i j
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
| Include (_,path) -> "include \"" ^ path ^ "\""
| GrafiteAst.Default (loc, name, uris) ->
let uris = List.map rehash_uri uris in
GrafiteAst.Default (loc, name, uris)
- | GrafiteAst.Coercion (loc, uri, close, arity) ->
- GrafiteAst.Coercion (loc, rehash_uri uri, close, arity)
+ | GrafiteAst.Coercion (loc, uri, close, arity, saturations) ->
+ GrafiteAst.Coercion (loc, rehash_uri uri, close, arity, saturations)
| GrafiteAst.Index (loc, key, uri) ->
GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri)
| cmd ->
type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity) =
- GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
+let coercion_moo_statement_of (uri,arity, saturations) =
+ GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations)
let refinement_toolkit = {
RefinementTool.type_of_aux' =
RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
}
-let eval_coercion status ~add_composites uri arity baseuri =
+let eval_coercion status ~add_composites uri arity saturations baseuri =
let status,compounds =
- GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
- baseuri
+ GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
+ saturations baseuri
in
let moo_content =
- List.map coercion_moo_statement_of ((uri,arity)::compounds)
+ List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
in
let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- List.map fst compounds
+ List.map (fun u,_,_ -> u) compounds
module MatitaStatus =
struct
in
let is_a_coercion, arity_coercion = is_a_coercion uri in
if is_a_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_coercion))
+ Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
else if is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_wanted))
+ Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
else
None)
lemmas)
*)
let status = GrafiteTypes.add_moo_content [cmd] status in
status,[]
- | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
- eval_coercion status ~add_composites uri arity
+ | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
+ eval_coercion status ~add_composites uri arity saturations
(GrafiteTypes.get_string_option status "baseuri")
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.universe = universe},
lemmas
-let add_coercion refinement_toolkit ~add_composites status uri arity baseuri =
+let add_coercion refinement_toolkit ~add_composites status uri arity
+ saturations baseuri
+=
let compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity baseuri in
+ LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity
+ saturations baseuri in
{status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
compounds
val add_coercion:
RefinementTool.kit ->
add_composites:bool -> GrafiteTypes.status ->
- UriManager.uri -> int ->
+ UriManager.uri -> int -> int ->
string (* baseuri *) ->
- GrafiteTypes.status * (UriManager.uri * int) list (* URI and arity *)
+ GrafiteTypes.status * (UriManager.uri * int * int) list
+ (* URI, arity, saturations *)
val time_travel:
present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+ | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
let arity = match arity with None -> 0 | Some x -> x in
- GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+ let saturations = match saturations with None -> 0 | Some x -> x in
+ GrafiteAst.Coercion
+ (loc, UriManager.uri_of_string suri, true, arity, saturations)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
(* $Id$ *)
let close_coercion_graph_ref = ref
- (fun _ _ _ _ -> [] :
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ (fun _ _ _ _ _ -> [] :
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list)
;;
let set_close_coercion_graph f = close_coercion_graph_ref := f;;
-let close_coercion_graph c1 c2 u s =
- !close_coercion_graph_ref c1 c2 u s
+let close_coercion_graph c1 c2 u sat s =
+ !close_coercion_graph_ref c1 c2 u sat s
;;
(* This module implements the Coercions transitive closure *)
val set_close_coercion_graph :
- (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list)
-> unit
val close_coercion_graph:
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list
;;
let to_list () =
- List.map (fun (s,t,l) -> s,t,List.map fst l) !db
+ List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db
;;
let rec myfilter p = function
| (s,t,l)::tl ->
let l =
HExtlib.filter_map
- (fun (u,n) ->
- if p (s,t,u) then
+ (fun (u,n,saturations) ->
+ if p (s,t,u,saturations) then
if n = 1 then
None
else
- Some (u,n-1)
+ Some (u,n-1,saturations)
else
- Some (u,n))
+ Some (u,n,saturations))
l
in
if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
let find_coercion f =
List.map
- fst
+ (fun uri,_,saturations -> uri,saturations)
(List.flatten
(HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
;;
try
let src, tgt, _ =
List.find
- (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq uri x) xl)
+ (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl)
!db
in
src, tgt
let is_a_coercion u =
List.exists
- (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl)
+ (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl)
!db
;;
| Term _ -> assert false
;;
-let add_coercion (src,tgt,u) =
+let add_coercion (src,tgt,u,saturations) =
let f s t = eq_carr s src && eq_carr t tgt in
let where = List.filter (fun (s,t,_) -> f s t) !db in
let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
match where with
- | [] -> db := (src,tgt,[u,1]) :: !db
+ | [] -> db := (src,tgt,[u,1,saturations]) :: !db
| (src,tgt,l)::tl ->
assert (tl = []); (* not sure, this may be a feature *)
- if List.exists (fun (x,_) -> UriManager.eq u x) l then
- let l' = List.map
- (fun (x,n) -> if UriManager.eq u x then (x,n+1) else (x,n))
+ if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
+ let l' = List.map
+ (fun (x,n,saturations') ->
+ assert (saturations=saturations');
+ if UriManager.eq u x then
+ (x,n+1,saturations)
+ else
+ (x,n,saturations))
l
in
db := (src,tgt,l')::tl @ rest
else
- db := (src,tgt,(u,1)::l)::tl @ rest
+ db := (src,tgt,(u,1,saturations)::l)::tl @ rest
;;
-
-
-
val to_list:
unit ->
- (coerc_carr * coerc_carr * UriManager.uri list) list
+ (coerc_carr * coerc_carr * (UriManager.uri * int) list) list
val add_coercion:
- coerc_carr * coerc_carr * UriManager.uri -> unit
+ coerc_carr * coerc_carr * UriManager.uri * int -> unit
val remove_coercion:
- (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
+ (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit
val find_coercion:
- (coerc_carr * coerc_carr -> bool) -> UriManager.uri list
+ (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list
val is_a_coercion: UriManager.uri -> bool
val is_a_coercion': Cic.term -> bool
let remove_all_coercions () =
UriManager.UriHashtbl.clear coercion_hashtbl;
- CoercDb.remove_coercion (fun (_,_,u1) -> true)
+ CoercDb.remove_coercion (fun (_,_,_,_) -> true)
-let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
+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
* should we saturate it with metas in case we insert it?
*
*)
- let spline2list ty =
+ let spine2list ty =
let rec aux = function
| Cic.Prod( _, src, tgt) -> src::aux tgt
| t -> [t]
aux ty
in
let src_carr, tgt_carr =
- let list_remove_from_tail n l =
- let rec aux n = function
- | hd::tl when n > 0 -> aux (n-1) tl
- | l when n = 0 -> l
- | _ -> assert false
+ let get_classes arity saturations l =
+ let rec aux target = function
+ 0,0,tgt::src::_ when target = None -> src,Some (`Class tgt)
+ | 0,0,src::_ when target <> None -> src,target
+ | 0,saturations,tgt::tl when target = None ->
+ aux (Some (`Class tgt)) (0,saturations,tl)
+ | 0,saturations,_::tl ->
+ aux target (0,saturations - 1,tl)
+ | arity,saturations,_::tl ->
+ aux (Some `Funclass) (arity - 1, saturations, tl)
+ | _,_,_ -> assert false
in
- aux n (List.rev l)
+ aux None (arity,saturations,List.rev l)
in
- let types = spline2list coer_ty in
- match arity, list_remove_from_tail arity types with
- | 0,tgt::src::_ ->
- (* if ~delta is true, it is impossible to define an identity coercion *)
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
- | n,_::src::_ ->
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- CoercDb.Fun arity
- | _ -> assert false
+ 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)
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
("Coercions " ^
UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
uri^" are not convertible, but are between the same nodes.\n"^
- "From now on nification can fail randomly.");
+ "From now on unification can fail randomly.");
false))
ul)
(CoercDb.to_list ())
in
if not add_composites then
- (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
else
let new_coercions =
- CicCoercion.close_coercion_graph src_carr tgt_carr uri
+ CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
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,saturations,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,_) -> CoercDb.add_coercion (src,tgt,uri))
+ (fun (src,tgt,uri,saturations,_) ->
+ CoercDb.add_coercion (src,tgt,uri,saturations))
new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri);
+ CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
(* add the composites obj and they eventual lemmas *)
let lemmas =
if add_composites then
List.fold_left
- (fun acc (_,tgt,uri,obj) ->
+ (fun acc (_,tgt,uri,saturations,obj) ->
add_single_obj uri obj refinement_toolkit;
let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
- (uri,arity)::acc)
+ (uri,arity,saturations)::acc)
[] new_coercions
else
[]
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
- CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
+ CoercDb.remove_coercion (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
try
List.iter2
(fun (uri, name, bo) (_name, coercion, arity) ->
+ let saturations = 0 in
try
let ty, ugraph =
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
every time. Right? *)
let x =
add_coercion ~add_composites:true refinement_toolkit uri arity
- (UriManager.buri_of_uri uri)
+ saturations (UriManager.buri_of_uri uri)
in
(*prerr_endline ("are: ");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
prerr_endline "---";
*)
(*CSC: I throw the arity away. See comment above *)
- List.map fst x
+ List.map (fun u,_,_ -> u) x
end
else
[]
val add_coercion:
add_composites:bool ->
RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
- string (* baseuri *) ->
- (UriManager.uri * int) list (* URI and arity *)
+ int (* saturations *) -> string (* baseuri *) ->
+ (UriManager.uri * int * int) list (* URI, arity, saturations *)
(* inverse of add_coercion, removes both the eventually created composite *)
(* coercions and the information that [uri] and the composites are coercion *)
(* generate_composite (c2 (c1 s)) in the universe graph univ
* both living in the same context and metasenv *)
-let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
+let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity
+ last_lam_with_inn_arg
+=
+assert (sat1 = 0);
+assert (sat2 = 0);
+let saturationsres = 0 in
let original_metasenv = metasenv in
let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
let rec mk_implicits = function
| 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
in
- let rec mk_lambda_spline c namer = function
+ let rec mk_lambda_spine c namer = function
| 0 -> c
| n ->
Cic.Lambda
(namer n,
(Cic.Implicit None),
- mk_lambda_spline (CicSubstitution.lift 1 c) namer (n-1))
+ mk_lambda_spine (CicSubstitution.lift 1 c) namer (n-1))
in
let count_saturations_needed t arity =
let rec aux acc n = function
| Cic.Appl l -> List.tl l
| _ -> assert false
in
- (* i should cut off the laet elem of l_c2 *)
+ (* i should cut off the last elem of l_c2 *)
let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in
let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
- let spline_len = saturations_for_c1 + saturations_for_c2 in
- let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
+ let spine_len = saturations_for_c1 + saturations_for_c2 in
+ let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
let old_insert_coercions = !CicRefine.insert_coercions in
let c, metasenv, univ =
(* let metasenv = order_metasenv metasenv in *)
(* debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *)
let body_metasenv, lambdas_metasenv =
- split_metasenv metasenv (spline_len + List.length context)
+ split_metasenv metasenv (spine_len + List.length context)
in
debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
let body_metasenv = order_body_menv term body_metasenv in
debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
- let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
+ let subst = create_subst_from_metas_to_rels spine_len body_metasenv in
debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
let term = CicMetaSubst.apply_subst subst term in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
CicRefine.type_of_aux' metasenv context term ugraph
in
let body_metasenv, lambdas_metasenv =
- split_metasenv metasenv (spline_len + List.length context)
+ split_metasenv metasenv (spine_len + List.length context)
in
let lambdas_metasenv =
List.filter
CicRefine.insert_coercions := old_insert_coercions;
raise exn
in
- c, metasenv, univ
+ c, metasenv, univ, saturationsres
;;
let build_obj c univ arity =
CoercDb.eq_carr s src &&
CoercDb.eq_carr t tgt &&
try
- List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
+ List.for_all2 (fun (u1,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
with
| Invalid_argument "List.for_all2" -> false)
coercions))
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
-let close_coercion_graph src tgt uri baseuri =
+let close_coercion_graph src tgt uri saturations baseuri =
(* check if the coercion already exists *)
let coercions = CoercDb.to_list () in
- let todo_list = get_closure_coercions src tgt uri coercions in
+ let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
let todo_list = filter_duplicates todo_list coercions in
try
let new_coercions =
try
(match l with
| [] -> assert false
- | he :: tl ->
+ | (he,saturations1) :: tl ->
let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
let first_step =
Cic.Constant ("",
Some (CoercDb.term_of_carr (CoercDb.Uri he)),
- Cic.Sort Cic.Prop, [], obj_attrs arity)
+ Cic.Sort Cic.Prop, [], obj_attrs arity), saturations1
in
let o,_ =
- List.fold_left (fun (o,univ) coer ->
+ List.fold_left (fun (o,univ) (coer,saturations) ->
match o with
- | Cic.Constant (_,Some c,_,[],_) ->
- let t, menv, univ =
- generate_composite c
- (CoercDb.term_of_carr (CoercDb.Uri coer))
+ | Cic.Constant (_,Some u,_,[],_),saturations1 ->
+ let t, menv, univ, saturationsres =
+ generate_composite' (u,saturations1)
+ (CoercDb.term_of_carr (CoercDb.Uri coer),
+ saturations)
[] [] univ arity true
in
if (menv = []) then
HLog.warn "MENV non empty after composing coercions";
- build_obj t univ arity
+ let o,univ = build_obj t univ arity in
+ (o,saturationsres),univ
| _ -> assert false
) (first_step, CicUniv.empty_ugraph) tl
in
let name_src = CoercDb.name_of_carr src in
let name_tgt = CoercDb.name_of_carr tgt in
- let by = List.map UriManager.name_of_uri l in
+ let by = List.map (fun u,_ -> UriManager.name_of_uri u) l in
let name = mangle name_tgt name_src by in
let c_uri =
number_if_already_defined baseuri name
- (List.map (fun (_,_,u,_) -> u) acc)
+ (List.map (fun (_,_,u,_,_) -> u) acc)
in
- let named_obj =
+ let named_obj,saturations =
match o with
- | Cic.Constant (_,bo,ty,vl,attrs) ->
- Cic.Constant (name,bo,ty,vl,attrs)
+ | Cic.Constant (_,bo,ty,vl,attrs),saturations ->
+ Cic.Constant (name,bo,ty,vl,attrs),saturations
| _ -> assert false
in
- (src,tgt,c_uri,named_obj))::acc
+ (src,tgt,c_uri,saturations,named_obj))::acc
with UnableToCompose -> acc
) [] todo_list
in
;;
CicCoercion.set_close_coercion_graph close_coercion_graph;;
+
+(* generate_composite (c2 (c1 s)) in the universe graph univ
+ * both living in the same context and metasenv *)
+let generate_composite c1 c2 context metasenv univ arity b =
+ let a,b,c,_ =
+ generate_composite' (c1,0) (c2,0) context metasenv univ arity b
+ in
+ a,b,c
+;;
(* This module implements the Coercions transitive closure *)
val close_coercion_graph:
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj)
+ list
exception UnableToCompose
List.iter
(fun (s,t,ul) ->
HLog.debug
- ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":"
+ ((String.concat ","
+ (List.map
+ (fun u,saturations ->
+ UriManager.name_of_uri u ^
+ "(" ^ string_of_int saturations ^ ")")
+ ul)) ^ ":"
^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
(CoercDb.to_list ()));
addDebugSeparator ();
projects / helm.git / commitdiff