From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Tue, 2 May 2017 19:53:05 +0200
Subject: Correct coqchk reduction

---
 checker/cic.mli      |  4 ++-
 checker/closure.ml   |  6 ++++
 checker/closure.mli  |  3 ++
 checker/indtypes.ml  | 46 ++++++++++++++++++++++++++
 checker/inductive.ml |  2 +-
 checker/reduction.ml | 91 +++++++++++++++++++++++++++++++++++++++++++---------
 checker/subtyping.ml |  4 +--
 checker/term.ml      | 36 +++++++++++++++++++++
 checker/term.mli     |  3 ++
 checker/univ.ml      | 65 ++++++++++++++++++++++++++++++++++++-
 checker/univ.mli     | 32 +++++++++++++++++-
 checker/values.ml    |  5 +--
 12 files changed, 273 insertions(+), 24 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index 3645587554..f9d082ab1c 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -323,7 +323,9 @@ type mutual_inductive_body = {
 
     mind_polymorphic : bool; (** Is it polymorphic or not *)
 
-    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
+    mind_cumulative : bool; (** Is it cumulative or not *)
+
+    mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index b8294e7958..ac8388f6ed 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -328,6 +328,12 @@ let zshift n s =
     | (_,Zshift(k)::s) -> Zshift(n+k)::s
     | _ -> Zshift(n)::s
 
+let rec stack_args_size = function
+  | Zapp v :: s -> Array.length v + stack_args_size s
+  | Zshift(_)::s -> stack_args_size s
+  | Zupdate(_)::s -> stack_args_size s
+  | _ -> 0
+
 (* Lifting. Preserves sharing (useful only for cell with norm=Red).
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
diff --git a/checker/closure.mli b/checker/closure.mli
index 8b1f246c28..8da9ad4ea5 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -125,6 +125,9 @@ type stack_member =
 and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
+
+val stack_args_size : stack -> int
+    
 val eta_expand_stack : stack -> stack
  
 val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 6c38f38e29..00ff447cc9 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -524,6 +524,50 @@ let check_positivity env_ar mind params nrecp inds =
   let wfp = Rtree.mk_rec irecargs in
   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 numchecked = ref 0 in
+  let basic_check ev tp =
+    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+    numchecked := !numchecked + 1
+  in
+  let check_typ typ typ_env =
+    match typ with
+    | LocalAssum (_, typ') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with NotConvertible -> 
+          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+      end
+    | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = dest_prod env arcn in
+  let last_env = fold_rel_context_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
+(* 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 mib paramsctxt env_ar inds =
+    let numparams = rel_context_nhyps paramsctxt in
+    let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
+    let dosubst = subst_univs_level_constr sbsubst in
+    let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
+    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+    let env' = Environ.push_context uctx env_ar in
+    let env'' = Environ.push_context uctx_other env' in
+    let envsb = push_context (Univ.UInfoInd.subtyp_context mib.mind_universes) 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 envsb dosubst full_arity numparams true;
+           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
+        | TemplateArity _ -> ()
+    ) inds
+
 (************************************************************************)
 (************************************************************************)
 
@@ -547,6 +591,8 @@ let check_inductive env kn mib =
   let env_ar = typecheck_arity env params mib.mind_packets in
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+  (* check the inferred subtyping relation *)
+  (* check_subtyping mib params env_ar mib.mind_packets; *)
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index f890adba9a..30c5f878a1 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -56,7 +56,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 let inductive_instance mib =
   if mib.mind_polymorphic then
-    UContext.instance mib.mind_universes
+    UContext.instance (UInfoInd.univ_context mib.mind_universes)
   else Instance.empty
 
 (************************************************************************)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ba0b017844..70c0bdad02 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -117,6 +117,10 @@ let beta_appvect c v =
 (*                         Conversion                               *)
 (********************************************************************)
 
+type conv_pb =
+  | CONV
+  | CUMUL
+
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> unit
 
@@ -152,11 +156,53 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-(* Convertibility of sorts *)
+let convert_inductive_instances cv_pb uinfind u u' univs =
+  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
+  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV ->
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
+
+let convert_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+  let num_param_arity =
+    mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+  in
+  if not (num_param_arity = sv1 && num_param_arity = sv2) then
+    convert_universes univs u1 u2
+  else
+    let uinfind = mind.mind_universes in
+    convert_inductive_instances cv_pb uinfind u1 u2 univs
+
+let convert_constructors
+    (mind, ind, cns) u1 sv1 u2 sv2 univs =
+  let num_cnstr_args =
+    let nparamsctxt =
+      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+    in
+    nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+  in
+  if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+    convert_universes univs u1 u2
+  else
+    let uinfind = mind.mind_universes in
+    convert_inductive_instances CONV uinfind u1 u2 univs
 
-type conv_pb =
-  | CONV
-  | CUMUL
+(* Convertibility of sorts *)
 
 let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
@@ -375,18 +421,31 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if mind_equiv_infos infos ind1 ind2
-	then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-        else raise NotConvertible
-
-     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	 if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
-	 then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-         else raise NotConvertible
+      if mind_equiv_infos infos ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+        let () =
+          if mind.mind_polymorphic && mind.mind_cumulative then
+              convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+                u2 (stack_args_size v2) univ
+          else
+            convert_universes univ u1 u2
+        in
+        convert_stacks univ infos lft1 lft2 v1 v2
+      else raise NotConvertible
+
+    | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+      if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+        let () =
+          if mind.mind_polymorphic && mind.mind_cumulative then
+            convert_constructors
+              (mind, snd ind1, j1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          else
+            convert_universes univ u1 u2
+        in
+        convert_stacks univ infos lft1 lft2 v1 v2
+      else raise NotConvertible
 
      (* Eta expansion of records *)
      | (FConstruct ((ind1,j1),u1), _) ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 2d04b77e46..8c10bd6eca 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -97,8 +97,8 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let u = 
     check bool_equal (fun x -> x.mind_polymorphic);
     if mib1.mind_polymorphic then (
-      check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
-      Univ.UContext.instance mib1.mind_universes)
+      check Univ.Instance.equal (fun x -> Univ.UContext.instance (Univ.UInfoInd.univ_context x.mind_universes));
+      Univ.UContext.instance (Univ.UInfoInd.univ_context mib1.mind_universes))
     else Univ.Instance.empty
   in
   let eq_projection_body p1 p2 =
diff --git a/checker/term.ml b/checker/term.ml
index 75c566aeb7..f604ac4bd3 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -227,6 +227,8 @@ let rel_context_nhyps hyps =
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
+let fold_rel_context_outside f l ~init = List.fold_right f l init
+
 let map_rel_decl f = function
   | LocalAssum (n, typ) as decl ->
      let typ' = f typ in
@@ -447,3 +449,37 @@ 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 6b026d056f..ccf5b59e0c 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -33,6 +33,8 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val fold_rel_context_outside :
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
 val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
@@ -55,3 +57,4 @@ 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 5717432315..fa884d9d06 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1056,7 +1056,9 @@ module Instance : sig
     val subst_fn : universe_level_subst_fn -> t -> t
     val subst : universe_level_subst -> t -> t
     val pr : t -> Pp.std_ppcmds
-    val check_eq : t check_function 
+    val check_eq : t check_function
+    val length : t -> int
+    val append : t -> t -> t
 end = 
 struct
   type t = Level.t array
@@ -1099,6 +1101,7 @@ struct
 	(* [h] must be positive. *)
 	let h = !accu land 0x3FFFFFFF in
 	  h
+
   end
 
   module HInstance = Hashcons.Make(HInstancestruct)
@@ -1135,6 +1138,10 @@ struct
 	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
 	 in aux 0)
 
+  let length = Array.length
+
+  let append = Array.append
+  
 end
 
 type universe_instance = Instance.t
@@ -1156,6 +1163,44 @@ end
 
 type universe_context = UContext.t
 
+module UInfoInd =
+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_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 universe_info_ind = UInfoInd.t
+
 module ContextSet =
 struct
   type t = LSet.t constrained
@@ -1166,6 +1211,8 @@ struct
 end
 type universe_context_set = ContextSet.t
 
+
+
 (** Substitutions. *)
 
 let is_empty_subst = LMap.is_empty
@@ -1185,6 +1232,22 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
+let subst_univs_level_instance subst i =
+  let i' = Instance.subst_fn (subst_univs_level_level subst) i in
+    if i == i' then i
+    else i'
+
+let subst_univs_level_constraint subst (u,d,v) =
+  let u' = subst_univs_level_level subst u 
+  and v' = subst_univs_level_level subst v in
+    if d != Lt && Level.equal u' v' then None
+    else Some (u',d,v')
+
+let subst_univs_level_constraints subst csts =
+  Constraint.fold 
+    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
+    csts Constraint.empty 
+
 (** Substitute instance inst for ctx in csts *)
 
 let subst_instance_level s l =
diff --git a/checker/univ.mli b/checker/univ.mli
index 7d4c629ab9..edf828daeb 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -71,6 +71,8 @@ type 'a check_function = universes -> 'a -> 'a -> bool
 val check_leq : universe check_function
 val check_eq : universe check_function
 
+
+
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
 
@@ -170,6 +172,12 @@ sig
 
   val check_eq : t check_function
   (** Check equality of instances w.r.t. a universe graph *)
+
+  val length : t -> int
+  (** Compute the length of the instance  *)
+
+  val append : t -> t -> t
+  (** Append two universe instances *)
 end
 
 type universe_instance = Instance.t
@@ -190,6 +198,27 @@ sig
 
 end
 
+type universe_context = UContext.t
+
+module UInfoInd :
+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_susbst : t -> universe_level_subst
+
+end
+
+type universe_info_ind = UInfoInd.t
+
 module ContextSet :
   sig 
     type t
@@ -198,7 +227,6 @@ module ContextSet :
     val constraints : t -> constraints
   end
 
-type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
 val merge_context : bool -> universe_context -> universes -> universes
@@ -210,6 +238,8 @@ val is_empty_level_subst : universe_level_subst -> bool
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
+val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
+val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 
 (** Level to universe substitutions. *)
 
diff --git a/checker/values.ml b/checker/values.ml
index c175aed680..c58f56a9bd 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
+MD5 6153d4f8fb414a8f14797636ab10f55e  checker/cic.mli
 
 *)
 
@@ -272,7 +272,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     v_rctxt;
     v_bool;
-    v_context;
+    v_bool;
+    v_tuple "universes" [|v_context; v_context|];
     Opt v_bool;
     v_typing_flags|]
 
