reparations de quelques petits bugs d\'unification + introduction de la notion de variable de sortes (mais pas encore utilise...

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

7 files changed, 203 insertions, 26 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 047b306ed6..835f1e00da 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -180,10 +180,8 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
-  if
-    (not (has_undefined_evars isevars term1) &
-    not (has_undefined_evars isevars term2) &
-    is_fconv pbty env (evars_of isevars) term1 term2) then
+  if is_ground_term isevars term1 && is_ground_term isevars term2 &
+     is_fconv pbty env (evars_of isevars) term1 term2 then
       (isevars,true)
   else if is_undefined_evar isevars term1 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0e87e58938..00c8195b37 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -309,11 +309,14 @@ let do_restrict_hyps evd ev args =
   let env = evar_env evi in
   let hyps = evi.evar_hyps in
   let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
-  let (evd',nc) =
-    new_evar_instance sign !evd evi.evar_concl
-      ~src:(evar_source ev !evd) ncargs in
-  evd := Evd.evar_define ev nc evd';
-  nc
+  (* No care is taken in case the evar type uses vars filtered out!
+     Is it important ? *)
+  let nc =
+    e_new_evar evd (reset_with_named_context sign env)
+      ~src:(evar_source ev !evd) evi.evar_concl in
+  evd := Evd.evar_define ev nc !evd;
+  let (evn,_) = destEvar nc in
+  mkEvar(evn,Array.of_list ncargs)
 
 
 let need_restriction isevars args = not (array_for_all closed0 args)
@@ -387,18 +390,20 @@ let evar_define env (ev,argsv) rhs isevars =
   let (isevars',body) = real_clean env isevars ev evi worklist rhs in
   if occur_meta body then error "Meta cannot occur in evar body"
   else
+    (* needed only if an inferred type *)
+    let body = refresh_universes body in
     let _ =
-(*      try*)
+      try
         let env = evar_env evi in
         let ty = evi.evar_concl in
         Typing.check env (evars_of isevars') body ty
-(*      with e ->
+      with e ->
         pperrnl
           (str "Ill-typed evar instantiation: " ++ fnl() ++
            pr_evar_defs isevars' ++ fnl() ++
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
-        raise e*) in
+        raise e in
     let isevars'' = Evd.evar_define ev body isevars' in
     isevars'',[ev]
 
@@ -412,6 +417,9 @@ let has_undefined_evars isevars t =
   try let _ = local_strong (whd_ise (evars_of isevars)) t in false
   with Uninstantiated_evar _ -> true
 
+let is_ground_term isevars t =
+  not (has_undefined_evars isevars t)
+
 let head_is_evar isevars = 
   let rec hrec k = match kind_of_term k with
     | Evar n   -> not (Evd.is_defined_evar isevars n)
@@ -513,10 +521,13 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  if n1 = n2 then
 	    solve_refl conv_algo env isevars n1 args1 args2
 	  else
-	    if Array.length args1 < Array.length args2 then 
+            (try evar_define env ev1 t2 isevars
+            with e when precatchable_exception e ->
+              evar_define env ev2 (mkEvar ev1) isevars)
+(*	    if Array.length args1 < Array.length args2 then
 	      evar_define env ev2 (mkEvar ev1) isevars
 	    else 
-	      evar_define env ev1 t2 isevars
+	      evar_define env ev1 t2 isevars*)
       | _ ->
 	  evar_define env ev1 t2 isevars in
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4bcec5ef6b..b3e5a4dd9f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -67,7 +67,7 @@ val non_instantiated : evar_map -> (evar * evar_info) list
 (***********************************************************)
 (* Unification utils *)
 
-val has_undefined_evars :  evar_defs -> constr -> bool
+val is_ground_term :  evar_defs -> constr -> bool
 val is_eliminator : constr -> bool
 val head_is_embedded_evar :  evar_defs -> constr -> bool
 val solve_simple_eqn :
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4cf17fb77e..7fd437e87d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -34,7 +34,7 @@ type evar_info = {
 
 module Evarmap = Intmap
 
-type evar_map = evar_info Evarmap.t
+type evar_map1 = evar_info Evarmap.t
 
 let empty = Evarmap.empty
 
@@ -126,6 +126,149 @@ let existential_opt_value sigma ev =
   with NotInstantiatedEvar -> None
 
 (*******************************************************************)
+(*                Constraints for sort variables                   *)
+(*******************************************************************)
+
+type sort_var = Univ.universe
+
+type sort_constraint =
+  | DefinedSort of sorts (* instantiated sort var *)
+  | SortVar of sort_var list * sort_var list (* (leq,geq) *)
+  | EqSort of sort_var
+
+module UniverseOrdered = struct
+  type t = Univ.universe
+  let compare = Pervasives.compare
+end
+module UniverseMap = Map.Make(UniverseOrdered)
+
+type sort_constraints = sort_constraint UniverseMap.t
+
+let rec canonical_find u scstr =
+  match UniverseMap.find u scstr with
+      EqSort u' -> canonical_find u' scstr
+    | c -> (u,c)
+
+let whd_sort_var scstr t =
+  match kind_of_term t with
+      Sort(Type u) ->
+        (try
+          match canonical_find u scstr with
+              _, DefinedSort s -> mkSort s
+            | _ -> t
+        with Not_found -> t)
+    | _ -> t
+
+let rec set_impredicative u s scstr =
+  match UniverseMap.find u scstr with
+    | DefinedSort s' ->
+        if family_of_sort s = family_of_sort s' then scstr
+        else failwith "sort constraint inconsistency"
+    | EqSort u' ->
+        UniverseMap.add u (DefinedSort s) (set_impredicative u' s scstr)
+    | SortVar(_,ul) ->
+        (* also set sorts lower than u as impredicative *)
+        UniverseMap.add u (DefinedSort s)
+          (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
+    | DefinedSort s' ->
+        if family_of_sort s = family_of_sort s' then scstr
+        else failwith "sort constraint inconsistency"
+    | EqSort u' ->
+        UniverseMap.add u (DefinedSort s) (set_predicative u' s scstr)
+    | SortVar(ul,_) ->
+        UniverseMap.add u (DefinedSort s)
+          (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
+
+let is_sort_var s scstr =
+  match s with
+      Type u ->
+        (try
+          match canonical_find u scstr with
+              _, DefinedSort _ -> false
+            | _ -> true
+        with Not_found -> false)
+    | _ -> false
+
+let new_sort_var cstr =
+  let u = Termops.new_univ() in
+  (u, UniverseMap.add u (SortVar([],[])) cstr)
+
+
+let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
+  let rec search_rec (is_b, betw, not_betw) u1 =
+    if List.mem u1 betw then (true, betw, not_betw)
+    else if List.mem u1 not_betw then (is_b, betw, not_betw)
+    else if u1 = u2 then (true, u1::betw,not_betw) else
+      match UniverseMap.find u1 scstr with
+          EqSort u1' -> search_rec (is_b,betw,not_betw) u1'
+        | SortVar(leq,_) ->
+            let (is_b',betw',not_betw') = 
+              List.fold_left search_rec (false,betw,not_betw) leq in
+            if is_b' then (true, u1::betw', not_betw')
+            else (false, betw', not_betw')
+        | DefinedSort _ -> (false,betw,u1::not_betw) in
+  let (is_betw,betw,_) = search_rec (false, [], []) u1 in
+  if is_betw then
+    UniverseMap.add u1 (SortVar(leq1@leq2,geq1@geq2))
+      (List.fold_left
+        (fun g u -> UniverseMap.add u (EqSort u1) g) scstr betw)
+  else
+    UniverseMap.add u1 (SortVar(u2::leq1,geq1))
+      (UniverseMap.add u2 (SortVar(leq2, u1::geq2)) scstr)
+
+let set_leq (Type u1) (Type u2) scstr =
+  let (cu1,c1) = canonical_find u1 scstr in
+  let (cu2,c2) = canonical_find u2 scstr in
+  if cu1=cu2 then scstr
+  else
+    match c1,c2 with
+        (EqSort _, _ | _, EqSort _) -> assert false
+      | SortVar(leq1,geq1), SortVar(leq2,geq2) ->
+          set_leq_sort (cu1,(leq1,geq1)) (cu2,(leq2,geq2)) scstr
+      | _, DefinedSort(Prop _ as s) -> set_impredicative u1 s scstr
+      | _, DefinedSort(Type _) -> scstr
+      | DefinedSort(Type _ as s), _ -> set_predicative u2 s scstr
+      | DefinedSort(Prop _), _ -> scstr
+
+let set_sort_variable (Type u) s scstr =
+  match s with
+      Prop _ -> set_impredicative u s scstr
+    | Type _ -> set_predicative u s scstr
+
+let pr_sort_cstrs g =
+  let l = UniverseMap.fold (fun u c l -> (u,c)::l) g [] in
+  str "SORT CONSTRAINTS:" ++ fnl() ++
+  prlist_with_sep fnl (fun (u,c) ->
+    match c with
+        EqSort u' -> Univ.pr_uni u ++ str" == " ++ Univ.pr_uni u'
+      | DefinedSort s -> Univ.pr_uni u ++ str " := " ++ print_sort s
+      | SortVar(leq,geq) ->
+          str"[" ++ hov 0 (prlist_with_sep spc Univ.pr_uni geq) ++
+          str"] <= "++ Univ.pr_uni u ++ brk(0,0) ++ str"<= [" ++
+          hov 0 (prlist_with_sep spc Univ.pr_uni leq) ++ str"]")
+    l
+
+type evar_map = evar_map1 * sort_constraints
+let empty = empty, UniverseMap.empty
+let add (sigma,sm) k v = (add sigma k v, sm)
+let dom (sigma,_) = dom sigma
+let map (sigma,_) = map sigma
+let rmv (sigma,sm) k = (rmv sigma k, sm)
+let remap (sigma,sm) k v = (remap sigma k v, sm)
+let in_dom (sigma,_) = in_dom sigma
+let to_list (sigma,_) = to_list sigma
+let fold f (sigma,_) = fold f sigma
+let define (sigma,sm) k v = (define sigma k v, sm)
+let is_evar (sigma,_) = is_evar sigma
+let is_defined (sigma,_) = is_defined sigma
+let existential_value (sigma,_) = existential_value sigma
+let existential_type (sigma,_) = existential_type sigma
+let existential_opt_value (sigma,_) = existential_opt_value sigma
+
+(*******************************************************************)
 type open_constr = evar_map * constr
 
 (*******************************************************************)
@@ -235,11 +378,8 @@ let evar_source ev d =
 
 (* define the existential of section path sp as the constr body *)
 let evar_define sp body isevars =
-  (* needed only if an inferred type *)
-  let body = refresh_universes body in
   {isevars with evars = define isevars.evars sp body}
 
-
 let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
   { evd with
     evars = add evd.evars evn
@@ -270,6 +410,22 @@ let get_conv_pbs isevars p =
   {isevars with conv_pbs = pbs1},
   pbs
 
+
+(**********************************************************)
+(* Sort variables *)
+
+let new_sort_variable (sigma,sm) =
+  let (u,scstr) = new_sort_var sm in
+  (Type u,(sigma,scstr))
+let is_sort_variable (_,sm) s =
+  is_sort_var s sm
+let whd_sort_variable (_,sm) t = whd_sort_var sm t
+let set_leq_sort_variable (sigma,sm) u1 u2 =
+  (sigma, set_leq u1 u2 sm)
+let define_sort_variable (sigma,sm) u s =
+  (sigma, set_sort_variable u s sm)
+let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
+
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index d321e332a1..9dd0c33fb4 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -153,9 +153,19 @@ val meta_assign    : metavariable -> constr -> evar_defs -> evar_defs
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
 
+(**********************************************************)
+(* Sort variables *)
+
+val new_sort_variable : evar_map -> sorts * evar_map
+val is_sort_variable : evar_map -> sorts -> bool
+val whd_sort_variable : evar_map -> constr -> constr
+val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
+val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
+
 (*********************************************************************)
 (* debug pretty-printer: *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
 val pr_evar_map  : evar_map -> Pp.std_ppcmds
 val pr_evar_defs : evar_defs -> Pp.std_ppcmds
+val pr_sort_constraints : evar_map -> Pp.std_ppcmds
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6101396a40..d7a5da4cc3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -532,10 +532,10 @@ let rec pretype tycon env isevars lvar = function
 		   Cases.pred_case_ml 
 		     env (evars_of !isevars) false indt (0,fj.uj_type) 
 		 in 
-		 if has_undefined_evars !isevars pred then
-		   use_constraint ()
-		 else
+		 if is_ground_term !isevars pred then
 		   true, pred
+		 else
+		   use_constraint ()
 	       with Cases.NotInferable _ ->
 		 use_constraint ()
 	     in 
@@ -754,7 +754,7 @@ let rec pretype tycon env isevars lvar = function
 		  let pred = 
 		    Cases.pred_case_ml (* eta-expanse *)
                       env (evars_of !isevars) isrec indt (i,fj.uj_type) in
-		  if has_undefined_evars !isevars pred then findtype (i+1)
+		  if not (is_ground_term !isevars pred) then findtype (i+1)
 		  else 
 		    let pty =
                       Retyping.get_type_of env (evars_of !isevars) pred in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a7573f5343..7476dc0a7d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -426,12 +426,14 @@ let whd_betadeltaiota_nolet env sigma x =
 (* Replacing defined evars for error messages *)
 let rec whd_evar sigma c =
   match kind_of_term c with
-    | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
+    | Evar (ev,args)
+        when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
 	whd_evar sigma (Evd.existential_value sigma (ev,args))
+    | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> collapse_appl c
 
-let nf_evar sigma =
-  local_strong (whd_evar sigma)
+let nf_evar evd =
+  local_strong (whd_evar evd)
 
 (* lazy reduction functions. The infos must be created for each term *)
 let clos_norm_flags flgs env sigma t =