First attempt to implement unification hints.

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 63ab446c77380f330ab30183398b83d83248cc0e..28551550d8a21d7abb54af5a4f3664b4a1a74e0e 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -570,7 +570,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-(*   let time = Unix.gettimeofday () in *)
+  let time = Unix.gettimeofday () in 
   let (diff, metasenv, _, cic, _) =
     singleton "third"
       (CicDisambiguate.disambiguate_obj 
@@ -581,7 +581,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
         (text,prefix_len,obj)) in
-  (*
+  
   let time = Unix.gettimeofday () -. time in
   prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
   (NCicLibrary.clear_cache ();
@@ -650,7 +650,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        )
     | _ -> ())
   ); 
-  *)
+  
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic
   

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 0efb49bff54f039f92b3ff1bbef997fe9091777b..9f14c503f3bc30a99cb9ae29457e7ecb345645ff 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -40,7 +40,8 @@ let refine_term
         assert false
     in
     let metasenv, subst, term, _ = 
-      NCicRefiner.typeof 
+      NCicRefiner.typeof
+        (NCicUnifHint.db ())
         ~look_for_coercion:(
           if use_coercions then 
            NCicCoercion.look_for_coercion coercion_db

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index c8ccb5d0cd0b559cb6fed001f80e97836eca5cd1..89e6fd7e9eb3a044a4e0b15b16ce70f959bd04e2 100644 (file)
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -1,10 +1,11 @@
-nCicCoercion.cmi: nDiscriminationTree.cmi 
 nDiscriminationTree.cmo: nDiscriminationTree.cmi 
 nDiscriminationTree.cmx: nDiscriminationTree.cmi 
 nCicMetaSubst.cmo: nCicMetaSubst.cmi 
 nCicMetaSubst.cmx: nCicMetaSubst.cmi 
-nCicCoercion.cmo: nDiscriminationTree.cmi nCicCoercion.cmi 
-nCicCoercion.cmx: nDiscriminationTree.cmx nCicCoercion.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 
 nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi 
 nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi 
 nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi 

diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile
index f3a7fba40e2d52a0e0c68d6db6e4caa6e9d3c560..1b2c293bc0858eb47e1cde5c6426306a52d31158 100644 (file)
--- a/helm/software/components/ng_refiner/Makefile
+++ b/helm/software/components/ng_refiner/Makefile
@@ -5,8 +5,9 @@ INTERFACE_FILES = \
        nDiscriminationTree.mli \
        nCicMetaSubst.mli \
        nCicCoercion.mli \
+       nCicUnifHint.mli \
        nCicUnification.mli \
-       nCicRefiner.mli \
+       nCicRefiner.mli
 
 IMPLEMENTATION_FILES = \
   $(INTERFACE_FILES:%.mli=%.ml)

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index c8f6bdb59eb763e99cc03d7875804e6c412452f8..d47767528a79801a84763e2537236d9e7b12bfe7 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -49,7 +49,7 @@ let exp_implicit metasenv context expty =
 ;;
 
 
-let check_allowed_sort_elimination localise r orig =
+let check_allowed_sort_elimination hdb localise r orig =
    let mkapp he arg =
      match he with
      | C.Appl l -> C.Appl (l @ [arg])
@@ -67,7 +67,7 @@ let check_allowed_sort_elimination localise r orig =
           NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type 
         in
         let metasenv, subst = 
-          try NCicUnification.unify metasenv subst context 
+          try NCicUnification.unify hdb metasenv subst context 
                 arity2 (C.Prod (name, so1, meta)) 
           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
             "expected %s, found %s" (* XXX localizzare meglio *)
@@ -79,7 +79,7 @@ let check_allowed_sort_elimination localise r orig =
      | C.Sort _ (* , t ==?== C.Prod _ *) ->
         let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
         let metasenv, subst = 
-          try NCicUnification.unify metasenv subst context 
+          try NCicUnification.unify hdb metasenv subst context 
                 arity2 (C.Prod ("_", ind, meta)) 
           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
             "expected %s, found %s" (* XXX localizzare meglio *)
@@ -97,7 +97,7 @@ let check_allowed_sort_elimination localise r orig =
     aux
 ;;
 
-let rec typeof 
+let rec typeof hdb 
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   ~look_for_coercion metasenv subst context term expty 
 =
@@ -114,11 +114,11 @@ let rec typeof
           (NCicPp.ppterm ~metasenv ~subst ~context expty)));
            try 
              let metasenv, subst =
