Merge branch 'v8.5'

5 files changed, 91 insertions, 55 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3fa037ffdd..5e99521a12 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -413,25 +413,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
           let sub = (env, c1) :: subargs env lc in
           try_aux sub mk_ctx next
-  | Case (ci,p,c,brs) ->
-      (* Warning: this assumes predicate and branches to be
-         in canonical form using let and fun of the signature *)
-      let nardecls = List.length ci.ci_pp_info.ind_tags in
-      let sign_p,p = decompose_lam_n_decls (nardecls + 1) p in
-      let env_p = Environ.push_rel_context sign_p env in
-      let brs = Array.map2 decompose_lam_n_decls ci.ci_cstr_ndecls brs in
-      let sign_brs = Array.map fst brs in
-      let f (sign,br) = (Environ.push_rel_context sign env, br) in
-      let sub_br = Array.map f brs in
+  | Case (ci,hd,c1,lc) ->
       let next_mk_ctx = function
-      | c :: p :: brs ->
-        let p = it_mkLambda_or_LetIn p sign_p in
-        let brs =
-          Array.map2 it_mkLambda_or_LetIn (Array.of_list brs) sign_brs in
-        mk_ctx (mkCase (ci,p,c,brs))
+      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       | _ -> assert false
       in
-      let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in
+      let sub = (env, c1) :: (env, hd) :: subargs env lc in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index dafe88d8db..de988aa2cd 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -53,8 +53,8 @@ let find_rectype_a env c =
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib typ params = 
-  let s = ind_subst mind mib Univ.Instance.empty (* FIXME *)in
+let type_constructor mind mib u typ params =
+  let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let nparams = Array.length params in
   if Int.equal nparams 0 then ctyp
@@ -68,13 +68,13 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   let params = Array.sub allargs 0 nparams in
   try
     if const then
-      let ctyp = type_constructor mind mib (mip.mind_nf_lc.(0)) params in
+      let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
       retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
     else
       raise Not_found
   with Not_found ->
   let i = invert_tag const tag mip.mind_reloc_tbl in
-  let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in
+  let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
   (mkApp(mkConstructU((ind,i),u), params), ctyp)
  
 
@@ -90,12 +90,12 @@ let construct_of_constr_const env tag typ =
 
 let construct_of_constr_block = construct_of_constr false
 
-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 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,cargs = find_rectype_a env indapp in
@@ -292,7 +292,7 @@ and nf_atom_type env atom =
       let pT = whd_betadeltaiota env pT in
       let dep, p = nf_predicate env ind mip params p pT in
       (* Calcul du type des branches *)