-- 
cgit v1.2.3


From 763f5d5d5c6f8b798cc138d0c68fffcb7c544e41 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 3 May 2017 11:21:47 +0200
Subject: Correct coqchk checking subtyping relation for inductives

---
 checker/indtypes.ml |  6 +++---
 checker/univ.ml     | 19 +------------------
 checker/univ.mli    |  4 +---
 3 files changed, 5 insertions(+), 24 deletions(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 00ff447cc9..69dd6f57a8 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -551,10 +551,10 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 let check_subtyping mib paramsctxt env_ar inds =
     let numparams = rel_context_nhyps paramsctxt in
     let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
-    let dosubst = subst_univs_level_constr sbsubst in
+    let dosubst = subst_instance_constr sbsubst in
     let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
-    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in
     let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
     let env' = Environ.push_context uctx env_ar in
     let env'' = Environ.push_context uctx_other env' in
diff --git a/checker/univ.ml b/checker/univ.ml
index fa884d9d06..525f535e92 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1194,8 +1194,7 @@ struct
                              create_trivial_subtyping inst freshunivs))
 
   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'
+      let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
 
 end
 
@@ -1232,22 +1231,6 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
-let subst_univs_level_instance subst i =
-  let i' = Instance.subst_fn (subst_univs_level_level subst) i in
-    if i == i' then i
-    else i'
-
-let subst_univs_level_constraint subst (u,d,v) =
-  let u' = subst_univs_level_level subst u 
-  and v' = subst_univs_level_level subst v in
-    if d != Lt && Level.equal u' v' then None
-    else Some (u',d,v')
-
-let subst_univs_level_constraints subst csts =
-  Constraint.fold 
-    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
-    csts Constraint.empty 
-
 (** Substitute instance inst for ctx in csts *)
 
 let subst_instance_level s l =
