diff options
Diffstat (limited to 'interp')
38 files changed, 844 insertions, 1762 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 7a14a4e708..49b9149675 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -10,7 +10,6 @@ open Names open Libnames -open Decl_kinds (** {6 Concrete syntax for terms } *) @@ -39,9 +38,9 @@ type explicitation = | ExplByName of Id.t type binder_kind = - | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool - (** Inner binding, outer bindings, typeclass-specific flag + | Default of Glob_term.binding_kind + | Generalized of Glob_term.binding_kind * bool + (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses *) type abstraction_kind = AbsLambda | AbsPi @@ -121,7 +120,7 @@ and constr_expr_r = | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation * constr_notation_substitution - | CGeneralization of binding_kind * abstraction_kind option * constr_expr + | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr and constr_expr = constr_expr_r CAst.t @@ -134,16 +133,17 @@ and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - lident * (lident option * recursion_order_expr) * + lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr and cofix_expr = lident * local_binder_expr list * constr_expr * constr_expr -and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) +and recursion_order_expr_r = + | CStructRec of lident + | CWfRec of lident * constr_expr + | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *) +and recursion_order_expr = recursion_order_expr_r CAst.t (* Anonymous defs allowed ?? *) and local_binder_expr = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 60610b92b8..b4798127f9 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -17,25 +17,19 @@ open Namegen open Glob_term open Constrexpr open Notation -open Decl_kinds (***********************) (* For binders parsing *) -let binding_kind_eq bk1 bk2 = match bk1, bk2 with -| Explicit, Explicit -> true -| Implicit, Implicit -> true -| _ -> false - let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with | AbsLambda, AbsLambda -> true | AbsPi, AbsPi -> true | _ -> false let binder_kind_eq b1 b2 = match b1, b2 with -| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 -| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> - binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 && +| Default bk1, Default bk2 -> Glob_ops.binding_kind_eq bk1 bk2 +| Generalized (ck1, b1), Generalized (ck2, b2) -> + Glob_ops.binding_kind_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false @@ -172,7 +166,7 @@ let rec constr_expr_eq e1 e2 = | CPrim i1, CPrim i2 -> prim_token_eq i1 i2 | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) -> - binding_kind_eq bk1 bk2 && + Glob_ops.binding_kind_eq bk1 bk2 && Option.equal abstraction_kind_eq ak1 ak2 && constr_expr_eq e1 e2 | CDelimiters(s1,e1), CDelimiters(s2,e2) -> @@ -196,10 +190,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 -and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = +and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = (eq_ast Id.equal id1 id2) && - Option.equal (eq_ast Id.equal) j1 j2 && - recursion_order_expr_eq r1 r2 && + Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -210,13 +203,17 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq a1 a2 && constr_expr_eq b1 b2 -and recursion_order_expr_eq r1 r2 = match r1, r2 with - | CStructRec, CStructRec -> true - | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 - | CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> +and recursion_order_expr_eq_r r1 r2 = match r1, r2 with + | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CWfRec (i1,e1), CWfRec (i2,e2) -> + constr_expr_eq e1 e2 + | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> + Option.equal (eq_ast Id.equal) i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false +and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 + and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 @@ -349,7 +346,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> + List.fold_right (fun (_,ro,lb,t,c) acc -> fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> @@ -628,7 +625,8 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open UState in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env) + (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f1a8ed202f..a05a9cb999 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -26,9 +26,6 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool val local_binder_eq : local_binder_expr -> local_binder_expr -> bool (** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *) -val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool -(** Equality on [binding_kind] *) - val binder_kind_eq : binder_kind -> binder_kind -> bool (** Equality on [binder_kind] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 24b1362e6d..217381d854 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -16,7 +16,6 @@ open Names open Nameops open Termops open Libnames -open Globnames open Namegen open Impargs open CAst @@ -28,7 +27,6 @@ open Glob_ops open Pattern open Notation open Detyping -open Decl_kinds module NamedDecl = Context.Named.Declaration (*i*) @@ -67,7 +65,10 @@ let print_no_symbol = ref false (**********************************************************************) (* Turning notations and scopes on and off for printing *) -module IRuleSet = InterpRuleSet +module IRuleSet = Set.Make(struct + type t = interp_rule + let compare x y = compare x y + end) let inactive_notations_table = Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty) @@ -104,16 +105,16 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> - if not (exists_notation_interpretation_in_scope scopt ntn) then - user_err ~hdr:"Notation" + match availability_of_notation (scopt, ntn) (scopt, []) with + | None -> user_err ~hdr:"Notation" (pr_notation ntn ++ spc () ++ str "does not exist" ++ (match scopt with | None -> spc () ++ str "in the empty scope." | Some _ -> show_scope scopt ++ str ".")) - else + | Some _ -> if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () @@ -212,7 +213,7 @@ let encode_record r = module PrintingRecordRecord = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Record" let title = "Types leading to pretty-printing using record notation: " let member_message s b = @@ -224,7 +225,7 @@ module PrintingRecordRecord = module PrintingRecordConstructor = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Constructor" let title = "Types leading to pretty-printing using constructor form: " let member_message s b = @@ -260,11 +261,6 @@ let rec insert_pat_coercion ?loc l c = match l with | [] -> c | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) -let add_lonely keyrule seen = - match keyrule with - | NotationRule (None,ntn) -> ntn::seen - | SynDefRule _ | NotationRule (Some _,_) -> seen - (**********************************************************************) (* conversion of references *) @@ -289,11 +285,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -363,8 +359,8 @@ let mkPat ?loc qid l = CAst.make ?loc @@ if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l) let pattern_printable_in_both_syntax (ind,_ as c) = - let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in - let nb_params = Inductiveops.inductive_nparams ind in + let impl_st = extract_impargs_data (implicits_of_global (GlobRef.ConstructRef c)) in + let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in List.exists (fun (_,impls) -> (List.length impls >= nb_params) && let params,args = Util.List.chop nb_params impls in @@ -388,8 +384,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_pattern allscopes [] vars pat - (uninterp_cases_pattern_notations scopes pat) + extern_notation_pattern allscopes vars pat + (uninterp_cases_pattern_notations pat) with No_match -> let loc = pat.CAst.loc in match DAst.get pat with @@ -418,7 +414,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = (* we don't want to have 'x := _' in our patterns *) acc | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) + ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc) | _ -> raise No_match in ip q tail acc | _ -> assert false @@ -426,14 +422,14 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> - let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in + let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in - match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with + match drop_implicits_in_patt (GlobRef.ConstructRef cstrsp) 0 full_args with | Some true_args -> CPatCstr (c, None, true_args) | None -> CPatCstr (c, Some full_args, []) in @@ -442,15 +438,18 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = insert_pat_coercion coercion pat and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) - (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars = + (custom, (tmp_scope, scopes) as allscopes) vars = function - | NotationRule (sc,ntn),key,need_delim -> + | NotationRule (sc,ntn) -> begin match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - let key = if need_delim || List.mem ntn lonely_seen then key else None in - let scopt = match key with Some _ -> sc | _ -> None in + match availability_of_notation (sc,ntn) (tmp_scope,scopes) with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some (scopt,key) -> let scopes' = Option.List.cons scopt scopes in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -472,8 +471,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (insert_pat_delimiters ?loc (make_pat_notation ?loc ntn (l,ll) l2') key) end - | SynDefRule kn,key,need_delim -> - assert (key = None && need_delim = false); + | SynDefRule kn -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> @@ -491,54 +489,49 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) -and extern_notation_pattern allscopes lonely_seen vars t = function +and extern_notation_pattern allscopes vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule,key,need_delim)::rules -> + | (keyrule,pat,n as _rule)::rules -> try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in match DAst.get t with | PatCstr (cstr,args,na) -> let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in - let p = apply_notation_to_pattern ?loc (ConstructRef cstr) - (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars - (keyrule,key,need_delim) in + let p = apply_notation_to_pattern ?loc (GlobRef.ConstructRef cstr) + (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with - No_match -> - let lonely_seen = add_lonely keyrule lonely_seen in - extern_notation_pattern allscopes lonely_seen vars t rules + No_match -> extern_notation_pattern allscopes vars t rules -let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function +let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match - | (keyrule,pat,n as _rule,key,need_delim)::rules -> + | (keyrule,pat,n as _rule)::rules -> try if is_inactive_rule keyrule then raise No_match; - apply_notation_to_pattern (IndRef ind) - (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim) + apply_notation_to_pattern (GlobRef.IndRef ind) + (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with - No_match -> - let lonely_seen = add_lonely keyrule lonely_seen in - extern_notation_ind_pattern allscopes lonely_seen vars ind args rules + No_match -> extern_notation_ind_pattern allscopes vars ind args rules let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) - if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then - let c = extern_reference vars (IndRef ind) in + if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then + let c = extern_reference vars (GlobRef.IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes [] vars ind args - (uninterp_ind_pattern_notations scopes ind) + extern_notation_ind_pattern allscopes vars ind args + (uninterp_ind_pattern_notations ind) with No_match -> - let c = extern_reference vars (IndRef ind) in + let c = extern_reference vars (GlobRef.IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in - match drop_implicits_in_patt (IndRef ind) 0 args with + match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args) |None -> CAst.make @@ CPatCstr (c, Some args, []) @@ -738,6 +731,14 @@ let extern_optimal extern r r' = | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match +(* Helper function for safe and optimal printing of primitive tokens *) +(* such as those for Int63 *) +let extern_prim_token_delimiter_if_required n key_n scope_n scopes = + match availability_of_prim_token n scope_n scopes with + | Some None -> CPrim n + | None -> CDelimiters(key_n, CAst.make (CPrim n)) + | Some (Some key) -> CDelimiters(key, CAst.make (CPrim n)) + (**********************************************************************) (* mapping decl *) @@ -754,11 +755,10 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType _ as s when !print_universes -> s - | GType _ -> GType [] + (* In case we print a glob_constr w/o having passed through detyping *) + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed _ when not !print_universes -> UAnonymous {rigid=true} + | UNamed _ | UAnonymous _ as u -> u let extern_universes = function | Some _ as l when !print_universes -> l @@ -770,32 +770,32 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx (custom,scopes as allscopes) vars r = +let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token allscopes) r r' + extern_optimal (extern_possible_prim_token scopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal - (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r)) + (fun r -> extern_notation scopes vars r (uninterp_notations r)) r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with - | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us) + | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) | c -> - match availability_of_entry_coercion custom InConstrEntrySomeLevel with + match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - let scopes = (InConstrEntrySomeLevel, scopes) in + let scopes = (InConstrEntrySomeLevel, snd scopes) in let c = match c with (* The remaining cases are only for the constr entry *) @@ -807,7 +807,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> - extern_evar n (List.map (on_snd (extern false allscopes vars)) l) + extern_evar n (List.map (on_snd (extern false scopes vars)) l) | GPatVar kind -> if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else @@ -823,7 +823,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r = begin try if !Flags.raw_print then raise Exit; - let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in + let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in let struc = Recordops.lookup_structure (fst cstrsp) in if PrintingRecord.active (fst cstrsp) then () @@ -847,16 +847,16 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | Some c :: q -> match locs with | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") - | (_, false) :: locs' -> + | { Recordops.pk_true_proj = false } :: locs' -> (* we don't want to print locals *) ip q locs' args acc - | (_, true) :: locs' -> + | { Recordops.pk_true_proj = true } :: locs' -> match args with | [] -> raise No_match (* we give up since the constructor is not complete *) | (arg, scopes) :: tail -> let head = extern true scopes vars arg in - ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) + ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc) in CRecord (List.rev (ip projs locals args [])) with @@ -938,13 +938,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r = let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in - let n = - match fst nv.(i) with - | None -> None - | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) - in - let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, + let n = + match nv.(i) with + | None -> None + | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) + in + ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) @@ -967,8 +966,11 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, map_cast_type (extern_typ scopes vars) c') + | GInt i -> - CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i))) + extern_prim_token_delimiter_if_required + (Numeral (SPlus, NumTok.int (Uint63.to_string i))) + "int63" "int63_scope" (snd scopes) in insert_coercion coercion (CAst.make ?loc c) @@ -1068,9 +1070,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function +and extern_notation (custom,scopes as allscopes) vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule,key,need_delim)::rules -> + | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try if is_inactive_rule keyrule then raise No_match; @@ -1118,8 +1120,11 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - let key = if need_delim || List.mem ntn lonely_seen then key else None in - let scopt = match key with Some _ -> sc | None -> None in + match availability_of_notation (sc,ntn) scopes with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some (scopt,key) -> let scopes' = Option.List.cons scopt (snd scopes) in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -1155,16 +1160,7 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function let args = extern_args (extern true) vars args in CAst.make ?loc @@ explicitize false argsimpls (None,e) args with - No_match -> - let lonely_seen = add_lonely keyrule lonely_seen in - extern_notation allscopes lonely_seen vars t rules - -and extern_recursion_order scopes vars = function - GStructRec -> CStructRec - | GWfRec c -> CWfRec (extern true scopes vars c) - | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, - Option.map (extern true scopes vars) r) - + No_match -> extern_notation allscopes vars t rules let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c @@ -1240,7 +1236,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) - | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), + | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None), [glob_of_pat avoid env sigma c]) | PApp (f,args) -> GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args) @@ -1294,7 +1290,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with let v = Array.map3 (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) bl tl ln in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -1313,10 +1309,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) - | PSort Sorts.InSProp -> GSort GSProp - | PSort Sorts.InProp -> GSort GProp - | PSort Sorts.InSet -> GSort GSet - | PSort Sorts.InType -> GSort (GType []) + | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0]) + | PSort Sorts.InProp -> GSort (UNamed [GProp,0]) + | PSort Sorts.InSet -> GSort (UNamed [GSet,0]) + | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i let extern_constr_pattern env sigma pat = diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f09b316cd6..7b8b93377b 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 59feb46dc1..f2cb4ae5c7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -31,7 +31,6 @@ open Notation_term open Notation_ops open Notation open Inductiveops -open Decl_kinds open Context.Rel.Declaration (** constr_expr -> glob_constr translation: @@ -96,21 +95,6 @@ let is_global id = with Not_found -> false -let global_reference_of_reference qid = - locate_reference qid - -let global_reference id = - locate_reference (qualid_of_ident id) - -let construct_reference ctx id = - try - VarRef (let _ = Context.Named.lookup id ctx in id) - with Not_found -> - global_reference id - -let global_reference_in_absolute_module dir id = - Nametab.global_of_path (Libnames.make_path dir id) - (**********************************************************************) (* Internalization errors *) @@ -387,45 +371,51 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "a parameter of the inductive type; bound variables in " ++ strbrk "the type of a constructor shall use a different name.") -let push_name_env ?(global_level=false) ntnvars implargs env = +let pure_push_name_env (id,implargs) env = + {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + +let push_name_env ntnvars implargs env = let open CAst in function | { loc; v = Anonymous } -> - if global_level then - user_err ?loc (str "Anonymous variables not allowed"); env | { loc; v = Name id } -> check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; - if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var" - else Dumpglob.dump_binding ?loc id; - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + Dumpglob.dump_binding ?loc id; + pure_push_name_env (id,implargs) env + +let remember_binders_impargs env bl = + List.map_filter (fun (na,_,_,_) -> + match na with + | Anonymous -> None + | Name id -> Some (id,Id.Map.find id env.impls)) bl + +let restore_binders_impargs env l = + List.fold_right pure_push_name_env l env -let intern_generalized_binder ?(global_level=false) intern_type ntnvars - env {loc;v=na} b b' t ty = +let intern_generalized_binder intern_type ntnvars + env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty + if t then ty, ids + else Implicit_quantifiers.implicit_application ids ty in let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in let env' = List.fold_left - (fun env {loc;v=x} -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) + (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) + (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with | Anonymous -> - if global_level then na - else - let name = + let name = let id = match ty with | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> @@ -434,7 +424,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl + in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl let intern_assumption intern ntnvars env nal bk ty = let intern_type env = intern (set_type_scope env) in @@ -448,8 +438,8 @@ let intern_assumption intern ntnvars env nal bk ty = (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in + | Generalized (b',t) -> + let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in env, b let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function @@ -485,7 +475,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = let na = make ?loc @@ Name id in env,((disjpat,il),id),na -let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function +let intern_local_binder_aux intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern ntnvars env nal bk ty in let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in @@ -656,9 +646,9 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (GlobRef.ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in - let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in + let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> @@ -753,7 +743,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) + | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.fold mk_env terms Id.Map.empty in @@ -815,7 +805,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat + | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try @@ -958,16 +948,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a goal or section variable *) let _ = Environ.lookup_named_ctxt id namedctx in try - (* [id] a section variable *) - (* Redundant: could be done in intern_qualid *) - let ref = VarRef id in - let impls = implicits_of_global ref in - let scopes = find_arguments_scope ref in - Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - DAst.make ?loc @@ GRef (ref, us), impls, scopes, [] + (* [id] a section variable *) + (* Redundant: could be done in intern_qualid *) + let ref = GlobRef.VarRef id in + let impls = implicits_of_global ref in + let scopes = find_arguments_scope ref in + Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *) + (* Someday we should stop relying on Dumglob raising exceptions *) + DAst.make ?loc @@ GRef (ref, us), impls, scopes, [] with e when CErrors.noncritical e -> - (* [id] a goal variable *) - gvar (loc,id) us, [], [], [] + (* [id] a goal variable *) + gvar (loc,id) us, [], [], [] let find_appl_head_data c = match DAst.get c with @@ -1013,24 +1004,16 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option = - match info with - | UAnonymous -> None - | UUnknown -> None - | UNamed id -> Some (id, 0) - let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType info -> GType [sort_info_of_level_info info] + | UAnonymous {rigid} -> UAnonymous {rigid} + | UNamed id -> UNamed [id,0] (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in match intern_extended_global_of_qualid qid with - | TrueGlobal (VarRef _) when no_secvar -> + | TrueGlobal (GlobRef.VarRef _) when no_secvar -> (* Rule out section vars since these should have been found by intern_var *) raise Not_found | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), Some ref, args @@ -1060,7 +1043,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (UAnonymous {rigid=true}) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) @@ -1079,6 +1062,7 @@ let check_applied_projection isproj realref qid = match isproj with | None -> () | Some projargs -> + let open GlobRef in let is_prim = match realref with | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false | Some (ConstRef c) -> @@ -1212,10 +1196,10 @@ let check_or_pat_variables loc ids idsl = @return if letin are included *) let check_constructor_length env loc cstr len_pl pl0 = let n = len_pl + List.length pl0 in - if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else - (Int.equal n (Inductiveops.constructor_nalldecls cstr) || + if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else + (Int.equal n (Inductiveops.constructor_nalldecls env cstr) || (error_wrong_numarg_constructor ?loc env cstr - (Inductiveops.constructor_nrealargs cstr))) + (Inductiveops.constructor_nrealargs env cstr))) open Declarations @@ -1235,16 +1219,18 @@ let insert_local_defs_in_pattern (ind,j) l = | _ -> assert false in aux decls l -let add_local_defs_and_check_length loc env g pl args = match g with +let add_local_defs_and_check_length loc env g pl args = + let open GlobRef in + match g with | ConstructRef cstr -> (* We consider that no variables corresponding to local binders have been given in the "explicit" arguments, which come from a "@C args" notation or from a custom user notation *) let pl' = insert_local_defs_in_pattern cstr pl in - let maxargs = Inductiveops.constructor_nalldecls cstr in + let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then - error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr); - (* Two possibilities: either the args are given with explict + error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); + (* Two possibilities: either the args are given with explicit variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be added later on; or the args are not enough to have all arguments, @@ -1273,24 +1259,24 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 in aux 0 (impl_list,pl2) let add_implicits_check_constructor_length env loc c len_pl1 pl2 = - let nargs = Inductiveops.constructor_nallargs c in - let nargs' = Inductiveops.constructor_nalldecls c in - let impls_st = implicits_of_global (ConstructRef c) in + let nargs = Inductiveops.constructor_nallargs env c in + let nargs' = Inductiveops.constructor_nalldecls env c in + let impls_st = implicits_of_global (GlobRef.ConstructRef c) in add_implicits_check_length (error_wrong_numarg_constructor ?loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = - let nallargs = inductive_nallargs_env env c in - let nalldecls = inductive_nalldecls_env env c in - let impls_st = implicits_of_global (IndRef c) in + let nallargs = inductive_nallargs env c in + let nalldecls = inductive_nalldecls env c in + let impls_st = implicits_of_global (GlobRef.IndRef c) in add_implicits_check_length (error_wrong_numarg_inductive ?loc env c) nallargs nalldecls impls_st len_pl1 pl2 (** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind in + then Inductiveops.inductive_nparamdecls (Global.env()) ind + else Inductiveops.inductive_nparams (Global.env()) ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (fun c -> match DAst.get c with @@ -1299,6 +1285,7 @@ let chop_params_pattern loc ind args with_letin = args let find_constructor loc add_params ref = + let open GlobRef in let (ind,_ as cstr) = match ref with | ConstructRef cstr -> cstr | IndRef _ -> @@ -1310,10 +1297,11 @@ let find_constructor loc add_params ref = in cstr, match add_params with | Some nb_args -> + let env = Global.env () in let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind + if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr) + then Inductiveops.inductive_nparamdecls env ind + else Inductiveops.inductive_nparams env ind in List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] @@ -1322,7 +1310,7 @@ let find_pattern_variable qid = if qualid_is_ident qid then qualid_basename qid else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) -let check_duplicate loc fields = +let check_duplicate ?loc fields = let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with @@ -1332,7 +1320,7 @@ let check_duplicate loc fields = pr_qualid r ++ str ".") let inductive_of_record loc record = - let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive (** [sort_fields ~complete loc fields completer] expects a list @@ -1354,7 +1342,7 @@ let sort_fields ~complete loc fields completer = | (first_field_ref, first_field_value):: other_fields -> let (first_field_glob_ref, record) = try - let gr = global_reference_of_reference first_field_ref in + let gr = locate_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> raise (InternalizationError(loc, NotAProjection first_field_ref)) @@ -1363,11 +1351,11 @@ let sort_fields ~complete loc fields completer = let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) let base_constructor = - let global_record_id = ConstructRef record.Recordops.s_CONST in + let global_record_id = GlobRef.ConstructRef record.Recordops.s_CONST in try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in - let () = check_duplicate loc fields in + let () = check_duplicate ?loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) @@ -1378,11 +1366,11 @@ let sort_fields ~complete loc fields completer = match projs with | [] -> (idx, acc_first_idx, acc) | (Some field_glob_id) :: projs -> - let field_glob_ref = ConstRef field_glob_id in + let field_glob_ref = GlobRef.ConstRef field_glob_id in let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch.") - | (_, regular) :: proj_kinds -> + | { Recordops.pk_true_proj = regular } :: proj_kinds -> (* "regular" is false when the field is defined by a let-in in the record declaration (its value is fixed from other fields). *) @@ -1412,7 +1400,7 @@ let sort_fields ~complete loc fields completer = let rec index_fields fields remaining_projs acc = match fields with | (field_ref, field_value) :: fields -> - let field_glob_ref = try global_reference_of_reference field_ref + let field_glob_ref = try locate_reference field_ref with Not_found -> user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in @@ -1422,7 +1410,7 @@ let sort_fields ~complete loc fields completer = raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) in let remaining_projs, (field_index, _) = - let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in + let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> let ind1 = inductive_of_record loc record in @@ -1481,7 +1469,7 @@ let alias_of als = match als.alias_ids with @returns a raw_case_pattern_expr : - no notations and syntactic definition - - global reference and identifeir instead of reference + - global reference and identifier instead of reference *) @@ -1533,12 +1521,12 @@ let drop_notations_pattern looked_for genv = let ensure_kind top loc g = try if top then looked_for g else - match g with ConstructRef _ -> () | _ -> raise Not_found + match g with GlobRef.ConstructRef _ -> () | _ -> raise Not_found with Not_found -> error_invalid_pattern_notation ?loc () in let test_kind top = - if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found + if top then looked_for else function GlobRef.ConstructRef _ -> () | _ -> raise Not_found in (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function @@ -1656,15 +1644,13 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supportted only in local binders and only at top - level. In fact, they are currently eliminated by the - parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor - the "(c : t)" notation with user defined notations (such as - the pair). In the long term, we will try to support such - casts everywhere, and use them to print the domains of - lambdas in the encoding of match in constr. This check is - here and not in the parser because it would require + are supported only in local binders and only at top level. + The only reason they are in the [cases_pattern_expr] type + is that the parser needs to factor the "c : t" notation + with user defined notations. In the long term, we will try to + support such casts everywhere, and perhaps use them to print + the domains of lambdas in the encoding of match in constr. + This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc ~hdr:"drop_notations_pattern" (Pp.strbrk "Casts are not supported in this pattern.") @@ -1753,7 +1739,7 @@ let rec intern_pat genv ntnvars aliases pat = let intern_cases_pattern genv ntnvars scopes aliases pat = intern_pat genv ntnvars aliases - (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) + (drop_notations_pattern (function GlobRef.ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := @@ -1762,13 +1748,13 @@ let _ = let intern_ind_pattern genv ntnvars scopes pat = let no_not = try - drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat + drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc in let loc = no_not.CAst.loc in match DAst.get no_not with | RCPatCstr (head, expl_pl, pl) -> - let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in + let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in @@ -1807,7 +1793,7 @@ let set_hole_implicit i b c = Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") end - | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None) + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (GlobRef.VarRef id,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -1862,48 +1848,45 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in - let n = - try List.index0 Id.equal iddef lf + let n = + try List.index0 Id.equal iddef lf with Not_found -> - raise (InternalizationError (locid,UnboundFixName (false,iddef))) - in - let idl_temp = Array.map - (fun (id,(n,order),bl,ty,_) -> - let intern_ro_arg f = - let before, after = split_at_annot bl n in - let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in - let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with - | GLocalAssum _ -> true - | _ -> false (* remove let-ins *)) - rbefore) n in - n', ro, List.fold_left intern_local_binder (env',rbefore) after - in - let n, ro, (env',rbl) = - match order with - | CStructRec -> - intern_ro_arg (fun _ -> GStructRec) - | CWfRec c -> - intern_ro_arg (fun f -> GWfRec (f c)) - | CMeasureRec (m,r) -> - intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) - in - let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - ((n, ro), bl, intern_type env' ty, env')) dl in - let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in - push_name_env ntnvars (impls_type_list ~args:fix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in - DAst.make ?loc @@ - GRec (GFix - (Array.map (fun (ro,_,_,_) -> ro) idl,n), + raise (InternalizationError (locid,UnboundFixName (false,iddef))) + in + let idl_temp = Array.map + (fun (id,recarg,bl,ty,_) -> + let recarg = Option.map (function { CAst.v = v } -> match v with + | CStructRec i -> i + | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg + in + let before, after = split_at_annot bl recarg in + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in + let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with + | GLocalAssum _ -> true + | _ -> false (* remove let-ins *)) + rbefore) recarg in + let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + let bl_impls = remember_binders_impargs env' bl in + (n, bl, intern_type env' ty, bl_impls)) dl in + (* We add the recursive functions to the environment *) + let env_rec = List.fold_left_i (fun i en name -> + let (_,bli,tyi,_) = idl_temp.(i) in + let fix_args = (List.map (fun (na, bk, _, _) -> build_impls bk na) bli) in + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) + en (CAst.make @@ Name name)) 0 env lf in + let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) -> + (* We add the binders common to body and type to the environment *) + let env_body = restore_binders_impargs env_rec before_impls in + (n,bl,ty,intern {env_body with tmp_scope = None} bd)) dl idl_temp in + DAst.make ?loc @@ + GRec (GFix + (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) + | CCoFix ({ CAst.loc = locid; v = iddef }, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in let dl = Array.of_list dl in @@ -1915,15 +1898,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - (List.rev (List.map glob_local_binder_of_extended rbl), - intern_type env' ty,env')) dl in - let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (bli,tyi,_) = idl_tmp.(i) in - let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in - push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + let bl_impls = remember_binders_impargs env' bl in + (bl,intern_type env' ty,bl_impls)) dl in + let env_rec = List.fold_left_i (fun i en name -> + let (bli,tyi,_) = idl_tmp.(i) in + let cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in + push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) + en (CAst.make @@ Name name)) 0 env lf in + let idl = Array.map2 (fun (_,_,_,bd) (b,c,bl_impls) -> + (* We add the binders common to body and type to the environment *) + let env_body = restore_binders_impargs env_rec bl_impls in + (b,c,intern {env_body with tmp_scope = None} bd)) dl idl_tmp in DAst.make ?loc @@ GRec (GCoFix n, Array.of_list lf, @@ -2178,7 +2164,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let loc = tm'.CAst.loc in match DAst.get tm', na with | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id, CAst.make ?loc @@ Name id - | GRef (VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id + | GRef (GlobRef.VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id | _, None -> None, CAst.make Anonymous | _, Some ({ CAst.loc; v = na } as lna) -> None, lna in (* the "in" part *) @@ -2437,12 +2423,12 @@ let interp_binder_evars env sigma na t = let my_intern_constr env lvar acc c = internalize env acc false lvar c -let intern_context global_level env impl_env binders = +let intern_context env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left (fun (lenv, bl) b -> - let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in + let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in @@ -2466,10 +2452,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let r = Retyping.relevance_of_type env sigma t in let d = LocalAssum (make_annot na r,t) in let impls = - if k == Implicit then - let na = match na with Name n -> Some n | Anonymous -> None in - (ExplByPos (n, na), (true, true, true)) :: impls - else impls + if k == Implicit then CAst.make (Some (na,true)) :: impls + else CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> @@ -2478,9 +2462,9 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let d = LocalDef (make_annot na r, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) - in sigma, ((env, par), impls) + in sigma, ((env, par), List.rev impls) -let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = - let int_env,bl = intern_context global_level env impl_env params in +let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = + let int_env,bl = intern_context env impl_env params in let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in sigma, (int_env, x) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2d14a0d0a7..2e7b832e55 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -61,10 +61,10 @@ type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env val compute_internalization_data : env -> evar_map -> var_internalization_type -> - types -> Impargs.manual_explicitation list -> var_internalization_data + types -> Impargs.manual_implicits -> var_internalization_data val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> - Id.t list -> types list -> Impargs.manual_explicitation list list -> + Id.t list -> types list -> Impargs.manual_implicits list -> internalization_env type ltac_sign = { @@ -90,7 +90,7 @@ val intern_gen : typing_constraint -> env -> evar_map -> val intern_pattern : env -> cases_pattern_expr -> lident list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list +val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -158,28 +158,15 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * (** Interpret contexts: returns extended env and context *) val interp_context_evars : - ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> + ?program_mode:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map -> local_binder_expr list -> evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) -(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) -(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) -(* ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) - -(* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder_expr list -> *) -(* internalization_env * *) -(* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) - (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) val locate_reference : Libnames.qualid -> GlobRef.t val is_global : Id.t -> bool -val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t -val global_reference : Id.t -> GlobRef.t -val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) @@ -202,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b (** Placeholder for global option, should be moved to a parameter *) val get_asymmetric_patterns : unit -> bool + +val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit +(** Check that a list of record field definitions doesn't contain + duplicates. *) diff --git a/interp/declare.ml b/interp/declare.ml deleted file mode 100644 index 717f8ef49a..0000000000 --- a/interp/declare.ml +++ /dev/null @@ -1,560 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** This module is about the low-level declaration of logical objects *) - -open Pp -open CErrors -open Util -open Names -open Libnames -open Globnames -open Constr -open Declarations -open Entries -open Libobject -open Lib -open Impargs -open Safe_typing -open Cooking -open Decls -open Decl_kinds - -(** flag for internal message display *) -type internal_flag = - | UserAutomaticRequest (* kernel action, a message is displayed *) - | InternalTacticRequest (* kernel action, no message is displayed *) - | UserIndividualRequest (* user action, a message is displayed *) - -(** Declaration of constants and parameters *) - -type constant_obj = { - cst_decl : global_declaration option; - (** [None] when the declaration is a side-effect and has already been defined - in the global environment. *) - cst_kind : logical_kind; - cst_locl : bool; -} - -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind - -(* At load-time, the segment starting from the module name to the discharge *) -(* section (if Remark or Fact) is needed to access a construction *) -let load_constant i ((sp,kn), obj) = - if Nametab.exists_cci sp then - alreadydeclared (Id.print (basename sp) ++ str " already exists"); - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con obj.cst_kind - -(* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn), obj) = - (* Never open a local definition *) - if obj.cst_locl then () - else - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con) - -let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) - -let check_exists sp = - let id = basename sp in - if exists_name id then alreadydeclared (Id.print id ++ str " already exists") - -let cache_constant ((sp,kn), obj) = - let id = basename sp in - let kn' = - match obj.cst_decl with - | None -> - if Global.exists_objlabel (Label.of_id (basename sp)) - then Constant.make1 kn - else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") - | Some decl -> - let () = check_exists sp in - Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl - in - assert (Constant.equal kn' (Constant.make1 kn)); - Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); - let cst = Global.lookup_constant kn' in - add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - add_constant_kind (Constant.make1 kn) obj.cst_kind - -let discharge_constant ((sp, kn), obj) = - let con = Constant.make1 kn in - let from = Global.lookup_constant con in - let modlist = replacement_context () in - let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let abstract = (named_of_variable_context hyps, subst, uctx) in - let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_decl = Some new_decl; } - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant cst = { - cst_decl = None; - cst_kind = cst.cst_kind; - cst_locl = cst.cst_locl; -} - -let classify_constant cst = Substitute (dummy_constant cst) - -let (inConstant : constant_obj -> obj) = - declare_object { (default_object "CONSTANT") with - cache_function = cache_constant; - load_function = load_constant; - open_function = open_constant; - classify_function = classify_constant; - subst_function = ident_subst_function; - discharge_function = discharge_constant } - -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f - -let update_tables c = - declare_constant_implicits c; - Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) - -let register_side_effect (c, role) = - let o = inConstant { - cst_decl = None; - cst_kind = IsProof Theorem; - cst_locl = false; - } in - let id = Label.to_id (Constant.label c) in - ignore(add_leaf id o); - update_tables c; - match role with - | Subproof -> () - | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] - -let declare_constant_common id cst = - let o = inConstant cst in - let _, kn as oname = add_leaf id o in - pull_to_head oname; - let c = Global.constant_of_delta_kn kn in - update_tables c; - c - -let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = - { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - const_entry_secctx = None; - const_entry_type = types; - const_entry_universes = univs; - const_entry_opaque = opaque; - const_entry_feedback = None; - const_entry_inline_code = inline} - -let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let is_poly de = match de.const_entry_universes with - | Monomorphic_entry _ -> false - | Polymorphic_entry _ -> true - in - let in_section = Lib.sections_are_opened () in - let export, decl = (* We deal with side effects *) - match cd with - | DefinitionEntry de when - export_seff || - not de.const_entry_opaque || - is_poly de -> - (* This globally defines the side-effects in the environment. We mark - exported constants as being side-effect not to redeclare them at - caching time. *) - let de, export = Global.export_private_constants ~in_section de in - export, ConstantEntry (PureEntry, DefinitionEntry de) - | _ -> [], ConstantEntry (EffectEntry, cd) - in - let () = List.iter register_side_effect export in - let cst = { - cst_decl = Some decl; - cst_kind = kind; - cst_locl = local; - } in - declare_constant_common id cst - -let declare_definition ?(internal=UserIndividualRequest) - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - id ?types (body,univs) = - let cb = - definition_entry ?types ~univs ~opaque body - in - declare_constant ~internal ~local id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) - -(** Declaration of section variables and local definitions *) -type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) - -type variable_declaration = DirPath.t * section_variable_entry * logical_kind - -let cache_variable ((sp,_),o) = - match o with - | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(p,d,mk)) -> - (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); - - let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx - | SectionLocalDef (de) -> - let (de, eff) = Global.export_private_constants ~in_section:true de in - let () = List.iter register_side_effect eff in - (* The body should already have been forced upstream because it is a - section-local definition, but it's not enforced by typing *) - let (body, uctx), () = Future.force de.const_entry_body in - let poly, univs = match de.const_entry_universes with - | Monomorphic_entry uctx -> false, uctx - | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx - in - let univs = Univ.ContextSet.union uctx univs in - (* We must declare the universe constraints before type-checking the - term. *) - let () = Global.push_context_set (not poly) univs in - let se = { - secdef_body = body; - secdef_secctx = de.const_entry_secctx; - secdef_feedback = de.const_entry_feedback; - secdef_type = de.const_entry_type; - } in - let () = Global.push_named_def (id, se) in - Explicit, de.const_entry_opaque, - poly, univs in - Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl poly ctx; - add_variable_data id (p,opaq,ctx,poly,mk) - -let discharge_variable (_,o) = match o with - | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope Evd.empty (VarRef id); - oname - -(** Declaration of inductive blocks *) -let declare_inductive_argument_scopes kn mie = - List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -let inductive_names sp kn mie = - let (dp,_) = repr_path sp in - let kn = Global.mind_of_delta_kn kn in - let names, _ = - List.fold_left - (fun (names, n) ind -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) ind.mind_entry_consnames in - let sp = Libnames.make_path dp ind.mind_entry_typename - in - ((sp, IndRef ind_p) :: names, n+1)) - ([], 0) mie.mind_entry_inds - in names - -let load_inductive i ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names - -let open_inductive i ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names - -let cache_inductive ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter check_exists (List.map fst names); - let id = basename sp in - let kn' = Global.add_mind id mie in - assert (MutInd.equal kn' (MutInd.make1 kn)); - let mind = Global.lookup_mind kn' in - add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names - -let discharge_inductive ((sp,kn),mie) = - let mind = Global.mind_of_delta_kn kn in - let mie = Global.lookup_mind mind in - let repl = replacement_context () in - let info = section_segment_of_mutual_inductive mind in - Some (Discharge.process_inductive info repl mie) - -let dummy_one_inductive_entry mie = { - mind_entry_typename = mie.mind_entry_typename; - mind_entry_arity = mkProp; - mind_entry_template = false; - mind_entry_consnames = mie.mind_entry_consnames; - mind_entry_lc = [] -} - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry m = { - mind_entry_params = []; - mind_entry_record = None; - mind_entry_finite = Declarations.BiFinite; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = default_univ_entry; - mind_entry_variance = None; - mind_entry_private = None; -} - -(* reinfer subtyping constraints for inductive after section is dischared. *) -let rebuild_inductive mind_ent = - let env = Global.env () in - InferCumulativity.infer_inductive env mind_ent - -let inInductive : mutual_inductive_entry -> obj = - declare_object {(default_object "INDUCTIVE") with - cache_function = cache_inductive; - load_function = load_inductive; - open_function = open_inductive; - classify_function = (fun a -> Substitute (dummy_inductive_entry a)); - subst_function = ident_subst_function; - discharge_function = discharge_inductive; - rebuild_function = rebuild_inductive } - -let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let id = Label.to_id label in - let univs, u = match univs with - | Monomorphic_entry _ -> - (* Global constraints already defined through the inductive *) - default_univ_entry, Univ.Instance.empty - | Polymorphic_entry (nas, ctx) -> - Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx - in - let term = Vars.subst_instance_constr u term in - let types = Vars.subst_instance_constr u types in - let entry = definition_entry ~types ~univs term in - let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - Recordops.declare_primitive_projection p cst - - -let declare_projections univs mind = - let env = Global.env () in - let mib = Environ.lookup_mind mind env in - match mib.mind_record with - | PrimRecord info -> - let iter_ind i (_, labs, _, _) = - let ind = (mind, i) in - let projs = Inductiveops.compute_projections env ind in - Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs - in - let () = Array.iteri iter_ind info in - true - | FakeRecord -> false - | NotRecord -> false - -(* for initial declaration *) -let declare_mind mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive mie) in - let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mie.mind_entry_universes mind in - declare_mib_implicits mind; - declare_inductive_argument_scopes mind mie; - oname, isprim - -(* Declaration messages *) - -let pr_rank i = pr_nth (i+1) - -let fixpoint_message indexes l = - Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "no recursive definition.") - | [id] -> Id.print id ++ str " is recursively defined" ++ - (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prvect_with_sep pr_comma pr_rank a ++ - str " arguments)" - | None -> mt ())) - -let cofixpoint_message l = - Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "No corecursive definition.") - | [id] -> Id.print id ++ str " is corecursively defined" - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are corecursively defined")) - -let recursive_message isfix i l = - (if isfix then fixpoint_message i else cofixpoint_message) l - -let definition_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") - -let assumption_message id = - (* Changing "assumed" to "declared", "assuming" referring more to - the type of the object than to the name of the object (see - discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") - -(** Monomorphic universes need to survive sections. *) - -let input_universe_context : Univ.ContextSet.t -> Libobject.obj = - declare_object @@ local_object "Monomorphic section universes" - ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) - ~discharge:(fun (_, x) -> Some x) - -let declare_universe_context poly ctx = - if poly then - (Global.push_context_set true ctx; Lib.add_section_context ctx) - else - Lib.add_anonymous_leaf (input_universe_context ctx) - -(** Global universes are not substitutive objects but global objects - bound at the *library* or *module* level. The polymorphic flag is - used to distinguish universes declared in polymorphic sections, which - are discharged and do not remain in scope. *) - -type universe_source = - | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) - | QualifiedUniv of Id.t (* global universe introduced by some global value *) - | UnqualifiedUniv (* other global universe *) - -type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list - -let check_exists sp = - if Nametab.exists_universe sp then - alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") - else () - -let qualify_univ i dp src id = - match src with - | BoundUniv | UnqualifiedUniv -> - i, Libnames.make_path dp id - | QualifiedUniv l -> - let dp = DirPath.repr dp in - Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id - -let do_univ_name ~check i dp src (id,univ) = - let i, sp = qualify_univ i dp src id in - if check then check_exists sp; - Nametab.push_universe i sp univ - -let cache_univ_names ((sp, _), (src, univs)) = - let depth = sections_depth () in - let dp = pop_dirpath_n depth (dirpath sp) in - List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs - -let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs - -let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs - -let discharge_univ_names = function - | _, (BoundUniv, _) -> None - | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x - -let input_univ_names : universe_name_decl -> Libobject.obj = - declare_object - { (default_object "Global universe name state") with - cache_function = cache_univ_names; - load_function = load_univ_names; - open_function = open_univ_names; - discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); - classify_function = (fun a -> Substitute a) } - -let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") - in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] - in - Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) - -let do_universe poly l = - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic universes outside sections") - in - let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in - let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) - Univ.LSet.empty l, Univ.Constraint.empty - in - let () = declare_universe_context poly ctx in - let src = if poly then BoundUniv else UnqualifiedUniv in - Lib.add_anonymous_leaf (input_univ_names (src, l)) - -let do_constraint poly l = - let open Univ in - let u_of_id x = - let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Lib.is_polymorphic_univ level, level - in - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic constraints outside sections") - in - let check_poly p p' = - if poly then () - else if p || p' then - user_err ~hdr:"Constraint" - (str "Cannot declare a global constraint on " ++ - str "a polymorphic universe, use " - ++ str "Polymorphic Constraint instead") - in - let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly p p'; - Constraint.add (lu, d, ru) acc) - Constraint.empty l - in - let uctx = ContextSet.add_constraints constraints ContextSet.empty in - declare_universe_context poly uctx diff --git a/interp/declare.mli b/interp/declare.mli deleted file mode 100644 index 8f1e73c88c..0000000000 --- a/interp/declare.mli +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Entries -open Decl_kinds - -(** This module provides the official functions to declare new variables, - parameters, constants and inductive types. Using the following functions - will add the entries in the global environment (module [Global]), will - register the declarations in the library (module [Lib]) --- so that the - reset works properly --- and will fill some global tables such as - [Nametab] and [Impargs]. *) - -(** Declaration of local constructions (Variable/Hypothesis/Local) *) - -type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) - -type variable_declaration = DirPath.t * section_variable_entry * logical_kind - -val declare_variable : variable -> variable_declaration -> Libobject.object_name - -(** Declaration of global constructions - i.e. Definition/Theorem/Axiom/Parameter/... *) - -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind - -type internal_flag = - | UserAutomaticRequest - | InternalTacticRequest - | UserIndividualRequest - -(* Defaut definition entries, transparent with no secctx or proj information *) -val definition_entry : ?fix_exn:Future.fix_exn -> - ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.universes_entry -> - ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry - -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent *) -val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t - -val declare_definition : - ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> Id.t -> ?types:constr -> - constr Entries.in_universes_entry -> Constant.t - -(** Since transparent constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * Constant.t) array -> unit) -> unit - -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool - -(** Declaration messages *) - -val definition_message : Id.t -> unit -val assumption_message : Id.t -> unit -val fixpoint_message : int array option -> Id.t list -> unit -val cofixpoint_message : Id.t list -> unit -val recursive_message : bool (** true = fixpoint *) -> - int array option -> Id.t list -> unit - -val exists_name : Id.t -> bool - -(** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit - -val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit - -val do_universe : polymorphic -> lident list -> unit -val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> - unit diff --git a/interp/decls.ml b/interp/decls.ml new file mode 100644 index 0000000000..d9d33b5e0b --- /dev/null +++ b/interp/decls.ml @@ -0,0 +1,80 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module registers tables for some non-logical informations + associated declarations *) + +open Names +open Libnames + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural | Context + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) + +(** Kinds *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(** Data associated to section variables and local definitions *) + +type variable_data = { + opaque:bool; + kind:logical_kind; +} + +let vartab = + Summary.ref (Id.Map.empty : (variable_data*DirPath.t) Id.Map.t) ~name:"VARIABLE" + +let secpath () = drop_dirpath_prefix (Lib.library_dp()) (Lib.cwd()) +let add_variable_data id o = vartab := Id.Map.add id (o,secpath()) !vartab + +let variable_opacity id = let {opaque},_ = Id.Map.find id !vartab in opaque +let variable_kind id = let {kind},_ = Id.Map.find id !vartab in kind + +let variable_secpath id = + let _, dir = Id.Map.find id !vartab in + make_qualid dir id + +let variable_exists id = Id.Map.mem id !vartab diff --git a/interp/decls.mli b/interp/decls.mli new file mode 100644 index 0000000000..56866aeb43 --- /dev/null +++ b/interp/decls.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Libnames + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural | Context + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) + +(** Kinds used in library *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(** This module manages non-kernel informations about declarations. It + is either non-logical informations or logical informations that + have no place to be (yet) in the kernel *) + +(** Registration and access to the table of variable *) + +type variable_data = { + opaque:bool; + kind:logical_kind; +} + +val add_variable_data : variable -> variable_data -> unit + +(* Only used in dumpglob *) +val variable_secpath : variable -> qualid +val variable_kind : variable -> logical_kind + +(* User in Lemma, Very dubious *) +val variable_opacity : variable -> bool + +(* Used in declare, very dubious *) +val variable_exists : variable -> bool diff --git a/interp/deprecation.ml b/interp/deprecation.ml new file mode 100644 index 0000000000..3b02ba4664 --- /dev/null +++ b/interp/deprecation.ml @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = { since : string option ; note : string option } + +let make ?since ?note () = { since ; note } + +let create_warning ~object_name ~warning_name name_printer = + let open Pp in + CWarnings.create ~name:warning_name ~category:"deprecated" + (fun (qid,depr) -> str object_name ++ spc () ++ name_printer qid ++ + strbrk " is deprecated" ++ + pr_opt (fun since -> str "since " ++ str since) depr.since ++ + str "." ++ pr_opt (fun note -> str note) depr.note) diff --git a/interp/discharge.mli b/interp/deprecation.mli index f7408937cf..f8083c2a5b 100644 --- a/interp/discharge.mli +++ b/interp/deprecation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -8,9 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Declarations -open Entries -open Opaqueproof +type t = { since : string option ; note : string option } -val process_inductive : - Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry +val make : ?since:string -> ?note:string -> unit -> t + +val create_warning : object_name:string -> warning_name:string -> + ('b -> Pp.t) -> ?loc:Loc.t -> 'b * t -> unit diff --git a/interp/discharge.ml b/interp/discharge.ml deleted file mode 100644 index 1efd13adb1..0000000000 --- a/interp/discharge.ml +++ /dev/null @@ -1,118 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Term -open Constr -open Vars -open Declarations -open Cooking -open Entries - -(********************************) -(* Discharging mutual inductive *) - -(* Replace - - Var(y1)..Var(yq):C1..Cq |- Ij:Bj - Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti - - by - - |- Ij: (y1..yq:C1..Cq)Bj - I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] -*) - -let abstract_inductive decls nparamdecls inds = - let ntyp = List.length inds in - let ndecls = Context.Named.length decls in - let args = Context.Named.to_instance mkVar (List.rev decls) in - let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (substl subs) lc in - let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to process_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - params - in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true - -let process_inductive info modlist mib = - let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx - | Polymorphic auctx -> - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_entry (nas, auctx) - in - let variance = match mib.mind_variance with - | None -> None - | Some _ -> Some (InferCumulativity.dummy_variance ind_univs) - in - let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in - let inds = - Array.map_to_list - (fun mip -> - let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = discharge ty in - let lc = Array.map discharge mip.mind_user_lc in - (mip.mind_typename, - arity, template, - Array.to_list mip.mind_consnames, - Array.to_list lc)) - mib.mind_packets in - let section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | PrimRecord info -> - Some (Some (Array.map (fun (x,_,_,_) -> x) info)) - | FakeRecord -> Some None - | NotRecord -> None - in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_variance = variance; - mind_entry_universes = ind_univs - } - diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index a537b4848c..41d1da9694 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,40 +12,30 @@ open Util (* Dump of globalization (to be used by coqdoc) *) -let glob_file = ref Pervasives.stdout +let glob_file = ref stdout let open_glob_file f = - glob_file := Pervasives.open_out f + glob_file := open_out f let close_glob_file () = - Pervasives.close_out !glob_file + close_out !glob_file -type glob_output_t = - | NoGlob - | StdOut - | MultFiles - | Feedback - | File of string +type glob_output = + | NoGlob + | Feedback + | MultFiles + | File of string let glob_output = ref NoGlob -let dump () = !glob_output != NoGlob +let dump () = !glob_output <> NoGlob -let noglob () = glob_output := NoGlob - -let dump_to_dotglob () = glob_output := MultFiles - -let dump_into_file f = - if String.equal f "stdout" then - (glob_output := StdOut; glob_file := Pervasives.stdout) - else - (glob_output := File f; open_glob_file f) - -let feedback_glob () = glob_output := Feedback +let set_glob_output mode = + glob_output := mode let dump_string s = - if dump () && !glob_output != Feedback then - Pervasives.output_string !glob_file s + if dump () && !glob_output != Feedback then + output_string !glob_file s let start_dump_glob ~vfile ~vofile = match !glob_output with @@ -57,19 +47,19 @@ let start_dump_glob ~vfile ~vofile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | Feedback | StdOut -> + | NoGlob | Feedback -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | Feedback | StdOut -> () + | NoGlob | Feedback -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state -open Decl_kinds +open Decls open Declarations let type_of_logical_kind = function @@ -91,7 +81,8 @@ let type_of_logical_kind = function (match a with | Definitional -> "defax" | Logical -> "prfax" - | Conjectural -> "prfax") + | Conjectural -> "prfax" + | Context -> "prfax") | IsProof th -> (match th with | Theorem @@ -103,16 +94,24 @@ let type_of_logical_kind = function | Corollary -> "thm") | IsPrimitive -> "prim" + +(** Data associated to global parameters and constants *) + +let csttab = Summary.ref (Names.Cmap.empty : logical_kind Names.Cmap.t) ~name:"CONSTANT" +let add_constant_kind kn k = csttab := Names.Cmap.add kn k !csttab +let constant_kind kn = Names.Cmap.find kn !csttab + let type_of_global_ref gr = if Typeclasses.is_class gr then "class" else + let open Names.GlobRef in match gr with - | Globnames.ConstRef cst -> - type_of_logical_kind (Decls.constant_kind cst) - | Globnames.VarRef v -> - "var" ^ type_of_logical_kind (Decls.variable_kind v) - | Globnames.IndRef ind -> + | ConstRef cst -> + type_of_logical_kind (constant_kind cst) + | VarRef v -> + "var" ^ type_of_logical_kind (Decls.variable_kind v) + | IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> Declarations.NotRecord then begin match mib.Declarations.mind_finite with @@ -126,7 +125,7 @@ let type_of_global_ref gr = | BiFinite -> "variant" | CoFinite -> "coind" end - | Globnames.ConstructRef _ -> "constr" + | ConstructRef _ -> "constr" let remove_sections dir = let cwd = Lib.cwd_except_section () in @@ -158,6 +157,9 @@ let dump_reference ?loc modpath ident ty = let filepath = Names.DirPath.to_string (Lib.library_dp ()) in dump_ref ?loc filepath modpath ident ty +let dump_secvar ?loc id = + dump_reference ?loc "<>" (Libnames.string_of_qualid (Decls.variable_secpath id)) "var" + let dump_modref ?loc mp ty = let (dp, l) = Lib.split_modpath mp in let filepath = Names.DirPath.to_string dp in diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 554da7603f..2b6a116a01 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -8,19 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val open_glob_file : string -> unit -val close_glob_file : unit -> unit - val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool -val noglob : unit -> unit -val dump_into_file : string -> unit (** special handling of "stdout" *) +type glob_output = + | NoGlob + | Feedback + | MultFiles (* one glob file per .v file *) + | File of string (* Single file for all coqc arguments *) -val dump_to_dotglob : unit -> unit -val feedback_glob : unit -> unit +(* Default "NoGlob" *) +val set_glob_output : glob_output -> unit val pause : unit -> unit val continue : unit -> unit @@ -32,6 +32,7 @@ val dump_definition : Names.lident -> bool -> string -> unit val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit +val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit @@ -45,3 +46,6 @@ val dump_constraint : Names.lname -> bool -> string -> unit val dump_string : string -> unit val type_of_global_ref : Names.GlobRef.t -> string + +(** Registration of constant information *) +val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit diff --git a/interp/genintern.ml b/interp/genintern.ml index 1b736b7977..e74f8d5f10 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.mli b/interp/genintern.mli index 4100f39029..5619a7b648 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/impargs.ml b/interp/impargs.ml index d83a0ce918..5f41c2a366 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,12 +15,10 @@ open Names open Constr open Globnames open Declarations -open Decl_kinds open Lib open Libobject open EConstr open Reductionops -open Constrexpr open Namegen module NamedDecl = Context.Named.Declaration @@ -96,11 +94,11 @@ let set_maximality imps b = this kind if there is enough arguments to infer them) - [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) - [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) @@ -120,8 +118,6 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false -let explicitation_eq = Constrexpr_ops.explicitation_eq - type implicit_explanation = | DepRigid of argument_position | DepFlex of argument_position @@ -343,77 +339,30 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -(* -If found, returns Some (x,(b,fi,fo)) and l with the entry removed, -otherwise returns None and l unchanged. - *) -let assoc_by_pos k l = - let rec aux = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl - | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl - | [] -> raise Not_found - in try aux l with Not_found -> None, l - -let check_correct_manual_implicits autoimps l = - List.iter (function - | ExplByName id,(b,fi,forced) -> - if not forced then - user_err - (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".") - | ExplByPos (i,_id),_t -> - if i<1 || i>List.length autoimps then - user_err - (str "Bad implicit argument number: " ++ int i ++ str ".") - else - user_err - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name.")) l - -(* Take a list l of explicitations, and map them to positions. *) -let flatten_explicitations l autoimps = - let rec aux k l = function - | (Name id,_)::imps -> - let value, l' = - try - let eq = Constrexpr_ops.explicitation_eq in - let flags = List.assoc_f eq (ExplByName id) l in - Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l - with Not_found -> assoc_by_pos k l - in value :: aux (k+1) l' imps - | (Anonymous,_)::imps -> - let value, l' = assoc_by_pos k l - in value :: aux (k+1) l' imps - | [] when List.is_empty l -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in aux 1 l autoimps - let set_manual_implicits flags enriching autoimps l = - if not (List.distinct l) then - user_err Pp.(str "Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) let rec merge k autoimps explimps = match autoimps, explimps with | autoimp::autoimps, explimp::explimps -> let imps' = merge (k+1) autoimps explimps in - begin match autoimp, explimp with - | (Name id,_), Some (_, (b, fi, _)) -> - Some (id, Manual, (set_maximality imps' b, fi)) + begin match autoimp, explimp.CAst.v with + | (Name id,_), Some (_,max) -> + Some (id, Manual, (set_maximality imps' max, true)) | (Name id,Some exp), None when enriching -> Some (id, exp, (set_maximality imps' flags.maximal, true)) | (Name _,_), None -> None - | (Anonymous,_), Some (Some id, (b, fi, true)) -> - Some (id,Manual,(b,fi)) - | (Anonymous,_), Some (None, (b, fi, true)) -> + | (Anonymous,_), Some (Name id,max) -> + Some (id,Manual,(max,true)) + | (Anonymous,_), Some (Anonymous,max) -> let id = Id.of_string ("arg_" ^ string_of_int k) in - Some (id,Manual,(b,fi)) - | (Anonymous,_), Some (_, (_, _, false)) -> None + Some (id,Manual,(max,true)) | (Anonymous,_), None -> None end :: imps' | [], [] -> [] - (* flatten_explicitations returns a list of the same length as autoimps *) - | _ -> assert false - in merge 1 autoimps (flatten_explicitations l autoimps) + | [], _ -> assert false + (* possibly more automatic than manual implicit arguments n + when the conclusion is an unfoldable constant *) + | autoimps, [] -> merge k autoimps [CAst.make None] + in merge 1 autoimps l let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] @@ -444,18 +393,18 @@ let compute_mib_implicits flags kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (* No need to care about constraints here *) - let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in + let ty, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef (kn,i)) in let r = Inductive.relevance_of_inductive env (kn,i) in Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), + let ar, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef ind) in + ((GlobRef.IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j (ctx, cty) -> let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) + (GlobRef.ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets @@ -474,7 +423,7 @@ let compute_var_implicits flags id = (* Implicits of a global reference. *) -let compute_global_implicits flags = function +let compute_global_implicits flags = let open GlobRef in function | VarRef id -> compute_var_implicits flags id | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> @@ -499,9 +448,9 @@ type implicit_interactive_request = type implicit_discharge_request = | ImplLocal - | ImplConstant of Constant.t * implicits_flags + | ImplConstant of implicits_flags | ImplMutualInductive of MutInd.t * implicits_flags - | ImplInteractive of GlobRef.t * implicits_flags * + | ImplInteractive of implicits_flags * implicit_interactive_request let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" @@ -536,12 +485,19 @@ let subst_implicits_decl subst (r,imps as o) = let subst_implicits (subst,(req,l)) = (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) +(* This was moved out of lib.ml, however it is not stored with regular + implicit data *) +let sec_implicits = + Summary.ref Id.Map.empty ~name:"section-implicits" + let impls_of_context ctx = - let map (decl, impl) = match impl with - | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) - | _ -> None + let map decl = + let id = NamedDecl.get_id decl in + match Id.Map.get id !sec_implicits with + | Glob_term.Implicit -> Some (id, Manual, (true, true)) + | Glob_term.Explicit -> None in - List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx) + List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx) let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) @@ -554,39 +510,24 @@ let add_section_impls vars extra_impls (cond,impls) = let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> - (try - let vars = variable_section_segment_of_reference ref in - let extra_impls = impls_of_context vars in - let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in - Some (ImplInteractive (ref,flags,exp),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) - | ImplConstant (con,flags) -> - (try - let vars = variable_section_segment_of_reference (ConstRef con) in - let extra_impls = impls_of_context vars in - let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in - let l' = [ConstRef con,newimpls] in - Some (ImplConstant (con,flags),l') - with Not_found -> (* con not defined in this section *) Some (req,l)) - | ImplMutualInductive (kn,flags) -> - (try - let l' = List.map (fun (gr, l) -> - let vars = variable_section_segment_of_reference gr in - let extra_impls = impls_of_context vars in - (gr, - List.map (add_section_impls vars extra_impls) l)) l - in - Some (ImplMutualInductive (kn,flags),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) + | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ -> + let l' = + try + List.map (fun (gr, l) -> + let vars = variable_section_segment_of_reference gr in + let extra_impls = impls_of_context vars in + let newimpls = List.map (add_section_impls vars extra_impls) l in + (gr, newimpls)) l + with Not_found -> l in + Some (req,l') let rebuild_implicits (req,l) = match req with | ImplLocal -> assert false - | ImplConstant (con,flags) -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags con in - req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] + | ImplConstant flags -> + let ref,oldimpls = List.hd l in + let newimpls = compute_global_implicits flags ref in + req, [ref, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = @@ -597,15 +538,14 @@ let rebuild_implicits (req,l) = | _, _ -> assert false in req, aux l newimpls - | ImplInteractive (ref,flags,o) -> + | ImplInteractive (flags,o) -> + let ref,oldimpls = List.hd l in (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags ref in [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in if flags.auto then let newimpls = List.hd (compute_global_implicits flags ref) in let p = List.length (snd newimpls) - userimplsize in @@ -640,16 +580,17 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with auto = true } in let req = - if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in + if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in declare_implicits_gen req flags ref -let declare_var_implicits id = +let declare_var_implicits id ~impl = let flags = !implicit_args in - declare_implicits_gen ImplLocal flags (VarRef id) + sec_implicits := Id.Map.add id impl !sec_implicits; + declare_implicits_gen ImplLocal flags (GlobRef.VarRef id) let declare_constant_implicits con = let flags = !implicit_args in - declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) + declare_implicits_gen (ImplConstant flags) flags (GlobRef.ConstRef con) let declare_mib_implicits kn = let flags = !implicit_args in @@ -660,9 +601,7 @@ let declare_mib_implicits kn = (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) (* Declare manual implicits *) -type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) - -type manual_implicits = manual_explicitation list +type manual_implicits = (Name.t * bool) option CAst.t list let compute_implicits_with_manual env sigma typ enriching l = let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in @@ -687,8 +626,6 @@ let projection_implicits env p impls = CList.skipn_at_least npars impls let declare_manual_implicits local ref ?enriching l = - assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l); - assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l); let flags = !implicit_args in let env = Global.env () in let sigma = Evd.from_env env in @@ -699,13 +636,12 @@ let declare_manual_implicits local ref ?enriching l = let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l])) let maybe_declare_manual_implicits local ref ?enriching l = - match l with - | [] -> () - | _ -> declare_manual_implicits local ref ?enriching l + if List.exists (fun x -> x.CAst.v <> None) l then + declare_manual_implicits local ref ?enriching l (* TODO: either turn these warnings on and document them, or handle these cases sensibly *) @@ -758,7 +694,7 @@ let set_implicits local ref l = compute_implicit_statuses autoimpls imps)) l in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l'])) let extract_impargs_data impls = @@ -768,12 +704,6 @@ let extract_impargs_data impls = | [] -> [] in aux 0 impls -let lift_implicits n = - List.map (fun x -> - match fst x with - ExplByPos (k, id) -> ExplByPos (k + n, id), snd x - | _ -> x) - let make_implicits_list l = [DefaultImpArgs, l] let rec drop_first_implicits p l = diff --git a/interp/impargs.mli b/interp/impargs.mli index 0070423530..2751b9d40b 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) + of a reference can be automatically inferred *) type argument_position = @@ -50,11 +50,11 @@ type implicit_explanation = this kind if there is enough arguments to infer them) *) | DepFlex of argument_position (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) *) @@ -84,13 +84,7 @@ val force_inference_of : implicit_status -> bool val positions_of_implicits : implicits_list -> int list -(** A [manual_explicitation] is a tuple of a positional or named explicitation with - maximal insertion, force inference and force usage flags. Forcing usage makes - the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Constrexpr.explicitation * - (maximal_insertion * force_inference * bool) - -type manual_implicits = manual_explicitation list +type manual_implicits = (Name.t * bool) option CAst.t list val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool -> manual_implicits -> implicit_status list @@ -99,7 +93,7 @@ val compute_implicits_names : env -> Evd.evar_map -> types -> Name.t list (** {6 Computation of implicits (done using the global environment). } *) -val declare_var_implicits : variable -> unit +val declare_var_implicits : variable -> impl:Glob_term.binding_kind -> unit val declare_constant_implicits : Constant.t -> unit val declare_mib_implicits : MutInd.t -> unit @@ -131,8 +125,6 @@ val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list -val lift_implicits : int -> manual_implicits -> manual_implicits - val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list @@ -143,7 +135,3 @@ val projection_implicits : env -> Projection.t -> implicit_status list -> val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list - -val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool - [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"] -(** Equality on [explicitation]. *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 854651e7b7..455471a472 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,7 +11,6 @@ (*i*) open Names open Context -open Decl_kinds open CErrors open Util open Glob_term @@ -23,9 +22,6 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) - module RelDecl = Context.Rel.Declaration (*i*) @@ -66,9 +62,6 @@ let declare_generalizable ~local gen = let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table -let ids_of_list l = - List.fold_right Id.Set.add l Id.Set.empty - let is_global id = try ignore (Nametab.locate_extended (qualid_of_ident id)); true with Not_found -> false @@ -105,26 +98,6 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c -let ids_of_names l = - List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l - -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = - let rec aux bdvars l c = match c with - ((CLocalAssum (n, _, c)) :: tl) -> - let bound = ids_of_names n in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - - | ((CLocalDef (n, c, t)) :: tl) -> - let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in - aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - - | CLocalPattern _ :: tl -> assert false - | [] -> bdvars, l - in aux bound l binders - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs c = match DAst.get c with | GVar id -> @@ -149,7 +122,7 @@ let next_name_away_from na avoid = | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id -let combine_params avoid fn applied needed = +let combine_params avoid applied needed = let named, applied = List.partition (function @@ -167,48 +140,30 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false) named in - let is_unset (_, decl) = match decl with - | LocalAssum _ -> true - | LocalDef _ -> false - in - let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with - [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named -> + | _, (_, LocalDef _) :: need -> aux ids avoid app need + + | [], [] -> List.rev ids, avoid + + | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need -> + | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, _ as d) :: need -> - let t', avoid' = fn avoid d in - aux (t' :: ids) avoid' app need - | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need - | [], (None, _ as decl) :: need -> - let t', avoid' = fn avoid decl in - aux (t' :: ids) avoid' app need + | _, (Some _, decl) :: need | [], (None, decl) :: need -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + let t' = CAst.make @@ CRef (qualid_of_ident id',None) in + aux (t' :: ids) (Id.Set.add id' avoid) app need | (x,_) :: _, [] -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") - in aux [] avoid applied needed - -let combine_params_freevar = - fun avoid (_, decl) -> - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) - -let destClassApp cl = - let open CAst in - let loc = cl.loc in - match cl.v with - | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) - | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) - | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) - | _ -> raise Not_found + in + aux [] avoid applied needed let destClassAppExpl cl = let open CAst in @@ -218,36 +173,27 @@ let destClassAppExpl cl = | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found -let implicit_application env ?(allow_partial=true) f ty = +let implicit_application env ty = let is_class = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in - let gr = Nametab.locate qid in - if Typeclasses.is_class gr then Some (clapp, gr) else None + if Libnames.idset_mem_qualid qid env then None + else + let gr = Nametab.locate qid in + if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in - match is_class with - | None -> ty, env - | Some ({CAst.loc;v=(id, par, inst)}, gr) -> - let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in - let c, avoid = - let c = class_info gr in - let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in - CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid - in c, avoid + match is_class with + | None -> ty, env + | Some ({CAst.loc;v=(id, par, inst)}, gr) -> + let avoid = Id.Set.union env (Id.Set.of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let env = Global.env () in + let sigma = Evd.from_env env in + let c = class_info env sigma gr in + let (ci, rd) = c.cl_context in + let pars = List.rev (List.combine ci rd) in + let args, avoid = combine_params avoid par pars in + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" @@ -256,32 +202,23 @@ let warn_ignoring_implicit_status = Name.print na ++ strbrk " and following binders") let implicits_of_glob_constr ?(with_products=true) l = - let add_impl i na bk l = match bk with - | Implicit -> - let name = - match na with - | Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: l - | _ -> l + let add_impl ?loc na bk l = match bk with + | Implicit -> CAst.make ?loc (Some (na,true)) :: l + | _ -> CAst.make ?loc None :: l in - let rec aux i c = - let abs na bk b = - add_impl i na bk (aux (succ i) b) - in + let rec aux c = match DAst.get c with | GProd (na, bk, t, b) -> - if with_products then abs na bk b + if with_products then add_impl na bk (aux b) else let () = match bk with | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc | _ -> () in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b + | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) + | GLetIn (na, b, t, c) -> aux c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb)) | _ -> [] - in aux 1 l + in aux l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 437fef1753..4f9c47ec36 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,22 +11,14 @@ open Names open Glob_term open Constrexpr -open Libnames val declare_generalizable : local:bool -> lident list option -> unit -val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t -val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t - (** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list -val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list - (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) @@ -37,15 +29,4 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits -val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t - -val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t) -> - constr_expr -> constr_expr * Id.Set.t - -(* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a +val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t diff --git a/interp/interp.mllib b/interp/interp.mllib index 1262dbb181..cb6c527c83 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Deprecation NumTok Constrexpr Tactypes @@ -9,6 +10,7 @@ Notation Syntax_def Smartlocate Constrexpr_ops +Decls Dumpglob Reserve Impargs @@ -16,5 +18,3 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Discharge -Declare diff --git a/interp/modintern.ml b/interp/modintern.ml index 2f516f4f3c..ddf5b2d7b1 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,7 +12,6 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -21,9 +20,11 @@ type module_internalization_error = exception ModuleInternalizationError of module_internalization_error +type module_kind = Module | ModType | ModAny + let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = let open Declaremods in match kind with + let e = match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,7 +47,6 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind qid = - let open Declaremods in let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; diff --git a/interp/modintern.mli b/interp/modintern.mli index 529c438c1a..72695a680e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) +type module_kind = Module | ModType | ModAny + val interp_module_ast : - env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t diff --git a/interp/notation.ml b/interp/notation.ml index b9aca82cf4..ea2173860d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -21,7 +21,6 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration -open Classops (*i*) @@ -50,25 +49,15 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false -let notation_entry_level_compare s1 s2 = match (s1,s2) with -| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0 -| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> - pair_compare String.compare Int.compare (s1,n1) (s2,n2) -| InConstrEntrySomeLevel, _ -> -1 -| InCustomEntryLevel _, _ -> 1 - let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s -let notation_compare = - pair_compare notation_entry_level_compare String.compare - module NotationOrd = struct type t = notation - let compare = notation_compare + let compare = pervasives_compare end module NotationSet = Set.Make(NotationOrd) @@ -83,6 +72,7 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; + not_deprecation : Deprecation.t option; } type scope = { @@ -167,8 +157,6 @@ let scope_eq s1 s2 = match s1, s2 with | Scope _, SingleNotation _ | SingleNotation _, Scope _ -> false -(* Scopes for interpretation *) - let scope_stack = ref [] let current_scopes () = !scope_stack @@ -178,102 +166,14 @@ let scope_is_open_in_scopes sc l = let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) -(* Uninterpretation tables *) - -type interp_rule = - | NotationRule of scope_name option * notation - | SynDefRule of KerName.t - -type scoped_notation_rule_core = scope_name * notation * interpretation * int option -type notation_rule_core = interp_rule * interpretation * int option -type notation_rule = notation_rule_core * delimiters option * bool - -let interp_rule_compare r1 r2 = match r1, r2 with - | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) -> - pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2) - | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2 - | (NotationRule _ | SynDefRule _), _ -> -1 - -module InterpRuleSet = Set.Make(struct - type t = interp_rule - let compare = interp_rule_compare - end) - -(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *) - -type uninterp_scope_elem = - | UninterpScope of scope_name - | UninterpSingle of notation_rule_core - -let uninterp_scope_eq_weak s1 s2 = match s1, s2 with -| UninterpScope s1, UninterpScope s2 -> String.equal s1 s2 -| UninterpSingle s1, UninterpSingle s2 -> false -| (UninterpSingle _ | UninterpScope _), _ -> false - -module ScopeOrd = - struct - type t = scope_name option - let compare = Pervasives.compare - end - -module ScopeMap = CMap.Make(ScopeOrd) - -let uninterp_scope_stack = ref [] - -let push_uninterp_scope sc scopes = UninterpScope sc :: scopes - -let push_uninterp_scopes = List.fold_right push_uninterp_scope - -(**********************************************************************) -(* Mapping classes to scopes *) - -type scope_class = cl_typ - -let scope_class_compare : scope_class -> scope_class -> int = - cl_typ_ord - -let compute_scope_class sigma t = - let (cl,_,_) = find_class_type sigma t in - cl - -module ScopeClassOrd = -struct - type t = scope_class - let compare = scope_class_compare -end - -module ScopeClassMap = Map.Make(ScopeClassOrd) - -let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.empty - -let scope_class_map = ref initial_scope_class_map - -let declare_scope_class sc cl = - scope_class_map := ScopeClassMap.add cl sc !scope_class_map - -let find_scope_class cl = - ScopeClassMap.find cl !scope_class_map - -let find_scope_class_opt = function - | None -> None - | Some cl -> try Some (find_scope_class cl) with Not_found -> None - -let current_type_scope_name () = - find_scope_class_opt (Some CL_SORT) - (* TODO: push nat_scope, z_scope, ... in scopes summary *) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = - if Int.equal i 1 then begin + if Int.equal i 1 then scope_stack := - if op then Scope sc :: !scope_stack - else List.except scope_eq (Scope sc) !scope_stack; - uninterp_scope_stack := - if op then UninterpScope sc :: !uninterp_scope_stack - else List.except uninterp_scope_eq_weak (UninterpScope sc) !uninterp_scope_stack - end + if op then sc :: !scope_stack + else List.except scope_eq sc !scope_stack let cache_scope o = open_scope 1 o @@ -288,7 +188,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_name -> obj = +let inScope : bool * bool * scope_elem -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -297,7 +197,7 @@ let inScope : bool * bool * scope_name -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,normalize_scope sc)) + Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) let empty_scope_stack = [] @@ -305,20 +205,9 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope -let make_type_scope_soft tmp_scope = - if Option.equal String.equal tmp_scope (current_type_scope_name ()) then - true, None - else - false, tmp_scope - let make_current_scopes (tmp_scope,scopes) = Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) -let make_current_uninterp_scopes (tmp_scope,scopes) = - let istyp,tmp_scope = make_type_scope_soft tmp_scope in - istyp,Option.fold_right push_uninterp_scope tmp_scope - (push_uninterp_scopes scopes !uninterp_scope_stack) - (**********************************************************************) (* Delimiters *) @@ -362,80 +251,40 @@ let find_delimiters_scope ?loc key = user_err ?loc ~hdr:"find_delimiters" (str "Unknown scope delimiting key " ++ str key ++ str ".") +(* Uninterpretation tables *) + +type interp_rule = + | NotationRule of scope_name option * notation + | SynDefRule of KerName.t + (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = | RefKey of GlobRef.t - | LambdaKey - | ProdKey | Oth let key_compare k1 k2 = match k1, k2 with | RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 -| RefKey _, _ -> -1 -| _, RefKey _ -> 1 -| k1, k2 -> Pervasives.compare k1 k2 +| RefKey _, Oth -> -1 +| Oth, RefKey _ -> 1 +| Oth, Oth -> 0 module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -let keymap_add key sc interp (scope_map,global_map) = - (* Adding to scope keymap for printing based on open scopes *) - let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in - let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in - let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in - let scope_map = ScopeMap.add sc newscmap scope_map in - (* Adding to global keymap of scoped notations in case the scope is not open *) - let global_map = match interp with - | NotationRule (Some sc,ntn), interp, c -> - let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in - KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map - | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in - (scope_map, global_map) - -let keymap_extract istype keys sc map = - let keymap = - try ScopeMap.find (Some sc) map - with Not_found -> KeyMap.empty in - let delim = - if istype && Option.equal String.equal (Some sc) (current_type_scope_name ()) then - (* A type is re-interpreted with type_scope on top, so never need a delimiter *) - None - else - (* Pass the delimiter so that it can be used if ever the notation is masked *) - (String.Map.find sc !scope_map).delimiters in - let add_scope rule = (rule,delim,false) in - List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys - -let find_with_delimiters istype = function - | None -> - None - | Some _ as scope when istype && Option.equal String.equal scope (current_type_scope_name ()) -> - (* This is in case type_scope (which by default is open in the - initial state) has been explicitly closed *) - Some None - | Some scope -> - match (String.Map.find scope !scope_map).delimiters with - | Some key -> Some (Some key) - | None -> None +type notation_rule = interp_rule * interpretation * int option -let rec keymap_extract_remainder istype scope_seen = function - | [] -> [] - | (sc,ntn,interp,c) :: l -> - if String.Set.mem sc scope_seen then keymap_extract_remainder istype scope_seen l - else - match find_with_delimiters istype (Some sc) with - | None -> keymap_extract_remainder istype scope_seen l - | Some delim -> - let rule = (NotationRule (Some sc, ntn), interp, c) in - (rule,delim,true) :: keymap_extract_remainder istype scope_seen l +let keymap_add key interp map = + let old = try KeyMap.find key map with Not_found -> [] in + KeyMap.add key (interp :: old) map + +let keymap_find key map = + try KeyMap.find key map + with Not_found -> [] (* Scopes table : interpretation -> scope_name *) -let notations_key_table = - ref ((ScopeMap.empty, KeyMap.empty) : - notation_rule_core list KeyMap.t ScopeMap.t * - scoped_notation_rule_core list KeyMap.t) +let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) let glob_prim_constr_key c = match DAst.get c with | GRef (ref, _) -> Some (canonical_gr ref) @@ -447,18 +296,16 @@ let glob_prim_constr_key c = match DAst.get c with | _ -> None let glob_constr_keys c = match DAst.get c with - | GRef (ref,_) -> [RefKey (canonical_gr ref)] | GApp (c, _) -> begin match DAst.get c with | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth] | _ -> [Oth] end - | GLambda _ -> [LambdaKey] - | GProd _ -> [ProdKey] + | GRef (ref,_) -> [RefKey (canonical_gr ref)] | _ -> [Oth] let cases_pattern_key c = match DAst.get c with - | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) + | PatCstr (ref,_,_) -> RefKey (canonical_gr (GlobRef.ConstructRef ref)) | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) @@ -468,8 +315,6 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) - | NLambda _ | NBinderList (_,_,NLambda _,_,_) | NList (_,_,NLambda _,_,_) -> LambdaKey, None - | NProd _ | NBinderList (_,_,NProd _,_,_) | NList (_,_,NProd _,_,_) -> ProdKey, None | _ -> Oth, None (**********************************************************************) @@ -647,10 +492,10 @@ exception NotAValidPrimToken considered for parsing. *) let rec constr_of_glob env sigma g = match DAst.get g with - | Glob_term.GRef (ConstructRef c, _) -> + | Glob_term.GRef (GlobRef.ConstructRef c, _) -> let sigma,c = Evd.fresh_constructor_instance env sigma c in sigma,mkConstructU c - | Glob_term.GRef (IndRef c, _) -> + | Glob_term.GRef (GlobRef.IndRef c, _) -> let sigma,c = Evd.fresh_inductive_instance env sigma c in sigma,mkIndU c | Glob_term.GApp (gc, gcl) -> @@ -666,10 +511,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with let c = glob_of_constr token_kind ?loc env sigma c in let cel = List.map (glob_of_constr token_kind ?loc env sigma) (Array.to_list ca) in DAst.make ?loc (Glob_term.GApp (c, cel)) - | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) - | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) - | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) - | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None)) | Int i -> DAst.make ?loc (Glob_term.GInt i) | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c)) @@ -748,7 +593,7 @@ let rec rawnum_compare s s' = try for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; for i = d to l-1 do - let c = Pervasives.compare s.[i] s'.[i-d] in + let c = pervasives_compare s.[i] s'.[i-d] in if c != 0 then raise (Comp c) done; 0 @@ -991,7 +836,7 @@ let q_byte () = qualid_of_ref "core.byte.type" let unsafe_locate_ind q = match Nametab.locate q with - | IndRef i -> i + | GlobRef.IndRef i -> i | _ -> raise Not_found let locate_list () = unsafe_locate_ind (q_list ()) @@ -1211,31 +1056,37 @@ let check_required_module ?loc sc (sp,d) = (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) -let rec find_without_delimiters find (istype,ntn_scope,ntn as ntndata) = function - | UninterpScope scope :: scopes -> +let find_with_delimiters = function + | None -> None + | Some scope -> + match (String.Map.find scope !scope_map).delimiters with + | Some key -> Some (Some scope, Some key) + | None -> None + +let rec find_without_delimiters find (ntn_scope,ntn) = function + | Scope scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with | Some scope' when String.equal scope scope' -> - Some None + Some (None,None) | _ -> (* If the most recently open scope has a notation/numeral printer but not the expected one then we need delimiters *) if find scope then - find_with_delimiters istype ntn_scope + find_with_delimiters ntn_scope else - find_without_delimiters find ntndata scopes + find_without_delimiters find (ntn_scope,ntn) scopes end - | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes -> + | SingleNotation ntn' :: scopes -> begin match ntn_scope, ntn with | None, Some ntn when notation_eq ntn ntn' -> - Some None + Some (None, None) | _ -> - find_without_delimiters find ntndata scopes + find_without_delimiters find (ntn_scope,ntn) scopes end - | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find ntndata scopes | [] -> (* Can we switch to [scope]? Yes if it has defined delimiters *) - find_with_delimiters istype ntn_scope + find_with_delimiters ntn_scope (* The mapping between notations and their interpretation *) @@ -1245,7 +1096,7 @@ let warn_notation_overridden = str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ strbrk "was already used" ++ which_scope ++ str ".") -let declare_notation_interpretation ntn scopt pat df ~onlyprint = +let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if not onlyprint then begin @@ -1259,6 +1110,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = let notdata = { not_interp = pat; not_location = df; + not_deprecation = deprecation; } in let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in scope_map := String.Map.add scope sc !scope_map @@ -1268,27 +1120,17 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = | Some _ -> () end -let scope_of_rule = function - | NotationRule (None,_) | SynDefRule _ -> None - | NotationRule (Some sc as sco,_) -> sco - -let uninterp_scope_to_add pat n = function - | NotationRule (None,_) | SynDefRule _ as rule -> Some (UninterpSingle (rule,pat,n)) - | NotationRule (Some sc,_) -> None - let declare_uninterpretation rule (metas,c as pat) = let (key,n) = notation_constr_key c in - let sc = scope_of_rule rule in - notations_key_table := keymap_add key sc (rule,pat,n) !notations_key_table; - uninterp_scope_stack := Option.List.cons (uninterp_scope_to_add pat n rule) !uninterp_scope_stack + notations_key_table := keymap_add key (rule,pat,n) !notations_key_table let rec find_interpretation ntn find = function | [] -> raise Not_found | Scope scope :: scopes -> - (try let (pat,df) = find scope in pat,(df,Some scope) + (try let n = find scope in (n,Some scope) with Not_found -> find_interpretation ntn find scopes) | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> - (try let (pat,df) = find default_scope in pat,(df,None) + (try let n = find default_scope in (n,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) find_interpretation ntn find scopes) @@ -1296,8 +1138,7 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - let n = NotationMap.find ntn (find_scope sc).notations in - (n.not_interp, n.not_location) + NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n @@ -1307,7 +1148,9 @@ let notation_of_prim_token = function let find_prim_token check_allowed ?loc p sc = (* Try for a user-defined numerical notation *) try - let (_,c),df = find_notation (notation_of_prim_token p) sc in + let n = find_notation (notation_of_prim_token p) sc in + let (_,c) = n.not_interp in + let df = n.not_location in let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in check_allowed pat; pat, df @@ -1327,7 +1170,9 @@ let find_prim_token check_allowed ?loc p sc = let interp_prim_token_gen ?loc g p local_scopes = let scopes = make_current_scopes local_scopes in let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in - try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes + try + let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in + pat, (loc,sc) with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with @@ -1352,36 +1197,34 @@ let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function let interp_prim_token_cases_pattern_expr ?loc looked_for p = interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p +let warn_deprecated_notation = + Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-notation" + pr_notation + let interp_notation ?loc ntn local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation ntn (find_notation ntn) scopes + try + let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in + Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation; + n.not_interp, (n.not_location, sc) with Not_found -> - user_err ?loc + user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") -let extract_notations (istype,scopes) keys = - if keys == [] then [] (* shortcut *) else - let scope_map, global_map = !notations_key_table in - let rec aux scopes seen = - match scopes with - | UninterpScope sc :: scopes -> keymap_extract istype keys sc scope_map @ aux scopes (String.Set.add sc seen) - | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen - | [] -> - let find key = try KeyMap.find key global_map with Not_found -> [] in - keymap_extract_remainder istype seen (List.flatten (List.map find keys)) - in aux scopes String.Set.empty +let uninterp_notations c = + List.map_append (fun key -> keymap_find key !notations_key_table) + (glob_constr_keys c) -let uninterp_notations scopes c = - let scopes = make_current_uninterp_scopes scopes in - extract_notations scopes (glob_constr_keys c) +let uninterp_cases_pattern_notations c = + keymap_find (cases_pattern_key c) !notations_key_table -let uninterp_cases_pattern_notations scopes c = - let scopes = make_current_uninterp_scopes scopes in - extract_notations scopes [cases_pattern_key c] +let uninterp_ind_pattern_notations ind = + keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table -let uninterp_ind_pattern_notations scopes ind = - let scopes = make_current_uninterp_scopes scopes in - extract_notations scopes [RefKey (canonical_gr (IndRef ind))] +let availability_of_notation (ntn_scope,ntn) scopes = + let f scope = + NotationMap.mem ntn (String.Map.find scope !scope_map).notations in + find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) (* We support coercions from a custom entry at some level to an entry at some level (possibly the same), and from and to the constr entry. E.g.: @@ -1399,7 +1242,7 @@ type entry_coercion = notation list module EntryCoercionOrd = struct type t = notation_entry * notation_entry - let compare = Pervasives.compare + let compare = pervasives_compare end module EntryCoercionMap = Map.Make(EntryCoercionOrd) @@ -1516,7 +1359,7 @@ let uninterp_prim_token c = with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - match glob_constr_of_closed_cases_pattern c with + match glob_constr_of_closed_cases_pattern (Global.env()) c with | exception Not_found -> raise Notation_ops.No_match | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) @@ -1538,11 +1381,13 @@ let availability_of_prim_token n printer_scope local_scopes = | _ -> false with Not_found -> false in - let istype,scopes = make_current_uninterp_scopes local_scopes in - find_without_delimiters f (istype,Some printer_scope,None) scopes + let scopes = make_current_scopes local_scopes in + Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) (* Miscellaneous *) +let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 + let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 @@ -1556,10 +1401,9 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false -let var_attributes_eq (_, ((entry1, (tmpsc1, scl1)), tp1)) (_, ((entry2, (tmpsc2, scl2)), tp2)) = +let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = notation_entry_level_eq entry1 entry2 && - Option.equal String.equal tmpsc1 tmpsc2 && - List.equal String.equal scl1 scl2 && + pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && ntpe_eq tp1 tp2 let interpretation_eq (vars1, t1) (vars2, t2) = @@ -1574,17 +1418,46 @@ let exists_notation_in_scope scopt ntn onlyprint r = interpretation_eq n.not_interp r with Not_found -> false -let exists_notation_interpretation_in_scope scopt ntn = - let scope = match scopt with Some s -> s | None -> default_scope in - try - let sc = String.Map.find scope !scope_map in - let _ = NotationMap.find ntn sc.notations in - true - with Not_found -> false - let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) +(* Mapping classes to scopes *) + +open Classops + +type scope_class = cl_typ + +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord + +let compute_scope_class sigma t = + let (cl,_,_) = find_class_type sigma t in + cl + +module ScopeClassOrd = +struct + type t = scope_class + let compare = scope_class_compare +end + +module ScopeClassMap = Map.Make(ScopeClassOrd) + +let initial_scope_class_map : scope_name ScopeClassMap.t = + ScopeClassMap.empty + +let scope_class_map = ref initial_scope_class_map + +let declare_scope_class sc cl = + scope_class_map := ScopeClassMap.add cl sc !scope_class_map + +let find_scope_class cl = + ScopeClassMap.find cl !scope_class_map + +let find_scope_class_opt = function + | None -> None + | Some cl -> try Some (find_scope_class cl) with Not_found -> None + +(**********************************************************************) (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_classes sigma t = @@ -1604,6 +1477,9 @@ let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) let compute_type_scope sigma t = find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + let scope_class_of_class (x : cl_typ) : scope_class = x @@ -1657,7 +1533,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let n = try let vars = Lib.variable_section_segment_of_reference r in - vars |> List.map fst |> List.filter is_local_assum |> List.length + vars |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in Some (req,r,n,l,[]) @@ -1960,7 +1836,7 @@ let locate_notation prglob ntn scope = str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in - prlist_with_sep fnl + prlist (fun (sc,r,(_,df)) -> hov 0 ( pr_notation_info prglob df r ++ @@ -2023,18 +1899,17 @@ let pr_visibility prglob = function (* Synchronisation with reset *) let freeze ~marshallable = - (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope, + (!scope_map, !scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, !prim_token_interp_infos, !prim_token_uninterp_infos, !entry_coercion_map, !entry_has_global_map, !entry_has_ident_map) -let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; - uninterp_scope_stack := uscs; - arguments_scope := asc; delimiters_map := dlm; + arguments_scope := asc; notations_key_table := fkm; scope_class_map := clsc; prim_token_interp_infos := ptii; @@ -2045,9 +1920,8 @@ let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = let init () = init_scope_map (); - uninterp_scope_stack := []; delimiters_map := String.Map.empty; - notations_key_table := (ScopeMap.empty,KeyMap.empty); + notations_key_table := KeyMap.empty; scope_class_map := initial_scope_class_map; prim_token_interp_infos := String.Map.empty; prim_token_uninterp_infos := GlobRef.Map.empty diff --git a/interp/notation.mli b/interp/notation.mli index 57e2be16b9..bd9b50977b 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -216,10 +216,9 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of KerName.t -module InterpRuleSet : Set.S with type elt = interp_rule - val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> unit + interpretation -> notation_location -> onlyprint:bool -> + Deprecation.t option -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit @@ -227,28 +226,18 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule_core = - interp_rule (* kind of notation *) - * interpretation (* pattern associated to the notation *) - * int option (* number of expected arguments *) - -type notation_rule = - notation_rule_core - * delimiters option (* delimiter to possibly add *) - * bool (* true if the delimiter is mandatory *) +type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : inductive -> notation_rule list -(* (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option - *) (** {6 Miscellaneous} *) @@ -259,9 +248,6 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool -(** Checks for already existing notations *) -val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool - (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7d7e10a05b..f30a874426 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,7 +15,6 @@ open Names open Nameops open Constr open Globnames -open Decl_kinds open Namegen open Glob_term open Glob_ops @@ -781,8 +780,8 @@ let rec pat_binder_of_term t = DAst.map (function | GVar id -> PatVar (Name id) | GApp (t, l) -> begin match DAst.get t with - | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + | GRef (GlobRef.ConstructRef cstr,_) -> + let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) | _ -> raise No_match @@ -909,7 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) alp, add_env alp sigma var (DAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let env = Global.env () in + let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in @@ -956,7 +956,7 @@ let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 | GFix (nl1,n1), GFix (nl2,n2) -> - let test (n1, _) (n2, _) = match n1, n2 with + let test n1 n2 = match n1, n2 with | _, None -> true | Some id1, Some id2 -> Int.equal id1 id2 | _ -> false @@ -1189,7 +1189,11 @@ let rec match_ inner u alp metas sigma a1 a2 = Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 - | GSort (GType _), NSort (GType _) when not u -> sigma + + (* Next pair of lines useful only if not coming from detyping *) + | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match + | GSort _, NSort (UAnonymous _) when not u -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match @@ -1292,7 +1296,7 @@ let match_notation_constr u c (metas,pat) = | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> - let v = glob_constr_of_cases_pattern pat in + let v = glob_constr_of_cases_pattern (Global.env()) pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> @@ -1332,12 +1336,12 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) - | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 -> + let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in sigma,(0,l) - | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) + | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in + let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then @@ -1357,9 +1361,9 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 = let match_ind_pattern metas sigma ind pats a2 = match a2 with - | NRef (IndRef r2) when eq_ind ind r2 -> + | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> sigma,(0,pats) - | NApp (NRef (IndRef r2),l2) + | NApp (NRef (GlobRef.IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 58fa221b16..7919d0061f 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 6fe20486dc..908455bd05 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -38,7 +38,7 @@ type notation_constr = notation_constr * notation_constr | NIf of notation_constr * (Name.t * notation_constr option) * notation_constr * notation_constr - | NRec of fix_kind * Id.t array * + | NRec of glob_fix_kind * Id.t array * (Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort diff --git a/interp/reserve.ml b/interp/reserve.ml index edbdf1dbba..e81439c3d5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.mli b/interp/reserve.mli index a10858e71f..e180fc8071 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91491bdf8d..5d36ceca38 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -52,7 +52,7 @@ let locate_global_with_alias ?(head=false) qid = let global_inductive_with_alias qid = try match locate_global_with_alias qid with - | IndRef ind -> ind + | Names.GlobRef.IndRef ind -> ind | ref -> user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" (pr_qualid qid ++ spc () ++ str "is not an inductive type.") diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index e41ef78913..d2770a2e73 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index bf3a8fe215..555eb34aed 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index c974a4403c..dffbca0054 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 49273c4146..9dded8656c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,20 +19,24 @@ open Notation_term (* Syntactic definitions. *) -type version = Flags.compat_version option +type syndef = + { syndef_pattern : interpretation; + syndef_onlyparsing : bool; + syndef_deprecation : Deprecation.t option; + } let syntax_table = - Summary.ref (KNmap.empty : (interpretation*version) KNmap.t) - ~name:"SYNTAXCONSTANT" + Summary.ref (KNmap.empty : syndef KNmap.t) + ~name:"SYNDEFS" -let add_syntax_constant kn c onlyparse = - syntax_table := KNmap.add kn (c,onlyparse) !syntax_table +let add_syntax_constant kn syndef = + syntax_table := KNmap.add kn syndef !syntax_table -let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = +let load_syntax_constant i ((sp,kn),(_local,syndef)) = if Nametab.exists_cci sp then user_err ~hdr:"cache_syntax_constant" (Id.print (basename sp) ++ str " already exists"); - add_syntax_constant kn pat onlyparse; + add_syntax_constant kn syndef; Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function @@ -42,30 +46,29 @@ let is_alias_of_already_visible_name sp = function | _ -> false -let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = +let open_syntax_constant i ((sp,kn),(_local,syndef)) = + let pat = syndef.syndef_pattern in if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; - match onlyparse with - | None -> + if not syndef.syndef_onlyparsing then (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) + notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat - | _ -> () end let cache_syntax_constant d = load_syntax_constant 1 d; open_syntax_constant 1 d -let subst_syntax_constant (subst,(local,pat,onlyparse)) = - (local,Notation_ops.subst_interpretation subst pat,onlyparse) +let subst_syntax_constant (subst,(local,syndef)) = + let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in + (local, { syndef with syndef_pattern }) -let classify_syntax_constant (local,_,_ as o) = +let classify_syntax_constant (local,_ as o) = if local then Dispose else Substitute o -let in_syntax_constant - : bool * interpretation * Flags.compat_version option -> obj = - declare_object {(default_object "SYNTAXCONSTANT") with +let in_syntax_constant : (bool * syndef) -> obj = + declare_object {(default_object "SYNDEF") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; open_function = open_syntax_constant; @@ -79,36 +82,31 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) -let declare_syntactic_definition local id onlyparse pat = - let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () - -let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) - -let pr_compat_warning (kn, def, v) = - let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r - | _ -> strbrk " is a compatibility notation" +let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = + let syndef = + { syndef_pattern = in_pat pat; + syndef_onlyparsing = onlyparsing; + syndef_deprecation = deprecation; + } in - pr_syndef kn ++ pp_def + let _ = add_leaf id (in_syntax_constant (local,syndef)) in () -let warn_compatibility_notation = - CWarnings.(create ~name:"compatibility-notation" - ~category:"deprecated" ~default:Enabled pr_compat_warning) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) -let verbose_compat ?loc kn def = function - | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation ?loc (kn, def, v) - | _ -> () +let warn_deprecated_syntactic_definition = + Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition" + pr_syndef let search_syntactic_definition ?loc kn = - let pat,v = KNmap.find kn !syntax_table in - let def = out_pat pat in - verbose_compat ?loc kn def v; + let syndef = KNmap.find kn !syntax_table in + let def = out_pat syndef.syndef_pattern in + Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; def let search_filtered_syntactic_definition ?loc filter kn = - let pat,v = KNmap.find kn !syntax_table in - let def = out_pat pat in + let syndef = KNmap.find kn !syntax_table in + let def = out_pat syndef.syndef_pattern in let res = filter def in - (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + if Option.has_some res then + Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 77873f8f67..0065b45b14 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,8 +15,8 @@ open Notation_term type syndef_interpretation = (Id.t * subscopes) list * notation_constr -val declare_syntactic_definition : bool -> Id.t -> - Flags.compat_version option -> syndef_interpretation -> unit +val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> + onlyparsing:bool -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation |