index_hint db c a b precedence
;;
+(*
let db () =
let combine f l =
List.flatten
!user_db (List.flatten hints)
*)
;;
+*)
let saturate ?(delta=0) metasenv subst context ty goal_arity =
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
let metasenv1, _, arg,_ =
- NCicMetaSubst.mk_meta ~name:name metasenv context (`WithType s) in
+ NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context
+ ~with_type:s `IsTerm
+ in
let t, metasenv1, args, pno =
aux metasenv1 (NCicSubstitution.subst arg t)
in
;;
let look_for_hint hdb metasenv subst context t1 t2 =
+ if NDiscriminationTree.NCicIndexable.path_string_of t1 =
+ [Discrimination_tree.Variable] ||
+ NDiscriminationTree.NCicIndexable.path_string_of t2 =
+ [Discrimination_tree.Variable] then [] else begin
+
debug(lazy ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context t1));
debug(lazy ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context t2));
(*
| NCic.Meta _ as t -> acc, t
| NCic.LetIn (name,ty,bo,t) ->
let m,_,i,_=
- NCicMetaSubst.mk_meta ~name m context (`WithType ty)in
+ NCicMetaSubst.mk_meta ~attrs:[`Name name] m context
+ ~with_type:ty `IsTerm
+ in
let t = NCicSubstitution.subst i t in
aux () (m, (i,bo)::l) t
| t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t
rc)));
rc
+ end
;;
+let pp_hint t p =
+ let context, t =
+ let rec aux ctx = function
+ | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
+ | t -> ctx, t
+ in
+ aux [] t
+ in
+ let recproblems, concl =
+ let rec aux ctx = function
+ | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest
+ | t -> ctx, t
+ in
+ aux [] t
+ in
+ let buff = Buffer.create 100 in
+ let fmt = Format.formatter_of_buffer buff in
+(*
+ F.fprintf "@[<hov>"
+ F.fprintf "@[<hov>"
+(* pp_ctx [] context *)
+ F.fprintf "@]"
+ F.fprintf "@;"
+ F.fprintf "@[<hov>"
+(* pp_ctx context recproblems *)
+ F.fprintf "@]"
+ F.fprintf "\vdash@;";
+ NCicPp.ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[];
+ F.fprintf "@]"
+ F.fprintf formatter "@?";
+ prerr_endline (Buffer.contents buff);
+*)
+()
+;;
let generate_dot_file status fmt =
let module Pp = GraphvizPp.Dot in
(NCicPp.ppterm
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
in
- let hint = "???" (*
+ let shint = "???" (*
string_of_int precedence ^ "..." ^
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
(NCicPp.ppterm
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
in
nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
- edges := (mangle l, mangle r, hint) :: !edges)
+ edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
(HintSet.elements dataset);
);
List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
- List.iter (fun x, y, l ->
+ List.iter (fun x, y, l, _, _ ->
Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
!edges;
+ edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
+ List.iter (fun x, y, _, p, l -> pp_hint l p) !edges;
;;