diff options
Diffstat (limited to 'pretyping')
62 files changed, 827 insertions, 485 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 1bd03491a7..ea33f1c0d6 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,7 +43,7 @@ let section_segment_of_reference = function | ConstRef con -> Lib.section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.UContext.empty + | _ -> [], Univ.LMap.empty, Univ.AUContext.empty let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index e123e77862..804e38216c 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b88532e1b9..7455587c0a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -94,7 +94,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (CAst.make @@ PatVar Anonymous) + List.make n (DAst.make @@ PatVar Anonymous) (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -177,7 +177,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [CAst.make @@ PatCstr (pci, args, Anonymous)] rh + [DAst.make @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -187,12 +187,12 @@ let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh + feed_history (DAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = - feed_history (CAst.make @@ PatVar Anonymous) h + feed_history (DAst.make @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -273,8 +273,10 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | { CAst.v = PatVar _ } :: l -> find_row_ind l - | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c) + | p :: l -> + match DAst.get p with + | PatVar _ -> find_row_ind l + | PatCstr(c,_,_) -> Some (p.CAst.loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in @@ -348,7 +350,7 @@ let find_tomatch_tycon evdref env loc = function empty_tycon,None let make_return_predicate_ltac_lvar sigma na tm c lvar = - match na, tm.CAst.v with + match na, DAst.get tm with | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> if Id.Map.mem id lvar.ltac_genargs then let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in @@ -447,7 +449,7 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns.") -let alias_of_pat = CAst.with_val (function +let alias_of_pat = DAst.with_val (function | PatVar name -> name | PatCstr(_,_,name) -> name ) @@ -493,13 +495,14 @@ let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) + (DAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable -let check_and_adjust_constructor env ind cstrs = function - | { CAst.v = PatVar _ } as pat -> pat - | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat -> +let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with + | PatVar _ -> pat + | PatCstr (((_,i) as cstr),args,alias) -> + let loc = pat.CAst.loc in (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -510,7 +513,7 @@ let check_and_adjust_constructor env ind cstrs = function else try let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) - in CAst.make ?loc @@ PatCstr (cstr, args', alias) + in DAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ?loc env cstr nb_args_constr else @@ -522,9 +525,12 @@ let check_and_adjust_constructor env ind cstrs = function let check_all_variables env sigma typ mat = List.iter - (fun eqn -> match current_pattern eqn with - | { CAst.v = PatVar id } -> () - | { CAst.v = PatCstr (cstr_sp,_,_); loc } -> + (fun eqn -> + let pat = current_pattern eqn in + match DAst.get pat with + | PatVar id -> () + | PatCstr (cstr_sp,_,_) -> + let loc = pat.CAst.loc in error_bad_pattern ?loc env sigma cstr_sp typ) mat @@ -549,9 +555,9 @@ let occur_in_rhs na rhs = | Anonymous -> false | Name id -> Id.List.mem id rhs.rhs_vars -let is_dep_patt_in eqn = function - | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs - | { CAst.v = PatCstr _ } -> true +let is_dep_patt_in eqn pat = match DAst.get pat with + | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | PatCstr _ -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -771,7 +777,7 @@ let recover_and_adjust_alias_names names sign = | x::names, LocalAssum (_,t)::sign -> (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (CAst.make @@ PatVar na, decl) :: aux (names,sign) + (DAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -987,7 +993,7 @@ let use_unit_judge evd = evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in + let pats = List.map (fun _ -> DAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in @@ -1184,9 +1190,9 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (************************************************************************) (* Sorting equations by constructor *) -let rec irrefutable env = function - | { CAst.v = PatVar name } -> true - | { CAst.v = PatCstr (cstr,args,_) } -> +let rec irrefutable env pat = match DAst.get pat with + | PatVar name -> true + | PatCstr (cstr,args,_) -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in @@ -1206,15 +1212,15 @@ let group_equations pb ind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match check_and_adjust_constructor pb.env ind cstrs pat with - | { CAst.v = PatVar name } -> + match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with + | PatVar name -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in brs.(i-1) <- (args, name, rest) :: brs.(i-1) done; if !only_default == None then only_default := Some true - | { CAst.v = PatCstr (((_,i)),args,name) ; loc } -> + | PatCstr (((_,i)),args,name) -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1745,22 +1751,22 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env sigma t Anonymous) avoid in - CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in + DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with - | Construct (cstr,u) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc + | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in - let l,acc = List.fold_map' reveal_pattern l acc in - CAst.make (PatCstr (cstr,l,Anonymous)), acc + let l,acc = List.fold_right_map reveal_pattern l acc in + DAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with | [] -> [], acc_sign, acc | (t, IsInd (_,IndType(indf,realargs),_)) :: tms -> - let patl,acc = List.fold_map' reveal_pattern realargs acc in + let patl,acc = List.fold_right_map reveal_pattern realargs acc in let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in let sign = make_arity_signature env sigma true indf' in @@ -1830,7 +1836,7 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl; + [ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl; alias_stack = []; eqn_loc = None; used = ref false; @@ -2094,14 +2100,14 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole na = CAst.make @@ +let hole na = DAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = let loc = pat.CAst.loc in - match pat.CAst.v with + match DAst.get pat with | PatVar name -> let name, avoid = match name with Name n -> name, avoid @@ -2109,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid = let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -2140,7 +2146,7 @@ let constr_of_pat env evdref arsign pat avoid = in let args = List.rev args in let patargs = List.rev patargs in - let pat' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in + let pat' = DAst.make ?loc @@ PatCstr (cstr, patargs, alias) in let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in @@ -2196,18 +2202,18 @@ let vars_of_ctx sigma ctx = match decl with | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (CAst.make @@ GApp ( - (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole na; CAst.make @@ GVar prev])) :: vars + (DAst.make @@ GApp ( + (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole na; DAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, (CAst.make @@ GVar n) :: vars) + | Name n -> n, (DAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y let rec is_included x y = - match CAst.(x.v, y.v) with + match DAst.get x, DAst.get y with | PatVar _, _ -> true | _, PatVar _ -> true | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> @@ -2325,13 +2331,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = - let bref = CAst.make @@ GVar branch_name in + let bref = DAst.make @@ GVar branch_name in match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> CAst.make @@ GApp (bref, l) + | l -> DAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ]) + Some _ -> DAst.make @@ GApp (branch, [ hole Anonymous ]) | None -> branch in incr i; @@ -2501,14 +2507,14 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar in let tycon, arity = + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in match tycon' with - | None -> let ev = mkExistential env evdref in ev, ev + | None -> let ev = mkExistential env evdref in ev, lift nar ev | Some t -> let pred = match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with | Some (evd, pred) -> evdref := evd; pred | None -> - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t in Option.get tycon, pred in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 4b1fde25a8..428f64b999 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 6c2086f3e0..19d61a64db 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index eb25994bef..3ee7bebf08 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 8d87f6e99c..1cc072a2a2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -89,7 +89,7 @@ sig type t val compare : t -> t -> int val equal : t -> t -> bool - val print : t -> std_ppcmds + val print : t -> Pp.t end type 'a t val empty : 'a t @@ -324,7 +324,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* rajouter une coercion dans le graphe *) let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds) + : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) let install_path_printer f = path_printer := f @@ -403,7 +403,7 @@ type coercion = { (* Computation of the class arity *) let reference_arity_length ref = - let t = Universes.unsafe_type_of_global ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) let projection_arity_length p = diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c4238e8b0d..8707078b58 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -95,15 +95,14 @@ val lookup_pattern_path_between : (**/**) (* Crade *) -open Pp val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit + ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) val string_of_class : cl_typ -> string -val pr_class : cl_typ -> std_ppcmds -val pr_cl_index : cl_index -> std_ppcmds +val pr_class : cl_typ -> Pp.t +val pr_cl_index : cl_index -> Pp.t val get_coercion_value : coe_index -> Constr.t val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list val classes : unit -> cl_typ list diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 1282e3cb86..fc0a650bc2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -77,8 +77,8 @@ let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> let f i = - if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in - CAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) + if i<n then (DAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in + DAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index ab1f6c110f..a8c07d2efa 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index f78f585d31..ca7f633dc5 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 4734c90a87..1d7019d09f 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c93b1e568c..1eb22cdb81 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -28,6 +28,10 @@ open Misctypes open Decl_kinds open Context.Named.Declaration +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay + (** Should we keep details of universes during detyping ? *) let print_universes = Flags.univ_print @@ -81,7 +85,7 @@ let encode_tuple r = module PrintingInductiveMake = functor (Test : sig val encode : reference -> inductive - val member_message : std_ppcmds -> bool -> std_ppcmds + val member_message : Pp.t -> bool -> Pp.t val field : string val title : string end) -> @@ -277,7 +281,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = CAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in let cna = ci.ci_cstr_nargs in List.flatten @@ -300,7 +304,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with List.map (fun (hd,rest) -> pat::hd,rest) lines) clauses) | _ -> - let pat = CAst.make @@ PatVar(update_name sigma na rhs) in + let pat = DAst.make @@ PatVar(update_name sigma na rhs) in let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat @@ -323,7 +327,7 @@ let is_nondep_branch sigma c l = let extract_nondep_branches test c b l = let rec strip l r = - match r.CAst.v, l with + match DAst.get r, l with | r', [] -> r | GLambda (_,_,_,t), false::l -> strip l t | GLetIn (_,_,_,t), true::l -> strip l t @@ -333,7 +337,7 @@ let extract_nondep_branches test c b l = let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = - match c.CAst.v, l with + match DAst.get c, l with | _, [] -> (List.rev nal,c) | GLambda (na,_,_,c), false::l -> aux l (na::nal) c | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c @@ -347,11 +351,11 @@ let it_destRLambda_or_LetIn_names l c = x in let x = next (free_glob_vars c) in - let a = CAst.make @@ GVar x in + let a = DAst.make @@ GVar x in aux l (Name x :: nal) - (match c with - | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a]) - | _ -> CAst.make @@ GApp (c,[a])) + (match DAst.get c with + | GApp (p,l) -> DAst.make ?loc:c.CAst.loc @@ GApp (p,l@[a]) + | _ -> DAst.make @@ GApp (c,[a])) in aux l [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -367,7 +371,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | None -> Anonymous, None, None | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match typ.CAst.v with + let n,typ = match DAst.get typ with | GLambda (x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = @@ -437,12 +441,20 @@ let detype_instance sigma l = if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) -let rec detype flags avoid env sigma t = CAst.make @@ +let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g = + match d with + | Now -> DAst.make (f d flags env avoid sigma t) + | Later -> DAst.delay (fun () -> f d flags env avoid sigma t) + +let rec detype d flags avoid env sigma t = + delay d detype_r flags avoid env sigma t + +and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar id - | Anonymous -> (!detype_anonymous n).CAst.v + | Anonymous -> GVar (!detype_anonymous n) with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in GVar (Id.of_string s)) @@ -455,44 +467,44 @@ let rec detype flags avoid env sigma t = CAst.make @@ with Not_found -> GVar id) | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> - (detype flags avoid env sigma c1).CAst.v + DAst.get (detype d flags avoid env sigma c1) | Cast (c1,k,c2) -> - let d1 = detype flags avoid env sigma c1 in - let d2 = detype flags avoid env sigma c2 in + let d1 = detype d flags avoid env sigma c1 in + let d2 = detype d flags avoid env sigma c2 in let cast = match k with | VMcast -> CastVM d2 | NATIVEcast -> CastNative d2 | _ -> CastConv d2 in GCast(d1,cast) - | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c - | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c - | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c + | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma na None ty c + | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma na None ty c + | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> let mkapp f' args' = - match f'.CAst.v with + match DAst.get f' with | GApp (f',args'') -> GApp (f',args''@args') | _ -> GApp (f',args') in - mkapp (detype flags avoid env sigma f) - (Array.map_to_list (detype flags avoid env sigma) args) + mkapp (detype d flags avoid env sigma f) + (Array.map_to_list (detype d flags avoid env sigma) args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = let pb = Environ.lookup_projection p (snd env) in let pars = pb.Declarations.proj_npars in - let hole = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in + let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in let args = List.make pars hole in - GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype flags avoid env sigma c])) + GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + (args @ [detype d flags avoid env sigma c])) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () with _ -> (* lax mode, used by debug printers only *) - GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), - [detype flags avoid env sigma c]) + GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + [detype d flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then (** Print the compatibility match version *) @@ -509,12 +521,12 @@ let rec detype flags avoid env sigma t = CAst.make @@ substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> anomaly (str"Cannot detype an unfolded primitive projection.") - in (detype flags avoid env sigma c').CAst.v + in DAst.get (detype d flags avoid env sigma c') else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in - (detype flags avoid env sigma c).CAst.v + DAst.get (detype d flags avoid env sigma c) with Retyping.RetypeError _ -> noparams () else noparams () @@ -542,23 +554,23 @@ let rec detype flags avoid env sigma t = CAst.make @@ (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (id, - List.map (on_snd (detype flags avoid env sigma)) l) + List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> GRef (IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> GRef (ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in - detype_case comp (detype flags avoid env sigma) - (detype_eqns flags avoid env sigma ci comp) + detype_case comp (detype d flags avoid env sigma) + (detype_eqns d flags avoid env sigma ci comp) (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) (Some p) c bl - | Fix (nvn,recdef) -> detype_fix flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix flags avoid env sigma n recdef + | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef -and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = +and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> @@ -567,14 +579,14 @@ and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = (avoid, env, []) names tys in let n = Array.length tys in let v = Array.map3 - (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t)) + (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and detype_cofix flags avoid env sigma n (names,tys,bodies) = +and detype_cofix d flags avoid env sigma n (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> @@ -583,14 +595,14 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) = (avoid, env, []) names tys in let ntys = Array.length tys in let v = Array.map2 - (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t)) + (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) bodies tys in GRec(GCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and share_names flags n l avoid env sigma c t = +and share_names d flags n l avoid env sigma c t = match EConstr.kind sigma c, EConstr.kind sigma t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> @@ -598,59 +610,59 @@ and share_names flags n l avoid env sigma c t = Name _, _ -> na | _, Name _ -> na' | _ -> na in - let t' = detype flags avoid env sigma t in + let t' = detype d flags avoid env sigma t in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) None t env in - share_names flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype flags avoid env sigma t' in - let b' = detype flags avoid env sigma b in + let t'' = detype d flags avoid env sigma t' in + let b' = detype d flags avoid env sigma b in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in - share_names flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> - share_names flags n l avoid env sigma c (subst1 b t) + share_names d flags n l avoid env sigma c (subst1 b t) (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> - let t'' = detype flags avoid env sigma t' in + let t'' = detype d flags avoid env sigma t' in let id = next_name_away na' avoid in let avoid = id::avoid and env = add_name (Name id) None t' env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype flags avoid env sigma c in - let t = detype flags avoid env sigma t in + let c = detype d flags avoid env sigma c in + let t = detype d flags avoid env sigma t in (List.rev l,c,t) -and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = +and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype flags avoid env sigma c)) + List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list - (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl) + (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl) -and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = +and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = let make_pat x avoid env b body ty ids = if force_wildcard () && noccurn sigma 1 b then - CAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids + DAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids else let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in let na,avoid' = compute_displayed_name_in sigma flag avoid x b in - CAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na + DAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with | _, [] -> Loc.tag @@ (Id.Set.elements ids, - [CAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], - detype flags avoid env sigma b) + [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], + detype d flags avoid env sigma b) | Lambda (x,t,b), false::l -> let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in buildrec new_ids (pat::patlist) new_avoid new_env l b @@ -663,7 +675,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran buildrec ids patlist avoid env l c | _, true::l -> - let pat = CAst.make @@ PatVar Anonymous in + let pat = DAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -678,23 +690,23 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = +and detype_binder d (lax,isgoal as flags) bk avoid env sigma na body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c | _ -> compute_displayed_name_in sigma flag avoid na c in - let r = detype flags avoid' (add_name na' body ty env) sigma c in + let r = detype d flags avoid' (add_name na' body ty env) sigma c in match bk with - | BProd -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r) - | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r) + | BProd -> GProd (na',Explicit,detype d (lax,false) avoid env sigma ty, r) + | BLambda -> GLambda (na',Explicit,detype d (lax,false) avoid env sigma ty, r) | BLetIn -> - let c = detype (lax,false) avoid env sigma (Option.get body) in + let c = detype d (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in + let t = if s != InProp && not !Flags.raw_print then None else Some (detype d (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) -let detype_rel_context ?(lax=false) where avoid env sigma sign = +let detype_rel_context d ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] @@ -716,15 +728,18 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign = | LocalAssum _ -> None | LocalDef (_,b,_) -> Some b in - let b' = Option.map (detype (lax,false) avoid env sigma) b in - let t' = detype (lax,false) avoid env sigma t in + let b' = Option.map (detype d (lax,false) avoid env sigma) b in + let t' = detype d (lax,false) avoid env sigma t in (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest in aux avoid env (List.rev sign) let detype_names isgoal avoid nenv env sigma t = - detype (false,isgoal) avoid (nenv,env) sigma t -let detype ?(lax=false) isgoal avoid env sigma t = - detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t + detype Now (false,isgoal) avoid (nenv,env) sigma t +let detype d ?(lax=false) isgoal avoid env sigma t = + detype d (lax,isgoal) avoid (names_of_rel_context env, env) sigma t + +let detype_rel_context d ?lax where avoid env sigma sign = + detype_rel_context d ?lax where avoid env sigma sign let detype_closed_glob ?lax isgoal avoid env sigma t = let open Context.Rel.Declaration in @@ -736,7 +751,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | Name id -> Name (convert_id cl id) | Anonymous -> Anonymous in - let rec detype_closed_glob cl cg : Glob_term.glob_constr = CAst.map (function + let rec detype_closed_glob cl cg : Glob_term.glob_constr = DAst.map (function | GVar id -> (* if [id] is bound to a name. *) begin try @@ -750,11 +765,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = [Printer.pr_constr_under_binders_env] does. *) let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in let env = push_rel_context assums env in - (detype ?lax isgoal avoid env sigma c).CAst.v + DAst.get (detype Now ?lax isgoal avoid env sigma c) (* if [id] is bound to a [closed_glob_constr]. *) with Not_found -> try let {closure;term} = Id.Map.find id cl.untyped in - (detype_closed_glob closure term).CAst.v + DAst.get (detype_closed_glob closure term) (* Otherwise [id] stands for itself *) with Not_found -> GVar id @@ -781,7 +796,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = in GCases(sty,po,tml,eqns) | c -> - (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v + DAst.get (Glob_ops.map_glob_constr (detype_closed_glob cl) cg) ) cg in detype_closed_glob t.closure t.term @@ -789,7 +804,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst = CAst.map (function +let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn @@ -800,11 +815,11 @@ let rec subst_cases_pattern subst = CAst.map (function let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst = CAst.map (function +let rec subst_glob_constr subst = DAst.map (function | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else - (detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)).CAst.v + DAst.get (detype Now false [] (Global.env()) Evd.empty (EConstr.of_constr t)) | GSort _ | GVar _ @@ -905,8 +920,8 @@ let rec subst_glob_constr subst = CAst.map (function let simple_cases_matrix_of_branches ind brs = List.map (fun (i,n,b) -> let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = CAst.make @@ PatVar na in - let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = DAst.make @@ PatVar na in + let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index da287ae9f0..67c852af32 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,6 +16,10 @@ open Mod_subst open Misctypes open Evd +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay + (** Should we keep details of universes during detyping ? *) val print_universes : bool ref @@ -33,12 +37,12 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr -val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr +val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g val detype_sort : evar_map -> sorts -> glob_sort -val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> rel_context -> glob_decl list +val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> + evar_map -> rel_context -> 'a glob_decl_g list val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr @@ -47,7 +51,7 @@ val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option (* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit +val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool @@ -66,7 +70,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig val encode : Libnames.reference -> Names.inductive - val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds + val member_message : Pp.t -> bool -> Pp.t val field : string val title : string end) -> @@ -75,9 +79,9 @@ module PrintingInductiveMake : val compare : t -> t -> int val encode : Libnames.reference -> Names.inductive val subst : substitution -> t -> t - val printer : t -> Pp.std_ppcmds + val printer : t -> Pp.t val key : Goptions.option_name val title : string - val member_message : t -> bool -> Pp.std_ppcmds + val member_message : t -> bool -> Pp.t val synchronous : bool end diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3757ba7e6d..cb76df4e8a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let u, ctx' = Universes.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in let t' = EConstr.of_constr t' in @@ -350,6 +351,23 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) +let check_leq_inductives evd cumi u u' = + let u = EConstr.EInstance.kind evd u in + let u' = EConstr.EInstance.kind evd u' in + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + begin + let comp_subst = (Univ.Instance.append u u') in + let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in + Evd.add_constraints evd comp_cst + end + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -439,16 +457,102 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let univs = EConstr.eq_constr_universes evd term term' in - match univs with - | Some univs -> - ise_and evd [(fun i -> - let cstrs = Universes.to_constraints (Evd.universes i) univs in - try Success (Evd.add_constraints i cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - | None -> - UnifFailure (evd,NotSameHead) + let check_strict () = + let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + end + | None -> + UnifFailure (evd, NotSameHead) + in + let first_try_strict_check cond u u' try_subtyping_constraints = + if cond then + let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> try_subtyping_constraints () + end + | None -> + UnifFailure (evd, NotSameHead) + else + UnifFailure (evd, NotSameHead) + in + let compare_heads evd = + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') -> + check_strict () + | Ind (ind, u), Ind (ind', u') -> + let check_subtyping_constraints () = + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + begin + let mind = Environ.lookup_mind (fst ind) env in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> + begin + let num_param_arity = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + in + if not (num_param_arity = nparamsaplied + && num_param_arity = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) + end + end + end + in + first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints + | Construct (cons, u), Construct (cons', u') -> + let check_subtyping_constraints () = + let ind, ind' = fst cons, fst cons' in + let j, j' = snd cons, snd cons' in + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let mind = Environ.lookup_mind (fst ind) env in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> + begin + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(snd ind). + Declarations.mind_consnrealargs.(j - 1) + in + if not (num_cnstr_args = nparamsaplied + && num_cnstr_args = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) + end + end + in + first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints + | _, _ -> anomaly (Pp.str "") + in + ise_and evd [(fun i -> + try compare_heads i + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] in let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = let switch f a b = if on_left then f a b else f b a in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 45857df2ae..c30d1d26bf 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 2d86daadb6..7f5a780f9c 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index b8134a28c5..5477c5c99d 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,5 +43,5 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts (** {6 debug pretty-printer:} *) -val pr_tycon : env -> evar_map -> type_constraint -> Pp.std_ppcmds +val pr_tycon : env -> evar_map -> type_constraint -> Pp.t diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ff0aeff75d..ef0fb8ea6e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -34,12 +34,6 @@ let get_polymorphic_positions sigma f = (match oib.mind_arity with | RegularArity _ -> assert false | TemplateArity templ -> templ.template_param_levels) - | Const (cst, u) -> - let cb = Global.lookup_constant cst in - (match cb.const_type with - | RegularArity _ -> assert false - | TemplateArity (_, templ) -> - templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) @@ -70,7 +64,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) else t | UnivFlexible alg -> if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref false l; t) + (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) | Prop Pos when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 02b5c59d26..811b4dc18f 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 3fc569fc4a..9e7652da64 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index d22f94e4e5..e77d8ff645 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9c09396ccc..c40a24e3b7 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -23,8 +23,8 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp ?loc p t = CAst.make ?loc @@ - match p.CAst.v with +let mkGApp ?loc p t = DAst.make ?loc @@ + match DAst.get p with | GApp (f,l) -> GApp (f,l@[t]) | _ -> GApp (p,[t]) @@ -46,7 +46,7 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false -let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with +let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with | PatVar na1, PatVar na2 -> Name.equal na1 na2 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && @@ -98,7 +98,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with let instance_eq f (x1,c1) (x2,c2) = Id.equal x1 x2 && f c1 c2 -let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with +let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> @@ -137,7 +137,7 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c -let map_glob_constr_left_to_right f = CAst.map (function +let map_glob_constr_left_to_right f = DAst.map (function | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in @@ -186,7 +186,7 @@ let map_glob_constr = map_glob_constr_left_to_right let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt -let fold_glob_constr f acc = CAst.with_val (function +let fold_glob_constr f acc = DAst.with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left f (f acc c) args | GLambda (_,_,b,c) | GProd (_,_,b,c) -> @@ -217,7 +217,7 @@ let fold_glob_constr f acc = CAst.with_val (function let fold_return_type_with_binders f g v acc (na,tyopt) = Option.fold_left (f (Name.fold_right g na v)) acc tyopt -let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function +let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left (f v) (f v acc c) args | GLambda (na,_,b,c) | GProd (na,_,b,c) -> @@ -256,10 +256,9 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function let iter_glob_constr f = fold_glob_constr (fun () -> f) () let occur_glob_constr id = - let open CAst in - let rec occur barred acc = function - | { loc ; v = GVar id' } -> Id.equal id id' - | c -> + let rec occur barred acc c = match DAst.get c with + | GVar id' -> Id.equal id id' + | _ -> (* [g] looks if [id] appears in a binding position, in which case, we don't have to look in the corresponding subterm *) let g id' barred = barred || Id.equal id id' in @@ -268,21 +267,20 @@ let occur_glob_constr id = occur false false let free_glob_vars = - let open CAst in - let rec vars bound vs = function - | { loc ; v = GVar id' } -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs - | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in + let rec vars bound vs c = match DAst.get c with + | GVar id' -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs let glob_visible_short_qualid c = - let rec aux acc = function - | { CAst.v = GRef (c,_) } -> + let rec aux acc c = match DAst.get c with + | GRef (c,_) -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in if DirPath.is_empty dir then id :: acc else acc - | c -> + | _ -> fold_glob_constr aux acc c in aux [] c @@ -326,7 +324,7 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = CAst.map (function +let rec map_case_pattern_binders f = DAst.map (function | PatVar na as x -> let r = f na in if r == na then x @@ -396,7 +394,9 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function +let force c = DAst.make ?loc:c.CAst.loc (DAst.get c) + +let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' @@ -436,13 +436,13 @@ let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, Array.map (rename_glob_vars l) bs, Array.map (rename_glob_vars l) ts) - | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v + | _ -> DAst.get (map_glob_constr (rename_glob_vars l) c) ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = CAst.map (function +let rec cases_pattern_of_glob_constr na = DAst.map (function | GVar id -> begin match na with | Name _ -> @@ -452,8 +452,12 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function end | GHole (_,_,_) -> PatVar na | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) - | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) -> + | GApp (c, l) -> + begin match DAst.get c with + | GRef (ConstructRef cstr,_) -> PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | _ -> raise Not_found + end | _ -> raise Not_found ) @@ -469,7 +473,7 @@ let drop_local_defs typi args = | [], [] -> [] | Rel.Declaration.LocalDef _ :: decls, pat :: args -> begin - match pat.CAst.v with + match DAst.get pat with | PatVar Anonymous -> aux decls args | _ -> raise Not_found (* The pattern is used, one cannot drop it *) end @@ -487,21 +491,22 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = let typi = mip.mind_nf_lc.(j-1) in let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in drop_local_defs typi l in - Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l + Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function +let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) | PatCstr (cstr,l,Anonymous) -> - let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in + let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in let l = add_patterns_for_params_remove_local_defs cstr l in GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x -let glob_constr_of_closed_cases_pattern = function - | { CAst.loc ; v = PatCstr (cstr,l,na) } -> - na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) +let glob_constr_of_closed_cases_pattern p = match DAst.get p with + | PatCstr (cstr,l,na) -> + let loc = p.CAst.loc in + na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 6bb421e732..bacc8fbe4e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,21 +11,21 @@ open Glob_term (** Equalities *) -val cases_pattern_eq : cases_pattern -> cases_pattern -> bool +val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val cast_type_eq : ('a -> 'a -> bool) -> 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool -val glob_constr_eq : glob_constr -> glob_constr -> bool +val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> Loc.t option +val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option -val cases_predicate_names : tomatch_tuples -> Name.t list +val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list (** Apply one argument to a glob_constr *) -val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr +val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr @@ -42,12 +42,12 @@ val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit -val occur_glob_constr : Id.t -> glob_constr -> bool -val free_glob_vars : glob_constr -> Id.t list +val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool +val free_glob_vars : 'a glob_constr_g -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t (* Obsolete *) -val loc_of_glob_constr : glob_constr -> Loc.t option -val glob_visible_short_qualid : glob_constr -> Id.t list +val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option +val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list (* Renaming free variables using a renaming map; fails with [UnsoundRenaming] if applying the renaming would introduce @@ -57,7 +57,7 @@ val glob_visible_short_qualid : glob_constr -> Id.t list exception UnsoundRenaming val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t -val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr +val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented @@ -80,9 +80,9 @@ val map_pattern : (glob_constr -> glob_constr) -> @raise Not_found if translation is impossible *) val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern -val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr +val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g -val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list +val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name val empty_lvar : Glob_term.ltac_var_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 97aec1814f..aced42f839 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index a22470ae8c..2825c4d83a 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d8252ea9bb..88ca9b5ca8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -655,3 +655,93 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c + +(* inference of subtyping condition for inductive types *) + +let infer_inductive_subtyping_arity_constructor + (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in + let update_contexts (env, evd, csts) csts' = + (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') + in + let basic_check (env, evd, csts) tp = + let result = + if !numchecked >= numparams then + let csts' = + Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) + in update_contexts (env, evd, csts) csts' + else + (env, evd, csts) + in + numchecked := !numchecked + 1; result + in + let infer_typ typ ctxs = + match typ with + | LocalAssum (_, typ') -> + begin + try + let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) + with Reduction.NotConvertible -> + anomaly ~label:"inference of record/inductive subtyping relation failed" + (Pp.str "Can't infer subtyping for record/inductive type") + end + | _ -> anomaly (Pp.str "") + in + let arcn' = Term.it_mkProd_or_LetIn arcn params in + let typs, codom = Reduction.dest_prod env arcn' in + let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in + if not is_arity then basic_check last_contexts codom else last_contexts + +let infer_inductive_subtyping env evd mind_ent = + let { Entries.mind_entry_params = params; + Entries.mind_entry_inds = entries; + Entries.mind_entry_universes = ground_univs; + } = mind_ent + in + let uinfind = + match ground_univs with + | Entries.Monomorphic_ind_entry _ + | Entries.Polymorphic_ind_entry _ -> ground_univs + | Entries.Cumulative_ind_entry cumi -> + begin + let uctx = Univ.CumulativityInfo.univ_context cumi in + let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in + let dosubst = subst_univs_level_constr sbsubst 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 in + let env = Environ.push_context uctx_other env in + let evd = + Evd.merge_universe_context + evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) + in + let (_, _, subtyp_constraints) = + List.fold_left + (fun ctxs indentry -> + let _, params = Typeops.infer_local_decls env params in + let ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true params + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor + ctxs dosubst cons false params + ) + ctxs' indentry.Entries.mind_entry_lc + ) (env, evd, Univ.Constraint.empty) entries + in + Entries.Cumulative_ind_entry + (Univ.CumulativityInfo.make + (Univ.CumulativityInfo.univ_context cumi, + Univ.UContext.make + (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), + subtyp_constraints))) + end + in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index bdb6f996b9..aa38d3b47d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -199,3 +199,12 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit + +(* inference of subtyping condition for inductive types *) +(* for debugging purposes only to be removed *) +val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> +(Term.constr -> Term.constr) -> +Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t + +val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index e555742bca..86bc471323 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index c7661239e3..718d074cf4 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 69bc2d11ff..bc563b46dc 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index f30dc1a4b6..dae29208ed 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 61118cf777..39c2ceeba8 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,6 +26,59 @@ module RelDecl = Context.Rel.Declaration exception Find_at of int +(* profiling *) + +let profiling_enabled = ref false + +(* for supported platforms, filename for profiler results *) + +let profile_filename = ref "native_compute_profile.data" + +let profiler_platform () = + match [@warning "-8"] Sys.os_type with + | "Unix" -> + let in_ch = Unix.open_process_in "uname" in + let uname = input_line in_ch in + let _ = close_in in_ch in + Format.sprintf "Unix (%s)" uname + | "Win32" -> "Windows (Win32)" + | "Cygwin" -> "Windows (Cygwin)" + +let get_profile_filename () = !profile_filename + +let set_profile_filename fn = + profile_filename := fn + +(* find unused profile filename *) +let get_available_profile_filename () = + let profile_filename = get_profile_filename () in + let dir = Filename.dirname profile_filename in + let base = Filename.basename profile_filename in + (* starting with OCaml 4.04, could use Filename.remove_extension and Filename.extension, which + gets rid of need for exception-handling here + *) + let (name,ext) = + try + let nm = Filename.chop_extension base in + let nm_len = String.length nm in + let ex = String.sub base nm_len (String.length base - nm_len) in + (nm,ex) + with Invalid_argument _ -> (base,"") + in + try + (* unlikely race: fn deleted, another process uses fn *) + Filename.temp_file ~temp_dir:dir (name ^ "_") ext + with Sys_error s -> + let msg = "When trying to find native_compute profile output file: " ^ s in + let _ = Feedback.msg_info (Pp.str msg) in + assert false + +let get_profiling_enabled () = + !profiling_enabled + +let set_profiling_enabled b = + profiling_enabled := b + let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do @@ -379,6 +432,52 @@ let evars_of_evar_map sigma = Nativelambda.evars_typ = Evd.existential_type sigma; Nativelambda.evars_metas = Evd.meta_type sigma } +(* fork perf process, return profiler's process id *) +let start_profiler_linux profile_fn = + let coq_pid = Unix.getpid () in (* pass pid of running coqtop *) + (* we don't want to see perf's console output *) + let dev_null = Unix.descr_of_out_channel (open_out_bin "/dev/null") in + let _ = Feedback.msg_info (Pp.str ("Profiling to file " ^ profile_fn)) in + let perf = "perf" in + let profiler_pid = + Unix.create_process + perf + [|perf; "record"; "-g"; "-o"; profile_fn; "-p"; string_of_int coq_pid |] + Unix.stdin dev_null dev_null + in + (* doesn't seem to be a way to test whether process creation succeeded *) + if !Flags.debug then + Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn)); + Some profiler_pid + +(* kill profiler via SIGINT *) +let stop_profiler_linux m_pid = + match m_pid with + | Some pid -> ( + let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in + try + Unix.kill pid Sys.sigint; + let _ = Unix.waitpid [] pid in () + with Unix.Unix_error (Unix.ESRCH,"kill","") -> + Feedback.msg_info (Pp.str "Could not stop native code profiler, no such process") + ) + | None -> () + +let start_profiler () = + let profile_fn = get_available_profile_filename () in + match profiler_platform () with + "Unix (Linux)" -> start_profiler_linux profile_fn + | _ -> + let _ = Feedback.msg_info + (Pp.str (Format.sprintf "Native_compute profiling not supported on the platform: %s" + (profiler_platform ()))) in + None + +let stop_profiler m_pid = + match profiler_platform() with + "Unix (Linux)" -> stop_profiler_linux m_pid + | _ -> () + let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in @@ -392,12 +491,15 @@ let native_norm env sigma c ty = *) let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in - match Nativelib.compile ml_filename code with + let profile = get_profiling_enabled () in + match Nativelib.compile ml_filename code ~profile:profile with | true, fn -> if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); + let profiler_pid = if profile then start_profiler () else None in let t0 = Sys.time () in Nativelib.call_linker ~fatal:true prefix fn (Some upd); let t1 = Sys.time () in + if profile then stop_profiler profiler_pid; let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); let res = nf_val env sigma !Nativelib.rt1 ty in diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index c899340c8c..579a7d2acb 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,6 +12,13 @@ open Evd (** This module implements normalization by evaluation to OCaml code *) +val get_profile_filename : unit -> string +val set_profile_filename : string -> unit + +val get_profiling_enabled : unit -> bool +val set_profiling_enabled : bool -> unit + + val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c36542aebc..3b3ad021e4 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -326,7 +326,7 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function +let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -335,11 +335,14 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> + | GApp (c, cl) -> + begin match DAst.get c with + | GPatVar (Evar_kinds.SecondOrderPatVar n) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | GApp (c,cl) -> + | _ -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) + end | GLambda (na,bk,c1,c2) -> Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, @@ -364,8 +367,8 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda na c = CAst.make ?loc @@ - GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let mkGLambda na c = DAst.make ?loc @@ + GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; @@ -377,8 +380,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PCase (cip, PMeta None, pat_of_raw metas vars b, [0,tags,pat_of_raw metas vars c]) | GCases (sty,p,[c,(na,indnames)],brs) -> + let get_ind p = match DAst.get p with + | PatCstr((ind,_),_,_) -> Some ind + | _ -> None + in let get_ind = function - | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind + | (_,(_,[p],_))::_ -> get_ind p | _ -> None in let ind_tags,ind = match indnames with @@ -391,8 +398,11 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some { CAst.v = GHole _}), _ -> PMeta None + | None, _ -> PMeta None | Some p, None -> + match DAst.get p with + | GHole _ -> PMeta None + | _ -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = @@ -410,30 +420,36 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function ) and pats_of_glob_branches loc metas vars ind brs = - let get_arg = function - | { CAst.v = PatVar na } -> + let get_arg p = match DAst.get p with + | PatVar na -> Name.iter (fun n -> metas := n::!metas) na; na - | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") + | PatCstr(_,_,_) -> err ?loc:p.CAst.loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *) - | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs -> - let () = match ind with - | Some sp when eq_ind sp indsp -> () + | (loc',(_,[p], br)) :: brs -> + begin match DAst.get p, DAst.get br, brs with + | PatVar Anonymous, GHole _, [] -> + true, [] (* ends with _ => _ *) + | PatCstr((indsp,j),lv,_), _, _ -> + let () = match ind with + | Some sp when eq_ind sp indsp -> () + | _ -> + err ?loc (Pp.str "All constructors must be in the same inductive type.") + in + if Int.Set.mem (j-1) indexes then + err ?loc + (str "No unique branch for " ++ int j ++ str"-th constructor."); + let lna = List.map get_arg lv in + let vars' = List.rev lna @ vars in + let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in + let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in + ext, ((j-1, tags, pat) :: pats) | _ -> - err ?loc (Pp.str "All constructors must be in the same inductive type.") - in - if Int.Set.mem (j-1) indexes then - err ?loc - (str "No unique branch for " ++ int j ++ str"-th constructor."); - let lna = List.map get_arg lv in - let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in - let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in - let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in - ext, ((j-1, tags, pat) :: pats) + err ?loc:loc' (Pp.str "Non supported pattern.") + end | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 791fd74ed3..3a1faf1c77 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d7c04b08b0..54b477bed9 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index c303d5d949..124fa6e06c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7488f35bfe..79d2c3333b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -47,8 +47,6 @@ open Misctypes module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) @@ -385,9 +383,6 @@ let adjust_evar_source evdref na c = end | _, _ -> c -(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) -let allow_anonymous_refs = ref false - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j @@ -511,8 +506,8 @@ let pretype_global ?loc rigid env evd gr us = match us with | None -> evd, None | Some l -> - let _, ctx = Universes.unsafe_constr_of_global gr in - let len = Univ.UContext.size ctx in + let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in + let len = Univ.AUContext.size ctx in interp_instance ?loc evd ~len l in let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in @@ -577,7 +572,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in let loc = t.CAst.loc in - match t.CAst.v with + match DAst.get t with | GRef (ref,u) -> inh_conv_coerce_to_tycon ?loc env evdref (pretype_ref ?loc evdref env ref u) @@ -918,9 +913,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - List.map (set_name Anonymous) arsgn - else arsgn + List.map (set_name Anonymous) arsgn in let indt = build_dependent_inductive env.ExtraEnv.env indf in let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) @@ -981,10 +974,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in - if not !allow_anonymous_refs then - (* Make dependencies from arity signature impossible *) - List.map (set_name Anonymous) arsgn - else arsgn + (* Make dependencies from arity signature impossible *) + List.map (set_name Anonymous) arsgn in let nar = List.length arsgn in let indt = build_dependent_inductive env.ExtraEnv.env indf in @@ -1018,13 +1009,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in let csgn = - if not !allow_anonymous_refs then - List.map (set_name Anonymous) cs_args - else - List.map (map_name (function Name _ as n -> n - | Anonymous -> Name Namegen.default_non_dependent_ident)) - cs_args - in + List.map (set_name Anonymous) cs_args + in let env_c = push_rel_context !evdref csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs_args in @@ -1114,8 +1100,9 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function - | { loc; CAst.v = GHole (knd, naming, None) } -> +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with + | GHole (knd, naming, None) -> + let loc = loc_of_glob_constr c in let rec is_Type c = match EConstr.kind !evdref c with | Sort s -> begin match ESorts.kind !evdref s with @@ -1136,14 +1123,19 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in - { utj_val = v; - utj_type = s } + (* Correction of bug #5315 : we need to define an evar for *all* holes *) + let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in + let ev,_ = destEvar !evdref evkt in + evdref := Evd.define ev (to_constr !evdref v) !evdref; + (* End of correction of bug #5315 *) + { utj_val = v; + utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) - | c -> + | _ -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in @@ -1186,29 +1178,6 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let on_judgment sigma f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast sigma (f c) in - {uj_val = c; uj_type = t} - -let understand_judgment env sigma c = - let env = make_env env sigma in - let evdref = ref sigma in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment sigma (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in - evdref := evd; c) j - in j, Evd.evar_universe_context !evdref - -let understand_judgment_tcc env evdref c = - let env = make_env env !evdref in - let k0 = Context.Rel.length (rel_context env) in - let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment !evdref (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in - evdref := evd; c) j - let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in @@ -1226,36 +1195,10 @@ let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutT let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in (sigma, c) -let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = - let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in - evdref := sigma; - c - let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let constr_flags = { - use_typeclasses = true; - solve_unification_constraints = true; - use_hook = None; - fail_evar = true; - expand_evars = true } - -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - begin fun env sigma -> - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = Id.Map.empty; - } in - understand_ltac flags env sigma vars expected_type term - end - let pretype k0 resolve_tc typcon env evdref lvar t = pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e17468ef83..7395e94a09 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,9 +27,6 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * constr - type inference_hook = env -> evar_map -> evar -> evar_map * constr type inference_flags = { @@ -48,9 +45,6 @@ val all_no_fail_flags : inference_flags 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 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 @@ -61,9 +55,6 @@ val allow_anonymous_refs : bool ref val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr -val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> - ?expected_type:typing_constraint -> glob_constr -> constr - (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr @@ -78,7 +69,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr + typing_constraint -> glob_constr -> evar_map * EConstr.t (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; @@ -90,20 +81,6 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context -(** Idem but returns the judgment of the understood term *) - -val understand_judgment : env -> evar_map -> - glob_constr -> unsafe_judgment Evd.in_evar_universe_context - -(** Idem but do not fail on unresolved evars (type cl*) -val understand_judgment_tcc : env -> evar_map ref -> - glob_constr -> unsafe_judgment - -val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open - (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) diff --git a/pretyping/program.ml b/pretyping/program.ml index f9be82024a..bdc34bc532 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/program.mli b/pretyping/program.mli index 8439b9528c..70ab97e83e 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bc9e3a1f46..a23579609a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -134,7 +134,7 @@ let find_projection = function type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) @@ -189,22 +189,26 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (t,con_pp,proji_sp_pp) -> + (fun (sign,env,t,con,proji_sp) -> + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in + let env = Termops.push_rels_assum sign env in + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in strbrk "Projection value has no head constant: " - ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " + ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) let compute_canonical_projections warn (con,ind) = let env = Global.env () in - let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in - let u = Univ.UContext.instance ctx in + let ctx = Environ.constant_context env con in + let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in - let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in - let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in + let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in @@ -221,9 +225,7 @@ let compute_canonical_projections warn (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) - and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); l end | _ -> l) @@ -298,8 +300,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let ctx = Environ.constant_context env sp in - let u = Univ.UContext.instance ctx in + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 7c0d0ec6d4..5480b14af0 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,7 +57,7 @@ type cs_pattern = type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : constr list; (** ordered *) o_TPARAMS : constr list; (** ordered *) @@ -67,7 +67,7 @@ type obj_typ = { (** Return the form of the component of a canonical structure *) val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list -val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds +val pr_cs_pattern : cs_pattern -> Pp.t val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ val declare_canonical_structure : global_reference -> unit diff --git a/pretyping/redops.ml b/pretyping/redops.ml index 8e190f40b9..b5e4a7acbf 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/redops.mli b/pretyping/redops.mli index f6d4d80862..435b25091e 100644 --- a/pretyping/redops.mli +++ b/pretyping/redops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a6483012..3563235434 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,7 @@ exception Elimconst let refolding_in_reduction = ref false let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; + Goptions.optdepr = true; (* remove in 8.8 *) Goptions.optname = "Perform refolding of fixpoints/constants like cbn during reductions"; Goptions.optkey = ["Refolding";"Reduction"]; @@ -272,7 +272,7 @@ module Stack : sig open EConstr type 'a app_node - val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t type cst_member = | Cst_const of pconstant @@ -290,7 +290,7 @@ sig exception IncompatibleFold2 - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t val empty : 'a t val is_empty : 'a t -> bool val append_app : 'a array -> 'a t -> 'a t @@ -1313,8 +1313,8 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly _ = - let e = UserError (None, Pp.str "Conversion test raised an anomaly") in +let report_anomaly e = + let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in let e = CErrors.push e in iraise e @@ -1361,9 +1361,79 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible +let sigma_check_inductive_instances cv_pb uinfind u u' sigma = + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) + in + let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in + if not ((len_instance = Univ.Instance.length u) && + (len_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.AUContext.instantiate comp_subst ind_sbctx + in + let comp_cst = + match cv_pb with + Reduction.CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in + Univ.Constraint.union comp_cst comp_cst' + | Reduction.CUMUL -> comp_cst + in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + +let sigma_conv_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> + let num_param_arity = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + raise Reduction.NotConvertible + else + sigma_check_inductive_instances cv_pb cumi u1 u2 sigma + +let sigma_conv_constructors + (mind, ind, cns) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + raise Reduction.NotConvertible + else + sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma + let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.conv_inductives = sigma_conv_inductives; + Reduction.conv_constructors = sigma_conv_constructors} let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index af4ea3ac53..1828196fe4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,7 +26,7 @@ module ReductionBehaviour : sig bool -> Globnames.global_reference -> (int list * int * flag list) -> unit val get : Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.std_ppcmds + val print : Globnames.global_reference -> Pp.t end (** Option telling if reduction should use the refolding machinery of cbn @@ -63,14 +63,13 @@ module Cst_stack : sig val best_cst : t -> (constr * constr list) option val best_replace : Evd.evar_map -> constr -> t -> constr -> constr val reference : Evd.evar_map -> t -> Constant.t option - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end - module Stack : sig type 'a app_node - val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t type cst_member = | Cst_const of pconstant @@ -87,7 +86,7 @@ module Stack : sig | Update of 'a and 'a t = 'a member list - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t val empty : 'a t val is_empty : 'a t -> bool @@ -146,7 +145,7 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -val pr_state : state -> Pp.std_ppcmds +val pr_state : state -> Pp.t (** {6 Reduction Function Operators } *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a1d0977f5a..079524f344 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -192,11 +192,6 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters ~polyprop env (mip, u) argtyps with Reduction.NotArity -> retype_error NotAnArity) - | Const (cst, u) -> - let u = EInstance.kind sigma u in - EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps - with Reduction.NotArity -> retype_error NotAnArity) - | Var id -> type_of_var env id | Construct (cstr, u) -> let u = EInstance.kind sigma u in EConstr.of_constr (type_of_constructor env (cstr, u)) @@ -220,7 +215,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = | Const (cst, u) -> let t = constant_type_in env (cst, EInstance.kind sigma u) in (* TODO *) - sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||]) + sigma, EConstr.of_constr t | Var id -> sigma, type_of_var env id | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 25129db1c9..ed3a9d0f96 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -48,4 +48,4 @@ val sorts_of_context : env -> evar_map -> rel_context -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr -val print_retype_error : retype_error -> Pp.std_ppcmds +val print_retype_error : retype_error -> Pp.t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 62737b65e0..708788ab87 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -557,6 +557,12 @@ let match_eval_ref_value env sigma constr stack = Some (EConstr.of_constr (constant_value_in env (sp, u))) else None + | Proj (p, c) when not (Projection.unfolded p) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef (Projection.constant p)) then + Some (mkProj (Projection.unfold p, c)) + else None | Var id when is_evaluable env (EvalVarRef id) -> env |> lookup_named id |> NamedDecl.get_value | Rel n -> diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index c31212e26a..91726e8c6d 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..375a8a983f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,6 +57,9 @@ type direction = Forward | Backward (* This module defines type-classes *) type typeclass = { + (* Universe quantification *) + cl_univs : Univ.AUContext.t; + (* The class implementation *) cl_impl : global_reference; @@ -81,8 +84,8 @@ type instance = { is_class: global_reference; is_info: Vernacexpr.hint_info_expr; (* Sections where the instance should be redeclared, - -1 for discard, 0 for none. *) - is_global: int; + None for discard, Some 0 for none. *) + is_global: int option; is_poly: bool; is_impl: global_reference; } @@ -95,9 +98,11 @@ let hint_priority is = is.is_info.Vernacexpr.hint_priority let new_instance cl info glob poly impl = let global = - if glob then Lib.sections_depth () - else -1 + if glob then Some (Lib.sections_depth ()) + else None in + if match global with Some n -> n>0 && isVarRef impl | _ -> false then + CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable."); { is_class = cl.cl_impl; is_info = info ; is_global = global ; @@ -111,27 +116,11 @@ let new_instance cl info glob poly impl = let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes" let instances : instances ref = Summary.ref Refmap.empty ~name:"instances" -open Declarations - -let typeclass_univ_instance (cl,u') = - let subst = - let u = - match cl.cl_impl with - | ConstRef c -> - let cb = Global.lookup_constant c in - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty - | IndRef c -> - let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty - | _ -> Univ.Instance.empty - in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) - Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') - in - let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in - { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context); - cl_props = subst_ctx cl.cl_props}, u' +let typeclass_univ_instance (cl, u) = + assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u); + let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in + { cl with cl_context = on_snd subst_ctx cl.cl_context; + cl_props = subst_ctx cl.cl_props} let class_info c = try Refmap.find c !classes @@ -189,7 +178,8 @@ let subst_class (subst,cl) = do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in - { cl_impl = do_subst_gr cl.cl_impl; + { cl_univs = cl.cl_univs; + cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; cl_props = do_subst_ctx cl.cl_props; cl_projs = do_subst_projs cl.cl_projs; @@ -203,15 +193,14 @@ let discharge_class (_,cl) = let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in - let discharge_rel_context subst n rel = + let discharge_rel_context (subst, usubst) n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in - let ctx, _ = - List.fold_right - (fun decl (ctx, k) -> - RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k - ) - rel ([], n) - in ctx + let fold decl (ctx, k) = + let map c = subst_univs_level_constr usubst (substn_vars k subst c) in + RelDecl.map_constr map decl :: ctx, succ k + in + let ctx, _ = List.fold_right fold rel ([], n) in + ctx in let abs_context cl = match cl.cl_impl with @@ -231,12 +220,14 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, usubst, uctx = abs_context cl in + let ctx, _, _ as info = abs_context cl in let ctx, subst = rel_of_variable_context ctx in - let context = discharge_context ctx subst cl.cl_context in - let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in + let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in + let context = discharge_context ctx (subst, usubst) cl.cl_context in + let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in - { cl_impl = cl_impl'; + { cl_univs = cl_univs'; + cl_impl = cl_impl'; cl_context = context; cl_props = props; cl_projs = List.smartmap discharge_proj cl.cl_projs; @@ -283,8 +274,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in + let inst, ctx = Universes.fresh_instance_from ctx None in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = match class_of_constr sigma ty with | None -> [] @@ -321,7 +314,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + let term = Universes.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] @@ -359,22 +352,34 @@ let subst_instance (subst, (action, inst)) = action, is_impl = fst (subst_global subst inst.is_impl) } let discharge_instance (_, (action, inst)) = - if inst.is_global <= 0 then None - else Some (action, + match inst.is_global with + | None -> None + | Some n -> + assert (not (isVarRef inst.is_impl)); + Some (action, { inst with - is_global = pred inst.is_global; + is_global = Some (pred n); is_class = Lib.discharge_global inst.is_class; is_impl = Lib.discharge_global inst.is_impl }) -let is_local i = Int.equal i.is_global (-1) +let is_local i = (i.is_global == None) + +let is_local_for_hint i = + match i.is_global with + | None -> true (* i.e. either no Global keyword not in section, or in section *) + | Some n -> n <> 0 (* i.e. in a section, declare the hint as local + since discharge is managed by rebuild_instance which calls again + add_instance_hint; don't ask hints to take discharge into account + itself *) let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) + let local = is_local_for_hint inst in + add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local inst.is_info poly; List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path - (is_local inst) pri poly) + local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) @@ -409,10 +414,11 @@ let remove_instance i = remove_instance_hint i.is_impl let declare_instance info local glob = - let ty = Global.type_of_global_unsafe glob in + let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> + assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) | None -> () diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8d1c0b94ca..99cdbd3a36 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,6 +16,10 @@ type direction = Forward | Backward (** This module defines type-classes *) type typeclass = { + (** The toplevel universe quantification in which the typeclass lives. In + particular, [cl_props] and [cl_context] are quantified over it. *) + cl_univs : Univ.AUContext.t; + (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) cl_impl : global_reference; @@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) -val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses +val typeclass_univ_instance : typeclass puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 754dacd193..dc8ff2e208 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 558575ccce..557aa3c9f9 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7ad988ad0b..1f35fa19aa 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -35,11 +35,6 @@ let meta_type evd mv = let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty -let constant_type_knowing_parameters env sigma (cst, u) jl = - let u = Unsafe.to_instance u in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in - EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp) - let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in @@ -315,9 +310,6 @@ let rec execute env evdref cstr = | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> make_judge f (inductive_type_knowing_parameters env !evdref (ind, u) jl) - | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env -> - make_judge f - (constant_type_knowing_parameters env !evdref (cst, u) jl) | _ -> (* No template polymorphism *) execute env evdref f diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1f3ba34e51..1e20788268 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 67c8b07e78..f090921e5c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0d90ab1584..fce17d5641 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..66cc42cb61 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -174,8 +174,7 @@ and nf_whd env sigma whd typ = | 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 + Univ.AUContext.size (Declareops.inductive_polymorphic_context mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | 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 + Univ.AUContext.size (Declareops.constant_polymorphic_context cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 8a4202c887..d1a996a34b 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |