Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.

9 files changed, 151 insertions, 88 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index c1d7b0d73..2f33c60f5 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -170,7 +170,7 @@ type engagement = ImpredicativeSet
 
 
 type template_arity = {
-  template_param_levels : Univ.universe option list;
+  template_param_levels : Univ.universe_level option list;
   template_level : Univ.universe;
 }
 
@@ -212,8 +212,6 @@ type constant_body = {
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-    const_constraints : Univ.constraints;
-    const_native_name : native_name ref;
     const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
diff --git a/checker/environ.ml b/checker/environ.ml
index a04e95cfc..710ebc712 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -108,10 +108,9 @@ type const_evaluation_result = NoBody | Opaque
 
 (* Constant types *)
 
-let universes_and_subst_of cb u =
+let constraints_of cb u =
   let univs = cb.const_universes in
-  let subst = Univ.make_universe_subst u univs in
-    subst, Univ.instantiate_univ_context subst univs
+    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -123,8 +122,8 @@ let map_regular_arity f = function
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst, csts = universes_and_subst_of cb u in
-	(map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts)
+      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
 
 exception NotEvaluableConst of const_evaluation_result
@@ -135,8 +134,7 @@ let constant_value env (kn,u) =
     | Def l_body -> 
       let b = force_constr l_body in
 	if cb.const_polymorphic then
-	  let subst = Univ.make_universe_subst u cb.const_universes in
-	    subst_univs_level_constr subst b
+	  subst_instance_constr u (force_constr l_body)
 	else b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index adb9e0347..c23b2578b 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -54,29 +54,20 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 (** Polymorphic inductives *)
 
-let make_inductive_subst mib u =
-  if mib.mind_polymorphic then 
-    Univ.make_universe_subst u mib.mind_universes
-  else Univ.empty_level_subst
-
-let inductive_paramdecls (mib,u) = 
-  let subst = make_inductive_subst mib u in
-    subst_univs_level_context subst mib.mind_params_ctxt
-
 let inductive_instance mib =
-  if mib.mind_polymorphic then 
-    Univ.UContext.instance mib.mind_universes
-  else Univ.Instance.empty
+  if mib.mind_polymorphic then
+    UContext.instance mib.mind_universes
+  else Instance.empty
 
 let inductive_context mib =
   if mib.mind_polymorphic then 
-    mib.mind_universes 
-  else Univ.UContext.empty
+    instantiate_univ_context mib.mind_universes 
+  else UContext.empty
 
-let instantiate_inductive_constraints mib subst =
+let instantiate_inductive_constraints mib u =
   if mib.mind_polymorphic then
-    Univ.instantiate_univ_context subst mib.mind_universes
-  else Univ.Constraint.empty
+    subst_instance_constraints u (UContext.constraints mib.mind_universes)
+  else Constraint.empty
 
 (************************************************************************)
 
@@ -88,9 +79,9 @@ let ind_subst mind mib u =
   List.init ntypes make_Ik
 
 (* Instantiate inductives in constructor type *)
-let constructor_instantiate mind u subst mib c =
+let constructor_instantiate mind u mib c =
   let s = ind_subst mind mib u in
-  substl s (subst_univs_level_constr subst c)
+  substl s (subst_instance_constr u c)
 
 let instantiate_params full t args sign =
   let fail () =
@@ -112,13 +103,11 @@ let instantiate_params full t args sign =
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
   let t = mkArity (sign,dummy) in
-  let subst = make_inductive_subst mib u in
   let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
-    subst_univs_level_context subst ar
+    subst_instance_context u ar
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let subst = make_inductive_subst mib u in
-  let inst_ind = constructor_instantiate mind u subst mib in
+  let inst_ind = constructor_instantiate mind u mib in
   (fun t ->
     instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
 
@@ -155,8 +144,8 @@ let sort_as_univ = function
 
 let cons_subst u su subst =
   try
-    (u, Univ.sup su (List.assoc_f Univ.Universe.equal u subst)) ::
-      List.remove_assoc_f Univ.Universe.equal u subst
+    (u, Univ.sup su (List.assoc_f Univ.Level.equal u subst)) ::
+      List.remove_assoc_f Univ.Level.equal u subst
   with Not_found -> (u, su) :: subst
 
 let actualize_decl_level env lev t =
@@ -225,30 +214,11 @@ let is_prop_sort = function
   | Prop Null -> true
   | _ -> false
 
-let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
-  match mip.mind_arity with
-  | RegularArity a ->
-    if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
-    else 
-      let subst = make_inductive_subst mib u in
-	(subst_univs_level_constr subst a.mind_user_arity, subst)
-  | TemplateArity ar ->
-    let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes env ctx ar paramtyps in
-      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
-         the situation where a non-Prop singleton inductive becomes Prop
-         when applied to Prop params *)
-      if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
-      then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      mkArity (List.rev ctx,s), Univ.LMap.empty
-
 let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a ->
     if not mib.mind_polymorphic then a.mind_user_arity
-    else 
-      let subst = make_inductive_subst mib u in
-	(subst_univs_level_constr subst a.mind_user_arity)
+    else subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
@@ -263,13 +233,13 @@ let type_of_inductive env pind =
   type_of_inductive_gen env pind [||]
 
 let constrained_type_of_inductive env ((mib,mip),u as pind) =
-  let ty, subst = type_of_inductive_subst env pind [||] in
-  let cst = instantiate_inductive_constraints mib subst in
+  let ty = type_of_inductive_gen env pind [||] in
+  let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
 let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
-  let ty, subst = type_of_inductive_subst env pind args in
-  let cst = instantiate_inductive_constraints mib subst in
+  let ty = type_of_inductive_gen env pind args in
+  let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
 let type_of_inductive_knowing_parameters env mip args = 
@@ -293,36 +263,33 @@ let max_inductive_sort =
 (************************************************************************)
 (* Type of a constructor *)
 
-let type_of_constructor_subst cstr u subst (mib,mip) =
+let type_of_constructor_subst cstr u (mib,mip) =
   let ind = inductive_of_constructor cstr in
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
   if i > nconstr then error "Not enough constructors in the type.";
-  let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in
-    c
+    constructor_instantiate (fst ind) u mib specif.(i-1)
 
 let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
-  let subst = make_inductive_subst mib u in
-    type_of_constructor_subst cstr u subst mspec, subst
+  type_of_constructor_subst cstr u mspec
 
 let type_of_constructor cstru mspec = 
-  fst (type_of_constructor_gen cstru mspec)
+  type_of_constructor_gen cstru mspec
 
 let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
   let u = Univ.UContext.instance mib.mind_universes in
   let c = type_of_constructor_gen (cstr, u) mspec in
-    (fst c, mib.mind_universes)
+    (c, mib.mind_universes)
 
 let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
-  let ty, subst = type_of_constructor_gen cstru ind in
-  let cst = instantiate_inductive_constraints mib subst in
+  let ty = type_of_constructor_gen cstru ind in
+  let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
 let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
-  let subst = make_inductive_subst mib u in
-  Array.map (constructor_instantiate kn u subst mib) specif
+  Array.map (constructor_instantiate kn u mib) specif
 
 
 
diff --git a/checker/inductive.mli b/checker/inductive.mli
index d2f6788c5..50dd343ee 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -22,8 +22,6 @@ 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 make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> 
-  Univ.universe_level_subst
 val inductive_instance : mutual_inductive_body -> Univ.universe_instance
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
diff --git a/checker/term.ml b/checker/term.ml
index e8cdb03e9..3438f497a 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -24,6 +24,11 @@ let family_of_sort = function
 
 let family_equal = (==)
 
+let sort_of_univ u =
+  if Univ.is_type0m_univ u then Prop Null
+  else if Univ.is_type0_univ u then Prop Pos
+  else Type u
+
 (********************************************************************)
 (*       Constructions as implemented                               *)
 (********************************************************************)
@@ -469,3 +474,44 @@ let subst_univs_level_constr subst c =
 
 let subst_univs_level_context s = 
   map_rel_context (subst_univs_level_constr s)
+
+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 substkey = Profile.declare_profile "subst_instance_constr";; *)
+(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst 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
diff --git a/checker/term.mli b/checker/term.mli
index 5e98885fa..3c4835dbb 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -56,3 +56,7 @@ val eq_constr : constr -> constr -> bool
 val subst_univs_constr : Univ.universe_subst -> constr -> constr
 val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
 val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
+
+(** Instance substitution for polymorphism. *)
+val subst_instance_constr : Univ.universe_instance -> constr -> constr
+val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 77fc4af73..f69f10295 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -224,8 +224,7 @@ let judge_of_projection env p c ct =
     with Not_found -> error_case_not_inductive env (c, ct)
   in
     assert(eq_mind pb.proj_ind (fst ind));
-    let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = subst_univs_level_constr usubst pb.proj_type in
+    let ty = subst_instance_constr u pb.proj_type in
       substl (c :: List.rev args) ty
 
 (* Fixpoints. *)
@@ -392,8 +391,9 @@ let check_ctxt env rels =
 (* Polymorphic arities utils *)
 
 let check_kind env ar u =
-  if snd (dest_prod env ar) = Sort(Type u) then ()
-  else failwith "not the correct sort"
+  match (snd (dest_prod env ar)) with
+  | Sort (Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> ()
+  | _ -> failwith "not the correct sort"
 
 let check_polymorphic_arity env params par =
   let pl = par.template_param_levels in
diff --git a/checker/univ.ml b/checker/univ.ml
index e2e40ddc9..04897e85c 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -246,6 +246,7 @@ struct
     | Prop
     | Set
     | Level of int * DirPath.t
+    | Var of int
 
   (* Hash-consing *)
 
@@ -256,6 +257,7 @@ struct
       | Set, Set -> true
       | Level (n,d), Level (n',d') ->
         Int.equal n n' && DirPath.equal d d'
+      | Var n, Var n' -> Int.equal n n'
       | _ -> false
 
   let compare u v =
@@ -270,6 +272,9 @@ struct
       if i1 < i2 then -1
       else if i1 > i2 then 1
       else DirPath.compare dp1 dp2
+    | Level _, _ -> -1
+    | _, Level _ -> 1
+    | Var n, Var m -> Int.compare n m
 
   let hcons = function
     | Prop as x -> x
@@ -277,13 +282,15 @@ struct
     | Level (n,d) as x -> 
       let d' = Names.DirPath.hcons d in
         if d' == d then x else Level (n,d')
+    | Var n as x -> x
 
   open Hashset.Combine
 
   let hash = function
     | Prop -> combinesmall 1 0
     | Set -> combinesmall 1 1
-    | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d))
+    | Var n -> combinesmall 2 n
+    | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
 end
 
 module Level = struct
