val db = HDB.empty, EQDB.empty
method uhint_db = db
method set_uhint_db v = {< db = v >}
val db = HDB.empty, EQDB.empty
method uhint_db = db
method set_uhint_db v = {< db = v >}
let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
* the subst function that lives in the kernel *)
let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in
let t1_skeleton =
* the subst function that lives in the kernel *)
let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in
let t1_skeleton =
in
let t1_skeleton = cleanup_skeleton () t1_skeleton in
let t2_skeleton = cleanup_skeleton () t2_skeleton in
in
let t1_skeleton = cleanup_skeleton () t1_skeleton in
let t2_skeleton = cleanup_skeleton () t2_skeleton in
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[]
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[]
(let _,x,_,_ = data_hint in x)));
(let _,x,_,_ = data_hint in x)));
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
~with_type:s `IsTerm
in
let t, metasenv1, args, pno =
~with_type:s `IsTerm
in
let t, metasenv1, args, pno =
in
if pno + 1 = goal_arity then
ty, metasenv, [], goal_arity+1
else
t, metasenv1, arg::args, pno+1
| ty ->
in
if pno + 1 = goal_arity then
ty, metasenv, [], goal_arity+1
else
t, metasenv1, arg::args, pno+1
| ty ->
| NCic.Prod _ as ty -> aux metasenv ty
| _ -> ty, metasenv, [], 0 (* differs from the other impl in this line*)
in
| NCic.Prod _ as ty -> aux metasenv ty
| _ -> ty, metasenv, [], 0 (* differs from the other impl in this line*)
in
[] (* if the trie is unable to handle the key, we skip the query since
it sould retulr the whole content of the trie *)
else
[] (* if the trie is unable to handle the key, we skip the query since
it sould retulr the whole content of the trie *)
else
let candidates = EqSet.elements candidates in
let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
List.map snd candidates
in
let candidates = EqSet.elements candidates in
let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
List.map snd candidates
in
if NDiscriminationTree.NCicIndexable.path_string_of t1 =
[Discrimination_tree.Variable] ||
NDiscriminationTree.NCicIndexable.path_string_of t2 =
[Discrimination_tree.Variable] then [] else begin
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));
+ debug(lazy ("KEY1: "^status#ppterm ~metasenv ~subst ~context t1));
+ debug(lazy ("KEY2: "^status#ppterm ~metasenv ~subst ~context t2));
- let candidates1 = HDB.retrieve_unifiables (fst hdb#uhint_db) (pair t1 t2) in
- let candidates2 = HDB.retrieve_unifiables (fst hdb#uhint_db) (pair t2 t1) in
+ let candidates1 = HDB.retrieve_unifiables (fst status#uhint_db) (pair t1 t2) in
+ let candidates2 = HDB.retrieve_unifiables (fst status#uhint_db) (pair t2 t1) in
let candidates1 =
List.map (fun (prec,_,_,ty) ->
let candidates1 =
List.map (fun (prec,_,_,ty) ->
(HintSet.elements candidates1)
in
let candidates2 =
List.map (fun (prec,_,_,ty) ->
(HintSet.elements candidates1)
in
let candidates2 =
List.map (fun (prec,_,_,ty) ->
in
let (m,l), t = aux () (m,[]) t in
p,b,(t,m,l))
in
let (m,l), t = aux () (m,[]) t in
p,b,(t,m,l))
(fun (metasenv, (t1, t2), premises) ->
("\t" ^ String.concat "; "
(List.map (fun (a,b) ->
(fun (metasenv, (t1, t2), premises) ->
("\t" ^ String.concat "; "
(List.map (fun (a,b) ->
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
- " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
+ status#ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
+ " = "^status#ppterm ~margin:max_int ~metasenv ~subst ~context t2))
let module Pp = GraphvizPp.Dot in
let h_db, _ = status#uhint_db in
let names = ref [] in
let module Pp = GraphvizPp.Dot in
let h_db, _ = status#uhint_db in
let names = ref [] in
(fun (precedence, l,r, hint) ->
let l =
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
(fun (precedence, l,r, hint) ->
let l =
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] l)
in
let r =
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] l)
in
let r =
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
in
let shint = "???" (*
string_of_int precedence ^ "..." ^
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
in
let shint = "???" (*
string_of_int precedence ^ "..." ^
Str.global_substitute (Str.regexp "\n") (fun _ -> "")
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
in
nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
in
nodes := (mangle l,l) :: (mangle r,r) :: !nodes;