diff --git a/checker/univ.mli b/checker/univ.mli
index edf828daeb..2bc2653e09 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -213,7 +213,7 @@ sig
 
   val from_universe_context : universe_context -> universe_instance -> t
 
-  val subtyping_susbst : t -> universe_level_subst
+  val subtyping_susbst : t -> universe_instance
 
 end
 
@@ -238,8 +238,6 @@ val is_empty_level_subst : universe_level_subst -> bool
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
-val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
-val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 
 (** Level to universe substitutions. *)
 
-- 
cgit v1.2.3


From c01d225f9e112bb08f9df26f70805bde0c0d127a Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 13:45:08 +0200
Subject: Enable the checking of ind subtyping in checker

---
 checker/indtypes.ml | 36 ++++++++++++++++++------------------
 checker/univ.ml     | 33 +++++++++++++++++++++++++++++++--
 checker/univ.mli    | 14 ++++++++++++--
 3 files changed, 61 insertions(+), 22 deletions(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 69dd6f57a8..cac7e63134 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -549,25 +549,24 @@ 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 mib paramsctxt env_ar inds =
-    let numparams = rel_context_nhyps paramsctxt in
-    let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
-    let dosubst = subst_instance_constr sbsubst in
-    let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
-    let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in
-    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env' = Environ.push_context uctx env_ar in
-    let env'' = Environ.push_context uctx_other env' in
-    let envsb = push_context (Univ.UInfoInd.subtyp_context mib.mind_universes) env'' in
-    (* process individual inductive types: *)
-    Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
+  let numparams = rel_context_nhyps paramsctxt in
+  let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
+  let other_instnace = Univ.UInfoInd.subtyping_other_instance mib.mind_universes in
+  let dosubst = subst_univs_level_constr sbsubst in
+  let uctx = Univ.UInfoInd.univ_context mib.mind_universes 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.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) 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 envsb dosubst full_arity numparams true;
-           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
-        | TemplateArity _ -> ()
+      | 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
+      | TemplateArity _ -> ()
     ) inds