-               NCicUnification.unify metasenv subst context infty expty 
+               NCicUnification.unify hdb metasenv subst context infty expty 
              in
              metasenv, subst, t, expty
            with exc -> 
-             try_coercions ~look_for_coercion ~localise 
+             try_coercions hdb ~look_for_coercion ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
     (*D*)in outside(); rc with exc -> outside (); raise exc
@@ -165,12 +165,12 @@ let rec typeof
     | C.Prod (name,(s as orig_s),(t as orig_t)) ->
        let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
        let metasenv, subst, s, s1 = 
-         force_to_sort ~look_for_coercion
+         force_to_sort hdb ~look_for_coercion
            metasenv subst context s orig_s localise s1 in
        let context1 = (name,(C.Decl s))::context in
        let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
        let metasenv, subst, t, s2 = 
-         force_to_sort ~look_for_coercion
+         force_to_sort hdb ~look_for_coercion
            metasenv subst context1 t orig_t localise s2 in
        let metasenv, subst, s, t, ty = 
          sort_of_prod localise metasenv subst 
@@ -189,12 +189,12 @@ let rec typeof
        let metasenv, subst, s, ty_s = 
          typeof_aux metasenv subst context None s in
        let metasenv, subst, s, _ = 
-         force_to_sort ~look_for_coercion
+         force_to_sort hdb ~look_for_coercion
            metasenv subst context s orig_s localise ty_s in
        let (metasenv,subst), exp_ty_t = 
          match exp_s with 
          | Some exp_s -> 
-             (try NCicUnification.unify metasenv subst context s exp_s,exp_ty_t
+             (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t
              with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
                "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
                ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
@@ -210,7 +210,7 @@ let rec typeof
        let metasenv, subst, ty, ty_ty = 
          typeof_aux metasenv subst context None ty in
        let metasenv, subst, ty, _ = 
-         force_to_sort ~look_for_coercion
+         force_to_sort hdb ~look_for_coercion
            metasenv subst context ty orig_ty localise ty_ty in
        let metasenv, subst, t, _ = 
          typeof_aux metasenv subst context (Some ty) t in
@@ -223,7 +223,7 @@ let rec typeof
     | C.Appl ((he as orig_he)::(_::_ as args)) ->
        let metasenv, subst, he, ty_he = 
          typeof_aux metasenv subst context None he in
-       eat_prods ~localise ~look_for_coercion 
+       eat_prods hdb ~localise ~look_for_coercion 
          metasenv subst context orig_he he ty_he args
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
@@ -246,7 +246,7 @@ let rec typeof
       let metasenv, subst, ind, ind_ty = 
         typeof_aux metasenv subst context None ind in
       let metasenv, subst = 
-         check_allowed_sort_elimination localise r orig_term metasenv subst 
+         check_allowed_sort_elimination hdb localise r orig_term metasenv subst 
            context ind ind_ty outsort 
       in
       (* let's check if the type of branches are right *)
@@ -288,7 +288,7 @@ let rec typeof
   in
     typeof_aux metasenv subst context expty term
 
-and try_coercions 
+and try_coercions hdb 
   ~localise ~look_for_coercion 
   metasenv subst context t orig_t infty expty perform_unification exc 
 =
@@ -310,7 +310,7 @@ and try_coercions
             NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
         let metasenv, subst = 
-          NCicUnification.unify metasenv subst context meta t
+          NCicUnification.unify hdb metasenv subst context meta t
         in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
@@ -321,7 +321,7 @@ and try_coercions
             NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
         let metasenv, subst = 
           if perform_unification then
-            NCicUnification.unify metasenv subst context newtype expty
+            NCicUnification.unify hdb metasenv subst context newtype expty
           else metasenv, subst
         in
         metasenv, subst, newterm, newtype
@@ -332,7 +332,7 @@ and try_coercions
     first exc
       (look_for_coercion metasenv subst context infty expty)
 
-and force_to_sort 
+and force_to_sort hdb 
   ~look_for_coercion metasenv subst context t orig_t localise ty 
 =
   match NCicReduction.whd ~subst context ty with
@@ -350,7 +350,7 @@ and force_to_sort
      metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
   | C.Sort _ as ty -> metasenv, subst, t, ty 
   | ty -> 
-      try_coercions ~localise ~look_for_coercion metasenv subst context
+      try_coercions hdb ~localise ~look_for_coercion metasenv subst context
         t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false 
          (Uncertain (lazy (localise orig_t, 
          "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
@@ -378,7 +378,7 @@ and sort_of_prod
          (NCicPp.ppterm ~subst ~metasenv ~context y) 
          (NCicPp.ppterm ~subst ~metasenv ~context x))))
 
-and eat_prods 
+and eat_prods hdb
   ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args 
 =
   (*D*)inside 'E'; try let rc = 
@@ -388,14 +388,14 @@ and eat_prods
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
           let metasenv, subst, arg, _ = 
-            typeof ~look_for_coercion ~localise 
+            typeof hdb ~look_for_coercion ~localise 
               metasenv subst context arg (Some s) in
           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
           aux metasenv subst (arg :: args_so_far) he t tl
       | C.Meta _
       | C.Appl (C.Meta _ :: _) as t ->
           let metasenv, subst, arg, ty_arg = 
-            typeof ~look_for_coercion ~localise 
+            typeof hdb ~look_for_coercion ~localise 
               metasenv subst context arg None in
           let metasenv, meta, _ = 
             NCicMetaSubst.mk_meta metasenv 
@@ -404,7 +404,7 @@ and eat_prods
           let flex_prod = C.Prod ("_", ty_arg, meta) in
           (* next line grants that ty_args is a type *)
           let metasenv,subst, flex_prod, _ =
-           typeof ~look_for_coercion ~localise metasenv subst
+           typeof hdb ~look_for_coercion ~localise metasenv subst
             context flex_prod None in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
@@ -412,7 +412,7 @@ and eat_prods
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
           let metasenv, subst = 
-             try NCicUnification.unify metasenv subst context t flex_prod 
+             try NCicUnification.unify hdb 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" ^^
                " argument %s of type %s")
@@ -433,7 +433,7 @@ and eat_prods
             (List.length args) (List.length args_so_far))))
       | ty ->
           let metasenv, subst, newhead, newheadty = 
