From 726130d3d847e59d3556f6b302de155dc052d6a4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 4 Aug 2011 14:42:55 +0000
Subject: Fix unification: detect invalid evar instantiations due to scoping
 earlier. Add a debug printer for existential sets (used for frozen_evars in
 w_unify).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14384 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/include               |  1 +
 dev/top_printers.ml       |  4 ++++
 pretyping/unification.ml  | 22 ++++++++++++++--------
 pretyping/unification.mli |  9 +++++++++
 4 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/dev/include b/dev/include
index 5d48722732..705e8e3754 100644
--- a/dev/include
+++ b/dev/include
@@ -28,6 +28,7 @@
 #install_printer  (* Goal.goal *)  ppgoalgoal;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
+#install_printer  (* ExistentialSet.t *) ppexistentialset;;
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index bb8d0a68b2..278fdb399c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -114,6 +114,10 @@ let pp_transparent_state s = pp (pr_transparent_state s)
 let ppmetas metas = pp(pr_metaset metas)
 let ppevm evd = pp(pr_evar_map (Some 2) evd)
 let ppevmall evd = pp(pr_evar_map None evd)
+let pr_existentialset evars =
+  prlist_with_sep spc pr_meta (ExistentialSet.elements evars)
+let ppexistentialset evars =
+  pp (pr_existentialset evars)
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0d2b2af003..31bf431da1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -327,9 +327,10 @@ let oracle_order env cf1 cf2 =
       | None -> Some true
       | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
 
-let do_reduce ts env sigma c =
-  let (t, l) = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in
-    applist (t, list_of_stack l)
+let do_reduce ts (env, nb) sigma c =
+  let (t, stack') = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in
+  let l = list_of_stack stack' in
+    applist (t, l)
 
 let use_full_betaiota flags =
   flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
@@ -369,11 +370,16 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
 	| Evar (evk,_ as ev), _
             when not (ExistentialSet.mem evk flags.frozen_evars) ->
-            sigma,metasubst,((curenv, ev,cN)::evarsubst)
+	    let cmvars = free_rels cM and cnvars = free_rels cN in
+	      if Intset.subset cnvars cmvars then
+		sigma,metasubst,((curenv,ev,cN)::evarsubst)
+	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Evar (evk,_ as ev)
             when not (ExistentialSet.mem evk flags.frozen_evars) ->
-            sigma,metasubst,((curenv, ev,cM)::evarsubst)
-
+	    let cmvars = free_rels cM and cnvars = free_rels cN in
+	      if Intset.subset cmvars cnvars then
+		sigma,metasubst,((curenv,ev,cM)::evarsubst)
+	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| Sort s1, Sort s2 ->
 	    (try 
 	       let sigma' = 
@@ -457,11 +463,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 
   and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN =
     if use_full_betaiota flags && not (subterm_restriction b flags) then
-      let cM' = do_reduce flags.modulo_delta (fst curenvnb) sigma cM in
+      let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
 	if not (eq_constr cM cM') then
 	  unirec_rec curenvnb pb b substn cM' cN
 	else
-	  let cN' = do_reduce flags.modulo_delta (fst curenvnb) sigma cN in
+	  let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
 	    if not (eq_constr cN cN') then
 	      unirec_rec curenvnb pb b substn cM cN'
 	    else error_cannot_unify (fst curenvnb) sigma (cM,cN)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 37eaa58026..cc781c8712 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -66,3 +66,12 @@ val w_merge : env -> bool -> unify_flags -> evar_map *
   (metavariable * constr * (instance_constraint * instance_typing_status)) list *
   (env * types pexistential * types) list -> evar_map
 
+val unify_0 :            Environ.env ->
+           Evd.evar_map ->
+           Evd.conv_pb ->
+           unify_flags ->
+           Term.types ->
+           Term.types ->
+           Evd.evar_map * Evd.metabinding list *
+           (Environ.env * Term.types Term.pexistential * Term.constr) list
+
-- 
cgit v1.2.3