| Some _ -> assert false (* t must be a coercion not to funclass *)
;;
-let generate_dot_file () =
- let l = CoercDb.to_list () in
+let generate_dot_file fmt =
+ let l = CoercDb.to_list (CoercDb.dump ()) 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;
- if l <> [] then
+ 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\" >
(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) ul 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>")
+ 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 ";"
- (List.flatten (List.map (fun (s,t,_) ->
- let src_name = CoercDb.string_of_carr s in
- let tgt_name = CoercDb.string_of_carr t in
- [ "\""^src_name^"\""; "\""^tgt_name^"\"" ]
- ) l)));
- let pp_description carr =
- match carr with
- | CoercDb.Uri uri ->
- Pp.node (CoercDb.string_of_carr carr)
- ~attrs:["href", UriManager.string_of_uri uri] fmt
- | _ -> ()
+ (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, ul) ->
- let src_name = CoercDb.string_of_carr src in
- let tgt_name = CoercDb.string_of_carr tgt in
- pp_description src;
- pp_description tgt;
List.iter
- (fun (u,saturations,_) ->
+ (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 u ^
- if saturations = 0 then
- ""
- else
- "(" ^ string_of_int saturations ^ ")");
+ (deref_coercion u ^
+ if saturations = 0 then ""
+ else "(" ^ string_of_int saturations ^ ")");
"href", UriManager.string_of_uri u ]
fmt)
ul)
l;
- Pp.trailer fmt;
- Buffer.contents buf
;;
let coerced_arg l =
(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_to carr =
- let l = CoercDb.to_list () in
+ let l = CoercDb.to_list (CoercDb.dump ()) in
let splat_coercion_to carr (src,tgt,cl) =
if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
in
(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_from carr =
- let l = CoercDb.to_list () in
+ let l = CoercDb.to_list (CoercDb.dump ()) in
let splat_coercion_from carr (src,tgt,cl) =
if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
in
(* 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
+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 metasenv subst context (grow_left,left) (grow_right,right) =
in
List.map
(fun (c,uo1,uo2) ->
- let metasenv, uo1 =
- if grow_left then saturate metasenv uo1 else metasenv, None in
- let metasenv, uo2 =
- if grow_right then saturate metasenv uo2 else metasenv, None in
+ let metasenv, uo1 = saturate metasenv uo1 in
+ let metasenv, uo2 = saturate metasenv uo2 in
c,metasenv, uo1, uo2)
- (min [] (intersect (grow left) (grow right)))
+ (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