-            try_coercions ~localise ~look_for_coercion metasenv subst context
+            try_coercions hdb ~localise ~look_for_coercion metasenv subst context
               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
               (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
               false

diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index 7414770807cd2dde41355286ce4b8150cc90ba2e..2df108697cc2fcf6518d2e2f22d362b31519e1ad 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.mli
+++ b/helm/software/components/ng_refiner/nCicRefiner.mli
@@ -16,6 +16,7 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val typeof :
+ NCicUnifHint.db ->
  ?localise:(NCic.term -> Stdpp.location) ->
  look_for_coercion:(
     NCic.metasenv -> NCic.substitution -> NCic.context -> 

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c324b0ec6d90b0360eb75ebebf6d7af4c9ed19fe..abbafc4583dc09b9d1553414cbc0de47bde2324a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -99,14 +99,14 @@ let fix_sorts swap metasenv subst context meta t =
     aux () t
 ;;
 
-let rec beta_expand num test_eq_only swap metasenv subst context t arg =
+let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg =
   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
     let metasenv, subst =
      if swap then
-      unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
+      unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
      else
-      unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
+      unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
     in
      (metasenv, subst), NCic.Rel (1 + n)
    with Uncertain _ | UnificationFailure _ ->
@@ -141,7 +141,7 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg =
   with NCicTypeChecker.TypeCheckerFailure _ -> 
     metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 
-and beta_expand_many test_equality_only swap metasenv subst context t args =
+and beta_expand_many hdb test_equality_only swap metasenv subst context t args =
 (* (*D*)  inside 'B'; try let rc = *)
   pp (lazy (String.concat ", "
      (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
@@ -150,7 +150,7 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
     List.fold_right
       (fun arg (num,subst,metasenv,t) ->
          let metasenv, subst, t =
-           beta_expand num test_equality_only swap metasenv subst context t arg
+           beta_expand hdb num test_equality_only swap metasenv subst context t arg
          in
            num+1,subst,metasenv,t)
       args (1,subst,metasenv,t) 
@@ -160,13 +160,13 @@ and beta_expand_many test_equality_only swap metasenv subst context t args =
     metasenv, subst, hd
 (* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
 
-and instantiate test_eq_only metasenv subst context n lc t swap =
+and instantiate hdb test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
          pp (lazy(string_of_int n ^ " :=?= "^
            NCicPp.ppterm ~metasenv ~subst ~context t));
   let unify test_eq_only m s c t1 t2 = 
-    if swap then unify test_eq_only m s c t2 t1 
-    else unify test_eq_only m s c t1 t2
+    if swap then unify hdb test_eq_only m s c t2 t1 
+    else unify hdb test_eq_only m s c t1 t2
   in
   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
   let metasenv, subst, t = 
@@ -245,200 +245,223 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
     metasenv, subst
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
 
-and unify test_eq_only metasenv subst context t1 t2 =
- (*D*) inside 'U'; try let rc = 
-   let fo_unif test_eq_only metasenv subst t1 t2 =
+and unify hdb test_eq_only metasenv subst context t1 t2 =
+ (*D*) inside 'U'; try let rc =
+   let rec fo_unif test_eq_only metasenv subst t1 t2 =
+     let try_hints metasenv subst context t1 t2 (* exc*) =
+       let candidates = NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
+       in
+       let rec cand_iter = function
+         | [] -> None (* raise exc *)
+         | (metasenv,c1,c2)::tl -> 
+             try 
+               prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
+               prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c1);
+               prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
+               prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c2);
+               let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
+               let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
+               Some (fo_unif test_eq_only metasenv subst t1 t2)
+             with
+               UnificationFailure _ | Uncertain _ -> cand_iter tl
+       in
+         cand_iter candidates
+     in
+
     (*D*) inside 'F'; try let rc =  
      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
          NCicPp.ppterm ~metasenv ~subst ~context t2));
      if t1 === t2 then
        metasenv, subst
      else
-       match (t1,t2) with
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
-           if NCicEnvironment.universe_leq a b then metasenv, subst
-           else raise (fail_exc metasenv subst context t1 t2)
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
-           if NCicEnvironment.universe_eq a b then metasenv, subst
-           else raise (fail_exc metasenv subst context t1 t2)
-       | (C.Sort C.Prop,C.Sort (C.Type _)) -> 
-           if (not test_eq_only) then metasenv, subst
-           else raise (fail_exc metasenv subst context t1 t2)
-
-       | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
-       | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           let metasenv, subst = unify true metasenv subst context s1 s2 in
-           unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
-       | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
-           let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
-           let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
-           let context = (name1, C.Def (s1,ty1))::context in
-           unify test_eq_only metasenv subst context t1 t2
-
-       | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
-          (try 
-           let l1 = NCicUtils.expand_local_context l1 in
-           let l2 = NCicUtils.expand_local_context l2 in
-           let metasenv, subst, to_restrict, _ =
-            List.fold_right2 
-             (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
-                try 
-                  let metasenv, subst = 
-                   unify test_eq_only metasenv subst context 
-                    (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
-                  in
-                  metasenv, subst, to_restrict, i-1  
-                with UnificationFailure _ | Uncertain _ ->
-                  metasenv, subst, i::to_restrict, i-1)
-             l1 l2 (metasenv, subst, [], List.length l1)
-           in
-           if to_restrict <> [] then
-             let metasenv, subst, _ = 
-               NCicMetaSubst.restrict metasenv subst n1 to_restrict
-             in
-               metasenv, subst
-           else metasenv, subst
-          with 
-           | Invalid_argument _ -> assert false
-           | NCicMetaSubst.MetaSubstFailure msg ->
-              try 
-                let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
-                let term1 = NCicSubstitution.subst_meta lc1 term in
-                let term2 = NCicSubstitution.subst_meta lc2 term in
-                  unify test_eq_only metasenv subst context term1 term2
-              with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
-
-       | C.Meta (n,lc), t -> 
-           (try 
-             let _,_,term,_ = NCicUtils.lookup_subst n subst in
-             let term = NCicSubstitution.subst_meta lc term in
-               unify test_eq_only metasenv subst context term t
-           with NCicUtils.Subst_not_found _-> 
-             instantiate test_eq_only metasenv subst context n lc t false)
-
-       | t, C.Meta (n,lc) -> 
-           (try 
-             let _,_,term,_ = NCicUtils.lookup_subst n subst in
-             let term = NCicSubstitution.subst_meta lc term in
-               unify test_eq_only metasenv subst context t term
-           with NCicUtils.Subst_not_found _-> 
-             instantiate test_eq_only metasenv subst context n lc t true)
-
-       | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
-            let _,_,term,_ = NCicUtils.lookup_subst i subst in
-            let term = NCicSubstitution.subst_meta l term in
-              unify test_eq_only metasenv subst context (mk_appl term args) t2
-
-       | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
-            let _,_,term,_ = NCicUtils.lookup_subst i subst in
-            let term = NCicSubstitution.subst_meta l term in
-              unify test_eq_only metasenv subst context t1 (mk_appl term args)
-
-       |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
-          NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
-            (try
-              List.fold_left2 
-                (fun (metasenv, subst) t1 t2 ->
-                  unify test_eq_only metasenv subst context t1 t2)
-                (metasenv,subst) l1 l2
-            with Invalid_argument _ -> 
-              raise (fail_exc metasenv subst context t1 t2))
-
-       | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
-           (* we verify that none of the args is a Meta, 
-              since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, subst, beta_expanded =
-                beta_expand_many 
-                  test_eq_only false 
-                  metasenv subst context t2 args
-              in
-                unify test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) beta_expanded 
-
-       | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
-              let metasenv, subst, beta_expanded =
-                beta_expand_many 
-                  test_eq_only true 
-                  metasenv subst context t1 args
-              in
-                unify test_eq_only metasenv subst context 
-                  beta_expanded (C.Meta (i,l))
-
-       (* processing this case here we avoid a useless small delta step *)
-       | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
-         when Ref.eq r1 r2 ->
-           let relevance = NCicEnvironment.get_relevance r1 in
-           let relevance = match r1 with
-             | Ref.Ref (_,Ref.Con (_,_,lno)) ->
-                 let _,relevance = HExtlib.split_nth lno relevance in
-                   HExtlib.mk_list false lno @ relevance
-             | _ -> relevance
-           in
-           let metasenv, subst, _ = 
-             try
-               List.fold_left2 
-                 (fun (metasenv, subst, relevance) t1 t2 ->
-                    let b, relevance = 
-                      match relevance with b::tl -> b,tl | _ -> true, [] in
+       match (try_hints metasenv subst context t1 t2) with
+       | Some x -> x
+       | None ->
+         match (t1,t2) with
+         | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
+             if NCicEnvironment.universe_leq a b then metasenv, subst
+             else raise (fail_exc metasenv subst context t1 t2)
+         | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
+             if NCicEnvironment.universe_eq a b then metasenv, subst
+             else raise (fail_exc metasenv subst context t1 t2)
+         | (C.Sort C.Prop,C.Sort (C.Type _)) -> 
+             if (not test_eq_only) then metasenv, subst
+             else raise (fail_exc metasenv subst context t1 t2)
+
+         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
+         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+             let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
+             unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+         | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
+             let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
+             let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
+             let context = (name1, C.Def (s1,ty1))::context in
+             unify hdb test_eq_only metasenv subst context t1 t2
+
+         | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
+            (try 
+             let l1 = NCicUtils.expand_local_context l1 in
+             let l2 = NCicUtils.expand_local_context l2 in
+             let metasenv, subst, to_restrict, _ =
+              List.fold_right2 
+               (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
+                  try 
                     let metasenv, subst = 
-                      try unify test_eq_only metasenv subst context t1 t2
-                      with UnificationFailure _ | Uncertain _ when not b ->
-                        metasenv, subst
+                     unify hdb test_eq_only metasenv subst context 
+                      (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
                     in
-                      metasenv, subst, relevance)
-                 (metasenv, subst, relevance) tl1 tl2
-             with Invalid_argument _ -> 
-               raise (uncert_exc metasenv subst context t1 t2)
-           in 
-             metasenv, subst
-
-       | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
-          C.Match (ref2,outtype2,term2,pl2)) ->
-          let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
-          let _,_,ty,_ = List.nth itl tyno in
-          let rec remove_prods ~subst context ty = 
-             let ty = NCicReduction.whd ~subst context ty in
-             match ty with
-             | C.Sort _ -> ty
-            | C.Prod (name,so,ta) -> 
-                   remove_prods ~subst ((name,(C.Decl so))::context) ta
-             | _ -> assert false
-           in
-           let is_prop = 
-             match remove_prods ~subst [] ty with
-             | C.Sort C.Prop -> true
-             | _ -> false 
-           in
-          let rec remove_prods ~subst context ty = 
-             let ty = NCicReduction.whd ~subst context ty in
-             match ty with
-             | C.Sort _ -> ty
-            | C.Prod (name,so,ta) -> 
-                   remove_prods ~subst ((name,(C.Decl so))::context) ta
-             | _ -> assert false
-           in
-           if not (Ref.eq ref1 ref2) then 
-             raise (uncert_exc metasenv subst context t1 t2) 
-           else
-             let metasenv, subst = 
-               unify test_eq_only metasenv subst context outtype1 outtype2 in
-             let metasenv, subst = 
-               try unify test_eq_only metasenv subst context term1 term2 
-               with UnificationFailure _ | Uncertain _ when is_prop -> 
+                    metasenv, subst, to_restrict, i-1  
+                  with UnificationFailure _ | Uncertain _ ->
+                    metasenv, subst, i::to_restrict, i-1)
+               l1 l2 (metasenv, subst, [], List.length l1)
+             in
+             if to_restrict <> [] then
+               let metasenv, subst, _ = 
+                 NCicMetaSubst.restrict metasenv subst n1 to_restrict
+               in
                  metasenv, subst
+             else metasenv, subst
+            with 
+             | Invalid_argument _ -> assert false
+             | NCicMetaSubst.MetaSubstFailure msg ->
+                try 
+                  let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
+                  let term1 = NCicSubstitution.subst_meta lc1 term in
+                  let term2 = NCicSubstitution.subst_meta lc2 term in
+                    unify hdb test_eq_only metasenv subst context term1 term2
+                with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+         | C.Meta (n,lc), t -> 
+             (try 
+               let _,_,term,_ = NCicUtils.lookup_subst n subst in
+               let term = NCicSubstitution.subst_meta lc term in
+                 unify hdb test_eq_only metasenv subst context term t
+             with NCicUtils.Subst_not_found _-> 
+               instantiate hdb test_eq_only metasenv subst context n lc t false)
+
+         | t, C.Meta (n,lc) -> 
+             (try 
+               let _,_,term,_ = NCicUtils.lookup_subst n subst in
+               let term = NCicSubstitution.subst_meta lc term in
+                 unify hdb test_eq_only metasenv subst context t term
+             with NCicUtils.Subst_not_found _-> 
+               instantiate hdb test_eq_only metasenv subst context n lc t true)
+
+         | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
+              let _,_,term,_ = NCicUtils.lookup_subst i subst in
+              let term = NCicSubstitution.subst_meta l term in
+                unify hdb test_eq_only metasenv subst context (mk_appl term args) t2
+
+         | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+              let _,_,term,_ = NCicUtils.lookup_subst i subst in
+              let term = NCicSubstitution.subst_meta l term in
+                unify hdb test_eq_only metasenv subst context t1 (mk_appl term args)
+
+         |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
+            NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+              (try
+                List.fold_left2 
+                  (fun (metasenv, subst) t1 t2 ->
+                    unify hdb test_eq_only metasenv subst context t1 t2)
+                  (metasenv,subst) l1 l2
+              with Invalid_argument _ -> 
+                raise (fail_exc metasenv subst context t1 t2))
+
+         | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
+             (* we verify that none of the args is a Meta, 
+                since beta expanding w.r.t a metavariable makes no sense  *)
+                let metasenv, subst, beta_expanded =
+                  beta_expand_many hdb 
+                    test_eq_only false 
+                    metasenv subst context t2 args
+                in
+                  unify hdb test_eq_only metasenv subst context 
+                    (C.Meta (i,l)) beta_expanded 
+
+         | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
+                let metasenv, subst, beta_expanded =
+                  beta_expand_many hdb 
+                    test_eq_only true 
+                    metasenv subst context t1 args
+                in
+                  unify hdb test_eq_only metasenv subst context 
+                    beta_expanded (C.Meta (i,l))
+
+         (* processing this case here we avoid a useless small delta step *)
+         | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
+           when Ref.eq r1 r2 ->
+             let relevance = NCicEnvironment.get_relevance r1 in
+             let relevance = match r1 with
+               | Ref.Ref (_,Ref.Con (_,_,lno)) ->
+                   let _,relevance = HExtlib.split_nth lno relevance in
+                     HExtlib.mk_list false lno @ relevance
+               | _ -> relevance
+             in
+             let metasenv, subst, _ = 
+               try
+                 List.fold_left2 
+                   (fun (metasenv, subst, relevance) t1 t2 ->
+                      let b, relevance = 
+                        match relevance with b::tl -> b,tl | _ -> true, [] in
+                      let metasenv, subst = 
+                        try unify hdb test_eq_only metasenv subst context t1 t2
+                        with UnificationFailure _ | Uncertain _ when not b ->
+                          metasenv, subst
+                      in
+                        metasenv, subst, relevance)
+                   (metasenv, subst, relevance) tl1 tl2
+               with Invalid_argument _ -> 
+                 raise (uncert_exc metasenv subst context t1 t2)
+             in 
+               metasenv, subst
+
+         | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+            C.Match (ref2,outtype2,term2,pl2)) ->
+             let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
+             let _,_,ty,_ = List.nth itl tyno in
+             let rec remove_prods ~subst context ty = 
+               let ty = NCicReduction.whd ~subst context ty in
+               match ty with
+               | C.Sort _ -> ty
+               | C.Prod (name,so,ta) -> 
+                     remove_prods ~subst ((name,(C.Decl so))::context) ta
+               | _ -> assert false
+             in
+             let is_prop = 
+               match remove_prods ~subst [] ty with
+               | C.Sort C.Prop -> true
+               | _ -> false 
+             in
+             let rec remove_prods ~subst context ty = 
+               let ty = NCicReduction.whd ~subst context ty in
+               match ty with
+               | C.Sort _ -> ty
+               | C.Prod (name,so,ta) -> 
+                     remove_prods ~subst ((name,(C.Decl so))::context) ta
+               | _ -> assert false
              in
-             (try
-              List.fold_left2 
-               (fun (metasenv,subst) -> 
-                  unify test_eq_only metasenv subst context)
-               (metasenv, subst) pl1 pl2
-             with Invalid_argument _ -> 
-               raise (uncert_exc metasenv subst context t1 t2))
-       | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
-       | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
-                NCicUntrusted.metas_of_term subst context t2 = [] -> 
-                  raise (fail_exc metasenv subst context t1 t2)
-       | _ -> raise (uncert_exc metasenv subst context t1 t2)
+             if not (Ref.eq ref1 ref2) then 
+               raise (uncert_exc metasenv subst context t1 t2) 
+             else
+               let metasenv, subst = 
+                 unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
+               let metasenv, subst = 
+                 try unify hdb test_eq_only metasenv subst context term1 term2 
+                 with UnificationFailure _ | Uncertain _ when is_prop -> 
+                   metasenv, subst
+               in
+               (try
+                List.fold_left2 
+                 (fun (metasenv,subst) -> 
+                    unify hdb test_eq_only metasenv subst context)
+                 (metasenv, subst) pl1 pl2
+               with Invalid_argument _ -> 
+                 raise (uncert_exc metasenv subst context t1 t2))
+         | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+         | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
+                  NCicUntrusted.metas_of_term subst context t2 = [] -> 
+                    raise (fail_exc metasenv subst context t1 t2)
+         | _ -> raise (uncert_exc metasenv subst context t1 t2)
      (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in
     let height_of = function
@@ -520,8 +543,8 @@ and unify test_eq_only metasenv subst context t1 t2 =
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
-let unify = 
+let unify hdb = 
   indent := "";      
-  unify false;;
+  unify hdb false;;
 
 

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 97976b7a308bbe34aae83a06b5b1f147ccd9b290..54ccf2143f479a2aec9251aba5296098f0fa8e0a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -16,6 +16,7 @@ exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val unify :
+  NCicUnifHint.db ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term ->
    NCic.metasenv * NCic.substitution