Imported Upstream version 8.5~beta3+dfsg

1 files changed, 225 insertions, 106 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bf519fb7..4a9466f4 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -277,15 +277,14 @@ end
 type evar_universe_context = 
  { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
    uctx_local : Univ.universe_context_set; (** The local context of variables *)
-    uctx_univ_variables : Universes.universe_opt_subst;
-      (** The local universes that are unification variables *)
-    uctx_univ_algebraic : Univ.universe_set; 
-    (** The subset of unification variables that
-	can be instantiated with algebraic universes as they appear in types 
-	and universe instances only. *)
-    uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-    uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
-  }
+   uctx_univ_variables : Universes.universe_opt_subst;
+   (** The local universes that are unification variables *)
+   uctx_univ_algebraic : Univ.universe_set; 
+   (** The subset of unification variables that can be instantiated with
+	algebraic universes as they appear in inferred types only. *)
+   uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+ }
   
 let empty_evar_universe_context = 
   { uctx_names = UNameMap.empty, Univ.LMap.empty;
@@ -310,6 +309,12 @@ let union_evar_universe_context ctx ctx' =
   else
     let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
     let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
+    let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
+			       (Univ.ContextSet.levels ctx.uctx_local) in
+    let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+    let declarenew g =
+      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+    in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
 	uctx_local = local;
@@ -317,12 +322,12 @@ let union_evar_universe_context ctx ctx' =
 	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
 	uctx_univ_algebraic = 
 	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
-	uctx_initial_universes = ctx.uctx_initial_universes;
+	uctx_initial_universes = declarenew ctx.uctx_initial_universes;
 	uctx_universes = 
 	  if local == ctx.uctx_local then ctx.uctx_universes
 	  else
 	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr ctx.uctx_universes }
+	      Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
 (* let union_evar_universe_context =  *)
@@ -330,17 +335,38 @@ let union_evar_universe_context ctx ctx' =
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let evar_universe_context_set ctx = ctx.uctx_local
+let evar_universe_context_set diff ctx =
+  let initctx = ctx.uctx_local in
+  let cstrs =
+    Univ.LSet.fold
+      (fun l cstrs ->
+       try
+	 match Univ.LMap.find l ctx.uctx_univ_variables with
+	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+	 | None -> cstrs
+       with Not_found | Option.IsNone -> cstrs)
+      (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
+  in
+    Univ.ContextSet.add_constraints cstrs initctx 
+		      
 let evar_universe_context_constraints ctx = snd ctx.uctx_local
 let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
+    
 let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
 
+let add_uctx_names s l (names, names_rev) =
+  (UNameMap.add s l names, Univ.LMap.add l s names_rev)
+
+let evar_universe_context_of_binders b =
+  let ctx = empty_evar_universe_context in
+  let names =
+    List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
+		   ctx.uctx_names b
+  in { ctx with uctx_names = names }
+					
 let instantiate_variable l b v =
-  (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *)
-  (* if Univ.univ_depends (Univ.Universe.make l) b then  *)
-  (*   error ("Occur-check in universe variable instantiation") *)
-  (* else *) v := Univ.LMap.add l (Some b) !v
+  v := Univ.LMap.add l (Some b) !v
 
 exception UniversesDiffer
 
@@ -374,7 +400,7 @@ let process_universe_constraints univs vars alg cstrs =
 		  let levels = Univ.Universe.levels l in
 		    Univ.LSet.fold (fun l local ->
 		      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
-			Univ.enforce_eq (Univ.Universe.make l) r local
+			unify_universes fo (Univ.Universe.make l) Universes.UEq r local
 		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
 		      levels local
 		else
@@ -406,7 +432,16 @@ let process_universe_constraints univs vars alg cstrs =
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
-           | _, _ (* One of the two is algebraic or global *) -> 
+	    | Inr (l, loc, alg), Inl r
+	    | Inl r, Inr (l, loc, alg) ->
+	       let inst = Univ.univ_level_rem l r r in
+		 if alg then (instantiate_variable l inst vars; local)
+		 else
+		   let lu = Univ.Universe.make l in
+		   if Univ.univ_level_mem l r then
+		     Univ.enforce_leq inst lu local
+		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
@@ -433,7 +468,7 @@ let add_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes }
+      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
 
 (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -553,7 +588,7 @@ type evar_map = {
   (** Metas *)
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
-  effects    : Declareops.side_effects;
+  effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
                                   eventually turned into goals if not solved.*)
   principal_future_goal : Evar.t option; (** if [Some e], [e] must be
@@ -564,6 +599,7 @@ type evar_map = {
                                              name) of the evar which
                                              will be instantiated with
                                              a term containing [e]. *)
+  extras : Store.t;
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -723,7 +759,7 @@ let cmap f evd =
   { evd with
       metas = Metamap.map (map_clb f) evd.metas;
       defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
-      undf_evars = EvMap.map (map_evar_info f) evd.defn_evars
+      undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
   }
 
 (* spiwack: deprecated *)
@@ -741,16 +777,17 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
-  effects    = Declareops.no_seff;
+  effects    = Safe_typing.empty_private_constants;
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
+  extras = Store.empty;
 }
 
-let from_env ?ctx e = 
-  match ctx with
-  | None -> { empty with universes = evar_universe_context_from e }
-  | Some ctx -> { empty with universes = ctx }
+let from_env e = 
+  { empty with universes = evar_universe_context_from e }
+
+let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
@@ -914,38 +951,6 @@ let evars_of_filtered_evar_info evi =
 	(evars_of_named_context (evar_filtered_context evi)))
 
 (**********************************************************)
