Populate the sort constraints set correctly during unification. Add a

[set_eq_sort_variable] for cases where two universes should be equal,
fix [evars_reset_evd] to keep sort constraints and use [whd_sort_var]
directly in [whd_evar].


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

6 files changed, 64 insertions, 20 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 352b76dd9..0d5df1615 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,15 +24,22 @@ open Evarutil
 open Libnames
 open Evd
 
-let base_sort_conv evd pb s0 s1 =
-  match (s0,s1) with
+let base_sort_conv evd pb s1 s2 =
+  match (s1,s2) with
     | (Prop c1, Prop c2) -> if c1 = Null or c2 = Pos then Some evd else None (* Prop <= Set *)
-    | (Prop c1, Type u)  -> if pb = Reduction.CUMUL then Some evd else None
+    | (Prop c1, Type u)  -> 
+	if pb = Reduction.CUMUL then Some evd 
+	else if Evd.is_sort_variable evd s2 then
+	  Some (Evd.define_sort_variable evd s2 s1)
+	else None
     | (Type u, Prop c)   -> 
-	if Evd.is_sort_variable evd s0 then
-	  Some (Evd.define_sort_variable evd s0 s1)
+	if Evd.is_sort_variable evd s1 then
+	  Some (Evd.define_sort_variable evd s1 s2)
 	else None
-    | (Type u1, Type u2) -> Some evd
+    | (Type u1, Type u2) -> 
+	match pb with
+	| CONV -> Some (Evd.set_eq_sort_variable evd s1 s2)
+	| CUMUL -> Some (Evd.set_leq_sort_variable evd s1 s2)
 
 let unify_constr_univ evd f cv_pb t1 t2 = 
   match kind_of_term t1, kind_of_term t2 with
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 2a2cd5271..ec4247600 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -17,6 +17,9 @@ open Evd
 (*i*)
 
 (* Comparison function considering sort variables. *)
+val base_sort_conv : evar_defs -> conv_pb ->
+  sorts -> sorts -> evar_defs option
+
 val constr_unify_with_sorts : evar_defs -> conv_pb ->
   types -> types -> bool * evar_defs
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index cfdd76de8..3c87defa0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -202,7 +202,7 @@ let whd_sort_var scstr t =
     | _ -> t
 
 let rec set_impredicative u s scstr =
-  match UniverseMap.find u scstr with
+  match snd (find_univ u scstr) with
     | DefinedSort s' ->
         if family_of_sort s = family_of_sort s' then scstr
         else failwith "sort constraint inconsistency"
