Bugfix in tipify: a metavariable was set to type without sortifying its type.

[helm.git] / helm / software / components / ng_refiner / nCicUnifHint.ml

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index bdd5b080b87bc2cdb2e45b44c39b18bccfb186b9..0f0708d638f58cef8fac17303492c6f7111a68b6 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -144,6 +144,7 @@ let add_user_provided_hint db t precedence =
    index_hint db c a b precedence
 ;;
 
+(*
 let db () = 
   let combine f l =
    List.flatten
@@ -203,13 +204,16 @@ let db () =
     !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
@@ -246,6 +250,11 @@ let eq_class_of hdb t1 =
 ;;
 
 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));
 (*
@@ -275,7 +284,9 @@ let look_for_hint hdb metasenv subst context t1 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
@@ -312,8 +323,43 @@ let look_for_hint hdb metasenv subst context t1 t2 =
     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
@@ -342,18 +388,20 @@ let generate_dot_file status fmt =
                (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)
+                ~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;
 ;;