-      let btypes = build_branches_type env (fst ind) mib mip params dep p in
+      let btypes = build_branches_type env (fst ind) mib mip u params dep p in
       (* calcul des branches *)
       let bsw = branch_of_switch (nb_rel env) ans bs in
       let mkbranch i v =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index a6aa086579..5f0e19cf2b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -66,9 +66,12 @@ val all_and_fail_flags : inference_flags
 (** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
-(** Generic call to the interpreter from glob_constr to open_constr, leaving
-    unresolved holes as evars and returning the typing contexts of
-    these evars. Work as [understand_gen] for the rest. *)
+(** Generic calls to the interpreter from glob_constr to open_constr;
+    by default, inference_flags tell to use type classes and
+    heuristics (but no external tactic solver hooks), as well as to
+    ensure that conversion problems are all solved and expand evars,
+    but unresolved evars can remain. The difference is in whether the
+    evar_map is modified explicitly or by side-effect. *)
 
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> open_constr
@@ -92,7 +95,12 @@ val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
   typing_constraint -> glob_constr -> pure_open_constr
 
-(** Standard call to get a constr from a glob_constr, resolving implicit args *)
+(** Standard call to get a constr from a glob_constr, resolving
+    implicit arguments and coercions, and compiling pattern-matching;
+    the default inference_flags tells to use type classes and
+    heuristics (but no external tactic solver hook), as well as to
+    ensure that conversion problems are all solved and that no
+    unresolved evar remains, expanding evars. *)
 
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
@@ -102,12 +110,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
 val understand_judgment : env -> evar_map -> 
   glob_constr -> unsafe_judgment Evd.in_evar_universe_context
 
-(** Idem but do not fail on unresolved evars *)
+(** Idem but do not fail on unresolved evars (type cl*)
 val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
 (** Trying to solve remaining evars and remaining conversion problems
-    with type classes, heuristics, and possibly an external solver *)
+    possibly using type classes, heuristics, external tactic solver
+    hook depending on given flags. *)
 (* For simplicity, it is assumed that current map has no other evars
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
@@ -115,7 +124,8 @@ val understand_judgment_tcc : env -> evar_map ref ->
 val solve_remaining_evars : inference_flags ->
   env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
 
-(** Checking evars are all solved and reporting an appropriate error message *)
+(** Checking evars and pending conversion problems are all solved,
+    reporting an appropriate error message *)
 
 val check_evars_are_solved :
   env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bb1bc7d2ea..0714c93b4f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1282,7 +1282,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
     
-let sigma_compare_instances flex i0 i1 sigma =
+let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
   with Evd.UniversesDiffer
      | Univ.UniverseInconsistency _ ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 46af784dda..c4c85a62ed 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -93,19 +93,6 @@ let construct_of_constr_const env tag typ =
 
 let construct_of_constr_block = construct_of_constr false
 
-let constr_type_of_idkey env idkey =
-  match idkey with
-  | ConstKey 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
-  | RelKey i ->
-      let n = (nb_rel env - i) in
-      let (_,_,ty) = lookup_rel n env in
-      mkRel n, lift n ty
-
 let type_of_ind env (ind, u) =
   type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
 
@@ -164,7 +151,8 @@ and nf_whd env whd typ =
       let t = ta.(i) in
       let _, args = nf_args env vargs t in
       mkApp(cfd,args)
-  | Vconstr_const n -> construct_of_constr_const env n typ
+  | Vconstr_const n ->
+    construct_of_constr_const env n typ
   | Vconstr_block b ->
       let tag = btag b in
       let (tag,ofs) =
@@ -177,22 +165,72 @@ and nf_whd env whd typ =
       let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
-      let c,typ = constr_type_of_idkey env idkey in
-      nf_stk env c typ stk
-  | Vatom_stk(Aind ind, stk) ->
-      nf_stk env (mkIndU ind) (type_of_ind env ind) stk
+      constr_type_of_idkey env idkey stk
+  | Vatom_stk(Aind ((mi,i) as ind), stk) ->
+     let mib = Environ.lookup_mind mi env in
+     let nb_univs =
+       if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes
+       else 0
+     in
+     let mk u =
+       let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
+     in
+     nf_univ_args ~nb_univs mk env stk
+  | Vatom_stk(Atype u, stk) -> assert false
+  | Vuniv_level lvl ->
+    assert false
+
+and nf_univ_args ~nb_univs mk env stk =
+  let u =
+    if Int.equal nb_univs 0 then Univ.Instance.empty
+    else match stk with
+    | Zapp args :: _ ->
+       let inst =
+	 Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i))
+       in
+       Univ.Instance.of_array inst
+    | _ -> assert false
+  in
+  let (t,ty) = mk u in
+  nf_stk ~from:nb_univs env t ty stk
+
+and constr_type_of_idkey env (idkey : Vars.id_key) stk =
+  match idkey with
+  | ConstKey cst ->
+     let cbody = Environ.lookup_constant cst env in
+     let nb_univs =
+       if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes
+       else 0
+     in
+     let mk u =
+       let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)
+     in
+     nf_univ_args ~nb_univs mk env stk
+   | VarKey id ->
+      let (_,_,ty) = lookup_named id env in
+      nf_stk env (mkVar id) ty stk
+  | RelKey i ->
+      let n = (nb_rel env - i) in
+      let (_,_,ty) = lookup_rel n env in
+      nf_stk env (mkRel n) (lift n ty) stk
 
-and nf_stk env c t stk  =
+and nf_stk ?from:(from=0) env c t stk  =
   match stk with
   | [] -> c
   | Zapp vargs :: stk ->
-      let t, args = nf_args env vargs t in
-      nf_stk env (mkApp(c,args)) t stk
+      if nargs vargs >= from then
+	let t, args = nf_args ~from:from env vargs t in
+	nf_stk env (mkApp(c,args)) t stk
+      else
+	let rest = from - nargs vargs in
+	nf_stk ~from:rest env c t stk
   | Zfix (f,vargs) :: stk ->
+      assert (from = 0) ;
       let fa, typ = nf_fix_app env f vargs in
       let _,_,codom = decompose_prod env typ in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
+      assert (from = 0) ;
       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
@@ -215,6 +253,7 @@ and nf_stk env c t stk  =
       let ci = case_info sw in
       nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
   | Zproj p :: stk ->
+     assert (from = 0) ;
      let p' = Projection.make p true in
      let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
      nf_stk env (mkProj(p',c)) ty stk
@@ -240,14 +279,14 @@ and nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
 
-and nf_args env vargs t =
+and nf_args env vargs ?from:(f=0) t =
   let t = ref t in
-  let len = nargs vargs in
+  let len = nargs vargs - f in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (arg vargs i) dom in
+	let c = nf_val env (arg vargs (f+i)) dom in
 	t := subst1 c codom; c) in
   !t,args