unification encore...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 163 insertions, 76 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 7753ec7ed7..ef0425e377 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -24,14 +24,21 @@ open Tacexpr
 open Tacred
 open Pretype_errors
 open Evarutil
+open Unification
 
 (* *)
-let get_env   evc = Global.env_of_context evc.it
+let pf_env gls = Global.env_of_context gls.it.evar_hyps
+let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
+let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
+
+let get_env wc = Global.env_of_context wc.it
 let w_type_of wc c  =
   Typing.type_of (get_env wc) wc.sigma c
 let w_hnf_constr wc c        = hnf_constr (get_env wc) wc.sigma c
 let get_concl gl = gl.it.evar_concl
 
+let mk_wc gls = {it=gls.it.evar_hyps; sigma=gls.sigma}
+
 (* Generator of metavariables *)
 let new_meta =
   let meta_ctr = ref 0 in
@@ -74,6 +81,10 @@ type 'a clausenv = {
 
 type wc = named_context sigma
 
+let clenv_nf_meta clenv c = nf_meta clenv.env c
+let clenv_meta_type clenv mv = meta_type clenv.env mv
+let clenv_value clenv = meta_instance clenv.env clenv.templval
+let clenv_type clenv = meta_instance clenv.env clenv.templtyp
 
 (* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
  * mv0, or if one of the free vars on mv1's freelist mentions
@@ -136,15 +147,15 @@ let clenv_environments bound c =
   in 
   clrec (Metamap.empty,Metamap.empty,[]) bound c
 
-let mk_clenv_from_n wc n (c,cty) =
+let mk_clenv_from_n gls n (c,cty) =
   let (namenv,env,args,concl) = clenv_environments n cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
     namenv = namenv;
     env = env;
-    hook = wc }
+    hook = mk_wc gls }
 
-let mk_clenv_from wc = mk_clenv_from_n wc None
+let mk_clenv_from gls = mk_clenv_from_n gls None
 
 let subst_clenv f sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
