Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker

6 files changed, 35 insertions, 130 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 92e94c1ab0..22c8438126 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -525,10 +525,10 @@ let check_positivity env_ar mind params nrecp inds =
   Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
 (* Check arities and constructors *)
-let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) numparams is_arity =
+let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity =
   let numchecked = ref 0 in
   let basic_check ev tp =
-    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+    if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp);
     numchecked := !numchecked + 1
   in
   let check_typ typ typ_env =
@@ -548,26 +548,27 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 
 (* Check that the subtyping information inferred for inductive types in the block is correct. *)
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
-let check_subtyping cumi paramsctxt env_ar inds =
+let check_subtyping cumi paramsctxt env inds =
+  let open Univ in
   let numparams = rel_context_nhyps paramsctxt in
-  let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
-  let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in
-  let dosubst = subst_univs_level_constr sbsubst in
-  let uctx = Univ.CumulativityInfo.univ_context cumi in
-  let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
-  let env = Environ.push_context uctx env_ar 
-  in
-  let env = Environ.push_context uctx_other env 
-  in
-  let env =  Environ.push_context 
-      (Univ.CumulativityInfo.subtyp_context cumi) env
-  in
+  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+      with the cumulativity constraints [ cumul_cst ]. *)
+  let len = AUContext.size (ACumulativityInfo.univ_context cumi) in
+  let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in
+  let other_context = ACumulativityInfo.univ_context cumi in
+  let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
+  let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in
+  let cumul_cst = UContext.constraints cumul_context in
+  let env = Environ.push_context uctx_other env in
+  let env = Environ.add_constraints cumul_cst env in
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
       | RegularArity { mind_user_arity = full_arity} ->
-        check_subtyping_arity_constructor env dosubst full_arity numparams true;
-        Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
+        check_subtyping_arity_constructor env inst full_arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc
       | TemplateArity _ -> ()
     ) inds
     
@@ -579,10 +580,10 @@ let check_inductive env kn mib =
   (* check mind_constraints: should be consistent with env *)
   let ind_ctx =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> ctx
-    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *)
+    | Polymorphic_ind auctx -> Univ.AUContext.repr auctx
     | Cumulative_ind cumi -> 
-      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+      Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
   in
   let env = Environ.push_context ind_ctx env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
@@ -606,8 +607,7 @@ let check_inductive env kn mib =
     match mib.mind_universes with
     | Monomorphic_ind _ | Polymorphic_ind _ -> ()
     | Cumulative_ind acumi ->
