(* to apply the coercion it is sufficient to unify the last coercion
argument (that is a Meta) with the term to be coerced *)
| SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+ | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
| NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
+ | NotHandled
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
+ (fun u,saturations ->
+ let t = CicUtil.term_of_uri u in
+ let arity =
+ match CoercDb.is_a_coercion t with
+ | Some (_,CoercDb.Fun i,_,_,_) -> i
+ | _ -> 0
+ in
+ arity,t,saturations) ul
+ in
+ let freshmeta = CicMkImplicit.new_meta metasenv subst in
+ List.map
+ (fun (arity,c,saturations) ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' ~subst metasenv context c
+ CicUniv.oblivion_ugraph in
+ let _,metasenv,args,lastmeta =
+ TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
+ match args with
+ [] -> c
+ | _ -> Cic.Appl (c::args)
+ ) cl
+;;
+
(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
- try
+let look_for_coercion_carr metasenv subst context src tgt =
+ let is_dead = function CoercDb.Dead -> true | _ -> false in
+ let pp_l s l =
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata[%s] da %s a %s" s
+ (CoercDb.string_of_carr src)
+ (CoercDb.string_of_carr tgt)));
+ | _::_ ->
+ debug_print (lazy (
+ sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
+ (List.length l)
+ (CoercDb.string_of_carr src)
+ (CoercDb.string_of_carr tgt)));
+ in
+ if is_dead src || is_dead tgt then NotHandled
+ else
let l =
CoercDb.find_coercion
- (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
- let uri =
- match l with
- | [] ->
- debug_print
- (lazy
- (sprintf ":-( coercion non trovata da %s a %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- None
- | _::_ ->
- debug_print (lazy (
- sprintf ":-) TROVATE %d coercion(s) da %s a %s"
- (List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- Some l
+ (fun (s,t) ->
+ CoercDb.eq_carr s src &&
+ match t, tgt with
+ | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop
+ | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set
+ | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true
+ | _ -> CoercDb.eq_carr t tgt)
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)
- with
- | CoercDb.EqCarrNotImplemented s -> NotHandled s
- | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
+ pp_l "precise" l;
+ (match l with
+ | [] ->
+ let l =
+ CoercDb.find_coercion
+ (fun (_,t) -> CoercDb.eq_carr t tgt)
+ in
+ pp_l "approx" l;
+ (match l with
+ | [] -> NoCoercion
+ | ul ->
+ SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+ | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
+;;
+
+let rec count_pi c s t =
+ match CicReduction.whd ~delta:false ~subst:s c t with
+ | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+ | _ -> 0
;;
let look_for_coercion metasenv subst context src tgt =
- let src_uri = CoercDb.coerc_carr_of_term src in
- let tgt_uri = CoercDb.coerc_carr_of_term tgt in
- look_for_coercion' metasenv subst context src_uri tgt_uri
+ let src_arity = count_pi context subst src in
+ let tgt_arity = count_pi context subst tgt in
+ let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+ let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+ look_for_coercion_carr metasenv subst context src_carr tgt_carr
let source_of t =
- try
- let uri = CicUtil.uri_of_term t in
- CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
- with Invalid_argument _ -> assert false (* t must be a coercion *)
+ match CoercDb.is_a_coercion t with
+ | None -> assert false
+ | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
+ | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
+ | Some _ -> assert false (* t must be a coercion not to funclass *)
+;;
let generate_dot_file () =
+ let l = CoercDb.to_list () in
let module Pp = GraphvizPp.Dot in
let buf = Buffer.create 10240 in
let fmt = Format.formatter_of_buffer buf in
Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
~edge_attrs:["fontsize", "10"] fmt;
- let l = CoercDb.to_list () in
- let pp_description carr =
- match CoercDb.uri_of_carr carr with
- | None -> ()
- | Some uri ->
- Pp.node (CoercDb.name_of_carr carr)
- ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then
+ Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
+ color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n"
+ ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
+ <TR><TD BGCOLOR=\"gray95\">Source</TD>
+ <TD BGCOLOR=\"gray95\">Target</TD>
+ <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
+ String.concat "</TR>"
+ (List.map
+ (fun (src,tgt,ul) ->
+ let src_name = CoercDb.string_of_carr src in
+ let tgt_name = CoercDb.string_of_carr tgt in
+ let names =
+ List.map (fun (u,_,_) ->
+ UriManager.name_of_uri u ^
+ (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+ when List.exists ((=) (`Flavour `Variant)) attrs -> "*"
+ | _ -> "")
+ ) ul
+ in
+ "<TR><TD>" ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
+ String.concat ", " names ^ "</TD>")
+ (List.sort (fun (x,y,_) (x1,y1,_) ->
+ let rc = compare x x1 in
+ if rc = 0 then compare y y1 else rc) l))
+ ^ "</TR></TABLE></FONT>")
+ (String.concat ";" ["Type"]);
+ let type_uri u =
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
+ CicUniv.oblivion_ugraph
+ in
+ ty
+ in
+ let deref_coercion u =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+ when List.exists ((=) (`Flavour `Variant)) attrs ->
+ UriManager.name_of_uri u'
+ | Cic.Constant (_,Some t,_,_,_), _ when
+ let rec is_id = function
+ | Cic.Lambda (_,_,t) -> is_id t
+ | Cic.Rel _ -> true
+ | _ -> false
+ in is_id t -> "ID"
+ | _ -> UriManager.name_of_uri u
+ in
List.iter
- (fun (src, tgt, cl) ->
- let src_name = CoercDb.name_of_carr src in
- let tgt_name = CoercDb.name_of_carr tgt in
- pp_description src;
- pp_description tgt;
+ (fun (src, tgt, ul) ->
List.iter
- (fun c ->
+ (fun (u,saturations,cpos) ->
+ let ty = type_uri u in
+ let src_name, tgt_name =
+ let rec aux ctx cpos t =
+ match cpos, t with
+ | 0,Cic.Prod (_,src,tgt) ->
+ CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx)
+ | 0,t -> CicPp.pp t ctx, Cic.Implicit None, []
+ | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt
+ | _ -> assert false
+ in
+ let ssrc, rest, ctx = aux [] cpos ty in
+ let stgt, rest, _ = aux ctx saturations rest in
+ let stgt =
+ if rest <> Cic.Implicit None then
+ match tgt with
+ | CoercDb.Fun _ -> CoercDb.string_of_carr tgt
+ | _ -> assert false
+ else
+ stgt
+ in
+ ssrc, stgt
+ in
+ Pp.node src_name fmt;
+ Pp.node tgt_name fmt;
Pp.edge src_name tgt_name
- ~attrs:[ "label", UriManager.name_of_uri c;
- "href", UriManager.string_of_uri c ]
+ ~attrs:[ "label",
+ (deref_coercion 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
;;
-let is_composite t =
- try
- let uri =
- match t with
- | Cic.Appl (he::_) -> CicUtil.uri_of_term he
- | _ -> CicUtil.uri_of_term t
- in
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
- | Cic.Constant (_,_, _, _, attrs),_ ->
- List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
- | _ -> false
- with Invalid_argument _ -> false
+let coerced_arg l =
+ match l with
+ | [] | [_] -> None
+ | c::tl ->
+ match CoercDb.is_a_coercion c with
+ | None -> None
+ | Some (_,_,_,_,cpos) ->
+ if List.length tl > cpos then Some (List.nth tl cpos, cpos) else 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 uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
+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 splat e l = List.map (fun x -> e, x) l;;
+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 (x1,x2,_) -> e, Some (x1,x2)) 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
;;
-let rec min acc = function
+(* 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 skipped = function
| c::tl ->
- if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
- | [] -> acc
+ if List.exists (lb c) (tl@acc)
+ then min acc (c::skipped) tl else min (c::acc) skipped tl
+ | [] -> acc, skipped
+;;
+
+
+let sort l =
+ let low, high = min [] [] l in low @ high
;;
-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 (grow_left,left) (grow_right,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)
+ (sort (intersect
+ (if grow_left then grow left else [left,None])
+ (if grow_right then grow right else [right,None])))
;;
(* EOF *)
projects / helm.git / blobdiff