-(* Side effects *)
-
-let emit_side_effects eff evd =
-  { evd with effects = Declareops.union_side_effects eff evd.effects; }
-
-let drop_side_effects evd =
-  { evd with effects = Declareops.no_seff; }
-
-let eval_side_effects evd = evd.effects
-
-(* Future goals *)
-let declare_future_goal evk evd =
-  { evd with future_goals = evk::evd.future_goals }
-
-let declare_principal_goal evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk; }
-  | Some _ -> Errors.error "Only one main subgoal per instantiation."
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal=None }
-
-let restore_future_goals evd gls pgl =
-  { evd with future_goals = gls ; principal_future_goal = pgl }
-
-(**********************************************************)
 (* Sort variables *)
 
 type rigid = 
@@ -960,19 +965,56 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = d.universes.uctx_local
 
-let universe_context evd =
-  Univ.ContextSet.to_context evd.universes.uctx_local
+let pr_uctx_level uctx = 
+  let map, map_rev = uctx.uctx_names in 
+    fun l ->
+      try str(Univ.LMap.find l map_rev)
+      with Not_found -> 
+	Universes.pr_with_global_universes l
 
+let universe_context ?names evd =
+  match names with
+  | None -> [], Univ.ContextSet.to_context evd.universes.uctx_local
+  | Some pl ->
+     let levels = Univ.ContextSet.levels evd.universes.uctx_local in
+     let newinst, map, left =
+       List.fold_right
+         (fun (loc,id) (newinst, map, acc) ->
+	  let l =
+	    try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
+	    with Not_found ->
+	      user_err_loc (loc, "universe_context",
+			    str"Universe " ++ pr_id id ++ str" is not bound anymore.")
+	  in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
+	 pl ([], [], levels)
+     in
+       if not (Univ.LSet.is_empty left) then
+         let n = Univ.LSet.cardinal left in
+           errorlabstrm "universe_context"
+			(str(CString.plural n "Universe") ++ spc () ++
+			     Univ.LSet.pr (pr_uctx_level evd.universes) left ++
+			     spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
+       else
+	 let inst = Univ.Instance.of_array (Array.of_list newinst) in
+	 let ctx = Univ.UContext.make (inst,
+           Univ.ContextSet.constraints evd.universes.uctx_local)
+	 in map, ctx
+
+let restrict_universe_context evd vars =
+  let uctx = evd.universes in
+  let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
+    { evd with universes = { uctx with uctx_local = uctx' } }
+						 
 let universe_subst evd =
   evd.universes.uctx_univ_variables
 
-let merge_uctx rigid uctx ctx' =
+let merge_uctx sideff rigid uctx ctx' =
   let open Univ in
-  let uctx = 
+  let levels = ContextSet.levels ctx' in
+  let uctx = if sideff then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
-      let levels = ContextSet.levels ctx' in
       let fold u accu =
         if LMap.mem u accu then accu
         else LMap.add u None accu
@@ -983,12 +1025,23 @@ let merge_uctx rigid uctx ctx' =
 	  uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
 	else { uctx with uctx_univ_variables = uvars' }
   in
-  let uctx_local = ContextSet.append ctx' uctx.uctx_local in
-  let uctx_universes = merge_constraints (ContextSet.constraints ctx') uctx.uctx_universes in
-  { uctx with uctx_local; uctx_universes }
+  let uctx_local =
+    if sideff then uctx.uctx_local
+    else ContextSet.append ctx' uctx.uctx_local
+  in
+  let declare g =
+    LSet.fold (fun u g ->
+	       try Univ.add_universe u false g
+	       with Univ.AlreadyDeclared when sideff -> g)
+	      levels g
+  in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare uctx.uctx_universes in
+  let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
+    { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
 
-let merge_context_set rigid evd ctx' = 
-  {evd with universes = merge_uctx rigid evd.universes ctx'}
+let merge_context_set ?(sideff=false) rigid evd ctx' = 
+  {evd with universes = merge_uctx sideff rigid evd.universes ctx'}
 
 let merge_uctx_subst uctx s =
   { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
@@ -999,41 +1052,61 @@ let merge_universe_subst evd subst =
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let add_uctx_names s l (names, names_rev) =
-    (UNameMap.add s l names, Univ.LMap.add l s names_rev)
-
-let uctx_new_univ_variable rigid name
+let emit_universe_side_effects eff u =
+  let uctxs = Safe_typing.universes_of_private eff in
+  List.fold_left (merge_uctx true univ_rigid) u uctxs
+        
+let uctx_new_univ_variable rigid name predicative
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.add_universe u ctx in
-  let uctx' = 
+  let uctx', pred =
     match rigid with
-    | UnivRigid -> uctx
+    | UnivRigid -> uctx, true
     | UnivFlexible b -> 
       let uvars' = Univ.LMap.add u None uvars in
 	if b then {uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.add u avars}
-	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
+	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
+	else {uctx with uctx_univ_variables = uvars'}, false
+  in
   let names = 
     match name with
     | Some n -> add_uctx_names n u uctx.uctx_names
     | None -> uctx.uctx_names
   in
+  let initial =
+    Univ.add_universe u false uctx.uctx_initial_universes
+  in						     
+  let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-      uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
-
-let new_univ_level_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+		uctx_universes = Univ.add_universe u false uctx.uctx_universes;
+		uctx_initial_universes = initial}
+  in uctx', u
+						     
+let new_univ_level_variable ?name ?(predicative=true) rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+let new_univ_variable ?name ?(predicative=true) rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?name rigid d =
-  let (d', u) = new_univ_variable rigid ?name d in
+let new_sort_variable ?name ?(predicative=true) rigid d =
+  let (d', u) = new_univ_variable rigid ?name ~predicative d in
     (d', Type u)
 
+let add_global_univ d u =
+  let uctx = d.universes in
+  let initial =
+    Univ.add_universe u true uctx.uctx_initial_universes
+  in
+  let univs = 
+    Univ.add_universe u true uctx.uctx_universes
+  in
+    { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
+				     uctx_initial_universes = initial;
+				     uctx_universes = univs } }
+      
 let make_flexible_variable evd b u =
   let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in
   let uvars' = Univ.LMap.add u None uvars in
@@ -1050,6 +1123,16 @@ let make_flexible_variable evd b u =
     {evd with universes = {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}}
 
+let make_evar_universe_context e l = 
+  let uctx = evar_universe_context_from e in
+    match l with
+    | None -> uctx
+    | Some us ->
+       List.fold_left
+	 (fun uctx (loc,id) ->
+	  fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx))
+	 uctx us
+    
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
@@ -1213,12 +1296,16 @@ let refresh_undefined_univ_variables uctx =
 	Univ.LMap.add (Univ.subst_univs_level_level subst u) 
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
-  in 
+  in
+  let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
+				   (Univ.ContextSet.levels ctx') g in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare Univ.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
 	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-	       uctx_universes = Univ.initial_universes;
-	       uctx_initial_universes = uctx.uctx_initial_universes } in
+	       uctx_universes = univs;
+	       uctx_initial_universes = initial } in
     uctx', subst
 
 let refresh_undefined_universes evd =
@@ -1232,8 +1319,7 @@ let normalize_evar_universe_context uctx =
       Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
         uctx.uctx_univ_algebraic
     in
-      if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
-        uctx
+      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
       else
 	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	let uctx' = 
@@ -1271,9 +1357,18 @@ let add_universe_name evd s l =
 
 let universes evd = evd.universes.uctx_universes
 
+let update_sigma_env evd env =
+  let univs = Environ.universes env in
+  let eunivs =
+    { evd.universes with uctx_initial_universes = univs;
+			 uctx_universes = univs }
+  in
+  let eunivs = merge_uctx true univ_rigid eunivs eunivs.uctx_local in
+  { evd with universes = eunivs }
+
 (* Conversion w.r.t. an evar map and its local universes. *)
 
-let conversion_gen env evd pb t u =
+let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
     Reduction.trans_conv_universes 
@@ -1283,14 +1378,8 @@ let conversion_gen env evd pb t u =
      full_transparent_state ~evars:(existential_opt_value evd) env 
     evd.universes.uctx_universes t u
 
-(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
-(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
-
-let conversion env d pb t u =
-  conversion_gen env d pb t u; d
-
 let test_conversion env d pb t u =
-  try conversion_gen env d pb t u; true
+  try test_conversion_gen env d pb t u; true
   with _ -> false
 
 let eq_constr_univs evd t u =
@@ -1304,8 +1393,38 @@ let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
     evdref := evd; b
 
-let eq_constr_univs_test evd t u =
-  snd (eq_constr_univs evd t u)
+(**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+  { evd with effects = Safe_typing.concat_private eff evd.effects;
+	     universes = emit_universe_side_effects eff evd.universes }
+
+let drop_side_effects evd =
+  { evd with effects = Safe_typing.empty_private_constants; }
+
+let eval_side_effects evd = evd.effects
+
+(* Future goals *)
+let declare_future_goal evk evd =
+  { evd with future_goals = evk::evd.future_goals }
+
+let declare_principal_goal evk evd =
+  match evd.principal_future_goal with
+  | None -> { evd with
+    future_goals = evk::evd.future_goals;
+    principal_future_goal=Some evk; }
+  | Some _ -> Errors.error "Only one main subgoal per instantiation."
+
+let future_goals evd = evd.future_goals
+
+let principal_future_goal evd = evd.principal_future_goal
+
+let reset_future_goals evd =
+  { evd with future_goals = [] ; principal_future_goal=None }
+
+let restore_future_goals evd gls pgl =
+  { evd with future_goals = gls ; principal_future_goal = pgl }
 
 (**********************************************************)
 (* Accessing metas *)
@@ -1323,6 +1442,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
+  extras = evd.extras;
 }
 
 let meta_list evd = metamap_to_list evd.metas
@@ -1471,6 +1591,12 @@ let dependent_evar_ident ev evd =
   | (_,Evar_kinds.VarInstance id) -> id
   | _ -> anomaly (str "Not an evar resulting of a dependent binding")
 
+(**********************************************************)
+(* Extra data *)
+
+let get_extra_data evd = evd.extras
+let set_extra_data extras evd = { evd with extras }
+
 (*******************************************************************)
 
 type pending = (* before: *) evar_map * (* after: *) evar_map
@@ -1677,13 +1803,6 @@ let evar_dependency_closure n sigma =
 let has_no_evar sigma =
   EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
-let pr_uctx_level uctx = 
-  let map, map_rev = uctx.uctx_names in 
-    fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
-	Universes.pr_with_global_universes l
-
 let pr_evd_level evd = pr_uctx_level evd.universes
 
 let pr_evar_universe_context ctx =