Imported Upstream version 8.5~beta1+dfsg

1 files changed, 61 insertions, 58 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 047971d5..19613c4e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -1,14 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Declarations
 open Term
+open Vars
 open Environ
 open Inductive
 open Reduction
@@ -22,8 +24,9 @@ let crazy_type =  mkSet
 
 let decompose_prod env t =
   let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
-  if name = Anonymous then (Name (id_of_string "x"),dom,codom)
-  else res
+  match name with
+  | Anonymous -> (Name (Id.of_string "x"), dom, codom)
+  | Name _ -> res
 
 exception Find_at of int
 
@@ -34,7 +37,8 @@ let invert_tag cst tag reloc_tbl =
   try
     for j = 0 to Array.length reloc_tbl - 1 do
       let tagj,arity = reloc_tbl.(j) in
-      if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
+      let no_arity = Int.equal arity 0 in
+      if Int.equal tag tagj && (cst && no_arity || not (cst || no_arity)) then
 	raise (Find_at j)
       else ()
     done;raise Not_found
@@ -44,30 +48,31 @@ let invert_tag cst tag reloc_tbl =
 let find_rectype_a env c =
   let (t, l) =
     let t = whd_betadeltaiota env c in
-    try destApp t with e when Errors.noncritical e -> (t,[||]) in
+    try destApp t with DestKO -> (t,[||]) in
   match kind_of_term t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib typ params =
-  let s = ind_subst mind mib in
+let type_constructor mind mib u typ params =
+  let s = ind_subst mind mib u in
   let ctyp = substl s typ in
+  let ctyp = subst_instance_constr u ctyp in
   let nparams = Array.length params in
-  if nparams = 0 then ctyp
+  if Int.equal nparams 0 then ctyp
   else
     let _,ctyp = decompose_prod_n nparams ctyp in
-    substl (List.rev (Array.to_list params)) ctyp
+    substl (Array.rev_to_list params) ctyp
 
 
 
 let construct_of_constr const env tag typ =