-      check_subtyping 
-        (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets
+      check_subtyping acumi params env_ar mib.mind_packets
   in
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 15e9ae2951..4948f6008f 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,22 +26,21 @@ let refresh_arity ar =
 
 let check_constant_declaration env kn cb =
   Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
-  let env', u =
+  (** [env'] contains De Bruijn universe variables *)
+  let env' =
     match cb.const_universes with
-    | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+    | Monomorphic_const ctx -> push_context ~strict:true ctx env
     | Polymorphic_const auctx ->
-      let ctx = Univ.instantiate_univ_context auctx in
-      push_context ~strict:false ctx env, Univ.UContext.instance ctx
+      let ctx = Univ.AUContext.repr auctx in
+      push_context ~strict:false ctx env
   in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
-        let ty = subst_instance_constr u ty in
         let ty', cu = refresh_arity ty in
         let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
-        assert(Univ.Instance.is_empty u);
         let _ = check_ctxt env' ctxt in
         check_polymorphic_arity env' ctxt par;
 	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
@@ -49,7 +48,6 @@ let check_constant_declaration env kn cb =
   let () = 
     match body_of_constant cb with
     | Some bd ->
-      let bd = subst_instance_constr u bd in
       (match cb.const_proj with 
       | None -> let j = infer envty bd in
 		  conv_leq envty j ty
diff --git a/checker/term.ml b/checker/term.ml
index 9bcb15bc72..5995dfcc61 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -447,37 +447,3 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
-
-let subst_univs_level_constr subst c =
-  if Univ.is_empty_level_subst subst then c
-  else 
-    let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
-    let changed = ref false in
-    let rec aux t = 
-      match t with
-      | Const (c, u) -> 
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Const (c, u'))
-      | Ind (i, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-	  let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Ind (i, u'))
-      | Construct (c, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Construct (c, u'))
-      | Sort (Type u) -> 
-         let u' = Univ.subst_univs_level_universe subst u in
-	   if u' == u then t else 
-	     (changed := true; Sort (sort_of_univ u'))
-      | _ -> map_constr aux t
-    in
-    let c' = aux c in
-      if !changed then c' else c
diff --git a/checker/term.mli b/checker/term.mli
index ccf5b59e0c..679a56ee45 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -57,4 +57,3 @@ val eq_constr : constr -> constr -> bool
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Univ.universe_instance -> constr -> constr
 val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
-val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
diff --git a/checker/univ.ml b/checker/univ.ml
index 2cd4252b20..e3abc436f0 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1075,6 +1075,7 @@ module Instance : sig
     val check_eq : t check_function
     val length : t -> int
     val append : t -> t -> t
+    val of_array : Level.t array -> t
 end = 
 struct
   type t = Level.t array
@@ -1157,7 +1158,9 @@ struct
   let length = Array.length
 
   let append = Array.append
-  
+
+  let of_array i = i
+
 end
 
 (** Substitute instance inst for ctx in csts *)
@@ -1231,43 +1234,11 @@ module CumulativityInfo =
 struct
   type t = universe_context * universe_context
 
-  let make x =
-    if (Array.length (UContext.instance (snd x))) =
-       (Array.length (UContext.instance (fst x))) * 2 then x
-    else anomaly (Pp.str "Invalid subtyping information encountered!")
-
-  let empty = (UContext.empty, UContext.empty)
-
-  let halve_context ctx =
-    let len = Array.length ctx in
-    let halflen = len / 2 in
-    ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen))
-
   let univ_context (univcst, subtypcst) = univcst
   let subtyp_context (univcst, subtypcst) = subtypcst
 
-  let create_trivial_subtyping ctx ctx' =
-    CArray.fold_left_i
-      (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
-      Constraint.empty ctx
-
-  let from_universe_context univcst freshunivs =
-    let inst = (UContext.instance univcst) in
-    assert (Array.length freshunivs = Array.length inst);
-    (univcst, UContext.make (Array.append inst freshunivs,
-                             create_trivial_subtyping inst freshunivs))
-
-  let subtyping_other_instance (univcst, subtypcst) =
-    let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
-  
-  let subtyping_susbst (univcst, subtypcst) =
-    let (ctx, ctx') = (halve_context (UContext.instance subtypcst)) in
-    Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
-
 end
 
-type cumulativity_info = CumulativityInfo.t
-
 module ACumulativityInfo = CumulativityInfo
 type abstract_cumulativity_info = ACumulativityInfo.t
 
@@ -1315,13 +1286,6 @@ let subst_univs_level_universe subst u =
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) = 
-  (ctx, subst_instance_constraints ctx csts)
-
-let instantiate_cumulativity_info (ctx, ctx') = 
-  (instantiate_univ_context ctx, instantiate_univ_context ctx')
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 01df46fa1e..7f5aa76260 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,8 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val var : int -> t
+
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)
   
@@ -179,6 +181,8 @@ sig
   val length : t -> int
   (** Compute the length of the instance  *)
 
+  val of_array : Level.t array -> t
+
   val append : t -> t -> t
   (** Append two universe instances *)
 end
@@ -208,7 +212,6 @@ module AUContext :
 sig
   type t
 
-  val instance : t -> Instance.t
   val size : t -> int
 
   val instantiate : Instance.t -> t -> Constraint.t
@@ -218,27 +221,6 @@ end
 
 type abstract_universe_context = AUContext.t
 
-module CumulativityInfo :
-sig
-  type t
-
-  val make : universe_context * universe_context -> t
-
-  val empty : t
-
-  val univ_context : t -> universe_context
-  val subtyp_context : t -> universe_context
-
-  val from_universe_context : universe_context -> universe_instance -> t
-
-  val subtyping_other_instance : t -> universe_instance
-  
-  val subtyping_susbst : t -> universe_level_subst
-
-end
-
-type cumulativity_info = CumulativityInfo.t
-
 module ACumulativityInfo :
 sig
   type t
@@ -284,10 +266,6 @@ val subst_instance_universe : universe_instance -> universe -> universe
 (* val make_instance_subst : universe_instance -> universe_level_subst *)
 (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
 
-(** Get the instantiated graph. *)
-val instantiate_univ_context : abstract_universe_context -> universe_context
-val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
-
 (** Build the relative instance corresponding to the context *)
 val make_abstract_instance : abstract_universe_context -> universe_instance