]> matita.cs.unibo.it Git - helm.git/commitdiff
snapshot for CSC
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 8 Sep 2009 18:48:03 +0000 (18:48 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 8 Sep 2009 18:48:03 +0000 (18:48 +0000)
12 files changed:
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/ng_refiner/.depend
helm/software/components/ng_refiner/Makefile
helm/software/components/ng_refiner/nCicCoercion.ml
helm/software/components/ng_refiner/nCicCoercion.mli
helm/software/components/ng_refiner/nCicMetaSubst.ml
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_refiner/nCicUnifHint.ml
helm/software/components/ng_refiner/nCicUnifHint.mli
helm/software/components/ng_refiner/nRstatus.ml
helm/software/components/ng_refiner/nRstatus.mli
helm/software/components/ng_tactics/nCicElim.ml

index c82fb457a2c4727bc8cf816729e53db9b4726e20..0904cf33119b99ff7183b998af6d1edbd95f01cb 100644 (file)
@@ -538,9 +538,18 @@ let term_at i t =
 let src_tgt_of_ty_cpos_arity ty cpos arity =
   let pis = count_prod ty in
   let tpos = pis - arity in
-  let rec aux i j = function
+  let rec pi_nth i j = function
     | NCic.Prod (_,s,_) when i = j -> s
-    | NCic.Prod (_,_,t) -> aux (i+1) j t
+    | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
+    | t -> assert (i = j); t
+  in
+  let rec cleanup_prod = function
+    | NCic.Prod (_,_,t) -> NCic.Prod ("_",NCic.Implicit `Type, cleanup_prod t)
+    | _ -> NCic.Implicit `Type
+  in
+  let rec pi_tail i j = function
+    | NCic.Prod (_,_,_) as t when i = j -> cleanup_prod t
+    | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
     | t -> assert (i = j); t
   in
   let mask t =
@@ -552,7 +561,8 @@ let src_tgt_of_ty_cpos_arity ty cpos arity =
     in
      aux () t
   in 
-  mask (aux 0 cpos ty), mask (aux 0 tpos ty)
+  mask (pi_nth 0 cpos ty), 
+  mask (pi_tail 0 tpos ty)
 ;;
 
 let close_in_context t metasenv = 
index 924b43fe8b1e756cd613663bd3e09f5adf9fd7d8..35146bcc8f40f04a7e0cbc62db7dafcf5769a643 100644 (file)
@@ -1,22 +1,26 @@
 nDiscriminationTree.cmi: 
 nCicMetaSubst.cmi: 
-nCicCoercion.cmi: 
 nCicUnifHint.cmi: 
-nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi 
+nCicCoercion.cmi: nCicUnifHint.cmi 
+nRstatus.cmi: nCicCoercion.cmi 
 nCicUnification.cmi: nRstatus.cmi 
 nCicRefiner.cmi: nRstatus.cmi 
 nDiscriminationTree.cmo: nDiscriminationTree.cmi 
 nDiscriminationTree.cmx: nDiscriminationTree.cmi 
 nCicMetaSubst.cmo: nCicMetaSubst.cmi 
 nCicMetaSubst.cmx: nCicMetaSubst.cmi 
-nCicCoercion.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicCoercion.cmi 
-nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi 
 nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi 
 nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi 
-nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi 
-nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi 
-nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi 
-nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi 
+nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
+    nCicCoercion.cmi 
+nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
+    nCicCoercion.cmi 
+nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi 
+nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi 
+nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
+    nCicCoercion.cmi nCicUnification.cmi 
+nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
+    nCicCoercion.cmx nCicUnification.cmi 
 nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \
     nCicRefiner.cmi 
 nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicCoercion.cmx \
index 1fa79cd1cc0acc6a059c4b8a0338cf3bb2206213..9e0959c0d7900fedaac2ea6bad20da6c5b0604d2 100644 (file)
@@ -4,8 +4,8 @@ PREDICATES =
 INTERFACE_FILES = \
        nDiscriminationTree.mli \
        nCicMetaSubst.mli \
-       nCicCoercion.mli \
        nCicUnifHint.mli \
+       nCicCoercion.mli \
        nRstatus.mli \
        nCicUnification.mli \
        nCicRefiner.mli
index e48e772079b86ef6d0d0eb8fafc9fca6706b3852..18540dcda060c1551341ebcd3ed403f9fc60213a 100644 (file)
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
-module COT : Set.OrderedType with type t = NCic.term * int * int = 
+module COT : Set.OrderedType with type t = NCic.term * int * int  * NCic.term *
+NCic.term = 
   struct
-        type t = NCic.term * int * int
+        type t = NCic.term * int * int * NCic.term * NCic.term
         let compare = Pervasives.compare
   end
 
@@ -31,18 +32,21 @@ let empty_db = DB.empty,DB.empty
 
 class status =
  object
+  inherit NCicUnifHint.status
   val db = empty_db
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
   method set_coercion_status
-   : 'status. < coerc_db : db; .. > as 'status -> 'self
-   = fun o -> {< db = o#coerc_db >}
+  : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> 
+          'self
+          = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
 let index_coercion status c src tgt arity arg =
   let db_src,db_tgt = status#coerc_db in
-  let data = (c,arity,arg) in
+  let data = (c,arity,arg,src,tgt) in
 
+  let debug s = prerr_endline (Lazy.force s) in
   debug (lazy ("INDEX:" ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
@@ -103,17 +107,30 @@ let look_for_coercion status metasenv subst context infty expty =
       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
       NCicPp.ppterm ~metasenv ~subst ~context expty));
 
-    let set_src = DB.retrieve_unifiables db_src infty in
-    let set_tgt = DB.retrieve_unifiables db_tgt expty in
+    let src_class = infty :: NCicUnifHint.eq_class_of status infty in
+    let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
+
+    let set_src = 
+      List.fold_left 
+        (fun set infty -> 
+          CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
+        CoercionSet.empty src_class
+    in
+    let set_tgt = 
+      List.fold_left 
+        (fun set expty -> 
+          CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
+        CoercionSet.empty tgt_class
+    in
     let candidates = CoercionSet.inter set_src set_tgt in
 
     debug (lazy ("CANDIDATES: " ^ 
-      String.concat "," (List.map (fun (t,_,_) ->
+      String.concat "," (List.map (fun (t,_,_,_,_) ->
         NCicPp.ppterm ~metasenv ~subst ~context t) 
       (CoercionSet.elements candidates))));
 
     List.map
-      (fun (t,arity,arg) ->
+      (fun (t,arity,arg,_,_) ->
           let ty =
             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
             with NCicTypeChecker.TypeCheckerFailure s ->
@@ -142,7 +159,7 @@ let match_coercion status ~metasenv ~subst ~context t =
   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
  in
     (HExtlib.list_findopt
-      (fun (p,arity,cpos) _ ->
+      (fun (p,arity,cpos,_,_) _ ->
         try
          let t =
           match p,t with
@@ -165,3 +182,63 @@ let match_coercion status ~metasenv ~subst ~context t =
          Failure _ -> None (* raised by split_nth *)
       ) db)
 ;;
+
+let generate_dot_file status =
+  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;
+  let src_db, _ = status#coerc_db in
+  let edges = ref [] in
+  DB.iter src_db (fun _ dataset -> 
+     edges := !edges @ 
+      List.map
+        (fun (t,a,g,sk,dk) -> 
+                prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
+                ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk);
+          let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in
+          let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in
+          (t,a,g),eq_s,eq_t
+          )
+        (CoercionSet.elements dataset);
+    );
+  let nodes = 
+    HExtlib.list_uniq
+     (List.sort compare 
+       (List.flatten
+         (List.map
+           (fun (_,a,b) ->
+             [a;b]
+            )
+           !edges)))
+  in
+  let names = ref [] in
+  let id = ref 0 in
+  let mangle l =
+    try List.assoc l !names
+    with Not_found ->
+      incr id;
+      names := (l,"node"^string_of_int!id) :: !names;
+      List.assoc l !names
+  in
+  List.iter 
+    (fun cl -> 
+      Pp.node (mangle cl) 
+      ~attrs:["label",String.concat "\\n"
+        (List.map (fun t->
+          NCicPp.ppterm ~metasenv:[] ~subst:[]
+           ~context:[] t ~margin:max_int
+        ) cl)]
+      fmt)
+    nodes;
+  List.iter 
+    (fun ((t,a,b),src,tgt) ->
+       Pp.edge (mangle src) (mangle tgt)
+         ~attrs:["label",
+           NCicPp.ppterm ~metasenv:[]
+           ~subst:[] ~context:[] t] fmt)
+    !edges;
+  Pp.trailer fmt;
+  Buffer.contents buf
+;;
index ca65aa953b9edcdf2d6dd28782107d06e3d0cd66..dc62cb86d032955700e3d173fc414213a0aaf019 100644 (file)
@@ -15,9 +15,11 @@ type db
 
 class status :
  object ('self)
+  inherit NCicUnifHint.status
   method coerc_db: db
   method set_coerc_db: db -> 'self
-  method set_coercion_status: <coerc_db: db; ..> -> 'self
+  method set_coercion_status: <coerc_db: db; uhint_db: NCicUnifHint.db; ..> 
+    -> 'self
  end
 
 val empty_db: db
@@ -45,3 +47,5 @@ val look_for_coercion:
 val match_coercion:
  #status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   context:NCic.context -> NCic.term -> (NCic.term * int * int) option
+
+val generate_dot_file: #status -> string
index 9cc6ac67c755c16e4208413f1cd7565859c64557..927c288a0543766830a730ee0df60ac39d33b773 100644 (file)
@@ -254,7 +254,7 @@ let delift ~unify metasenv subst context n l t =
     in
     try aux () () t; false with Found -> true
   in
-  let unify_list ~alpha in_scope = 
+  let unify_list in_scope = 
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
@@ -264,23 +264,16 @@ let delift ~unify metasenv subst context n l t =
           (fun (li,flexible) i ->
             if flexible || i < in_scope then None else
              let li = NCicSubstitution.lift (k+shift) li in
-              if alpha then
-               if NCicReduction.alpha_eq metasenv subst context li t then
-                Some ((metasenv,subst), NCic.Rel (i+1+k))
-               else
-                None
-              else
-               match unify metasenv subst context li t with
-               | Some (metasenv,subst) -> 
-                   Some ((metasenv, subst), NCic.Rel (i+1+k))
-               | None -> None)
+             match unify metasenv subst context li t with
+             | Some (metasenv,subst) -> 
+                 Some ((metasenv, subst), NCic.Rel (i+1+k))
+             | None -> None)
           lb
   in
   let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
-   match unify_list ~alpha:true in_scope metasenv subst context k t with
+   match unify_list in_scope metasenv subst context k t with
    | Some x -> x
    | None -> 
-   try
     match t with 
     | NCic.Rel n as t when n <= k -> ms, t
     | NCic.Rel n -> 
@@ -411,10 +404,6 @@ let delift ~unify metasenv subst context n l t =
     | t -> 
         NCicUntrusted.map_term_fold_a 
           (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
-   with NotInTheList ->
-    match unify_list ~alpha:false in_scope metasenv subst context k t with
-    | Some x -> x
-    | None -> raise NotInTheList
   in
    try aux (context,0,0) (metasenv,subst) t
    with NotInTheList ->
index 26fc593b7dde5ab15ac86a6e6b401d2c84cc380b..48d1eeb1caa491631052740f68c3c159dada558c 100644 (file)
@@ -378,7 +378,8 @@ and try_coercions rdb
       | NCicUnification.Uncertain _ as exc -> first exc tl
   in 
     first exc
-      (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
+      (NCicCoercion.look_for_coercion 
+        rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
   match NCicReduction.whd ~subst context ty with
@@ -440,27 +441,26 @@ and guess_name subst ctx ty =
 
 and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
   (*D*)inside 'E'; try let rc = 
-  let too_many_args = ref false in
   let rec aux metasenv subst args_so_far he ty_he = function 
   | [] ->
      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
-      (match NCicReduction.whd ~subst context ty_he with
-          NCic.Meta _ | NCic.Appl (NCic.Meta _::_) ->
-           too_many_args := true;
-        | _ -> ());
       force_ty true false metasenv subst context orig_t res ty_he expty
   | NCic.Implicit `Vector::tl ->
+      let has_some_more_pis x =
+        match NCicReduction.whd ~subst context x with
+        |  NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false
+        | _ -> true
+      in
      (try
-       too_many_args := false;
        aux metasenv subst args_so_far he ty_he tl
       with
-         Uncertain _
-       | RefineFailure _ as exc when !too_many_args <> true ->
-          try
+      | Uncertain _
+      | RefineFailure _ as exc when has_some_more_pis ty_he ->
+          (try
            aux metasenv subst args_so_far he ty_he
-            (NCic.Implicit `Vector :: NCic.Implicit `Term :: tl)
+            (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
           with
-           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
+           Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)))
   | arg::tl ->
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
@@ -490,7 +490,6 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
           let metasenv, subst =
-             too_many_args := true;
              try NCicUnification.unify rdb metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
               ("The term %s has an inferred type %s, but is applied to the" ^^
@@ -506,14 +505,12 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
       | C.Match (_,_,C.Meta _,_) 
       | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
       | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
-          too_many_args := true;
           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
             ("The term %s is here applied to %d arguments but expects " ^^
             "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
             (List.length args) (List.length args_so_far))))
       | ty ->
           let metasenv, subst, newhead, newheadty = 
-            too_many_args := true;
             try_coercions rdb ~localise metasenv subst context
               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
               (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
@@ -523,7 +520,6 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
                "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
                (List.length args) (List.length args_so_far))))
           in
-           too_many_args := false;
            aux metasenv subst [] newhead newheadty (arg :: tl)
   in
    (* We need to reverse the order of the new created metas since they
index d166b19360fa391fd0a4febc334fe7f28bdaded5..abca189d9665bbd66503d641298b9d4e146339be 100644 (file)
@@ -19,14 +19,21 @@ module COT : Set.OrderedType with type t = int * NCic.term =
 
 module HintSet = Set.Make(COT)
 
-module DB = 
+module HDB = 
   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
 
-type db = DB.t
+module EQDB = 
+  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
+
+type db =
+  HDB.t * (* hint database: (dummy A B)[?] |-> \forall X.(summy a b)[X] *)
+  EQDB.t (* eqclass DB: A[?] |-> \forall X.B[X] and viceversa *)
+
+exception HintNotValid
 
 class status =
  object
-  val db = DB.empty
+  val db = HDB.empty, EQDB.empty
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
   method set_unifhint_status
@@ -45,29 +52,35 @@ let index_hint hdb context t1 t2 precedence =
     (match t2 with
     | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
   );
-  let pair' = pair t1 t2 in
-  let data = 
+  let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in
+  let t1_skeleton = 
+    List.fold_left (fun t _ -> NCicSubstitution.subst hole t) t1 context
+  in
+  let t2_skeleton = 
+    List.fold_left (fun t _ -> NCicSubstitution.subst hole t) t2 context
+  in
+  let src = pair t1_skeleton t2_skeleton in
+  let ctx2abstractions context t = 
     List.fold_left 
      (fun t (n,e) -> 
         match e with
         | NCic.Decl ty -> NCic.Prod (n,ty,t)
         | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t))
-      pair' context in
-  let src = 
-    List.fold_left 
-     (fun t (_,e) -> 
-        match e with
-        | NCic.Decl _ -> 
-            NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
-        | NCic.Def _ -> 
-            NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t)
-     pair' context in
+      t context 
+  in
+  let data_hint = ctx2abstractions context (pair t1 t2) in
+  let data_t1 = t2_skeleton in
+  let data_t2 = t1_skeleton in
 (*
   prerr_endline ("INDEXING: " ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data);
 *)
-  hdb#set_uhint_db (DB.index hdb#uhint_db src (precedence, data))
+  hdb#set_uhint_db (
+      HDB.index (fst (hdb#uhint_db)) src (precedence, data_hint),
+      EQDB.index  
+        (EQDB.index (snd (hdb#uhint_db)) t2_skeleton (precedence, data_t2))
+        t1_skeleton (precedence, data_t1))
 ;;
 
 let add_user_provided_hint db t precedence =
@@ -75,7 +88,21 @@ let add_user_provided_hint db t precedence =
     let rec aux ctx = function
       | NCic.Appl l ->
           (match List.rev l with
-          | b::a::_ -> ctx, a, b
+          | b::a::_ -> 
+              if
+                 let ty_a = 
+                   NCicTypeChecker.typeof ~metasenv:[] ~subst:[] ctx a
+                 in
+                 let ty_b = 
+                   NCicTypeChecker.typeof ~metasenv:[] ~subst:[] ctx b
+                 in
+                 NCicReduction.are_convertible 
+                  ~metasenv:[] ~subst:[] ctx ty_a ty_b              
+                 &&     
+                 NCicReduction.are_convertible 
+                  ~metasenv:[] ~subst:[] ctx a b              
+              then ctx, a, b
+              else raise HintNotValid
           | _ -> assert false)
       | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t
       | NCic.LetIn (n,ty,t,b) -> aux  ((n, NCic.Def (t,ty)) :: ctx) b
@@ -133,7 +160,7 @@ let db () =
           aux [] l r
     | _ -> []
   in
-  let hints = 
+  let _hints = 
     List.fold_left 
       (fun acc (_,_,l) -> 
           acc @ 
@@ -173,19 +200,31 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity =
   res, newmetasenv, arguments
 ;;
 
+let eq_class_of hdb t1 = 
+  if NDiscriminationTree.NCicIndexable.path_string_of t1 = 
+     [Discrimination_tree.Variable]
+  then
+    [] (* 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 = EQDB.retrieve_unifiables (snd hdb#uhint_db) t1 in
+    let candidates = HintSet.elements candidates in
+    List.map snd (List.sort (fun (x,_) (y,_) -> compare x y) candidates)
+;;
+
 let look_for_hint hdb metasenv subst context t1 t2 =
 (*
   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
+  HDB.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 = 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 = 
     List.map (fun (prec,ty) -> 
        prec,true,saturate ~delta:max_int metasenv subst context ty 0) 
index 7b8536ba77e98a937d161c4c6c88630fde4bded7..87519352c4b783b0ba4955cb300517b34cc95bb3 100644 (file)
@@ -13,6 +13,8 @@
 
 type db
 
+exception HintNotValid
+
 class status :
  object ('self)
   method uhint_db: db
@@ -32,3 +34,6 @@ val look_for_hint:
     NCic.term -> NCic.term -> 
       (NCic.metasenv * 
         (NCic.term * NCic.term) * (NCic.term * NCic.term) list) list
+
+val eq_class_of:
+      #status -> NCic.term -> NCic.term list
index bb2d357d754abc4cd55dae50d8be7e80eb9e037e..26482e61b4138deec35cae8c12a0bb5774f24f16 100644 (file)
@@ -13,7 +13,6 @@
 
 class status =
  object (self)
-  inherit NCicUnifHint.status
   inherit NCicCoercion.status
   inherit NCicLibrary.status
   method set_rstatus
@@ -22,7 +21,7 @@ class status =
          uhint_db : NCicUnifHint.db;
          timestamp: NCicLibrary.timestamp; .. > as 'status -> 'self
    = fun o ->
-      ((self#set_unifhint_status o)#set_coercion_status o)#set_library_status o
+      (self#set_coercion_status o)#set_library_status o
  end
 
 type sstatus = status
@@ -33,8 +32,8 @@ module Serializer =
 
   let require ~baseuri status = 
    let rstatus = require ~baseuri (status : #status :> status) in
-   let status = status#set_uhint_db (rstatus#uhint_db) in
    let status = status#set_coerc_db (rstatus#coerc_db) in
+   let status = status#set_uhint_db (rstatus#uhint_db) in
    let status = status#set_timestamp (rstatus#timestamp) in
     status 
  end
index 89f62ce1d3c5d42bb79b06a3161af110972ac1b5..10a4a8a622a5203f7dce1be998b7c373a64f2571 100644 (file)
@@ -13,7 +13,6 @@
 
 class status :
  object ('self)
-  inherit NCicUnifHint.status
   inherit NCicCoercion.status
   inherit NCicLibrary.status
   method set_rstatus: 
index 9db98de498d99e7e10e2f154d22e9a5f4c723484..d5cbca892e15f045d446e82903dbbdd84106cfdf 100644 (file)
@@ -38,6 +38,7 @@ let mk_appl =
  function
     [] -> assert false
   | [x] -> x
+  | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2)
   | l -> CicNotationPt.Appl l
 ;;