@@ -294,6 +301,7 @@ module Level = struct
   | Prop
   | Set
   | Level of int * DirPath.t
+  | Var of int
 
   (** Embed levels with their hash value *)
   type t = { 
@@ -357,6 +365,7 @@ module Level = struct
     | Prop -> "Prop"
     | Set -> "Set"
     | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Var i -> "Var("^string_of_int i^")"
 
   let pr u = str (to_string u)
 
@@ -1149,13 +1158,9 @@ let remove_large_constraint u v min =
   | None -> Huniv.remove (Universe.Expr.make u) v
 
 let subst_large_constraint u u' v =
-  match level u with
-  | Some u ->
-      (* if is_direct_constraint u v then  *)
-	Universe.sup u' (remove_large_constraint u v type0m_univ)
-      (* else v *)
-  | _ ->
-      anomaly (Pp.str "expect a universe level")
+  (* if is_direct_constraint u v then  *)
+  Universe.sup u' (remove_large_constraint u v type0m_univ)
+  (* else v *)
 
 let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
@@ -1181,7 +1186,7 @@ let level_subst_of f =
     with Not_found -> l
      
 module Instance : sig 
-    type t
+    type t = Level.t array
 
     val empty : t
     val is_empty : t -> bool
@@ -1329,9 +1334,42 @@ let subst_univs_level_constraints subst csts =
     (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
     csts Constraint.empty 
 
+(* let instantiate_univ_context subst (_, csts) =  *)
+(*   subst_univs_level_constraints subst csts *)
+
 (** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context subst (_, csts) = 
-  subst_univs_level_constraints subst csts
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
+(** Substitute instance inst for ctx in csts *)
+let instantiate_univ_context (ctx, csts) = 
+  (ctx, subst_instance_constraints ctx csts)
+
+let instantiate_univ_constraints u (_, csts) = 
+  subst_instance_constraints u csts
 
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
diff --git a/checker/univ.mli b/checker/univ.mli
index b2f2c9c18..27f4c9a6e 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,7 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val equal : t -> t -> bool
 end
 
 type universe_level = Level.t
@@ -122,7 +123,7 @@ val check_constraints : constraints -> universes -> bool
 (** {6 Support for old-style sort-polymorphism } *)
 
 val subst_large_constraints :
-  (universe * universe) list -> universe -> universe
+  (universe_level * universe) list -> universe -> universe
 
 (** {6 Support for universe polymorphism } *)
 
@@ -209,6 +210,19 @@ val make_subst : universe_subst -> universe_subst_fn
 val subst_univs_universe : universe_subst_fn -> universe -> universe
 val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 
+
+(** 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 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
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : universes -> Pp.std_ppcmds