-
+    
 (************************************************************************)
 (************************************************************************)
 
@@ -592,7 +591,8 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check the inferred subtyping relation *)
-  (* check_subtyping mib params env_ar mib.mind_packets; *)
+  if mib.mind_cumulative then
+    check_subtyping mib params env_ar mib.mind_packets;
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
diff --git a/checker/univ.ml b/checker/univ.ml
index 525f535e92..92b6a9e867 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -968,7 +968,23 @@ struct
       else Level.compare v v'
 end
 
-module Constraint = Set.Make(UConstraintOrd)
+let pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
+
+  let pr prl c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
+end
 
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
@@ -1159,6 +1175,11 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 end
 
 type universe_context = UContext.t
@@ -1193,8 +1214,12 @@ struct
     (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') = (halve_context (UContext.instance subtypcst)) in ctx'
+    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
 
@@ -1308,6 +1333,10 @@ let merge_context_set strict ctx g =
 
 (** Pretty-printing *)
 
+let pr_constraints prl = Constraint.pr prl
+    
+let pr_universe_context = UContext.pr
+
 let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
diff --git a/checker/univ.mli b/checker/univ.mli
index 2bc2653e09..018f8aee2e 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,9 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+  
   val equal : t -> t -> bool
 end
 
@@ -195,7 +198,8 @@ sig
   val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
-
+  val is_empty : t -> bool
+    
 end
 
 type universe_context = UContext.t
@@ -213,7 +217,9 @@ sig
 
   val from_universe_context : universe_context -> universe_instance -> t
 
-  val subtyping_susbst : t -> universe_instance
+  val subtyping_other_instance : t -> universe_instance
+  
+  val subtyping_susbst : t -> universe_level_subst
 
 end
 
@@ -263,4 +269,8 @@ val make_abstract_instance : universe_context -> universe_instance
 									    
 (** {6 Pretty-printing of universes. } *)
 
+val pr_constraint_type : constraint_type -> Pp.std_ppcmds
+val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
+val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
+
 val pr_universes : universes -> Pp.std_ppcmds
-- 
cgit v1.2.3


From 960b6d7e17d7a44ad2e058a5b24a2628293408bc Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 13:56:51 +0200
Subject: Properly instantiate contexts before pushing

---
 checker/indtypes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index cac7e63134..2716489a4f 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -555,8 +555,8 @@ let check_subtyping mib paramsctxt env_ar inds =
   let dosubst = subst_univs_level_constr sbsubst in
   let uctx = Univ.UInfoInd.univ_context mib.mind_universes 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.instantiate_univ_context uctx) env_ar in
+  let env = Environ.push_context (Univ.instantiate_univ_context uctx_other) env in
   let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env in
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
-- 
cgit v1.2.3


From 81a22cd3bee8fa6144d4eb46128ee8bb287ecb36 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 14:40:36 +0200
Subject: Checker add test for non-trivial constraints

---
 checker/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 2716489a4f..cc3493aa25 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -573,7 +573,7 @@ let check_subtyping mib paramsctxt env_ar inds =
 let check_inductive env kn mib =
   Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
