diff options
Diffstat (limited to 'pretyping')
35 files changed, 796 insertions, 676 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index d59102b6c7..8ac471404a 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -40,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) = let r' = fst (subst_global subst r) in if r==r' then orig else (r', names) -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.AUContext.empty - let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> (try - let vars,_,_ = section_segment_of_reference c in + let vars = Lib.variable_section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in let names' = var_names @ names in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4f3669a2b9..a0434f9279 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -450,11 +450,6 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns.") -let alias_of_pat = DAst.with_val (function - | PatVar name -> name - | PatCstr(_,_,name) -> name - ) - let remove_current_pattern eqn = match eqn.patterns with | pat::pats -> @@ -1276,7 +1271,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* This is a bit too strong I think, in the sense that what we would *) (* really like is to have beta-iota reduction only at the positions where *) (* parameters are substituted *) - let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in + let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in (* We build the matrix obtained by expanding the matching on *) (* "C x1..xn as x" followed by a residual matching on eqn into *) @@ -1426,7 +1421,7 @@ and match_current pb (initial,tomatch) = find_predicate pb.caseloc pb.env pb.evdref pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in - let pred = nf_betaiota !(pb.evdref) pred in + let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in @@ -1566,11 +1561,9 @@ substituer après par les initiaux *) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) + * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,lpat,rhs)) = - let initial_lpat,initial_rhs = lpat,rhs in - let initial_rhs = rhs in + let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = let avoid = ids_of_named_context_val (named_context_val env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = @@ -1665,7 +1658,7 @@ let rec list_assoc_in_triple x = function *) let abstract_tycon ?loc env evdref subst tycon extenv t = - let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*) + let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 192eca63bb..e42576d95b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk = let cofixp_reducible flgs _ stk = if red_set flgs fCOFIX then match stk with - | (CASE _ | APP(_,CASE _)) -> true + | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true | _ -> false else false diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c36630f5d3..6d5ee504e5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -344,8 +344,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -433,13 +433,13 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; @@ -450,15 +450,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -497,7 +497,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } diff --git a/pretyping/classops.mli b/pretyping/classops.mli index b41d0efac5..47b41f17b2 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -96,7 +96,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 20ef65c884..c3a221944d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Termops -open Reductionops open Term open EConstr open Vars @@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -265,7 +260,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (PApp (h, a1), a2), _ -> sorec ctx env subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) -> (let diff = Array.length args2 - Array.length args1 in if diff >= 0 then let args21, args22 = Array.chop diff args2 in @@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma pat c = + let names, subst = matches_core env sigma false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma (Id.Set.empty,pat) c) let special_meta = (-1) @@ -410,9 +405,9 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx = +let authorized_occ env sigma closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -421,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx = let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) -let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = +let sub_match ?(closed=true) env sigma pat c = let open EConstr in let rec aux env c mk_ctx next = - let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let here = authorized_occ env sigma closed pat c mk_ctx in let next () = match EConstr.kind sigma c with | Cast (c1,k,c2) -> let next_mk_ctx = function @@ -454,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let topdown = true in - if partial_app then - if topdown then - let lc1 = Array.sub lc 0 (Array.length lc - 1) in - let app = mkApp (c1,lc1) in - let mk_ctx = function - | [app';c] -> mk_ctx (mkApp (app',[|c|])) - | _ -> assert false in - try_aux [(env, app); (env, Array.last lc)] mk_ctx next - else - let rec aux2 app args next = - match args with - | [] -> - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next - | arg :: args -> - let app = mkApp (app,[|arg|]) in - let next () = aux2 app args next in - let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in - aux env app mk_ctx next in - aux2 c1 (Array.to_list lc) next - else - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [(env, app); (env, Array.last lc)] mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) @@ -489,29 +462,28 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = in let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next - | Fix (indx,(names,types,bodies)) -> + | Fix (indx,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next - | CoFix (i,(names,types,bodies)) -> + | CoFix (i,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - if partial_app then - try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () - else - try_aux [env, c'] next_mk_ctx next + begin try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> next () + end | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> next () in @@ -532,13 +504,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let result () = aux env c (fun x -> x) lempty in IStream.thunk result -let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c - -let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c - -let match_subterm_gen env sigma app pat c = - sub_match ~partial_app:app env sigma pat c +let match_subterm env sigma pat c = sub_match env sigma pat c let is_matching env sigma pat c = try let _ = matches env sigma pat c in true @@ -550,12 +516,5 @@ let is_matching_head env sigma pat c = let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in - let results = sub_match ~partial_app:true ~closed env sigma pat c in + let results = sub_match ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 780ccc23d1..e4d9ff9e1e 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -55,38 +55,19 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; m_ctx : EConstr.t } -(** [match_subterm n pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat]. *) -val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_appsubterm pat c] returns the substitution and the context +(** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], considering application contexts as well. *) -val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> - bool (** true = with app context *) -> +val match_subterm : env -> Evd.evar_map -> binding_bound_vars * constr_pattern -> constr -> matching_result IStream.t (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0d1e401d98..18ecbf8ed3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -252,6 +252,89 @@ let lookup_index_as_renamed env sigma t n = in lookup n 1 t (**********************************************************************) +(* Factorization of match patterns *) + +let print_factorize_match_patterns = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "factorization of \"match\" patterns in printing"; + optkey = ["Printing";"Factorizable";"Match";"Patterns"]; + optread = (fun () -> !print_factorize_match_patterns); + optwrite = (fun b -> print_factorize_match_patterns := b) } + +let print_allow_match_default_clause = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "possible use of \"match\" default pattern in printing"; + optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; + optread = (fun () -> !print_allow_match_default_clause); + optwrite = (fun b -> print_allow_match_default_clause := b) } + +let rec join_eqns (ids,rhs as x) patll = function + | (loc,(ids',patl',rhs') as eqn')::rest -> + if not !Flags.raw_print && !print_factorize_match_patterns && + List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' + then + join_eqns x (patl'::patll) rest + else + let eqn,rest = join_eqns x patll rest in + eqn, eqn'::rest + | [] -> + patll, [] + +let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll + +let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = [] + +let rec move_more_factorized_default_candidate_to_end eqn n = function + | eqn' :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in + if isbest then false, dft, eqns else false, dft, eqn' :: eqns + else + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in + isbest, dft, eqn' :: eqns + | [] -> true, Some eqn, [] + +let rec select_default_clause = function + | eqn :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in + if isbest then dft, eqns else dft, eqn :: eqns + else + let dft, eqns = select_default_clause eqns in dft, eqn :: eqns + | [] -> None, [] + +let factorize_eqns eqns = + let rec aux found = function + | (loc,(ids,patl,rhs))::rest -> + let patll,rest = join_eqns (ids,rhs) [patl] rest in + aux ((loc,(ids,patll,rhs))::found) rest + | [] -> + found in + let eqns = aux [] (List.rev eqns) in + let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in + if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + match select_default_clause eqns with + (* At least two clauses and the last one is disjunctive with no variables *) + | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)] + (* Only one clause which is disjunctive with no variables: we keep at least one constructor *) + (* so that it is not interpreted as a dummy "match" *) + | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)] + | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false + | None, eqns -> eqns + else + eqns + +(**********************************************************************) (* Fragile algorithm to reverse pattern-matching compilation *) let update_name sigma na ((_,(e,_)),c) = @@ -284,13 +367,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = let rec build_tree na isgoal e sigma ci cl = 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 (List.init (Array.length cl) - (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) + (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) sigma = match nal with - | [] -> [[],rhs] + | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with | Case (ci,p,c,cl) when @@ -300,19 +382,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e sigma ci cl in List.flatten - (List.map (fun (pat,rhs) -> + (List.map (fun (ids,pat,rhs) -> let lines = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) lines) + List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines) clauses) | _ -> - 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 + let na = update_name sigma na rhs in + let pat = DAst.make @@ PatVar na in + let mat = align_tree nal isgoal rhs sigma in + List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat -and contract_branch isgoal e sigma (cdn,can,mkpat,b) = - let nal,rhs = decomp_branch cdn [] isgoal e sigma b in +and contract_branch isgoal e sigma (cdn,mkpat,rhs) = + let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat + List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) @@ -368,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match Option.map detype p with - | None -> Anonymous, None, None - | Some p -> - let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match DAst.get typ with - | GLambda (x,_,t,c) -> x, c - | _ -> Anonymous, typ in - let aliastyp = - if List.for_all (Name.equal Anonymous) nl then None - else Some (Loc.tag (indsp,nl)) in - n, aliastyp, Some typ + let p = detype p in + let nl,typ = it_destRLambda_or_LetIn_names k p in + let n,typ = match DAst.get typ with + | GLambda (x,_,t,c) -> x, c + | _ -> Anonymous, typ in + let aliastyp = + if List.for_all (Name.equal Anonymous) nl then None + else Some (Loc.tag (indsp,nl)) in + n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in let tag = @@ -414,15 +495,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_universe sigma u = + let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in + Univ.Universe.map fn u + let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - then - let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in - [Loc.tag @@ Name.mk_name (Id.of_string_soft u)] + then detype_universe sigma u else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,8 +517,8 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in - GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l))) + let l = Termops.reference_of_level sigma l in + GType (UNamed l) let detype_instance sigma l = let l = EInstance.kind sigma l in @@ -496,12 +579,7 @@ and detype_r d flags avoid env sigma t = | 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 = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - let args = List.make pars hole in - GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype d flags avoid env sigma c])) + GProj (p, detype d flags avoid env sigma c) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () @@ -570,7 +648,7 @@ and detype_r d flags avoid env sigma t = (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 + p c bl | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef @@ -646,7 +724,7 @@ 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 d flags avoid env sigma c)) + List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list @@ -917,6 +995,13 @@ let rec subst_glob_constr subst = DAst.map (function let r1' = subst_glob_constr subst r1 in let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + + | GProj (p,c) as raw -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_glob_constr subst c in + if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c') ) (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cb1c0d8d4b..f150cb1956 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -26,10 +26,20 @@ val print_universes : bool ref (** If true, prints full local context of evars *) val print_evar_arguments : bool ref +(** If true, contract branches with same r.h.s. and same matching + variables in a disjunctive pattern *) +val print_factorize_match_patterns : bool ref + +(** If true and the last non unique clause of a "match" is a + variable-free disjunctive pattern, turn it into a catch-call case *) +val print_allow_match_default_clause : bool ref + val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern val subst_glob_constr : substitution -> glob_constr -> glob_constr +val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g + (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in [avoid] [isgoal] tells if naming must avoid global-level synonyms as intro does diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 18e0c31dd6..dc3acbc3e2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -218,6 +218,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = EConstr.of_constr t' in let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in + let params = List.map (fun c -> subst_univs_level_constr subst c) params in + let us = List.map (fun c -> subst_univs_level_constr subst c) us in let h, _ = decompose_app_vect sigma t' in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, @@ -274,11 +276,6 @@ let rec ise_app_stack2 env f evd sk1 sk2 = end | _, _ -> (sk1,sk2), Success evd -let push_rec_types pfix env = - let (i, c, t) = pfix in - let inj c = EConstr.Unsafe.to_constr c in - push_rec_types (i, Array.map inj c, Array.map inj t) env - (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is @@ -310,8 +307,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i' -> ise_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin match ise_app_stack2 env f i sk1 sk2 with @@ -344,8 +339,6 @@ let exact_ise_stack2 env evd f sk1 sk2 = if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> begin match ise_app_stack2 env f i sk1 sk2 with |_,(UnifFailure _ as x) -> x @@ -360,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = 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 + Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u') let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in @@ -457,7 +438,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 @@ -1046,7 +1027,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in @@ -1067,8 +1048,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index b646a37f8a..fd83795f55 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -28,8 +28,8 @@ let env_nf_evar sigma env = let env_nf_betaiotaevar sigma env = process_rel_context - (fun d e -> - push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env + (fun d env -> + push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota env sigma c) d) env) env (****************************************) (* Operations on value/type constraints *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 093f1f0b68..25817478e7 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -19,6 +19,16 @@ open Ltac_pretype let cases_pattern_loc c = c.CAst.loc +let alias_of_pat pat = DAst.with_val (function + | PatVar name -> name + | PatCstr(_,_,name) -> name + ) pat + +let set_pat_alias id = DAst.map (function + | PatVar Anonymous -> PatVar (Name id) + | PatCstr (cstr,patl,Anonymous) -> PatCstr (cstr,patl,Name id) + | pat -> assert false) + let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] @@ -133,8 +143,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 + | GProj (p1, t1), GProj (p2, t2) -> + Projection.equal p1 p2 && f t1 t2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | - GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c @@ -180,6 +192,8 @@ let map_glob_constr_left_to_right f = DAst.map (function let comp1 = f c in let comp2 = Miscops.map_cast_type f k in GCast (comp1,comp2) + | GProj (p,c) -> + GProj (p, f c) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x ) @@ -212,6 +226,8 @@ let fold_glob_constr f acc = DAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c + | GProj(_,c) -> + f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc ) @@ -253,6 +269,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c + | GProj(_,c) -> + f v acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc)) let iter_glob_constr f = fold_glob_constr (fun () -> f) () @@ -444,6 +462,10 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + let rec cases_pattern_of_glob_constr na = DAst.map (function | GVar id -> begin match na with @@ -460,6 +482,9 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found end + | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous -> + (* A canonical encoding of aliases *) + DAst.get (cases_pattern_of_glob_constr na' b) | _ -> raise Not_found ) @@ -495,23 +520,34 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = drop_local_defs typi l in Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l +let add_alias ?loc na c = + match na with + | Anonymous -> c + | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id)) + (* Turn a closed cases pattern into a glob_constr *) -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 rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function + | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None)) + | PatCstr (cstr,l,na) -> 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) + add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l)) + | PatVar (Name id) when not isclosed -> + GVar id + | PatVar Anonymous when not isclosed -> + GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None) | _ -> raise Not_found ) x 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)) + na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found +let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p + (**********************************************************************) (* Interpreting ltac variables *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 9dd7068cbc..0d9fb1f453 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,10 @@ open Glob_term val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool +val alias_of_pat : 'a cases_pattern_g -> Name.t + +val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g + val cast_type_eq : ('a -> 'a -> bool) -> 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool @@ -78,10 +82,14 @@ val map_pattern : (glob_constr -> glob_constr) -> Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern +val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g +(** A canonical encoding of cases pattern into constr such that + composed with [cases_pattern_of_glob_constr Anonymous] gives identity *) +val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g + val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 34df7d3d72..275a079d5d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec (_,i) -> Int.List.mem i listind + | Mrec (_,i) -> Int.List.mem i listind | _ -> false) rvec in Array.exists one_is_rec (dest_subterms rarg) @@ -275,7 +275,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | Some (Some _) -> mib.mind_finite == BiFinite | _ -> true (* Annotation for cases *) @@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches = if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" - Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in let n, subst = List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) + ctx (0, []) in Vars.substl subst br (* substitution in a signature *) @@ -486,7 +486,7 @@ let find_inductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found @@ -496,7 +496,7 @@ let find_coinductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found @@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign = let pv' = whd_all env sigma pval in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> - srec (push_rel_assum (na, t) env) b arsign + srec (push_rel_assum (na, t) env) b arsign | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names - given by the tactics "case" and "inversion": when the - elimination is not dependent, "case" uses Anonymous for - inductive types in Prop and names created by mkProd_name for - inductive types in Set/Type while "inversion" uses anonymous - for inductive types both in Prop and Set/Type !! - - Previously, whether names were created or not relied on - whether the predicate created in Indrec.make_case_com had a - dependent arity or not. To avoid different predicates - printed the same in v8, all predicates built in indrec.ml - got a dependent arity (Aug 2004). The new way to decide - whether names have to be created or not is to use an - Anonymous or Named variable to enforce the expected - dependency status (of course, Anonymous implies non - dependent, but not conversely). + given by the tactics "case" and "inversion": when the + elimination is not dependent, "case" uses Anonymous for + inductive types in Prop and names created by mkProd_name for + inductive types in Set/Type while "inversion" uses anonymous + for inductive types both in Prop and Set/Type !! + + Previously, whether names were created or not relied on + whether the predicate created in Indrec.make_case_com had a + dependent arity or not. To avoid different predicates + printed the same in v8, all predicates built in indrec.ml + got a dependent arity (Aug 2004). The new way to decide + whether names have to be created or not is to use an + Anonymous or Named variable to enforce the expected + dependency status (of course, Anonymous implies non + dependent, but not conversely). From Coq > 8.2, using or not the the effective dependency of the predicate is parametrable! *) @@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function let ctx,_ = Reduction.dest_arity env ty in let u = Univ.Universe.make l in let s = - (* Does the sort of parameter [u] appear in (or equal) + (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) if univ_level_mem l is then scl (* constrained sort: replace by scl *) else (* unconstrained sort: replace by fresh universe *) let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in - let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in - evdref := evm; s + let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in + evdref := evm; s in (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp) | sign, [] -> sign (* Uniform parameters are exhausted *) @@ -656,93 +656,3 @@ 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 : 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 58b1ce6c3f..55149552aa 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,12 +199,3 @@ 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 -> -(constr -> constr) -> -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/inferCumulativity.ml b/pretyping/inferCumulativity.ml new file mode 100644 index 0000000000..a4097237ff --- /dev/null +++ b/pretyping/inferCumulativity.ml @@ -0,0 +1,208 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +open Reduction +open Declarations +open Constr +open Univ +open Util + +(** Throughout this module we modify a map [variances] from local + universes to [Variance.t]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. *) + +let infer_level_eq u variances = + if LMap.mem u variances + then LMap.set u Variance.Invariant variances + else variances + +let infer_level_leq u variances = + match LMap.find u variances with + | exception Not_found -> variances + | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let variance_pb cv_pb var = + let open Variance in + match cv_pb, var with + | _, Irrelevant -> Irrelevant + | _, Invariant -> Invariant + | CONV, Covariant -> Invariant + | CUMUL, Covariant -> Covariant + +let infer_cumulative_ind_instance cv_pb cumi variances u = + Array.fold_left2 (fun variances varu u -> + match LMap.find u variances with + | exception Not_found -> variances + | varu' -> + LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) + variances (ACumulativityInfo.variance cumi) (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb cumi variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance CONV cumi variances u + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key infos variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let open CClosure in + let hd,stk = whd_stack infos hd stk in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> variances + | FFlex fl -> + let variances = infer_table_key infos variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances codom [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env infos) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env infos) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (ci,p,br,e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let infos = create_clos_infos all env in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor is_arity env variances arcn = + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, infer_term CUMUL env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let typs, codom = Reduction.dest_prod env arcn in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then infer_term CUMUL env variances codom else variances + +let infer_inductive env mie = + let open Entries in + let { mind_entry_params = params; + mind_entry_inds = entries; } = mie + in + let univs = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ + | Polymorphic_ind_entry _ as univs -> univs + | Cumulative_ind_entry cumi -> + let uctx = CumulativityInfo.univ_context cumi in + let uarray = Instance.to_array @@ UContext.instance uctx in + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) + LMap.empty uarray + in + let env, _ = Typeops.infer_local_decls env params in + let variances = List.fold_left (fun variances entry -> + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity + in + List.fold_left (infer_arity_constructor false env) + variances entry.mind_entry_lc) + variances + entries + in + let variances = Array.map (fun u -> LMap.find u variances) uarray in + Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + in + { mie with mind_entry_universes = univs } diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli new file mode 100644 index 0000000000..a5037ea475 --- /dev/null +++ b/pretyping/inferCumulativity.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index bc563b46dc..f0cb8fd1f2 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,8 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index dafe8cb269..b41e15f5a6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -224,7 +224,7 @@ and nf_accu env sigma accu = if Int.equal (accu_nargs accu) 0 then nf_atom env sigma atom else let a,typ = nf_atom_type env sigma atom in - let _, args = nf_args env sigma accu typ in + let _, args = nf_args env sigma (args_of_accu accu) typ in mkApp(a,Array.of_list args) and nf_accu_type env sigma accu = @@ -232,10 +232,10 @@ and nf_accu_type env sigma accu = if Int.equal (accu_nargs accu) 0 then nf_atom_type env sigma atom else let a,typ = nf_atom_type env sigma atom in - let t, args = nf_args env sigma accu typ in + let t, args = nf_args env sigma (args_of_accu accu) typ in mkApp(a,Array.of_list args), t -and nf_args env sigma accu t = +and nf_args env sigma args t = let aux arg (t,l) = let _,dom,codom = try decompose_prod env t with @@ -246,7 +246,7 @@ and nf_args env sigma accu t = let c = nf_val env sigma arg dom in (subst1 c codom, c::l) in - let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in + let t,l = Array.fold_right aux args (t,[]) in t, List.rev l and nf_bargs env sigma b t = @@ -277,7 +277,6 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aevar (ev,_) -> mkEvar ev | Aproj(p,c) -> let c = nf_accu env sigma c in mkProj(Projection.make p true,c) @@ -347,9 +346,9 @@ and nf_atom_type env sigma atom = let env = push_rel (LocalAssum (n,dom)) env in let codom,s2 = nf_type_sort env sigma (codom vn) in mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2 - | Aevar(ev,ty) -> - let ty = nf_type env sigma ty in - mkEvar ev, ty + | Aevar(evk,ty,args) -> + let ty = nf_type env sigma ty in + nf_evar env sigma evk ty args | Ameta(mv,ty) -> let ty = nf_type env sigma ty in mkMeta mv, ty @@ -386,6 +385,19 @@ and nf_predicate env sigma ind mip params v pT = true, mkLambda(name,dom,body) | _, _ -> false, nf_type env sigma v +and nf_evar env sigma evk ty args = + let evi = try Evd.find sigma evk with Not_found -> assert false in + let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in + if List.is_empty hyps then begin + assert (Int.equal (Array.length args) 0); + mkEvar (evk, [||]), ty + end + else + let fold accu d = Term.mkNamedProd_or_LetIn d accu in + let t = List.fold_left fold ty hyps in + let ty, args = nf_args env sigma args t in + mkEvar (evk, Array.of_list args), ty + let evars_of_evar_map sigma = { Nativelambda.evars_val = Evd.existential_opt_value sigma; Nativelambda.evars_typ = Evd.existential_type sigma; @@ -436,11 +448,11 @@ 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 - if Coq_config.no_native_compiler then + if not Coq_config.native_compiler then user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 41e09004c6..1bec4a6f15 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -137,8 +137,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id - | PProj (p,c) -> ConstRef (Projection.constant p) - | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern @@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) + | GProj(p,c) -> + PProj(p, pat_of_raw metas vars c) + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> err ?loc (Pp.str "Non supported pattern.")) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 00c254dbe2..6700748ebc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -70,7 +70,7 @@ let get_extra env sigma = let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) - (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } let rel_context env = rel_context env.env @@ -90,12 +90,11 @@ let push_rel_context sigma ctx env = { let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = - let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in - let (subst, vsubst, _, nc) = Lazy.force env.extra in - let typ' = subst2 subst vsubst typ in + let (subst, _, nc) = Lazy.force env.extra in + let typ' = csubst_subst subst typ in let instance = inst_rels @ inst_vars in let sign = val_of_named_context nc in let sigma = !evdref in @@ -177,61 +176,77 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd id = + +let interp_known_universe_level evd r = + let loc, qid = Libnames.qualid_of_reference r in try - let level = Evd.universe_of_name evd id in - level + match r with + | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id + | Libnames.Qualid _ -> raise Not_found with Not_found -> - let names, _ = Global.global_universe_names () in - snd (Id.Map.find id names) - -let interp_universe_level_name ~anon_rigidity evd (loc, s) = - match s with - | Anonymous -> - new_univ_level_variable ?loc anon_rigidity evd - | Name id -> - let s = Id.to_string id in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try evd, interp_known_universe_level evd id - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:id univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + let univ, k = Nametab.locate_universe qid in + Univ.Level.make univ k + +let interp_universe_level_name ~anon_rigidity evd r = + try evd, interp_known_universe_level evd r + with Not_found -> + match r with (* Qualified generated name *) + | Libnames.Qualid (loc, qid) -> + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + | Libnames.Ident (loc, id) -> (* Undeclared *) + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> - List.fold_left (fun (evd, u) l -> - (* [univ_flexible_alg] can produce algebraic universes in terms *) - let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in - (evd', Univ.sup u (Univ.Universe.make l))) + List.fold_left (fun (evd, u) l -> + let evd', u' = + match l with + | Some (l,n) -> + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + let u' = Univ.Universe.make l in + (match n with + | 0 -> evd', u' + | 1 -> evd', Univ.Universe.super u' + | _ -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n))) + | None -> + let evd, l = new_univ_level_variable ?loc univ_flexible evd in + evd, Univ.Universe.make l + in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l let interp_known_level_info ?loc evd = function - | None | Some (_, Anonymous) -> + | UUnknown | UAnonymous -> user_err ?loc ~hdr:"interp_known_level_info" (str "Anonymous universes not allowed here.") - | Some (loc, Name id) -> - try interp_known_universe_level evd id + | UNamed ref -> + try interp_known_universe_level evd ref with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id) + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) let interp_level_info ?loc evd : Misctypes.level_info -> _ = function - | None -> new_univ_level_variable ?loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) + | UUnknown -> new_univ_level_variable ?loc univ_rigid evd + | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd + | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr @@ -363,10 +378,10 @@ let check_evars_are_solved env current_sigma init_sigma = let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in check_evars_are_solved env current_sigma frozen -let process_inference_flags flags env initial_sigma (sigma,c) = +let process_inference_flags flags env initial_sigma (sigma,c,cty) = let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in - sigma,c + sigma,c,cty let adjust_evar_source evdref na c = match na, kind !evdref c with @@ -722,6 +737,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_sort ?loc evdref s in inh_conv_coerce_to_tycon ?loc env evdref j tycon + | GProj (p, c) -> + (* TODO: once GProj is used as an input syntax, use bidirectional typing here *) + let cj = pretype empty_tycon env evdref lvar c in + judge_of_projection env.ExtraEnv.env !evdref p cj + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in @@ -1153,15 +1173,18 @@ let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in - let c' = match kind with + let c', c'_ty = match kind with | WithoutTypeConstraint -> - (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in + j.uj_val, j.uj_type | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in + j.uj_val, j.uj_type | IsType -> - (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val + let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in + tj.utj_val, mkSort tj.utj_type in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty) let default_inference_flags fail = { use_typeclasses = true; @@ -1181,7 +1204,7 @@ let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false 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, c, _ = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd @@ -1193,12 +1216,15 @@ let understand env sigma c = ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c -let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = - let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in - (sigma, c) +let understand_tcc_ty ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = + ise_pretype_gen flags env sigma empty_lvar expected_type c + +let understand_tcc ?flags env sigma ?expected_type c = + let sigma, c, _ = understand_tcc_ty ?flags env sigma ?expected_type c in + sigma, c let understand_ltac flags env sigma lvar kind c = - let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in + let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) let pretype k0 resolve_tc typcon env evdref lvar t = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index fe10be9e7c..864768fe56 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -58,6 +58,11 @@ val all_and_fail_flags : inference_flags val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr +(** As [understand_tcc] but also returns the type of the elaborated term. + The [expand_evars] flag is not applied to the type (only to the term). *) +val understand_tcc_ty : ?flags:inference_flags -> env -> evar_map -> + ?expected_type:typing_constraint -> glob_constr -> evar_map * constr * types + (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr @@ -116,7 +121,7 @@ val pretype_type : val ise_pretype_gen : inference_flags -> env -> evar_map -> - ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types (**/**) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 1da5b4567f..ae4ad0be7d 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,6 +4,7 @@ Locusops Pretype_errors Reductionops Inductiveops +InferCumulativity Vnorm Arguments_renaming Nativenorm diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 9ff9a75b3e..ab1f3cd320 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -298,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) (*s High-level declaration of a canonical structure *) -let error_not_structure ref = +let error_not_structure ref description = user_err ~hdr:"object_declare" - (Id.print (basename_of_global ref) ++ str" is not a structure object.") + (str"Could not declare a canonical structure " ++ + (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + str(description))) let check_and_decompose_canonical_structure ref = - let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in + let sp = + match ref with + ConstRef sp -> sp + | _ -> error_not_structure ref "Expected an instance of a record or structure." + in let env = Global.env () 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 + | None -> error_not_structure ref "Could not find its value in the global environment." in let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args - | _ -> error_not_structure ref in + | _ -> + error_not_structure ref "Expected a record or structure constructor applied to arguments." in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref in - let s = try lookup_structure indsp with Not_found -> error_not_structure ref in + | _ -> error_not_structure ref "Expected an instance of a record or structure." in + let s = + try lookup_structure indsp + with Not_found -> + error_not_structure ref + ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref; + error_not_structure ref "Got too few arguments to the record or structure constructor."; (sp,indsp) let declare_canonical_structure ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ba0502ca45..418ea271cd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -121,10 +121,10 @@ module ReductionBehaviour = struct let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) let discharge = function - | _,(ReqGlobal (ConstRef c, req), (_, b)) -> + | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) -> let b = - if Lib.is_in_section (ConstRef c) then - let vars, _, _ = Lib.section_segment_of_constant c in + if Lib.is_in_section gr then + let vars = Lib.variable_section_segment_of_reference gr in let extra = List.length vars in let nargs' = if b.b_nargs = max_int then max_int @@ -284,8 +284,6 @@ sig | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list exception IncompatibleFold2 @@ -296,12 +294,12 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) - val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool) - -> 'a t -> 'a t -> (int * int) option + val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool) + -> 'a t -> 'a t -> bool val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val append_app_list : 'a list -> 'a t -> 'a t val strip_app : 'a t -> 'a t * 'a t val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -343,8 +341,6 @@ struct | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list let rec pr_member pr_c member = @@ -367,8 +363,6 @@ struct ++ pr_comma () ++ prlist_with_sep pr_semicolon int remains ++ pr_comma () ++ pr pr_c params ++ str ")" - | Shift i -> str "ZShift(" ++ int i ++ str ")" - | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l @@ -403,54 +397,42 @@ struct else (l.(j), sk) let equal f f_fix sk1 sk2 = - let equal_cst_member x lft1 y lft2 = + let equal_cst_member x y = match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + Constant.equal (Projection.constant p1) (Projection.constant p2) | _, _ -> false in - let rec equal_rec sk1 lft1 sk2 lft2 = + let rec equal_rec sk1 sk2 = match sk1,sk2 with - | [],[] -> Some (lft1,lft2) - | (Update _ :: _, _ | _, Update _ :: _) -> assert false - | Shift k :: s1, _ -> equal_rec s1 (lft1+k) sk2 lft2 - | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k) + | [],[] -> true | App a1 :: s1, App a2 :: s2 -> - let t1,s1' = decomp_node_last a1 s1 in - let t2,s2' = decomp_node_last a2 s2 in - if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None + let t1,s1' = decomp_node_last a1 s1 in + let t2,s2' = decomp_node_last a2 s2 in + (f t1 t2) && (equal_rec s1' s2') | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> - if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2 - then equal_rec s1 lft1 s2 lft2 - else None + f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> - if Int.equal n1 n2 && Int.equal m1 m2 - && Constant.equal (Projection.constant p) (Projection.constant p2) - then equal_rec s1 lft1 s2 lft2 - else None + Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) + && equal_rec s1 s2 | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> - if f_fix (f1,lft1) (f2,lft2) then - match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with - | None -> None - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - else None + f_fix f1 f2 + && equal_rec (List.rev s1) (List.rev s2) + && equal_rec s1' s2' | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> - if equal_cst_member c1 lft1 c2 lft2 then - match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - | None -> None - else None - | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None - in equal_rec (List.rev sk1) 0 (List.rev sk2) 0 + equal_cst_member c1 c2 + && equal_rec (List.rev params1) (List.rev params2) + && equal_rec s1' s2' + | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false + in equal_rec (List.rev sk1) (List.rev sk2) let compare_shape stk1 stk2 = let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with ([],[]) -> Int.equal bal 0 - | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2 - | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> @@ -466,40 +448,29 @@ struct exception IncompatibleFold2 let fold2 f o sk1 sk2 = - let rec aux o lft1 sk1 lft2 sk2 = - let fold_array = - Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y)) - in + let rec aux o sk1 sk2 = match sk1,sk2 with - | [], [] -> o,lft1,lft2 - | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2 - | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2 + | [], [] -> o | App n1 :: q1, App n2 :: q2 -> - let t1,l1 = decomp_node_last n1 q1 in - let t2,l2 = decomp_node_last n2 q2 in - aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - lft1 l1 lft2 l2 + let t1,l1 = decomp_node_last n1 q1 in + let t2,l2 = decomp_node_last n2 q2 in + aux (f o t1 t2) l1 l2 | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> - aux (fold_array - (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - a1 a2) lft1 q1 lft2 q2 + aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> - aux o lft1 q1 lft2 q2 + aux o q1 q2 | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> - let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2) - lft1 (List.rev s1) lft2 (List.rev s2) in - aux o' lft1' q1 lft2' q2 + let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in + aux o' q1 q2 | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> - let (o',lft1',lft2') = - aux o lft1 (List.rev params1) lft2 (List.rev params2) - in aux o' lft1' q1 lft2' q2 - | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> - raise IncompatibleFold2 - in aux o 0 (List.rev sk1) 0 (List.rev sk2) + let o' = aux o (List.rev params1) (List.rev params2) in + aux o' q1 q2 + | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + raise IncompatibleFold2 + in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function - | Update _ -> assert false - | (Proj (_,_,_,_) | Shift _) as e -> e + | (Proj (_,_,_,_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -516,18 +487,15 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | Shift(_)::s -> args_size s - | Update(_)::s -> args_size s | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 let strip_app s = let rec aux out = function - | ( App _ | Shift _ as e) :: s -> aux (e :: out) s + | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s let strip_n_app n s = let rec aux n out = function - | Shift k as e :: s -> aux n (e :: out) s | App (i,a,j) as e :: s -> let nb = j - i + 1 in if n >= nb then @@ -552,14 +520,12 @@ struct let list_of_app_stack s = let rec aux = function | App (i,a,j) :: s -> - let (k,(args',s')) = aux s in - let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in - k,(Array.fold_right (fun x y -> x::y) a' args', s') - | Shift n :: s -> - let (k,(args',s')) = aux s in (k+n,(args', s')) - | s -> (0,([],s)) in - let (lft,(out,s')) = aux s in - let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in + let (args',s') = aux s in + let a' = Array.sub a i (j - i + 1) in + (Array.fold_right (fun x y -> x::y) a' args', s') + | s -> ([],s) in + let (out,s') = aux s in + let init = match s' with [] -> true | _ -> false in Option.init init out let assign s p c = @@ -568,20 +534,18 @@ struct | None -> assert false let tail n0 s0 = - let rec aux lft n s = - let out s = if Int.equal lft 0 then s else Shift lft :: s in - if Int.equal n 0 then out s else + let rec aux n s = + if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> let nb = j - i + 1 in if n >= nb then - aux lft (n - nb) s + aux (n - nb) s else let p = i+n in if j >= p then App(p,a,j)::s else s - | Shift k :: s' -> aux (lft+k) n s' | _ -> raise (Invalid_argument "Reductionops.Stack.tail") - in aux 0 n0 s0 + in aux n0 s0 let nth s p = match strip_n_app p s with @@ -627,11 +591,9 @@ struct zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Shift n::s) -> zip (lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) - | _, (Update _::_) -> assert false in zip s @@ -868,11 +830,9 @@ let _ = Goptions.declare_bool_option { } let equal_stacks sigma (x, l) (y, l') = - let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in - let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in - match Stack.equal f_equal eq_fix l l' with - | None -> false - | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) + let f_equal x y = eq_constr sigma x y in + let eq_fix a b = f_equal (mkFix a) (mkFix b) in + Stack.equal f_equal eq_fix l l' && f_equal x y let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in @@ -1074,7 +1034,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg, Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end - |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1155,7 +1115,7 @@ let local_whd_state_gen flags sigma = |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) - |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1281,9 +1241,9 @@ let clos_whd_flags flgs env sigma t = (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") -let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) -let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) -let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) +let nf_beta = clos_norm_flags CClosure.beta +let nf_betaiota = clos_norm_flags CClosure.betaiota +let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta let nf_all env sigma = clos_norm_flags CClosure.all env sigma @@ -1292,11 +1252,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = @@ -1306,7 +1266,7 @@ let is_transparent e k = (* Conversion utility functions *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t let pb_is_equal pb = pb == Reduction.CONV @@ -1364,79 +1324,17 @@ 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_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = - { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances; - Reduction.conv_inductives = sigma_conv_inductives; - Reduction.conv_constructors = sigma_conv_constructors} + let open Reduction in + { compare_sorts = sigma_compare_sorts; + compare_instances = sigma_compare_instances; + compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = @@ -1685,7 +1583,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' - |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' + |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index db0c29aeff..0565baf45f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -82,8 +82,6 @@ module Stack : sig | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list val pr : ('a -> Pp.t) -> 'a t -> Pp.t @@ -102,12 +100,12 @@ module Stack : sig @return the result and the lifts to apply on the terms @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *) val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App or Shift *) + start by App *) val strip_app : 'a t -> 'a t * 'a t (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -170,9 +168,9 @@ val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) -val nf_beta : local_reduction_function -val nf_betaiota : local_reduction_function -val nf_betaiotazeta : local_reduction_function +val nf_beta : reduction_function +val nf_betaiota : reduction_function +val nf_betaiotazeta : reduction_function val nf_all : reduction_function val nf_evar : evar_map -> constr -> constr @@ -262,7 +260,7 @@ val is_transparent : Environ.env -> Constant.t tableKey -> bool (** {6 Conversion Functions (uses closures, lazy strategy) } *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5dd6879d39..00b175c486 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -166,23 +166,6 @@ let retype ?(polyprop=true) sigma = | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> decomp_sort env sigma (type_of env t) - and sort_family_of env t = - match EConstr.kind sigma t with - | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) - | Sort _ -> InType - | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in - if not (is_impredicative_set env) && - s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> - let t = type_of_global_reference_knowing_parameters env f args in - Sorts.family (sort_of_atomic_type env sigma t args) - | App(f,args) -> - Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) - | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> - Sorts.family (decomp_sort env sigma (type_of env t)) - and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in @@ -198,15 +181,34 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (type_of_constructor env (cstr, u)) | _ -> assert false - in type_of, sort_of, sort_family_of, - type_of_global_reference_knowing_parameters + in type_of, sort_of, type_of_global_reference_knowing_parameters + +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = + let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in + let rec sort_family_of env t = + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) + | Sort _ -> InType + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in + if not (is_impredicative_set env) && + s2 == InSet && sort_family_of env t == InType then InType else s2 + | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else + let t = type_of_global_reference_knowing_parameters env f args in + Sorts.family (sort_of_atomic_type env sigma t args) + | App(f,args) -> + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) + | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | _ -> + Sorts.family (decomp_sort env sigma (type_of env t)) + in sort_family_of env t let get_sort_of ?(polyprop=true) env sigma t = - let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t -let get_sort_family_of ?(polyprop=true) env sigma c = - let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c + let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with @@ -225,14 +227,14 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = - let f,_,_,_ = retype ~polyprop sigma in + let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index af86df499c..6fdde90463 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -31,8 +31,11 @@ val get_type_of : val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> Sorts.family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 85383ba398..9b9408698d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u = match evref with | EvalConstRef con -> let u = Unsafe.to_instance u in - EConstr.of_constr (try constant_value_in env (con,u) - with NotEvaluableConst IsProj -> - raise (Invalid_argument "value_of_evaluable_ref")) + EConstr.of_constr (constant_value_in env (con, u)) | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function @@ -476,7 +474,7 @@ let contract_fix_use_function env sigma f let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = List.init nbodies make_Fi in - substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum)) + substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) let reduce_fix_use_function env sigma f whfun fix stack = match fix_recarg fix (Stack.append_app_list stack Stack.empty) with @@ -500,7 +498,7 @@ let contract_cofix_use_function env sigma f let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev subbodies) - sigma (nf_beta sigma bodies.(bodynum)) + sigma (nf_beta env sigma bodies.(bodynum)) let reduce_mind_case_use_function func env sigma mia = match EConstr.kind sigma mia.mconstr with @@ -697,7 +695,7 @@ let rec red_elim_const env sigma ref u largs = let whfun = whd_construct_stack env sigma in (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase) + | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> let rec descend (ref,u) args = let c = reference_value env sigma ref u in @@ -712,7 +710,7 @@ let rec red_elim_const env sigma ref u largs = let whfun = whd_construct_stack env sigma in (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase) + | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | NotAnElimination when unfold_nonelim -> let c = reference_value env sigma ref u in (whd_betaiotazeta sigma (applist (c, largs)), []), nocase @@ -927,8 +925,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a @@ -1103,7 +1101,7 @@ let unfoldoccs env sigma (occs,name) c = | [] -> () | _ -> error_invalid_occurrence rest in - nf_betaiotazeta sigma uc + nf_betaiotazeta env sigma uc in match occs with | NoOccurrences -> c @@ -1284,7 +1282,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = else raise Not_found with Not_found -> try - let t' = nf_betaiota sigma (one_step_reduce env sigma t) in + let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in elimrec env t' l with NotStepReducible -> error_cannot_recognize ref in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2e213a51d7..3f947fd23f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -65,7 +65,7 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + cl_context : global_reference option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -87,7 +87,6 @@ type instance = { (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_poly: bool; is_impl: global_reference; } @@ -97,7 +96,7 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl info glob poly impl = +let new_instance cl info glob impl = let global = if glob then Some (Lib.sections_depth ()) else None @@ -107,7 +106,6 @@ let new_instance cl info glob poly impl = { is_class = cl.cl_impl; is_info = info ; is_global = global ; - is_poly = poly; is_impl = impl } (* @@ -175,7 +173,7 @@ let subst_class (subst,cl) = and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + List.smartmap (Option.smartmap do_subst_gr) grs, 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 @@ -213,15 +211,16 @@ let discharge_class (_,cl) = let newgrs = List.map (fun decl -> match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None - | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + List.smartmap (Option.smartmap Lib.discharge_global) grs @ newgrs 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, _, _ as info = abs_context cl in + let info = abs_context cl in + let ctx = info.Lib.abstr_ctx in let ctx, subst = rel_of_variable_context ctx 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 @@ -420,7 +419,7 @@ let declare_instance info local glob = 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) + add_instance (new_instance tc info (not local) glob) | None -> () let add_class cl = @@ -442,19 +441,20 @@ let add_class cl = let instance_constructor (cl,u) args = let lenpars = List.count is_local_assum (snd cl.cl_context) in + let open EConstr in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> let ind = ind, u in - (Some (applistc (mkConstructUi (ind, 1)) args), - applistc (mkIndU ind) pars) + (Some (applist (mkConstructUi (ind, 1), args)), + applist (mkIndU ind, pars)) | ConstRef cst -> let cst = cst, u in let term = match args with | [] -> None | _ -> Some (List.last args) in - (term, applistc (mkConstU cst) pars) + (term, applist (mkConstU cst, pars)) | _ -> assert false let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes [] @@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 618826f3d0..ee28ec173b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,9 +25,8 @@ type typeclass = { cl_impl : global_reference; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. - The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + The global reference gives a direct link to the class itself. *) + cl_context : global_reference option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -54,7 +53,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -83,8 +82,8 @@ val is_instance : global_reference -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) -val instance_constructor : typeclass Univ.puniverses -> constr list -> - constr option * types +val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> + EConstr.t option * EConstr.t (** Filter which evars to consider for resolution. *) type evar_filter = Evar.t -> Evar_kinds.t -> bool diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 43066c8099..3132d2ad53 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -23,11 +23,6 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration -let push_rec_types pfix env = - let (i, c, t) = pfix in - let inj c = EConstr.Unsafe.to_constr c in - push_rec_types (i, Array.map inj c, Array.map inj t) env - let meta_type evd mv = let ty = try Evd.meta_ftype evd mv diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 9f084ae8df..153a48a710 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 84ffab4260..e1720ec955 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module CVars = Vars - open CErrors open Pp open Util @@ -196,7 +194,7 @@ let pose_all_metas_as_evars env evd t = let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let ty = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld - then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) + then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar env evdref ~src ty in @@ -666,7 +664,7 @@ let is_eta_constructor_app env sigma ts f l1 term = | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term @@ -1077,13 +1075,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e in try let opt' = {opt with with_types = false} in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in + let substn = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) unirec_rec curenvnb pb opt' substn c1 app @@ -1279,7 +1277,7 @@ let w_coerce env evd mv c = let unify_to_type env sigma flags c status u = let sigma, c = refresh_universes (Some false) env sigma c in let t = get_type_of env sigma (nf_meta sigma c) in - let t = nf_betaiota sigma (nf_meta sigma t) in + let t = nf_betaiota env sigma (nf_meta sigma t) in unify_0 env sigma CUMUL flags t u let unify_type env sigma flags mv status c = @@ -1527,7 +1525,7 @@ let indirectly_dependent sigma c d decls = let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1617,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | Some (sigma,_,l) -> let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) let make_eq_test env evd c = let out cstr = @@ -2015,8 +2013,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b5b8987e33..c93b41786b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -15,6 +15,7 @@ open Vars open Environ open Inductive open Reduction +open Vmvalues open Vm open Context.Rel.Declaration @@ -134,7 +135,7 @@ let build_case_type dep p realargs c = (* La fonction de normalisation *) -let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t +let rec nf_val env sigma v t = nf_whd env sigma (Vmvalues.whd_val v) t and nf_vtype env sigma v = nf_val env sigma v crazy_type @@ -144,7 +145,7 @@ and nf_whd env sigma whd typ = | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in - let vc = body_of_vfun (nb_rel env) (codom p) in + let vc = reduce_fun (nb_rel env) (codom p) in let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in mkProd(name,dom,codom) | Vfun f -> nf_fun env sigma f typ @@ -191,7 +192,7 @@ and nf_univ_args ~nb_univs mk env sigma stk = else match stk with | Zapp args :: _ -> let inst = - Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i)) + Array.init nb_univs (fun i -> uni_lvl_val (arg args i)) in Univ.Instance.of_array inst | _ -> assert false @@ -239,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) @@ -254,7 +256,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in - let ci = case_info sw in + let ci = sw.sw_annot.Cbytecodes.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -266,14 +268,14 @@ and nf_predicate env sigma ind mip params v pT = match whd_val v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) | Vfun f, _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in @@ -307,7 +309,7 @@ and nf_bargs env sigma b ofs t = and nf_fun env sigma f typ = let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = try decompose_prod env typ with DestKO -> @@ -365,4 +367,4 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) ~catch_incon:true ~pb env sigma t1 t2 -let _ = Reductionops.set_vm_infer_conv vm_infer_conv +let _ = if Coq_config.bytecode_compiler then Reductionops.set_vm_infer_conv vm_infer_conv |