that are not added anymore.
Nicer api for meets used by unification.
metasenv (C.Appl l1) (C.Appl l2) ugraph
| _ -> raise exn)
else
- let meets = CoercGraph.meets car1 car2 in
+ let meets =
+ CoercGraph.meets metasenv subst context car1 car2
+ in
(match meets with
| [] -> raise exn
- | _::_::_ ->
-prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-let m1::m2::_ = meets in
-prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2);
-assert false
- | [m] ->
+ | (carr,metasenv,to1,to2)::xxx ->
+ (match xxx with
+ [] -> ()
+ | (m2,_,c2,c2')::_ ->
+ let m1,_,c1,c1' = carr,metasenv,to1,to2 in
+ let unopt =
+ function Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
+ HLog.warn
+ ("There are two minimal joins of "^
+ CoercDb.name_of_carr car1^" and "^
+ CoercDb.name_of_carr car2^": " ^
+ CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
+ unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+ unopt c2^" + "^unopt c2'));
let last_tl1',(subst,metasenv,ugraph) =
- match last_tl1 with
- | Cic.Meta (i1,l1)
- when not (CoercDb.eq_carr m car1) ->
- (match
- CoercGraph.look_for_coercion' metasenv subst
- context m car1
- with
- | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
- ->
- last,
- fo_unif_subst test_equality_only subst context
+ match last_tl1,to1 with
+ | Cic.Meta (i1,l1),Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
metasenv coerced last_tl1 ugraph
- | _ ->
-prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
- | _ -> last_tl1,(subst,metasenv,ugraph) in
+ | _ -> last_tl1,(subst,metasenv,ugraph)
+ in
let last_tl2',(subst,metasenv,ugraph) =
- match last_tl2 with
- Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
- (match
- CoercGraph.look_for_coercion' metasenv subst
- context m car2
- with
- (*CSC: bu here: I am considering only the first one*)
- | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
- ->
- last,
- fo_unif_subst test_equality_only subst context
+ match last_tl2,to2 with
+ | Cic.Meta (i2,l2),Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
metasenv coerced last_tl2 ugraph
- | _ ->
-prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
- | _ -> last_tl2,(subst,metasenv,ugraph)
+ | _ -> last_tl2,(subst,metasenv,ugraph)
in
-(*DEBUGGING ONLY:
+ (*DEBUGGING ONLY:
prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
*)
let subst,metasenv,ugraph =
let debug = false
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 funclass_arityl =
+ let _,tgtcarl = List.split (List.map CoercDb.get_carr 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 ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' ~subst metasenv context c
+ CicUniv.empty_ugraph in
+ let _,metasenv,args,lastmeta =
+ TermUtil.saturate_term freshmeta metasenv context ty arity in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ metasenv, Cic.Meta (lastmeta-1,irl),
+ match args with
+ [] -> c
+ | _ -> Cic.Appl (c::args)
+ ) funclass_arityl cl
+;;
+
(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion' metasenv subst context src tgt =
try
in
(match uri with
None -> NoCoercion
- | Some ul ->
- let cl = List.map CicUtil.term_of_uri ul in
- let funclass_arityl =
- let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
- List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
- in
- let freshmeta = CicMkImplicit.new_meta metasenv subst in
- let newtl =
- List.map2
- (fun arity c ->
- let ty,_ =
- CicTypeChecker.type_of_aux' ~subst metasenv context c
- CicUniv.empty_ugraph in
- let _,metasenv,args,lastmeta =
- TermUtil.saturate_term freshmeta metasenv context ty arity in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- metasenv, Cic.Meta (lastmeta-1,irl),
- match args with
- [] -> c
- | _ -> Cic.Appl (c::args)
- ) funclass_arityl cl
- in
- SomeCoercion newtl)
+ | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
with Invalid_argument _ -> false
;;
-let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
+let coerced_arg l =
+ match l with
+ | [] | [_] -> assert false
+ | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+ | c::tl ->
+ let arity =
+ match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
+ in
+ (* decide a decent structure for coercion carriers so that all this stuff is
+ * useless *)
+ let pi =
+ (* this calculation is not complete, since we have strange carriers *)
+ let rec count_pi = function
+ | Cic.Prod(_,_,t) -> 1+ (count_pi t)
+ | _ -> 0
+ in
+ let uri = CicUtil.uri_of_term c in
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ | Cic.Constant (_, _, ty, _, _) -> count_pi ty
+ | _ -> assert false
+ in
+ try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+;;
+
+(************************* meet calculation stuff ********************)
+let eq_uri_opt u1 u2 =
+ match u1,u2 with
+ | Some u1, Some u2 -> UriManager.eq u1 u2
+ | None,Some _ | Some _, None -> false
+ | None, None -> true
+;;
+
+let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
+
+let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
+ CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
+;;
+
+let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
+
+let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
-let splat e l = List.map (fun x -> e, x) l;;
+let splat e l = List.map (fun x -> e, Some x) l;;
+(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_to carr =
let l = CoercDb.to_list () in
- List.flatten
- (HExtlib.filter_map
- (fun (src,tgt,cl) ->
- if CoercDb.eq_carr tgt carr then Some (splat src cl) else None)
- l)
+ let splat_coercion_to carr (src,tgt,cl) =
+ if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
+ in
+ let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
+ l
;;
+(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_from carr =
let l = CoercDb.to_list () in
- List.flatten
- (HExtlib.filter_map
- (fun (src,tgt,cl) ->
- if CoercDb.eq_carr src carr then Some (splat tgt cl) else None)
- l)
+ let splat_coercion_from carr (src,tgt,cl) =
+ if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
+ in
+ List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
;;
+(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 }
+ * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
let intersect l1 l2 =
- let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
- uniq (List.filter is_in_l1 l2)
+ let is_in_l1 (x,u2) =
+ HExtlib.filter_map
+ (fun (src,u1) ->
+ if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
+ l1
+ in
+ uniq2 (List.flatten (List.map is_in_l1 l2))
;;
-let grow s =
- uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
+(* grow tgt gives all the (src,u) such that u:tgt->src *)
+let grow tgt =
+ uniq ((tgt,None)::(get_coercions_to tgt))
;;
-let lb c =
+let lb (c,_,_) =
let l = get_coercions_from c in
- function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
+ fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
;;
+(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
+ * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
let rec min acc = function
| c::tl ->
if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
| [] -> acc
;;
-let meets left right =
- let u = UriManager.uri_of_string "cic:/foo.con" in
- min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
+let meets metasenv subst context left right =
+ let saturate metasenv uo =
+ match uo with
+ | None -> metasenv, None
+ | Some u ->
+ match saturate_coercion [u] metasenv subst context with
+ | [metasenv, sat, last] -> metasenv, Some (sat, last)
+ | _ -> assert false
+ in
+ List.map
+ (fun (c,uo1,uo2) ->
+ let metasenv, uo1 = saturate metasenv uo1 in
+ let metasenv, uo2 = saturate metasenv uo2 in
+ c,metasenv, uo1, uo2)
+ (min [] (intersect (grow left) (grow right)))
;;
(* EOF *)
val generate_dot_file: unit -> string
+(* given the Appl contents returns the argument of the head coercion *)
+val coerced_arg: Cic.term list -> Cic.term option
+
+(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
+ Cic.metasenv -> Cic.substitution -> Cic.context ->
CoercDb.coerc_carr -> CoercDb.coerc_carr ->
- CoercDb.coerc_carr list
+ (CoercDb.coerc_carr * Cic.metasenv *
+ (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list
CoercDb.Fun arity
| _ -> assert false
in
- let already_in =
+ let already_in_obj src_carr tgt_carr uri obj =
List.exists
(fun (s,t,ul) ->
List.exists
(fun u ->
- UriManager.eq u uri &&
+ let bo =
+ match obj with
+ | Cic.Constant (_, Some bo, _, _, _) -> bo
+ | _ -> assert false
+ in
CoercDb.eq_carr s src_carr &&
- CoercDb.eq_carr t tgt_carr)
+ CoercDb.eq_carr t tgt_carr &&
+ if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+ CicUniv.oblivion_ugraph)
+ then true else
+ (HLog.warn
+ ("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.");
+ false))
ul)
(CoercDb.to_list ())
in
CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
baseuri
in
+ let new_coercions =
+ 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
- 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
- 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 (_,tgt,uri,obj) ->
- add_single_obj uri obj refinement_toolkit;
- let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
- (uri,arity)::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
+ (* 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 (_,tgt,uri,obj) ->
+ add_single_obj uri obj refinement_toolkit;
+ let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+ (uri,arity)::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
;;
let remove_coercion uri =
projects / helm.git / commitdiff