-  let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in
+  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 checker/cic.mli          | 16 ++++++-----
 checker/declarations.ml  |  5 ++++
 checker/declarations.mli |  1 +
 checker/environ.ml       | 27 ++++++++++-------
 checker/environ.mli      |  2 +-
 checker/indtypes.ml      | 36 ++++++++++++++++-------
 checker/inductive.ml     | 33 +++++++++++++++++----
 checker/inductive.mli    |  8 +++++-
 checker/mod_checking.ml  | 20 +++++++------
 checker/modops.ml        |  8 +++---
 checker/reduction.ml     | 75 +++++++++++++++++++++++++-----------------------
 checker/subtyping.ml     | 27 ++++++++++-------
 checker/typeops.ml       |  1 -
 checker/univ.ml          | 20 +++++++++----
 checker/univ.mli         | 33 +++++++++++++++++----
 checker/values.ml        | 17 +++++++----
 16 files changed, 217 insertions(+), 112 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index f9d082ab1c..bbddb678bc 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -209,7 +209,9 @@ type constant_def =
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
-type constant_universes = Univ.universe_context
+type constant_universes =
+  | Monomorphic_const of Univ.universe_context
+  | Polymorphic_const of Univ.abstract_universe_context
 
 (** The [typing_flags] are instructions to the type-checker which
     modify its behaviour. The typing flags used in the type-checking
@@ -226,7 +228,6 @@ type constant_body = {
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-    const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
@@ -303,6 +304,11 @@ type one_inductive_body = {
     mind_reloc_tbl : reloc_table;
   }
 
+type abstrac_inductive_universes =
+  | Monomorphic_ind of Univ.universe_context
+  | Polymorphic_ind of Univ.abstract_universe_context
+  | Cumulative_ind of Univ.abstract_cumulativity_info
+
 type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
@@ -321,11 +327,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_polymorphic : bool; (** Is it polymorphic or not *)
-
-    mind_cumulative : bool; (** Is it cumulative or not *)
-
-    mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
+    mind_universes : abstrac_inductive_universes; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index ad93146d55..2eefe47816 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -521,6 +521,11 @@ let subst_template_cst_arity sub (ctx,s as arity) =
 
 let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s
 
+let constant_is_polymorphic cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> false
+  | Polymorphic_const _ -> true
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 (* NB: we leave bytecode and native code fields untouched *)
 let subst_const_body sub cb =
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 456df83699..6fc71bb942 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -14,6 +14,7 @@ val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
 val opaque_univ_context : constant_body -> Univ.ContextSet.t
+val constant_is_polymorphic : constant_body -> bool
 
 (* Mutual inductives *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 22d1eec178..11b8ea67cc 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -115,13 +115,15 @@ let add_constant kn cs env =
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result = NoBody | Opaque | IsProj
 
 (* Constant types *)
 
 let constraints_of cb u =
-  let univs = cb.const_universes in
-    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -132,23 +134,28 @@ let map_regular_arity f = function
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then
-      let csts = constraints_of cb u in
-	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
-    else cb.const_type, Univ.Constraint.empty
+  match cb.const_universes with
+  | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    let csts = constraints_of cb u in
+    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
 
 exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (kn,u) =
   let cb = lookup_constant kn env in
+  if cb.const_proj = None then
     match cb.const_body with
     | Def l_body -> 
       let b = force_constr l_body in
-	if cb.const_polymorphic then
-	  subst_instance_constr u (force_constr l_body)
-	else b
+      begin
+        match cb.const_universes with
+        | Monomorphic_const _ -> b
+        | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+      end
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
+  else raise (NotEvaluableConst IsProj)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index 87f143d1bb..754c295d27 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -47,7 +47,7 @@ val check_constraints : Univ.constraints -> env -> bool
 val lookup_constant : constant -> env -> Cic.constant_body
 val add_constant : constant -> Cic.constant_body -> env -> env
 val constant_type : env -> constant puniverses -> constant_type Univ.constrained
-type const_evaluation_result = NoBody | Opaque
+type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index cc3493aa25..54dec56b54 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -548,16 +548,20 @@ 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 mib paramsctxt env_ar inds =
+let check_subtyping cumi paramsctxt env_ar inds =
   let numparams = rel_context_nhyps paramsctxt in
-  let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
-  let other_instnace = Univ.UInfoInd.subtyping_other_instance mib.mind_universes 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.UInfoInd.univ_context mib.mind_universes 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 (Univ.instantiate_univ_context uctx) env_ar in
-  let env = Environ.push_context (Univ.instantiate_univ_context uctx_other) env in
-  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env 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
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
@@ -573,7 +577,14 @@ let check_subtyping mib paramsctxt env_ar inds =
 let check_inductive env kn mib =
   Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
-  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)) env in
+  let ind_ctx =
+    match mib.mind_universes with
+    | Monomorphic_ind ctx -> ctx
+    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Cumulative_ind cumi -> 
+      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  in
+  let env = Environ.push_context ind_ctx env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
@@ -591,8 +602,13 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check the inferred subtyping relation *)
-  if mib.mind_cumulative then
-    check_subtyping mib params env_ar mib.mind_packets;
+  let () = 
+    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
+  in
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 30c5f878a1..e1860a23f0 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -54,10 +54,31 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 (** Polymorphic inductives *)
 
-let inductive_instance mib =
-  if mib.mind_polymorphic then
-    UContext.instance (UInfoInd.univ_context mib.mind_universes)
-  else Instance.empty
+let inductive_is_polymorphic mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> true
+  | Cumulative_ind cumi -> true
+
+let inductive_is_cumulative mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> false
+  | Cumulative_ind cumi -> true
+
+let inductive_polymorphic_instance mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Instance.empty
+  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
+  | Cumulative_ind cumi -> 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
+
+let inductive_polymorphic_context mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.UContext.empty
+  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
+  | Cumulative_ind cumi -> 
+    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
 
 (************************************************************************)
 