-  let (mind,_ as ind), allargs = find_rectype_a env typ in
+  let ((mind,_ as ind), u) as indu, allargs = find_rectype_a env typ in
   (* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
   try
     if const then
-      ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag),
+      ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag),
        typ) (*spiwack: this may need to be changed in case there are parameters in the
 	               type which may cause a constant value to have an arity.
 	               (type_constructor seems to be all about parameters actually)
@@ -80,8 +85,8 @@ let construct_of_constr const env tag typ =
     let nparams = mib.mind_nparams in
     let i = invert_tag const tag mip.mind_reloc_tbl in
     let params = Array.sub allargs 0 nparams in
-    let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in
-      (mkApp(mkConstruct(ind,i), params), ctyp)
+    let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
+      (mkApp(mkConstructUi(indu,i), params), ctyp)
 
 let construct_of_constr_const env tag typ =
   fst (construct_of_constr true env tag typ)
@@ -91,7 +96,8 @@ let construct_of_constr_block = construct_of_constr false
 let constr_type_of_idkey env idkey =
   match idkey with
   | ConstKey cst ->
-      mkConst cst, Typeops.type_of_constant env cst
+    let const_type = Typeops.type_of_constant_in env cst in
+      mkConstU cst, const_type
   | VarKey id ->
       let (_,_,ty) = lookup_named id env in
       mkVar id, ty
@@ -100,30 +106,33 @@ let constr_type_of_idkey env idkey =
       let (_,_,ty) = lookup_rel n env in
       mkRel n, lift n ty
 
-let type_of_ind env ind =
-  type_of_inductive env (Inductive.lookup_mind_specif env ind)
+let type_of_ind env (ind, u) =
+  type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
 
-let build_branches_type env (mind,_ as _ind) mib mip params dep p =
+let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
   let rtbl = mip.mind_reloc_tbl in
   (* [build_one_branch i cty] construit le type de la ieme branche (commence
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
-    let typi = type_constructor mind mib cty params in
-    let decl,indapp = decompose_prod_assum typi in
-    let ind,cargs = find_rectype_a env indapp in
+    let typi = type_constructor mind mib u cty params in
+    let decl,indapp = Reductionops.splay_prod env Evd.empty typi in
+    let decl_with_letin,_ = decompose_prod_assum typi in
+    let ((ind,u),cargs) = find_rectype_a env indapp in
     let nparams = Array.length params in
     let carity = snd (rtbl.(i)) in
     let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
     let codom =
-      let papp = mkApp(lift (List.length decl) p,crealargs) in
+      let ndecl = List.length decl in
+      let papp = mkApp(lift ndecl p,crealargs) in
       if dep then
 	let cstr = ith_constructor_of_inductive ind (i+1) in
         let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
-	let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in
+	let params = Array.map (lift ndecl) params in
+	let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in
 	mkApp(papp,[|dep_cstr|])
       else papp
     in
-    decl, codom
+    decl, decl_with_letin, codom
   in Array.mapi build_one_branch mip.mind_nf_lc
 
 let build_case_type dep p realargs c =
@@ -141,7 +150,7 @@ and nf_whd env whd typ =
   | Vsort s -> mkSort s
   | Vprod p ->
       let dom = nf_vtype env (dom p) in
-      let name = Name (id_of_string "x") in
+      let name = Name (Id.of_string "x") in
       let vc = body_of_vfun (nb_rel env) (codom p) in
       let codom = nf_vtype (push_rel (name,None,dom) env) vc  in
       mkProd(name,dom,codom)
@@ -166,7 +175,7 @@ and nf_whd env whd typ =
   | Vatom_stk(Aiddef(idkey,v), stk) ->
       nf_whd env (whd_stack v stk) typ
   | Vatom_stk(Aind ind, stk) ->
-      nf_stk env (mkInd ind) (type_of_ind env ind) stk
+      nf_stk env (mkIndU ind) (type_of_ind env ind) stk
 
 and nf_stk env c t stk  =
   match stk with
@@ -176,28 +185,25 @@ and nf_stk env c t stk  =
       nf_stk env (mkApp(c,args)) t stk
   | Zfix (f,vargs) :: stk ->
       let fa, typ = nf_fix_app env f vargs in
-      let _,_,codom =
-        try decompose_prod env typ
-        with e when Errors.noncritical e -> exit 120
-      in
+      let _,_,codom = decompose_prod env typ in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
-      let (mind,_ as ind),allargs = find_rectype_a env t in
+      let ((mind,_ as ind), u), allargs = find_rectype_a env t in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
-      let params,realargs = Util.array_chop nparams allargs in
+      let params,realargs = Util.Array.chop nparams allargs in
       let pT =
-	hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
+	hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
       let pT = whd_betadeltaiota env pT in
-      let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
+      let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
-      let btypes = build_branches_type env ind mib mip params dep p in
+      let btypes = build_branches_type env ind mib mip u params dep p in
       (* calcul des branches *)
       let bsw = branch_of_switch (nb_rel env) sw in
       let mkbranch i (n,v) =
-	let decl,codom = btypes.(i) in
-	let b = nf_val (push_rel_context decl env) v codom in
-	it_mkLambda_or_LetIn b decl
+	let decl,decl_with_letin,codom = btypes.(i) in
+	let b = nf_val (Termops.push_rels_assum decl env) v codom in
+        Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type dep p realargs c in
@@ -209,21 +215,18 @@ and nf_predicate env ind mip params v pT =
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name,dom,codom =
-        try decompose_prod env pT
-        with e when Errors.noncritical e -> exit 121
-      in
+      let name,dom,codom = decompose_prod env pT in
       let dep,body =
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
   | Vfun f, _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name = Name (id_of_string "c") in
+      let name = Name (Id.of_string "c") in
       let n = mip.mind_nrealargs in
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
-      let params = if n=0 then params else Array.map (lift n) params in
-      let dom = mkApp(mkInd ind,Array.append params rargs) in
+      let params = if Int.equal n 0 then params else Array.map (lift n) params in
+      let dom = mkApp(mkIndU ind,Array.append params rargs) in
       let body = nf_vtype (push_rel (name,None,dom) env) vb in
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
@@ -234,10 +237,7 @@ and nf_args env vargs t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom =
-          try decompose_prod env !t
-          with e when Errors.noncritical e -> exit 123
-        in
+	let _,dom,codom = decompose_prod env !t in
 	let c = nf_val env (arg vargs i) dom in
 	t := subst1 c codom; c) in
   !t,args
@@ -248,10 +248,7 @@ and nf_bargs env b t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom =
-          try decompose_prod env !t
-          with e when Errors.noncritical e -> exit 124
-        in
+	let _,dom,codom = decompose_prod env !t in
 	let c = nf_val env (bfield b i) dom in
 	t := subst1 c codom; c) in
   args
@@ -261,8 +258,10 @@ and nf_fun env f typ =
   let vb = body_of_vfun k f in
   let name,dom,codom =
     try decompose_prod env typ
-    with e when Errors.noncritical e ->
-      raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
+    with DestKO ->
+      (* 27/2/13: Turned this into an anomaly *)
+      Errors.anomaly
+        (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
   in
   let body = nf_val (push_rel (name,None,dom) env) vb codom in
   mkLambda(name,dom,body)
@@ -274,9 +273,13 @@ and nf_fix env f =
   let vb, vt = reduce_fix k f in
   let ndef = Array.length vt in
   let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
-  let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
+  let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in
+  (* Third argument of the tuple is ignored by push_rec_types *)
   let env = push_rec_types (name,ft,ft) env in
-  let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in
+  (* We lift here because the types of arguments (in tt) will be evaluated
+     in an environment where the fixpoints have been pushed *)
+  let norm_vb v t = nf_fun env v (lift ndef t) in
+  let fb = Util.Array.map2 norm_vb vb ft in
   mkFix ((rec_args,init),(name,ft,fb))
 
 and nf_fix_app env f vargs =
@@ -292,9 +295,9 @@ and nf_cofix env cf =
   let vb,vt = reduce_cofix k cf in
   let ndef = Array.length vt in
   let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
-  let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
+  let name = Array.init ndef (fun _ -> (Name (Id.of_string "Fcofix"))) in
   let env = push_rec_types (name,cft,cft) env in
-  let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
+  let cfb = Util.Array.map2 (fun v t -> nf_val env v t) vb cft in
   mkCoFix (init,(name,cft,cfb))
 
 let cbv_vm env c t  =