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

1 files changed, 160 insertions, 4 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4cf17fb77..7fd437e87 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 *)