@@ -93,7 +114,7 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (subst_instance_context u sign,dummy) in
+  let t = mkArity (Term.subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
@@ -199,7 +220,7 @@ let instantiate_universes env ctx ar argsorts =
 let type_of_inductive_gen env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a ->
-    if not mib.mind_polymorphic then a.mind_user_arity
+    if not (inductive_is_polymorphic mib) then a.mind_user_arity
     else subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
diff --git a/checker/inductive.mli b/checker/inductive.mli
index ed3a7b53ce..9a5541f39b 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -22,7 +22,13 @@ type mind_specif = mutual_inductive_body * one_inductive_body
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-val inductive_instance : mutual_inductive_body -> Univ.universe_instance
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+
+val inductive_is_cumulative : mutual_inductive_body -> bool
+
+val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance
+
+val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7f93e15609..15e9ae2951 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,4 +1,3 @@
-
 open Pp
 open Util
 open Names
@@ -26,21 +25,23 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
-  let env' =
-    if cb.const_polymorphic then
-      let inst = Univ.make_abstract_instance cb.const_universes in
-      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
-        push_context ~strict:false ctx env
-    else push_context ~strict:true cb.const_universes env
+  Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  let env', u =
+    match cb.const_universes with
+    | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+    | Polymorphic_const auctx ->
+      let ctx = Univ.instantiate_univ_context auctx in
+      push_context ~strict:false ctx env, Univ.UContext.instance ctx
   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 
@@ -48,6 +49,7 @@ 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
@@ -57,7 +59,7 @@ let check_constant_declaration env kn cb =
 	  conv_leq envty j ty)
     | None -> ()
   in
-  if cb.const_polymorphic then add_constant kn cb env
+  if constant_is_polymorphic cb then add_constant kn cb env
   else add_constant kn cb env'
 
 (** {6 Checking modules } *)
diff --git a/checker/modops.ml b/checker/modops.ml
index bed31143bf..be35c7e981 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -83,10 +83,10 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      let u = 
-	if cb.const_polymorphic then
-	  Univ.make_abstract_instance cb.const_universes
-	else Univ.Instance.empty
+      let u =
+        match cb.const_universes with
+      | Monomorphic_const _ -> Univ.Instance.empty
+      | Polymorphic_const auctx -> Univ.make_abstract_instance auctx
       in
       { cb with
 	const_body = Def (Declarations.from_val (Const (con,u))) }
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 70c0bdad02..5010920bcb 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -156,22 +156,27 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-let convert_inductive_instances cv_pb uinfind u u' univs =
-  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+let convert_inductive_instances cv_pb cumi u u' univs =
+  let ind_instance =
+      Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+    anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.subst_instance_constraints comp_subst ind_sbcst
+      Univ.UContext.constraints
+      (Univ.subst_instance_context comp_subst ind_subtypctx)
     in
     let comp_cst =
       match cv_pb with
         CONV ->
-        let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        let comp_cst' =
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints
+            (Univ.subst_instance_context comp_subst ind_subtypctx)
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
@@ -179,28 +184,32 @@ let convert_inductive_instances cv_pb uinfind u u' univs =
 
 let convert_inductives
     cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  let num_param_arity =
-    mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-  in
-  if not (num_param_arity = sv1 && num_param_arity = sv2) then
-    convert_universes univs u1 u2
-  else
-    let uinfind = mind.mind_universes in
-    convert_inductive_instances cv_pb uinfind u1 u2 univs
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_param_arity =
+      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances cv_pb cumi u1 u2 univs
 
 let convert_constructors
     (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  let num_cnstr_args =
-    let nparamsctxt =
-      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+      in
+      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
     in
-    nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
-  in
-  if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-    convert_universes univs u1 u2
-  else
-    let uinfind = mind.mind_universes in
-    convert_inductive_instances CONV uinfind u1 u2 univs
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances CONV cumi u1 u2 univs
 
 (* Convertibility of sorts *)
 
@@ -424,11 +433,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
       if mind_equiv_infos infos ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
         let () =
-          if mind.mind_polymorphic && mind.mind_cumulative then
-              convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
-                u2 (stack_args_size v2) univ
-          else
-            convert_universes univ u1 u2
+          convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+            u2 (stack_args_size v2) univ
         in
         convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
@@ -437,12 +443,9 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
       if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
         let () =
-          if mind.mind_polymorphic && mind.mind_cumulative then
-            convert_constructors
-              (mind, snd ind1, j1) u1 (stack_args_size v1)
-              u2 (stack_args_size v2) univ
-          else
-            convert_universes univ u1 u2
+          convert_constructors
+            (mind, snd ind1, j1) u1 (stack_args_size v1)
+            u2 (stack_args_size v2) univ
         in
         convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 8c10bd6eca..bfe19584a7 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -88,18 +88,25 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let check_conv f = check_conv_error error f in
   let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> mib
+      | IndType ((_,0), mib) -> subst_mind subst1 mib
       | _ -> error ()
   in
   let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let bool_equal (x : bool) (y : bool) = x = y in
-  let u = 
-    check bool_equal (fun x -> x.mind_polymorphic);
-    if mib1.mind_polymorphic then (
-      check Univ.Instance.equal (fun x -> Univ.UContext.instance (Univ.UInfoInd.univ_context x.mind_universes));
-      Univ.UContext.instance (Univ.UInfoInd.univ_context mib1.mind_universes))
-    else Univ.Instance.empty
+  let u =
+    let process inst inst' =
+      if Univ.Instance.equal inst inst' then inst else error ()
+    in
+    match mib1.mind_universes, mib2.mind_universes with
+    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
+      process
+        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+    | Cumulative_ind cumi, Cumulative_ind cumi' ->
+      process
+        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+    | _ -> error ()
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -308,7 +315,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		      "inductive type and give a definition to map the old name to the new " ^
 		      "name.")));
       if constant_has_body cb2 then error () ;