@@ -162,23 +173,23 @@ let clenv_wtactic f clenv =
     f (create_evar_defs clenv.hook.sigma, clenv.env) in
   {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
 
-let mk_clenv_hnf_constr_type_of wc t =
-  mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
+let mk_clenv_hnf_constr_type_of gls t =
+  mk_clenv_from gls (t,pf_hnf_constr gls (pf_type_of gls t))
 
-let mk_clenv_rename_from wc (c,t) = 
-  mk_clenv_from wc (c,rename_bound_var (get_env wc) [] t)
+let mk_clenv_rename_from gls (c,t) = 
+  mk_clenv_from gls (c,rename_bound_var (pf_env gls) [] t)
 
-let mk_clenv_rename_from_n wc n (c,t) = 
-  mk_clenv_from_n wc n (c,rename_bound_var (get_env wc) [] t)
-    
-let mk_clenv_rename_type_of wc t =
-  mk_clenv_from wc (t,rename_bound_var (get_env wc) [] (w_type_of wc t))
+let mk_clenv_rename_from_n gls n (c,t) = 
+  mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
+
+let mk_clenv_rename_type_of gls t =
+  mk_clenv_from gls (t,rename_bound_var (pf_env gls) [] (pf_type_of gls t))
     
-let mk_clenv_rename_hnf_constr_type_of wc t =
-  mk_clenv_from wc
-    (t,rename_bound_var (get_env wc) [] (w_hnf_constr wc (w_type_of wc t)))
+let mk_clenv_rename_hnf_constr_type_of gls t =
+  mk_clenv_from gls
+    (t,rename_bound_var (pf_env gls) [] (pf_hnf_constr gls (pf_type_of gls t)))
 
-let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 			      
 let clenv_assign mv rhs clenv =
   let rhs_fls = mk_freelisted rhs in 
@@ -250,12 +261,12 @@ let clenv_defined clenv mv =
     | Clval _ -> true
     | Cltyp _ -> false
 
-let clenv_value clenv mv =
+let clenv_value0 clenv mv =
   match Metamap.find mv clenv.env with
     | Clval(b,_) -> b
-    | Cltyp _ -> failwith "clenv_value"
+    | Cltyp _ -> failwith "clenv_value0"
 	  
-let clenv_type clenv mv =
+let clenv_type0 clenv mv =
   match Metamap.find mv clenv.env with
     | Cltyp b -> b
     | Clval(_,b) -> b
@@ -265,10 +276,10 @@ let clenv_template clenv = clenv.templval
 let clenv_template_type clenv = clenv.templtyp
 
 let clenv_instance_value clenv mv =
-  clenv_instance clenv (clenv_value clenv mv)
+  clenv_instance clenv (clenv_value0 clenv mv)
     
 let clenv_instance_type clenv mv =
-  clenv_instance clenv (clenv_type clenv mv)
+  clenv_instance clenv (clenv_type0 clenv mv)
     
 let clenv_instance_template clenv =
   clenv_instance clenv (clenv_template clenv)
@@ -291,12 +302,13 @@ let clenv_instance_type_of ce c =
 
 let clenv_unify allow_K cv_pb t1 t2 clenv =
   let env = get_env clenv.hook in
-  clenv_wtactic (Unification.w_unify allow_K env cv_pb t1 t2) clenv
+  clenv_wtactic (w_unify allow_K env cv_pb t1 t2) clenv
 
 let clenv_unique_resolver allow_K clause gl =
   clenv_unify allow_K CUMUL
     (clenv_instance_template_type clause) (get_concl gl) clause 
 
+
 (* [clenv_bchain mv clenv' clenv]
  *
  * Resolves the value of "mv" (which must be undefined) in clenv to be
@@ -438,6 +450,27 @@ let clenv_constrain_dep_args hyps_only clause = function
 	error ("Not the right number of missing arguments (expected "
 	       ^(string_of_int (List.length occlist))^")")
 
+(* [clenv_pose_dependent_evars clenv]
+ * For each dependent evar in the clause-env which does not have a value,
+ * pose a value for it by constructing a fresh evar.  We do this in
+ * left-to-right order, so that every evar's type is always closed w.r.t.
+ * metas. *)
+let clenv_pose_dependent_evars clenv =
+  let dep_mvs = clenv_dependent false clenv in
+  List.fold_left
+    (fun clenv mv ->
+       let evar = Evarutil.new_evar_in_sign (get_env clenv.hook) in
+       let (evar_n,_) = destEvar evar in
+       let tY = clenv_instance_type clenv mv in
+       let clenv' =
+         clenv_wtactic (w_Declare (get_env clenv.hook) evar_n tY) clenv in
+       clenv_assign mv evar clenv')
+    clenv
+    dep_mvs
+
+let evar_clenv_unique_resolver clenv gls =
+  clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)
+
 let clenv_constrain_missing_args mlist clause =
   clenv_constrain_dep_args true clause mlist
 
@@ -531,19 +564,25 @@ let clenv_constrain_with_bindings bl clause =
 
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen n wc (c,t) = function
+let make_clenv_binding_gen n gls (c,t) = function
   | ImplicitBindings largs ->
-      let clause = mk_clenv_from_n wc n (c,t) in
+      let clause = mk_clenv_from_n gls n (c,t) in
       clenv_constrain_dep_args (n <> None) clause largs
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_rename_from_n wc n (c,t) in
+      let clause = mk_clenv_rename_from_n gls n (c,t) in
       clenv_match_args lbind clause
   | NoBindings ->
-      mk_clenv_from_n wc n (c,t)
+      mk_clenv_from_n gls n (c,t)
 
 let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
 let make_clenv_binding = make_clenv_binding_gen None
 
+
+
+
+
+
+
 let pr_clenv clenv =
   let pr_name mv =
     try 
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index d3f36e7205..9ed07fc0d1 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -23,10 +23,20 @@ val new_meta : unit -> metavariable
 (* [exist_to_meta] generates new metavariables for each existential
    and performs the replacement in the given constr *)
 val exist_to_meta :
-  Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
+  evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
 
+(***************************************************************)
 (* The Type of Constructions clausale environments. *)
 
+(* [templval] is the template which we are trying to fill out.
+ * [templtyp] is its type.
+ * [namenv] is a mapping from metavar numbers to names, for
+ *          use in instanciating metavars by name.
+ * [evd] is the mapping from metavar and evar numbers to their types
+ *       and values.
+ * [hook] is generally signature (named_context) and a sigma: the
+ *        typing context
+ *)
 type 'a clausenv = {
   templval : constr freelisted;
   templtyp : constr freelisted;
@@ -36,70 +46,97 @@ type 'a clausenv = {
 
 type wc = named_context sigma (* for a better reading of the following *)
 
-(* [templval] is the template which we are trying to fill out.
- * [templtyp] is its type.
- * [namenv] is a mapping from metavar numbers to names, for
- *          use in instanciating metavars by name.
- * [env] is the mapping from metavar numbers to their types
- *       and values.
- * [hook] is the pointer to the current walking context, for
- *        integrating existential vars and metavars. *)
-
-val collect_metas : constr -> metavariable list
-val mk_clenv : 'a -> constr -> 'a clausenv
-val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
-val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
-val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
-val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
-val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
-val mk_clenv_type_of : wc -> constr -> wc clausenv
-
 val subst_clenv : (substitution -> 'a -> 'a) -> 
   substitution -> 'a clausenv -> 'a clausenv
-val clenv_wtactic :
-  (evar_defs * meta_map -> evar_defs * meta_map) -> wc clausenv -> wc clausenv
+
+val clenv_nf_meta   : wc clausenv -> constr -> constr
+val clenv_meta_type : wc clausenv -> int -> constr
+val clenv_value     : wc clausenv -> constr
+val clenv_type      : wc clausenv -> constr
+
+val mk_clenv_from : evar_info sigma -> constr * constr -> wc clausenv
+val mk_clenv_from_n :
+  evar_info sigma -> int option -> constr * constr -> wc clausenv
+val mk_clenv_rename_from_n :
+  evar_info sigma -> int option -> constr * constr -> wc clausenv
+val mk_clenv_type_of : evar_info sigma -> constr -> wc clausenv
+
+(***************************************************************)
+(* linking of clenvs *)
 
 val connect_clenv : evar_info sigma -> 'a clausenv -> wc clausenv
-val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
-val clenv_instance_term : wc clausenv -> constr -> constr
-val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
-val clenv_template : 'a clausenv -> constr freelisted
-val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : wc clausenv -> metavariable -> constr
-val clenv_instance_template : wc clausenv -> constr
-val clenv_instance_template_type : wc clausenv -> constr
-val clenv_instance : 'a clausenv -> constr freelisted -> constr
-val clenv_type_of : wc clausenv -> constr -> constr
 val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
 
-(* Unification with clenv *)
-type arg_bindings = (int * constr) list
+(***************************************************************)
+(* Unification with clenvs *)
 
+(* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *)
 val clenv_unify : 
   bool -> Reductionops.conv_pb -> constr -> constr ->
   wc clausenv -> wc clausenv
-val clenv_match_args :
-  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
 
+(* unifies the concl of the goal with the type of the clenv *)
+val clenv_unique_resolver :
+  bool -> wc clausenv -> evar_info sigma -> wc clausenv
+
+(* same as above (allow_K=false) but replaces remaining metas
+   with fresh evars *)
+val evar_clenv_unique_resolver :
+  wc clausenv -> evar_info sigma -> wc clausenv
+
+(***************************************************************)
 (* Bindings *)
+
+(* bindings where the key is the position in the template of the
+   clenv (dependent or not). Positions can be negative meaning to
+   start from the rightmost argument of the template. *)
+type arg_bindings = (int * constr) list
+
 val clenv_independent : wc clausenv -> metavariable list
-val clenv_dependent : bool -> 'a clausenv -> metavariable list
 val clenv_missing : 'a clausenv -> metavariable list
-val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
-  constr list -> wc clausenv -> wc clausenv
-(*
-val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
-*)
 val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
-val clenv_unique_resolver :
-  bool -> wc clausenv -> evar_info sigma -> wc clausenv
 
+(* defines metas corresponding to the name of the bindings *)
+val clenv_match_args :
+  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
+val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+
+(* start with a clenv to refine with a given term with bindings *)
+
+(* 1- the arity of the lemma is fixed *)
 val make_clenv_binding_apply :
-  wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
+  evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings ->
+   wc clausenv
 val make_clenv_binding :
-  wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
+  evar_info sigma -> constr * constr -> constr Rawterm.bindings -> wc clausenv
 
+(***************************************************************)
 (* Pretty-print *)
 val pr_clenv : 'a clausenv -> Pp.std_ppcmds
+
+(***************************************************************)
+(* Old or unused stuff... *)
+
+val collect_metas : constr -> metavariable list
+val mk_clenv : 'a -> constr -> 'a clausenv
+
+val mk_clenv_rename_from : evar_info sigma -> constr * constr -> wc clausenv
+val mk_clenv_hnf_constr_type_of : evar_info sigma -> constr -> wc clausenv
+
+val clenv_wtactic :
+  (evar_defs * meta_map -> evar_defs * meta_map) -> wc clausenv -> wc clausenv
+val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
+val clenv_instance_term : wc clausenv -> constr -> constr
+val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
+val clenv_template : 'a clausenv -> constr freelisted
+val clenv_template_type : 'a clausenv -> constr freelisted
+val clenv_instance_type : wc clausenv -> metavariable -> constr
+val clenv_instance_template : wc clausenv -> constr
+val clenv_instance_template_type : wc clausenv -> constr
+val clenv_instance : 'a clausenv -> constr freelisted -> constr
+val clenv_type_of : wc clausenv -> constr -> constr
+val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_dependent : bool -> 'a clausenv -> metavariable list
+val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
+  constr list -> wc clausenv -> wc clausenv
+
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 58b3f3ac2f..9a4c9cfed0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -279,7 +279,9 @@ let real_clean env isevars ev args rhs =
       | Evar (ev,args) ->
 	  let args' = Array.map (subs k) args in
 	  if need_restriction !evd args' then
-            begin
+            if Evd.is_defined !evd.evars ev then 
+	      subs k (existential_value !evd.evars (ev,args'))
+	    else begin
 	      let (sigma,rc) = do_restrict_hyps !evd.evars ev args' in
               evd :=
 	      {!evd with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83377449dd..4a9cab2067 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -51,6 +51,13 @@ let abstract_list_all env sigma typ c l =
 
 type maps = evar_defs * meta_map
 
+let w_Declare env sp ty (evd,mmap) =
+  let sigma = evars_of evd in
+  let _ = Typing.type_of env sigma ty in (* Utile ?? *)
+  let newdecl =
+    { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in 
+  (evars_reset_evd (Evd.add sigma sp newdecl) evd, mmap)
+
 (* [w_Define evd sp c]
  *
  * Defines evar [sp] with term [c] in evar context [evd].
@@ -66,7 +73,8 @@ let w_Define sp c (evd,mmap) =
   let spdecl = Evd.map sigma sp in
   let env = evar_env spdecl in
   let _ =
-    try Typing.mcheck env (Evd.rmv sigma sp,Metamap.empty) c spdecl.evar_concl
+    (* Do not consider the metamap because evars may not depend on metas *)
+    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
     with
 	Not_found -> error "Instantiation contains unlegal variables"
       | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index f033c9e87f..02d1918bed 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -20,6 +20,7 @@ open Evarutil
 
 type maps = evar_defs * meta_map
 
+val w_Declare : env -> evar -> types -> maps -> maps
 val w_Define : evar -> constr -> maps -> maps
 
 (* The "unique" unification fonction *)