-
- let candidates = DB.retrieve_unifiables hdb (pair t1 t2) in
- let res = List.map
- (fun ty ->
- let ty, metasenv, _ =
- NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
- in
- match ty with
- | NCic.Appl [_; t1; t2] ->
- prerr_endline ("candidate1: " ^ NCicPp.ppterm ~metasenv ~subst ~context t1);
- prerr_endline ("candidate2: " ^ NCicPp.ppterm ~metasenv ~subst ~context t2);
-
- metasenv, t1, t2
- | _ -> assert false)
- (HintSet.elements candidates)
+(*
+ prerr_endline ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t1 t2));
+ prerr_endline ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t2 t1));
+ DB.iter hdb
+ (fun p ds ->
+ prerr_endline ("ENTRY: " ^
+ NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
+ String.concat "|" (List.map (NCicPp.ppterm ~metasenv:[] ~subst:[]
+ ~context:[]) (HintSet.elements ds))));
+*)
+ let candidates1 = DB.retrieve_unifiables hdb#uhint_db (pair t1 t2) in
+ let candidates2 = DB.retrieve_unifiables hdb#uhint_db (pair t2 t1) in
+ let candidates1 =
+ List.map (fun (prec,ty) ->
+ prec,true,saturate ~delta:max_int metasenv subst context ty 0)
+ (HintSet.elements candidates1)
+ in
+ let candidates2 =
+ List.map (fun (prec,ty) ->
+ prec,false,saturate ~delta:max_int metasenv subst context ty 0)
+ (HintSet.elements candidates2)
+ in
+ let rc =
+ List.map
+ (fun (p,b,(t,m,_)) ->
+ let rec aux () (m,l as acc) = function
+ | NCic.Meta _ as t -> acc, t
+ | NCic.LetIn (name,ty,bo,t) ->
+ let m,_,i,_=
+ NCicMetaSubst.mk_meta ~name m context (`WithType ty)in
+ let t = NCicSubstitution.subst i t in
+ aux () (m, (i,bo)::l) t
+ | t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t
+ in
+ let (m,l), t = aux () (m,[]) t in
+ p,b,(t,m,l))
+ (candidates1 @ candidates2)