-      let u = inductive_instance mind1 in
+      let u = inductive_polymorphic_instance mind1 in
       let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
@@ -319,7 +326,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name.")));
       if constant_has_body cb2 then error () ;
-      let u1 = inductive_instance mind1 in
+      let u1 = inductive_polymorphic_instance mind1 in
       let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv env ty1 ty2
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 0163db3347..543f9acced 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -329,7 +329,6 @@ let rec execute env cstr =
         let pj = execute env p in
         let lfj = execute_array env lf in
         judge_of_case env ci (p,pj) (c,cj) lfj
-
     | Fix ((_,i as vni),recdef) ->
         let fix_ty = execute_recdef env recdef i in
         let fix = (vni,recdef) in
diff --git a/checker/univ.ml b/checker/univ.ml
index 92b6a9e867..0ee4686c1a 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1184,7 +1184,11 @@ end
 
 type universe_context = UContext.t
 
-module UInfoInd =
+module AUContext = UContext
+
+type abstract_universe_context = AUContext.t
+
+module CumulativityInfo =
 struct
   type t = universe_context * universe_context
 
@@ -1223,7 +1227,10 @@ struct
 
 end
 
-type universe_info_ind = UInfoInd.t
+type cumulativity_info = CumulativityInfo.t
+
+module ACumulativityInfo = CumulativityInfo
+type abstract_cumulativity_info = ACumulativityInfo.t
 
 module ContextSet =
 struct
@@ -1281,7 +1288,10 @@ let subst_instance_constraint s (u,d,v as c) =
 let subst_instance_constraints s csts =
   Constraint.fold 
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
+    csts Constraint.empty
+
+let subst_instance_context inst (inner_inst, inner_constr) =
+  (inner_inst, subst_instance_constraints inst inner_constr)
 
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
@@ -1290,8 +1300,8 @@ let make_abstract_instance (ctx, _) =
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
 
-let instantiate_univ_constraints u (_, csts) = 
-  subst_instance_constraints u 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 018f8aee2e..a503924708 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -204,7 +204,17 @@ end
 
 type universe_context = UContext.t
 
-module UInfoInd :
+module AUContext :
+sig
+  type t
+
+  val instance : t -> Instance.t
+
+end
+
+type abstract_universe_context = AUContext.t
+
+module CumulativityInfo :
 sig
   type t
 
@@ -223,7 +233,18 @@ sig
 
 end
 
-type universe_info_ind = UInfoInd.t
+type cumulativity_info = CumulativityInfo.t
+
+module ACumulativityInfo :
+sig
+  type t
+
+  val univ_context : t -> abstract_universe_context
+  val subtyp_context : t -> abstract_universe_context
+
+end
+
+type abstract_cumulativity_info = ACumulativityInfo.t
 
 module ContextSet :
   sig 
@@ -255,17 +276,17 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_constraints : universe_instance -> constraints -> constraints
+val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 (* 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 : universe_context -> universe_context
-val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
+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 : universe_context -> universe_instance
+val make_abstract_instance : abstract_universe_context -> universe_instance
 									    
 (** {6 Pretty-printing of universes. } *)
 
diff --git a/checker/values.ml b/checker/values.ml
index c58f56a9bd..422729ed55 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6153d4f8fb414a8f14797636ab10f55e  checker/cic.mli
+MD5 6950230ca9e99e9cc3a70488d8ab824c  checker/cic.mli
 
 *)
 
@@ -109,6 +109,8 @@ let v_cstrs =
 
 let v_instance = Annot ("instance", Array v_level)
 let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
+let v_abs_context = v_context (* only for clarity *)
+let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; v_context|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
@@ -215,13 +217,14 @@ let v_projbody =
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool|]
 
+let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|]
+
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
     v_cst_type;
     Any;
-    v_bool;
-    v_context;
+    v_const_univs;
     Opt v_projbody;
     v_bool;
     v_typing_flags|]