@@ -214,7 +214,7 @@ let rec set_impredicative u s scstr =
           (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
 
 let rec set_predicative u s scstr =
-  match UniverseMap.find u scstr with
+  match snd (find_univ u scstr) with
     | DefinedSort s' ->
         if family_of_sort s = family_of_sort s' then scstr
         else failwith "sort constraint inconsistency"
@@ -264,9 +264,7 @@ let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
     UniverseMap.add u1 (SortVar(u2::leq1,geq1))
       (UniverseMap.add u2 (SortVar(leq2, u1::geq2)) scstr)
 
-let set_leq s1 s2 scstr =
-  let u1 = var_of_sort s1 in
-  let u2 = var_of_sort s2 in
+let set_leq_var u1 u2 scstr =
   let (cu1,c1) = find_univ u1 scstr in
   let (cu2,c2) = find_univ u2 scstr in
   if cu1=cu2 then scstr
@@ -280,6 +278,31 @@ let set_leq s1 s2 scstr =
       | DefinedSort(Type _ as s), _ -> set_predicative u2 s scstr
       | DefinedSort(Prop _), _ -> scstr
 
+let set_leq s1 s2 scstr =
+  let u1 = var_of_sort s1 in
+  let u2 = var_of_sort s2 in
+    set_leq_var u1 u2 scstr
+
+let set_eq_sort (u1,(leq1,geq1)) u2 scstr =
+  UniverseMap.add u1 (EqSort u2)
+    (List.fold_left (fun g u -> set_leq_var u u2 g) 
+	(List.fold_left (fun g u -> set_leq_var u2 u g) scstr geq1) leq1)
+
+let set_eq s1 s2 scstr = 
+  let u1 = var_of_sort s1 in
+  let u2 = var_of_sort s2 in
+  let (cu1,c1) = find_univ u1 scstr in
+  let (cu2,c2) = find_univ u2 scstr in
+  if cu1=cu2 then scstr
+  else
+    match c1,c2 with
+        (EqSort _, _ | _, EqSort _) -> assert false
+      | SortVar(leq1,geq1), _ ->
+          set_eq_sort (cu1,(leq1,geq1)) cu2 scstr
+      | _, SortVar(leq2,geq2) ->
+          set_eq_sort (cu2,(leq2,geq2)) cu1 scstr
+      | DefinedSort s, DefinedSort s' -> scstr
+
 let set_sort_variable s1 s2 scstr =
   let u = var_of_sort s1 in
   match s2 with
@@ -319,10 +342,11 @@ module EvarMap = struct
     (EvarInfoMap.equal eq_evar_info (fst x) (fst y) &&
       UniverseMap.equal (=) (snd x) (snd y))
   let constraints (sigma,sm) = sm
+  let merge_constraints sm sm' =
+    UniverseMap.fold (fun u cstr sm -> UniverseMap.add u cstr sm) sm' sm
   let merge (sigma,sm) (sigma',sm') = 
     let ev = EvarInfoMap.fold (fun n v sigma -> EvarInfoMap.add sigma n v) sigma' sigma in
-    let sm = UniverseMap.fold (fun u cstr sm -> UniverseMap.add u cstr sm) sm' sm in
-      (ev,sm)
+      (ev,merge_constraints sm sm')
   
 end
  
@@ -507,7 +531,8 @@ let empty =  {
   metas=Metamap.empty 
 }
 
-let evars_reset_evd evd d = {d with evars = evd.evars}
+let evars_reset_evd evd d = {d with evars = (fst evd.evars, 
+					    EvarMap.merge_constraints (snd evd.evars) (snd d.evars))}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source evk d =
   try List.assoc evk d.history
@@ -595,6 +620,8 @@ let is_sort_variable {evars=(_,sm)} s =
 let whd_sort_variable {evars=(_,sm)} t = whd_sort_var sm t
 let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
   { d with evars = (sigma, set_leq u1 u2 sm) }
+let set_eq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
+  { d with evars = (sigma, set_eq u1 u2 sm) }
 let define_sort_variable ({evars=(sigma,sm)}as d) u s =
   { d with evars = (sigma, set_sort_variable u s sm) }
 let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a26c2dadc..040cbf28c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -240,6 +240,7 @@ val new_sort_variable : evar_defs -> sorts * evar_defs
 val is_sort_variable : evar_defs -> sorts -> bool
 val whd_sort_variable : evar_defs -> constr -> constr
 val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
+val set_eq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val solve_sort_constraints : evar_defs -> evar_defs
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 859f8bb21..17d8e5d80 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -510,7 +510,7 @@ let rec whd_evar sigma c =
         (match safe_evar_value sigma ev with
             Some c -> whd_evar sigma c
           | None -> c)
-    | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
+    | Sort s -> whd_sort_variable sigma c
     | _ -> c
 
 let nf_evar =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f412f5486..85ca0917d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -180,6 +180,14 @@ let is_trans_fconv_pb pb flags env sigma m n =
   | Cumul -> is_trans_fconv CUMUL flags env sigma m n
   | ConvUnderApp _ -> is_trans_fconv CONV flags env sigma m n
 
+let occur_meta_or_sortvar evd c =
+  let rec occrec c = match kind_of_term c with
+    | Meta _ -> raise Occur
+    | Sort s -> if Evd.is_sort_variable evd s then raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
+
+
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let trivial_unify curenv pb (sigma,metasubst,_) m n =
     let subst = if flags.use_metas_eagerly then metasubst else ms in
@@ -361,7 +369,8 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
 
   in
-    if (if occur_meta m || occur_meta n then false else
+  let m = whd_sort_variable sigma m and n = whd_sort_variable sigma n in
+    if (if occur_meta_or_sortvar sigma m || occur_meta_or_sortvar sigma n then false else
       if (match flags.modulo_conv_on_closed_terms with
       | Some flags ->
 	  is_trans_fconv_pb cv_pb flags env sigma m n
@@ -564,10 +573,7 @@ let unify_to_type env sigma flags c status u =
       unify_0 env sigma Cumul flags u t
     else if status = IsSubType then
       unify_0 env sigma Cumul flags t u
-    else 
-      try unify_0 env sigma Cumul flags t u
-      with e when precatchable_exception e ->
-	unify_0 env sigma Cumul flags u t
+    else unify_0 env sigma topconv flags t u
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in