@@ -262,6 +265,10 @@ let v_finite = v_enum "recursivity_kind" 3
 let v_mind_record = Annot ("mind_record", 
 			   Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
 
+let v_ind_pack_univs = 
+  v_sum "abstract_inductive_universes" 0
+    [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
     v_mind_record;
@@ -271,9 +278,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_bool;
-    v_bool;
-    v_tuple "universes" [|v_context; v_context|];
+    v_ind_pack_univs; (* universes *)
     Opt v_bool;
     v_typing_flags|]
 
-- 
cgit v1.2.3


From 49e4acab949da9861adcd37b8511a89c221ae129 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 17:05:52 +0200
Subject: Use a smart map_constr

---
 checker/term.ml | 44 ++++++++++++--------------------------------
 1 file changed, 12 insertions(+), 32 deletions(-)

(limited to 'checker')

diff --git a/checker/term.ml b/checker/term.ml
index f604ac4bd3..c0f8e0106c 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -413,38 +413,18 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c
 
 let subst_instance_constr subst c =
-  if Univ.Instance.is_empty subst then c
-  else
-    let f u = Univ.subst_instance_instance subst u 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_instance_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
+  let f u = Univ.subst_instance_instance subst u in
+  let rec aux t =
+    match t with
+    | Const (c, u) -> Const (c, f u)
+    | Ind (i, u) -> Ind (i, f u)
+    | Construct (c, u) -> Construct (c, f u)
+    | Sort (Type u) ->
+      let u' = Univ.subst_instance_universe subst u in
+      Sort (sort_of_univ u')
+    | _ -> map_constr aux t
+  in
+  aux c
 
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
-- 
cgit v1.2.3


From ab0c49baa8d57ed92a79e7d0b0737267042210f8 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 17:46:16 +0200
Subject: Optimization

Only try using cumulativity in conversion/subtyping if the universe
instances are non-empty
---
 checker/reduction.ml | 38 +++++++++++++++++++++++++-------------
 1 file changed, 25 insertions(+), 13 deletions(-)

(limited to 'checker')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 5010920bcb..95dc93f5d2 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -431,23 +431,35 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
       if mind_equiv_infos infos ind1 ind2 then
-        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
-        let () =
-          convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
-            u2 (stack_args_size v2) univ
-        in
-        convert_stacks univ infos lft1 lft2 v1 v2
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          in
+          convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
       if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
-        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
-        let () =
-          convert_constructors
-            (mind, snd ind1, j1) u1 (stack_args_size v1)
-            u2 (stack_args_size v2) univ
-        in
-        convert_stacks univ infos lft1 lft2 v1 v2
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            convert_constructors
+              (mind, snd ind1, j1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          in
+          convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
 
      (* Eta expansion of records *)
-- 
cgit v1.2.3


From 5fb30d6c06d47a8e6c4200cdd0ba9067be7cfe2f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Mon, 12 Jun 2017 17:44:29 +0200
Subject: use map_constr more efficiently

---
 checker/term.ml | 42 ++++++++++++++++++++++++++++++------------
 1 file changed, 30 insertions(+), 12 deletions(-)

(limited to 'checker')

diff --git a/checker/term.ml b/checker/term.ml
index c0f8e0106c..dea3d3e659 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -413,18 +413,36 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c
 
 let subst_instance_constr subst c =
-  let f u = Univ.subst_instance_instance subst u in
-  let rec aux t =
-    match t with
-    | Const (c, u) -> Const (c, f u)
-    | Ind (i, u) -> Ind (i, f u)
-    | Construct (c, u) -> Construct (c, f u)
-    | Sort (Type u) ->
-      let u' = Univ.subst_instance_universe subst u in
-      Sort (sort_of_univ u')
-    | _ -> map_constr aux t
-  in
-  aux c
+  if Univ.Instance.is_empty subst then c
+  else
+    let f u = Univ.subst_instance_instance subst u 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 (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 (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 (Construct (c, u'))
+      | Sort (Type u) ->
+         let u' = Univ.subst_instance_universe subst u in
+          if u' == u then t else
+            (Sort (sort_of_univ u'))
+      | _ -> map_constr aux t
+    in
+    aux c
 
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
-- 
cgit v1.2.3


From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 14 Jun 2017 16:32:47 +0200
Subject: A short cleanup

---
 checker/cic.mli   | 4 ++--
 checker/values.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index bbddb678bc..e298c41cf1 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -304,7 +304,7 @@ type one_inductive_body = {
     mind_reloc_tbl : reloc_table;
   }
 
-type abstrac_inductive_universes =
+type abstract_inductive_universes =
   | Monomorphic_ind of Univ.universe_context
   | Polymorphic_ind of Univ.abstract_universe_context
   | Cumulative_ind of Univ.abstract_cumulativity_info
@@ -327,7 +327,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_universes : abstrac_inductive_universes; (** Local universe variables and constraints together with subtyping constraints *)
+    mind_universes : abstract_inductive_universes; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/checker/values.ml b/checker/values.ml
index 422729ed55..b8b395aaf7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6950230ca9e99e9cc3a70488d8ab824c  checker/cic.mli
+MD5 b132075590daf5e202de0d9cc34e6003  checker/cic.mli
 
 *)
 
-- 
cgit v1.2.3