diff options
57 files changed, 922 insertions, 462 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index cb6e695865..42dd2dd052 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +Types `precedence`, `parenRelation`, `tolerability` in +`notgram_ops.ml` have been reworked. See `entry_level` and +`entry_relative_level` in `constrexpr.ml`. + +### ML API + Exception handling: - Coq's custom `Backtrace` module has been removed in favor of OCaml's diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index a888998ebf..d8d835d9b8 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -132,7 +132,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then warning "Your branch is ahead of ${REMOTE}." - warning "You should see this warning only if you've just merged another PR and did not push yet." + warning "On master, GitHub's branch protection rule prevents merging several PRs at once." + warning "You should run [git push ${REMOTE}] between each call to the merge script." ask_confirmation else error "Local branch is not up-to-date with ${REMOTE}." diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index 82f2e79549..da224aa5ab 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -74,6 +74,7 @@ install_printer Top_printers.ppuniverse_context_future install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval install_printer Top_printers.ppenv +install_printer Top_printers.ppglobenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f640a33773..e8129938a1 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -247,6 +247,8 @@ let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") +let ppglobenv e = ppenv (GlobEnv.env e) + let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 133326523b..ac9b63f60a 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -150,6 +150,7 @@ val ppuniverses : UGraph.t -> unit val ppnamedcontextval : Environ.named_context_val -> unit val ppenv : Environ.env -> unit +val ppglobenv : GlobEnv.t -> unit val ppenvwithcst : Environ.env -> unit val pptac : Ltac_plugin.Tacexpr.glob_tactic_expr -> unit diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst new file mode 100644 index 0000000000..51818c666b --- /dev/null +++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst @@ -0,0 +1,5 @@ +- **Added:** + :cmd:`Implicit Types` are now taken into account for printing. To inhibit it, + unset the :flag:`Printing Use Implicit Types` flag + (`#11261 <https://github.com/coq/coq/pull/11261>`_, + by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_). diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst new file mode 100644 index 0000000000..d95f554766 --- /dev/null +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -0,0 +1,17 @@ +- **Fixed:** Parsing and printing consistently handle inheritance of implicit + arguments in notations. With the exception of notations of + the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which + inhibit implicit arguments, all notations binding a partially + applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`, + or :n:`Notation @string := (@@qualid {+ @arg })`, or + :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident + := (@@qualid {+ @arg })`, inherit the remaining implicit arguments + (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo + Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and + `#11091 <https://github.com/coq/coq/pull/11091>`_). + +- **Changed:** Interpretation scopes are now always inherited in + notations binding a partially applied constant, including for + notations binding an expression of the form :n:`@@qualid`. The latter was + not the case beforehand + (part of `#11120 <https://github.com/coq/coq/pull/11120>`_). diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst new file mode 100644 index 0000000000..1d94cbf21b --- /dev/null +++ b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Notations in onlyprinting mode do not uselessly reserve parsing keywords + (`#11590 <https://github.com/coq/coq/pull/11590>`_, + by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_). diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f1dd7479c5..77cb3ecc21 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -108,7 +108,7 @@ master_doc = "index" # General information about the project. project = 'Coq' -copyright = '1999-2019, Inria, CNRS and contributors' +copyright = '1999-2020, Inria, CNRS and contributors' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f0bbaed8f3..9686500a35 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2208,6 +2208,13 @@ or :g:`m` to the type :g:`nat` of natural numbers). Adds blocks of implicit types with different specifications. +.. flag:: Printing Use Implicit Types + + By default, the type of bound variables is not printed when + the variable name is associated to an implicit type which matches the + actual type of the variable. This feature can be deactivated by + turning this flag off. + .. _implicit-generalization: Implicit generalization diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 7c628e534b..8bfcab0f4e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -417,6 +417,27 @@ identifiers or tokens starting with a single quote are dropped. Locate "exists". Locate "exists _ .. _ , _". +Inheritance of the properties of arguments of constants bound to a notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If the right-hand side of a notation is a partially applied constant, +the notation inherits the implicit arguments (see +:ref:`ImplicitArguments`) and interpretation scopes (see +:ref:`Scopes`) of the constant. For instance: + +.. coqtop:: in reset + + Record R := {dom : Type; op : forall {A}, A -> dom}. + Notation "# x" := (@op x) (at level 8). + +.. coqtop:: all + + Check fun x:R => # x 3. + +As an exception, if the right-hand side is just of the form +:n:`@@qualid`, this conventionally stops the inheritance of implicit +arguments (but not of interpretation scopes). + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -1415,6 +1436,12 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + Like for notations, if the right-hand side of an abbreviation is a + partially applied constant, the abbreviation inherits the implicit + arguments and interpretation scopes of the constant. As an + exception, if the right-hand side is just of the form :n:`@@qualid`, + this conventionally stops the inheritance of implicit arguments. + .. _numeral-notations: Numeral notations diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 1d51109b7f..4bdacda529 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -20,8 +20,12 @@ type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string + +type entry_level = int +type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome + type notation_entry = InConstrEntry | InCustomEntry of string -type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int +type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level type notation_key = string (* A notation associated to a given parsing rule *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0a3ee59f4e..4ec9f17c71 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes (* This suppresses printing of primitive tokens (e.g. numeral) and notations *) let print_no_symbol = ref false +(* This tells to skip types if a variable has this type by default *) +let print_use_implicit_types = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Use";"Implicit";"Types"] + ~value:true + +(**********************************************************************) + +let hole = CAst.make @@ CHole (None, IntroAnonymous, None) + +let is_reserved_type na t = + not !Flags.raw_print && print_use_implicit_types () && + match na with + | Anonymous -> false + | Name id -> + try + let pat = Reserve.find_reserved_type id in + let _ = match_notation_constr false t ([],pat) in + true + with Not_found | No_match -> false + (**********************************************************************) (* Turning notations and scopes on and off for printing *) module IRuleSet = Set.Make(struct @@ -381,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args) ) impl_st +let extern_record_pattern cstrsp args = + try + if !Flags.raw_print then raise Exit; + let projs = Recordops.lookup_projections (fst cstrsp) in + if PrintingRecord.active (fst cstrsp) then + () + else if PrintingConstructor.active (fst cstrsp) then + raise Exit + else if not (get_record_print ()) then + raise Exit; + let rec ip projs args acc = + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, { CAst.v = CPatAtom None } -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + let loc = pat.CAst.loc in + (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc + | _ -> raise No_match in + ip q tail acc + | _ -> assert false + in + Some (List.rev (ip projs args [])) + with + Not_found | No_match | Exit -> None + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try @@ -415,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in let p = - try - if !Flags.raw_print then raise Exit; - let projs = Recordops.lookup_projections (fst cstrsp) in - let rec ip projs args acc = - match projs, args with - | [], [] -> acc - | proj :: q, pat :: tail -> - let acc = - match proj, pat with - | _, { CAst.v = CPatAtom None } -> - (* we don't want to have 'x := _' in our patterns *) - acc - | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc) - | _ -> raise No_match in - ip q tail acc - | _ -> assert false - in - CPatRecord(List.rev (ip projs args [])) - with - Not_found | No_match | Exit -> + match extern_record_pattern cstrsp args with + | Some l -> CPatRecord l + | None -> let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp @@ -451,7 +485,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = in insert_pat_coercion coercion pat -and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) +and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args)) (custom, (tmp_scope, scopes) as allscopes) vars = function | NotationRule (_,ntn as specific_ntn) -> @@ -474,10 +508,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let subscope = (subentry,(scopt,scl@scopes')) in List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in - let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in + let subscopes = find_arguments_scope gr in + let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in + let more_args = fill_arg_scopes more_args more_args_scopes allscopes in + let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else - match drop_implicits_in_patt gr nb_to_drop l2 with + if no_implicit then l2 else + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in @@ -494,10 +532,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in - let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in + let subscopes = find_arguments_scope gr in + let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in + let more_args = fill_arg_scopes more_args more_args_scopes allscopes in + let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () then l2 else - match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with + if no_implicit then l2 else + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in @@ -720,7 +762,7 @@ let extern_applied_ref inctx impl (cf,f) us args = let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs = try let syndefargs = List.map (fun a -> (a,None)) syndefargs in - let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in + let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in let args = syndefargs @ extraargs in if args = [] then cf else CApp ((None, CAst.make cf), args) with Expl -> @@ -740,8 +782,10 @@ let extern_applied_notation n impl f args = if List.is_empty args then f.CAst.v else - let args = adjust_implicit_arguments false (List.length args) 1 args impl in + try + let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in mkFlattenedCApp (f,args) + with Expl -> raise No_match let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in @@ -790,6 +834,12 @@ let rec flatten_application c = match DAst.get c with end | a -> c +let same_binder_type ty nal c = + match nal, DAst.get c with + | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty' + | [], _ -> true + | _ -> assert false + (**********************************************************************) (* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) @@ -939,12 +989,10 @@ let rec extern inctx scopes vars r = extern inctx scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_prod scopes (add_vname vars na) na bk t c + factorize_prod scopes vars na bk t c | GLambda (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_lambda inctx scopes (add_vname vars na) na bk t c + factorize_lambda inctx scopes vars na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -973,17 +1021,19 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in + let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map CAst.make nal, + let inctx = inctx || typopt <> None in + CLetTuple (List.map CAst.make nal, (Option.map (fun _ -> (make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (c,(na,typopt),b1,b2) -> + let inctx = inctx || typopt <> None in CIf (sub_extern false scopes vars c, (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), @@ -1006,7 +1056,7 @@ let rec extern inctx scopes vars r = | 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 + sub_extern true scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> @@ -1017,7 +1067,7 @@ let rec extern inctx scopes vars r = 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 ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), - sub_extern false scopes vars1 bv.(i))) idv + sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) @@ -1043,7 +1093,10 @@ and extern_typ (subentry,(_,scopes)) = and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) -and factorize_prod scopes vars na bk aty c = +and factorize_prod scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1060,18 +1113,25 @@ and factorize_prod scopes vars na bk aty c = | _ -> CProdN ([binder],b)) | _ -> assert false) | _, _ -> - let c = extern_typ scopes vars c in - match na, c.v with + let c' = extern_typ scopes vars c in + match na, c'.v with | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + when binding_kind_eq bk bk' + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let ty = if implicit_type then ty else aty in + CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b) | _, CProdN (bl,b) -> - CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CProdN (CLocalAssum([make na],Default bk,ty)::bl,b) | _, _ -> - CProdN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CProdN ([CLocalAssum([make na],Default bk,ty)],c') -and factorize_lambda inctx scopes vars na bk aty c = +and factorize_lambda inctx scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1088,16 +1148,20 @@ and factorize_lambda inctx scopes vars na bk aty c = | _ -> CLambdaN ([binder],b)) | _ -> assert false) | _, _ -> - let c = sub_extern inctx scopes vars c in - match c.v with + let c' = sub_extern inctx scopes vars c in + match c'.v with | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + when binding_kind_eq bk bk' + && not (occur_name na ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let aty = if implicit_type then ty else aty in CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) | CLambdaN (bl,b) -> - CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b) | _ -> - CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CLambdaN ([CLocalAssum([make na],Default bk,ty)],c') and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -1111,15 +1175,17 @@ and extern_local_binder scopes vars = function Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> + let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) - when constr_expr_eq ty ty' && + when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> + let ty = if implicit_type then hole else ty in (na::assums,na::ids, CLocalAssum([CAst.make na],Default bk,ty) :: l)) @@ -1163,24 +1229,21 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [], [] in (* Adjust to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match n with - | Some n when nallargs >= n && nallargs > 0 -> + | Some n when nallargs >= n -> let args1, args2 = List.chop n args in let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in - let args2impls = try List.skipn n argsimpls with Failure _ -> [] in - (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) - (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), - args2, args2scopes, args2impls - | None when nallargs > 0 -> + let args2impls = + if n = 0 then + (* Note: NApp(NRef f,[]), hence n=0, encodes @f and + conventionally deactivates implicit arguments *) + [] + else try List.skipn n argsimpls with Failure _ -> [] in + DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls + | None -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | Some 0 when nallargs = 0 -> - begin match DAst.get f with - | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], [] - | _ -> t, [], [], [] - end - | None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1cfd50e26e..c39e61083d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c = (**********************************************************************) (* Syntax extensions *) +let check_not_notation_variable f ntnvars = + (* Check bug #4690 *) + match DAst.get f with + | GVar id when Id.Map.mem id ntnvars -> + user_err (str "Prefix @ is not applicable to notation variables.") + | _ -> + () + let option_mem_assoc id = function | Some (id',c) -> Id.equal id id' | None -> false @@ -1071,11 +1079,11 @@ let find_appl_head_data c = c, impls, scopes, [] | GApp (r, l) -> begin match DAst.get r with - | GRef (ref,_) when l != [] -> + | GRef (ref,_) -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, List.map (drop_first_implicits n) impls, + c, (if n = 0 then [] else List.map (drop_first_implicits n) impls), List.skipn_at_least n scopes,[] | _ -> c,[],[],[] end @@ -1659,10 +1667,11 @@ let drop_notations_pattern looked_for genv = let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc scopes) argscs pats) - | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *) test_kind top g; let () = assert (List.is_empty vars) in - Some (g, List.map (in_pat false scopes) pats, []) + let (_,argscs) = find_remaining_scopes [] pats g in + Some (g, List.map2 (in_pat_sc scopes) argscs pats, []) | NApp (NRef g,args) -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1680,7 +1689,7 @@ let drop_notations_pattern looked_for genv = test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; let (_,argscs) = find_remaining_scopes [] pats g in - Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) + Some (g,[],List.map2 (in_pat_sc scopes) argscs pats) with Not_found -> None and in_pat top scopes pt = let open CAst in @@ -1780,7 +1789,15 @@ let drop_notations_pattern looked_for genv = let (argscs1,argscs2) = find_remaining_scopes pl args g in let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in - DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) + let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in + let pat = + if List.length pl = 0 then + (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then + implicit arguments are not inherited *) + RCPatCstr (g, pl @ args, []) + else + RCPatCstr (g, pl, args) in + DAst.make ?loc @@ pat | NList (x,y,iter,terminator,revert) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -2054,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref in + check_not_notation_variable f ntnvars; (* Rem: GApp(_,f,[]) stands for @f *) if args = [] then DAst.make ?loc @@ GApp (f,[]) else smart_gapp f loc (intern_args env args_scopes (List.map fst args)) @@ -2070,9 +2088,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref - | CNotation (_,ntn,([],[],[],[])) -> + | CNotation (_,ntn,ntnargs) -> assert (Option.is_empty isproj); - let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in + let c = intern_notation intern env ntnvars loc ntn ntnargs in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d1eb50d370..59a58d643c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert = 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,[]) + | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[]) + | PatVar Anonymous, NHole _ -> sigma,(false,0,[]) | 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) + sigma,(false,0,l) | 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 (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 + if le2 > List.length l1 then raise No_match else let l1',more_args = Util.List.chop le2 l1 in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + (* Convention: notations to @f don't keep implicit arguments *) + let no_implicit = le2 = 0 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args) | r1, NList (x,y,iter,termin,revert) -> (match_cases_pattern_list (match_cases_pattern_no_more_args) - metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[]) + metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = match match_cases_pattern metas sigma a1 a2 with - | out,(_,[]) -> out + | out,(_,_,[]) -> out | _ -> raise No_match let match_ind_pattern metas sigma ind pats a2 = match a2 with | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> - sigma,(0,pats) + sigma,(false,0,pats) | NApp (NRef (GlobRef.IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in @@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 = raise No_match else let l1',more_args = Util.List.chop le2 pats in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) + let no_implicit = le2 = 0 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args) |_ -> raise No_match let reorder_canonically_substitution terms termlists metas = diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c62dac013b..2ab8b620df 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -69,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> val match_notation_constr_cases_pattern : 'a cases_pattern_g -> interpretation -> (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * - (int * 'a cases_pattern_g list) + (bool * int * 'a cases_pattern_g list) val match_notation_constr_ind_pattern : inductive -> 'a cases_pattern_g list -> interpretation -> (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * - (int * 'a cases_pattern_g list) + (bool * int * 'a cases_pattern_g list) (** {5 Matching a notation pattern against a [glob_constr]} *) diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 9f133ca9d4..427505c199 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -10,14 +10,11 @@ open Names open Extend +open Constrexpr (** Dealing with precedences *) -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list +type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = @@ -37,7 +34,4 @@ type one_notation_grammar = { notgram_prods : grammar_constr_prod_item list list; } -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} +type notation_grammar = one_notation_grammar list diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 661f9c5cad..b6699493bb 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -12,19 +12,19 @@ open Pp open CErrors open Util open Notation -open Notation_gram +open Constrexpr (* Register the level of notation for parsing and printing - (we also register a precomputed parsing rule) *) + (also register the parsing rule if not onlyprinting) *) let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty -let declare_notation_level ntn ~onlyprint parsing_rule level = +let declare_notation_level ntn parsing_rule level = try let _ = NotationMap.find ntn !notation_level_map in anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") with Not_found -> - notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map + notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map let level_of_notation ntn = NotationMap.find ntn !notation_level_map @@ -37,10 +37,11 @@ let get_defined_notations () = open Extend -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false +let entry_relative_level_eq t1 t2 = match t1, t2 with +| LevelLt n1, LevelLt n2 -> Int.equal n1 n2 +| LevelLe n1, LevelLe n2 -> Int.equal n1 n2 +| LevelSome, LevelSome -> true +| (LevelLt _ | LevelLe _ | LevelSome), _ -> false let production_position_eq pp1 pp2 = match (pp1,pp2) with | BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2 @@ -64,11 +65,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in let prod_eq (l1,pp1) (l2,pp2) = not strict || (production_level_eq l1 l2 && production_position_eq pp1 pp2) in - notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2 && List.equal (constr_entry_key_eq prod_eq) u1 u2 let level_eq = level_eq_gen false diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli index d5711569f0..d8b7e8e4c1 100644 --- a/parsing/notgram_ops.mli +++ b/parsing/notgram_ops.mli @@ -13,11 +13,12 @@ open Constrexpr open Notation_gram val level_eq : level -> level -> bool +val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit -val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level +val declare_notation_level : notation -> notation_grammar option -> level -> unit +val level_of_notation : notation -> notation_grammar option * level (** raise [Not_found] if not declared *) (** Returns notations with defined parsing/printing rules *) diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 2154f2f881..12311f9cd9 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -2,8 +2,8 @@ Tok CLexer Extend Notation_gram -Ppextend Notgram_ops +Ppextend Pcoq G_constr G_prim diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index 92f44faec8..393ab8a302 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -12,7 +12,8 @@ open Util open Pp open CErrors open Notation -open Notation_gram +open Constrexpr +open Notgram_ops (*s Pretty-print. *) @@ -37,29 +38,30 @@ let ppcmd_of_cut = function | PpBrk(n1,n2) -> brk(n1,n2) type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut -type unparsing_rule = unparsing list * precedence +type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with - | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2 - | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2 - | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2 - | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2 + | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 + | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2 | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2 | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2) | UnpCut p1, UnpCut p2 -> p1 = p2 | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ | UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false -(* Concrete syntax for symbolic-extension table *) +(* Register generic and specific printing rules *) + let generic_notation_printing_rules = Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t) diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 7996e7696d..346fc83f5f 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -9,7 +9,6 @@ (************************************************************************) open Constrexpr -open Notation_gram (** {6 Pretty-print. } *) @@ -31,15 +30,15 @@ val ppcmd_of_cut : ppcut -> Pp.t (** Declare and look for the printing rule for symbolic notations *) type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut -type unparsing_rule = unparsing list * precedence +type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list val unparsing_eq : unparsing -> unparsing -> bool diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index bab6bfd78e..5835d75c79 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -298,7 +298,7 @@ END let pr_by_arg_tac env sigma _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t) } diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 6dd51e4e01..dd4195f2ef 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,7 +67,7 @@ val wit_by_arg_tac : val pr_by_arg_tac : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Entry.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 7843faaef3..e2b8bcb5a9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Notation_gram open Tactypes open Locus open Genredexpr @@ -73,43 +72,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function @@ -294,7 +293,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg)) + let pr_farg prtac arg = prtac LevelSome (TacArg (CAst.make arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -314,35 +313,35 @@ let string_of_genarg_arg (ArgumentType arg) = let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t = fun prtac symb arg -> match symb with - | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac LevelSome arg | Extend.Ulist1 s | Extend.Ulist0 s -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_sequence (pr_any_arg prtac s) l end | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l end | Extend.Uopt s -> begin match get_opt arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_opt (pr_any_arg prtac s) l end | Extend.Uentry _ | Extend.Uentryl _ -> - str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> - prtac (1, Any) arg - | Extend.Uentryl (_, l) -> prtac (l, Any) arg + prtac LevelSome arg + | Extend.Uentryl (_, l) -> prtac LevelSome arg | _ -> match arg with | TacGeneric arg -> let pr l arg = prtac l (TacGeneric arg) in pr_any_arg pr symb arg - | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_raw_extend_rec prtac = pr_extend_gen (pr_farg prtac) @@ -630,7 +629,7 @@ let pr_goal_selector ~toplevel s = let pr_then () = str ";" - let ltop = (5,E) + let ltop = LevelLe 5 let lseq = 4 let ltactical = 3 let lorelse = 2 @@ -645,13 +644,13 @@ let pr_goal_selector ~toplevel s = let ltatom = 1 let linfo = 5 - let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq + let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels *) type 'a printer = { - pr_tactic : tolerability -> 'tacexpr -> Pp.t; + pr_tactic : entry_relative_level -> 'tacexpr -> Pp.t; pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t; @@ -780,7 +779,7 @@ let pr_goal_selector ~toplevel s = hov 1 ( primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++ - pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacAssert (ev,_,None,ipat,c) -> hov 1 ( @@ -857,7 +856,7 @@ let pr_goal_selector ~toplevel s = pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl - ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( @@ -893,11 +892,11 @@ let pr_goal_selector ~toplevel s = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with | TacAbstract (t,None) -> - keyword "abstract " ++ pr_tac (labstract,L) t, labstract + keyword "abstract " ++ pr_tac (LevelLt labstract) t, labstract | TacAbstract (t,Some s) -> hov 0 ( keyword "abstract" - ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () + ++ str" (" ++ pr_tac (LevelLt labstract) t ++ str")" ++ spc () ++ keyword "using" ++ spc () ++ pr_id s), labstract | TacLetIn (recflag,llc,u) -> @@ -906,7 +905,7 @@ let pr_goal_selector ~toplevel s = (hv 0 ( pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc ++ spc () ++ keyword "in" - ) ++ fnl () ++ pr_tac (llet,E) u), + ) ++ fnl () ++ pr_tac (LevelLe llet) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( @@ -931,17 +930,17 @@ let pr_goal_selector ~toplevel s = hov 2 ( keyword "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () - ++ pr_tac (lfun,E) body), + ++ pr_tac (LevelLe lfun) body), lfun | TacThens (t,tl) -> hov 1 ( - pr_tac (lseq,E) t ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t ++ pr_then () ++ spc () ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl), lseq | TacThen (t1,t2) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () - ++ pr_tac (lseq,L) t2), + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () + ++ pr_tac (LevelLt lseq) t2), lseq | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl, lseq @@ -949,78 +948,78 @@ let pr_goal_selector ~toplevel s = pr_tac_extend (pr_tac ltop) tf t tr , lseq | TacThens3parts (t1,tf,t2,tl) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () ++ pr_then_gen (pr_tac ltop) tf t2 tl), lseq | TacTry t -> hov 1 ( - keyword "try" ++ spc () ++ pr_tac (ltactical,E) t), + keyword "try" ++ spc () ++ pr_tac (LevelLe ltactical) t), ltactical | TacDo (n,t) -> hov 1 ( str "do" ++ spc () ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTimeout (n,t) -> hov 1 ( keyword "timeout " ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTime (s,t) -> hov 1 ( keyword "time" ++ pr_opt qstring s ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacRepeat t -> hov 1 ( keyword "repeat" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacProgress t -> hov 1 ( keyword "progress" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacShowHyps t -> hov 1 ( keyword "infoH" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacInfo t -> hov 1 ( keyword "info" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), linfo | TacOr (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "+" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacOnce t -> hov 1 ( keyword "once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacExactlyOnce t -> hov 1 ( keyword "exactly_once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacIfThenCatch (t,tt,te) -> hov 1 ( - str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ - str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ - str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + str"tryif" ++ spc() ++ pr_tac (LevelLe ltactical) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (LevelLe ltactical) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (LevelLe ltactical) te ++ brk(1,1)), ltactical | TacOrelse (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "||" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacFail (g,n,l) -> let arg = @@ -1042,7 +1041,7 @@ let pr_goal_selector ~toplevel s = | TacSolve tl -> keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - pr_tac (lcomplete,E) t, lcomplete + pr_tac (LevelLe lcomplete) t, lcomplete | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom @@ -1398,10 +1397,10 @@ let () = let () = let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_tactic printer printer printer - ltop (0,E) + ltop (LevelLe 0) let () = let pr_unit _env _sigma _ _ _ _ () = str "()" in let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit - ltop (0,E) + ltop (LevelLe 0) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 9cff3ea1eb..33db933168 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -16,7 +16,6 @@ open Geninterp open Names open Environ open Constrexpr -open Notation_gram open Genintern open Tacexpr open Tactypes @@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level : 'a raw_extra_genarg_printer_with_level -> 'b glob_extra_genarg_printer_with_level -> 'c extra_genarg_printer_with_level -> - (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t +val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t @@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('b, 'a) match_rule -> Pp.t -val pr_value : tolerability -> Val.t -> Pp.t +val pr_value : entry_relative_level -> Val.t -> Pp.t -val ltop : tolerability +val ltop : entry_relative_level -val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) -> +val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) -> 'a Genprint.top_printer diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 21b832a326..3f67d55e73 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -90,7 +90,7 @@ let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Notation_gram.E) +let tacltop = (LevelLe 5) let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index e6b1706b41..53c895f9d9 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -15,12 +15,12 @@ open Ltac_plugin val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> - (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) -> 'c val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> - (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) -> 'c -> 'd val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/pretyping/cases.ml b/pretyping/cases.ml index abc16f621e..55c1f41c2c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1817,6 +1817,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in + let typ = lift n typ in let d = LocalAssum (annotR (alias_of_pat pat),typ) in let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index fd2dc7c2fc..e85f6327f8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -19,6 +19,7 @@ open Evd (** Typecheck a term and return its type. May trigger an evarmap leak. *) val unsafe_type_of : env -> evar_map -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) diff --git a/printing/genprint.ml b/printing/genprint.ml index a04df31d30..a673cbd933 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -19,15 +19,15 @@ open Geninterp (* Printing generic values *) type 'a with_level = - { default_already_surrounded : Notation_gram.tolerability; - default_ensure_surrounded : Notation_gram.tolerability; + { default_already_surrounded : Constrexpr.entry_relative_level; + default_ensure_surrounded : Constrexpr.entry_relative_level; printer : 'a } type printer_result = | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/genprint.mli b/printing/genprint.mli index 21b8417ffa..59e36baeb6 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -13,15 +13,15 @@ open Genarg type 'a with_level = - { default_already_surrounded : Notation_gram.tolerability; - default_ensure_surrounded : Notation_gram.tolerability; + { default_already_surrounded : Constrexpr.entry_relative_level; + default_ensure_surrounded : Constrexpr.entry_relative_level; printer : 'a } type printer_result = | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2f60663c82..c2d760ae08 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -20,7 +20,6 @@ open Ppextend open Glob_term open Constrexpr open Constrexpr_ops -open Notation_gram open Namegen (*i*) @@ -66,21 +65,16 @@ let tag_var = tag Tag.variable let lapp = 10 let lposint = 0 let lnegint = 35 (* must be consistent with Notation "- x" *) - let ltop = (200,E) + let ltop = LevelLe 200 let lproj = 1 let ldelim = 1 - let lsimpleconstr = (8,E) - let lsimplepatt = (1,E) - - let prec_less child (parent,assoc) = - if parent < 0 && Int.equal child lprod then true - else - let parent = abs parent in - match assoc with - | E -> (<=) child parent - | L -> (<) child parent - | Prec n -> child<=n - | Any -> true + let lsimpleconstr = LevelLe 8 + let lsimplepatt = LevelLe 1 + + let prec_less child = function + | LevelLt parent -> (<) child parent + | LevelLe parent -> if parent < 0 && Int.equal child lprod then true else child <= abs parent + | LevelSome -> true let prec_of_prim_token = function | Numeral (SPlus,_) -> lposint @@ -98,22 +92,22 @@ let tag_var = tag Tag.variable let rec aux = function | [] -> mt () - | UnpMetaVar (_, prec) as unp :: l -> + | UnpMetaVar prec as unp :: l -> let c = pop env in let pp2 = aux l in - let pp1 = pr (n, prec) c in + let pp1 = pr prec c in return unp pp1 pp2 - | UnpBinderMetaVar (_, prec) as unp :: l -> + | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in let pp2 = aux l in - let pp1 = pr_patt (n, prec) c in + let pp1 = pr_patt prec c in return unp pp1 pp2 - | UnpListMetaVar (_, prec, sl) as unp :: l -> + | UnpListMetaVar (prec, sl) as unp :: l -> let cl = pop envlist in - let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in let pp2 = aux l in return unp pp1 pp2 - | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> + | UnpBinderListMetaVar (isopen, sl) as unp :: l -> let cl = pop bll in let pp2 = aux l in let pp1 = pr_binders (fun () -> aux sl) isopen cl in @@ -216,7 +210,7 @@ let tag_var = tag Tag.variable let pr_expl_args pr (a,expl) = match expl with - | None -> pr (lapp,L) a + | None -> pr (LevelLt lapp) a | Some {v=ExplByPos (n,_id)} -> anomaly (Pp.str "Explicitation by position not implemented.") | Some {v=ExplByName id} -> @@ -243,31 +237,32 @@ let tag_var = tag Tag.variable let las = lapp let lpator = 0 let lpatrec = 0 + let lpattop = LevelLe 200 let rec pr_patt sep inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> let pp (c, p) = - pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p + pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p in (if l = [] then str "{| |}" else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec | CPatAlias (p, na) -> - pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las + pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las | CPatCstr (c, None, []) -> pr_reference c, latom | CPatCstr (c, None, args) -> - pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp | CPatCstr (c, Some args, []) -> - str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp | CPatCstr (c, Some expl_args, extra_args) -> - surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args) - ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp + surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args) + ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp | CPatAtom (None) -> str "_", latom @@ -276,16 +271,16 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - let pp p = hov 0 (pr_patt mt (lpator,Any) p) in + let pp p = hov 0 (pr_patt mt lpattop p) in surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation (_,(_,"( _ )"),([p],[]),[]) -> - pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom + pr_patt (fun()->str"(") lpattop p ++ str")", latom | CPatNotation (which,s,(l,ll),args) -> let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in - (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not) - ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not + (if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not) + ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not | CPatPrim p -> pr_prim_token p, latom @@ -440,7 +435,7 @@ let tag_var = tag Tag.variable | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) let pr_case_item pr (tm,as_clause, in_clause) = - hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause) + hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause) let pr_case_type pr po = match po with @@ -456,17 +451,17 @@ let tag_var = tag Tag.variable pr_case_type pr po let pr_proj pr pr_app a f l = - hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + hov 0 (pr (LevelLe lproj) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") let pr_appexpl pr (f,us) l = hov 2 ( str "@" ++ pr_reference f ++ pr_universe_instance us ++ - prlist (pr_sep_com spc (pr (lapp,L))) l) + prlist (pr_sep_com spc (pr (LevelLt lapp))) l) let pr_app pr a l = hov 2 ( - pr (lapp,L) a ++ + pr (LevelLt lapp) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) let pr_record_body_gen pr l = @@ -483,7 +478,7 @@ let tag_var = tag Tag.variable let pr_dangling_with_for sep pr inherited a = match a.v with | (CFix (_,[_])|CCoFix(_,[_])) -> - pr sep (latom,E) a + pr sep (LevelLe latom) a | _ -> pr sep inherited a @@ -546,14 +541,14 @@ let tag_var = tag Tag.variable let c,l1 = List.sep_last l1 in let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in if not (List.is_empty l2) then - return (p ++ prlist (pr spc (lapp,L)) l2, lapp) + return (p ++ prlist (pr spc (LevelLt lapp)) l2, lapp) else return (p, lproj) | CAppExpl ((None,qid,us),[t]) | CApp ((_, {v = CRef(qid,us)}),[t,None]) when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var -> return ( - hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), + hov 0 (str ".." ++ pr spc (LevelLe latom) t ++ spc () ++ str ".."), larg ) | CAppExpl ((None,f,us),l) -> @@ -642,16 +637,16 @@ let tag_var = tag Tag.variable return (pr_glob_sort s, latom) | CCast (a,b) -> return ( - hv 0 (pr mt (lcast,L) a ++ spc () ++ + hv 0 (pr mt (LevelLt lcast) a ++ spc () ++ match b with - | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b - | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b - | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b + | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b + | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b + | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b | CastCoerce -> str ":>"), lcast ) | CNotation (_,(_,"( _ )"),([t],[],[],[])) -> - return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) + return (pr (fun()->str"(") ltop t ++ str")", latom) | CNotation (which,s,env) -> pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env | CGeneralization (bk,ak,c) -> @@ -659,7 +654,7 @@ let tag_var = tag Tag.variable | CPrim p -> return (pr_prim_token p, prec_of_prim_token p) | CDelimiters (sc,a) -> - return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) + return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim) in let loc = constr_loc a in pr_with_comments ?loc diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index c17ca251a8..288fb251c4 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -15,9 +15,8 @@ open Libnames open Constrexpr open Names -open Notation_gram -val prec_less : precedence -> tolerability -> bool +val prec_less : entry_level -> entry_relative_level -> bool val pr_tight_coma : unit -> Pp.t @@ -49,7 +48,7 @@ val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t -val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t +val pr_constr_expr_n : Environ.env -> Evd.evar_map -> entry_relative_level -> constr_expr -> Pp.t type term_pr = { pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; @@ -76,8 +75,8 @@ val default_term_pr : term_pr Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) -val lsimpleconstr : tolerability -val ltop : tolerability +val lsimpleconstr : entry_relative_level +val ltop : entry_relative_level val modular_constr_pr : - ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) -> - (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t + ((unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t diff --git a/printing/printer.mli b/printing/printer.mli index cd5151bd8f..24d0a8cf6a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -51,7 +51,7 @@ val enable_goal_names_printing : bool ref val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t +val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" @@ -63,7 +63,7 @@ val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t val pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t -val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t @@ -100,7 +100,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t -val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d3bce07814..3e4549f92c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -76,7 +76,6 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) -let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -117,9 +116,6 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl - let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl t - let pf_type_of gl t = pf_apply type_of gl t @@ -182,4 +178,12 @@ module New = struct let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t + + (* deprecated *) + let pf_unsafe_type_of gl t = + pf_apply (unsafe_type_of[@warning "-3"]) gl t + end + +(* deprecated *) +let pf_unsafe_type_of = pf_reduce unsafe_type_of[@warning "-3"] diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index aed1c89bfe..b4247f39b9 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,6 +34,7 @@ val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t val pf_last_hyp : Goal.goal sigma -> named_declaration val pf_ids_of_hyps : Goal.goal sigma -> Id.t list val pf_unsafe_type_of : Goal.goal sigma -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] val pf_type_of : Goal.goal sigma -> constr -> evar_map * types val pf_hnf_type_of : Goal.goal sigma -> constr -> types @@ -83,6 +84,7 @@ module New : sig (** WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it *) val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types + [@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved) *) diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v new file mode 100644 index 0000000000..f50866a990 --- /dev/null +++ b/test-suite/bugs/bug_4690.v @@ -0,0 +1,3 @@ +(* Check that @f is not allowed in notation when f is a notation variable *) + +Fail Notation "# g" := (@g O) (at level 0). diff --git a/test-suite/bugs/closed/bug_10917.v b/test-suite/bugs/closed/bug_10917.v new file mode 100644 index 0000000000..cdb132ede0 --- /dev/null +++ b/test-suite/bugs/closed/bug_10917.v @@ -0,0 +1,4 @@ +(* This was raising an anomaly *) + +Definition m (h : 0 = 1) P : P 1 -> P 0 := + fun H => match h, H with end. diff --git a/test-suite/bugs/closed/bug_11552.v b/test-suite/bugs/closed/bug_11552.v new file mode 100644 index 0000000000..189b1d9d8a --- /dev/null +++ b/test-suite/bugs/closed/bug_11552.v @@ -0,0 +1,9 @@ +From Ltac2 Require Import Ltac2. + +Goal True. +Proof. + Search unit. + (* Unbound constructor Search *) + Check tt. + (* Unbound constructor Check *) +Abort. diff --git a/test-suite/bugs/closed/bug_9741.v b/test-suite/bugs/closed/bug_9741.v new file mode 100644 index 0000000000..247155d8b3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9741.v @@ -0,0 +1,21 @@ +(* This was failing at parsing *) + +Notation "'a'" := tt (only printing). +Goal True. let a := constr:(1+1) in idtac a. Abort. + +(* Idem *) + +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Open Scope string_scope. + +Axiom Ox: string -> Z. + +Axiom isMMIOAddr: Z -> Prop. + +Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a"). + +Goal False. + set (f := isMMIOAddr). + set (x := f (Ox "0018")). +Abort. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 28afd06fbc..ef7667936c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -12,3 +12,8 @@ map id' (1 :: nil) : list nat map (id'' (A:=nat)) (1 :: nil) : list nat +fix f (x : nat) : option nat := match x with + | 0 => None + | S _ => x + end + : nat -> option nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 306532c0df..a7c4399e38 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x. Check map (@id'' nat) (1::nil). +Module MatchBranchesInContext. + +Set Implicit Arguments. +Set Contextual Implicit. + +Inductive option A := None | Some (a:A). +Coercion some_nat := @Some nat. +Check fix f x := match x with 0 => None | n => some_nat n end. + +End MatchBranchesInContext. diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out new file mode 100644 index 0000000000..824c260e92 --- /dev/null +++ b/test-suite/output/ImplicitTypes.out @@ -0,0 +1,26 @@ +forall b, b = b + : Prop +forall b : nat, b = b + : Prop +forall b : bool, @eq bool b b + : Prop +forall b : bool, b = b + : Prop +forall b c : bool, b = c + : Prop +forall c b : bool, b = c + : Prop +forall b1 b2, b1 = b2 + : Prop +fun b => b = b + : bool -> Prop +fix f b (n : nat) {struct n} : bool := + match n with + | 0 => b + | S p => f b p + end + : bool -> nat -> bool +∀ b c : bool, b = c + : Prop +∀ b1 b2, b1 = b2 + : Prop diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v new file mode 100644 index 0000000000..dbc83f9229 --- /dev/null +++ b/test-suite/output/ImplicitTypes.v @@ -0,0 +1,37 @@ +Implicit Types b : bool. +Check forall b, b = b. + +(* Check the type is not used if not the reserved one *) +Check forall b:nat, b = b. + +(* Check full printing *) +Set Printing All. +Check forall b, b = b. +Unset Printing All. + +(* Check printing of type *) +Unset Printing Use Implicit Types. +Check forall b, b = b. +Set Printing Use Implicit Types. + +(* Check factorization: we give priority on factorization over implicit type *) +Check forall b c, b = c. +Check forall c b, b = c. + +(* Check factorization of implicit types *) +Check forall b1 b2, b1 = b2. + +(* Check in "fun" *) +Check fun b => b = b. + +(* Check in binders *) +Check fix f b n := match n with 0 => b | S p => f b p end. + +(* Check in notations *) +Module Notation. + Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + Check forall b c, b = c. + Check forall b1 b2, b1 = b2. +End Notation. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index b870fa6f6f..53ad8a9612 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -107,14 +107,15 @@ fun x : option Z => match x with end : option Z -> Z fun x : option Z => match x with - | SOME2 x0 => x0 - | NONE2 => 0 + | SOME3 _ x0 => x0 + | NONE3 _ => 0 end : option Z -> Z -fun x : list ?T => match x with - | NIL => NONE2 - | (_ :') t => SOME2 t - end +fun x : list ?T => +match x with +| NIL => NONE3 (list ?T) +| (_ :') t => SOME3 (list ?T) t +end : list ?T -> option (list ?T) where ?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1, diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index c5b4d6f291..f59306c454 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -78,11 +78,11 @@ f T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b -p +u ?A : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where ?A : [ |- Type] -p +u ?A : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where ?A : [ |- Type] @@ -90,23 +90,23 @@ u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b -p 0 0 +u nat 0 0 ?B : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -p 0 0 +u nat 0 0 bool : forall b : bool, 0 = 0 /\ b = b -@p nat 0 0 +u nat 0 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b -@p nat 0 0 +u nat 0 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b u : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where ?A : [ |- Type] -u +@u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b -u +@u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b u : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b @@ -138,7 +138,7 @@ v 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -v 0 (B:=bool) true +v 0 true : 0 = 0 /\ true = true v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b @@ -158,7 +158,7 @@ v 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -v 0 (B:=bool) true +v 0 true : 0 = 0 /\ true = true v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b @@ -188,15 +188,15 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -p +## ?A : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where ?A : [ |- Type] @@ -204,45 +204,109 @@ where : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b ## : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b -p 0 +## nat 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b -p 0 +## nat 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b -@p nat 0 0 +## nat 0 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b -p 0 0 +## nat 0 0 ?B : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -p 0 0 +## nat 0 0 ?B : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -p 0 0 +## nat 0 0 bool : forall b : bool, 0 = 0 /\ b = b -p 0 0 true +## nat 0 0 bool true : 0 = 0 /\ true = true ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true +# 0 0 bool 0%bool + : T +fun a : T => match a with + | # 0 0 _ _ => 1 + | _ => 2 + end + : T -> nat +#' 0 0 0%bool + : T +fun a : T => match a with + | #' 0 0 _ => 1 + | _ => 2 + end + : T -> nat +## 0 0 0%bool + : T +fun a : T => match a with + | ## 0 0 _ => 1 + | _ => 2 + end + : T -> nat +##' 0 0 0%bool + : T +fun a : T => match a with + | ##' 0 0 _ => 1 + | _ => 2 + end + : T -> nat +P 0 0 bool 0%bool + : T +fun a : T => match a with + | P 0 0 _ _ => 1 + | _ => 2 + end + : T -> nat +P' 0 0 0%bool + : T +fun a : T => match a with + | P' 0 0 _ => 1 + | _ => 2 + end + : T -> nat +Q 0 0 0%bool + : T +fun a : T => match a with + | Q 0 0 _ => 1 + | _ => 2 + end + : T -> nat +Q' 0 0 0%bool + : T +fun a : T => match a with + | Q' 0 0 _ => 1 + | _ => 2 + end + : T -> nat diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index b3bea929ba..09d5e31c48 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -115,21 +115,21 @@ Module AppliedTermsPrinting. Notation u := @p. Check u _. - (* p *) + (* u ?A *) Check p. - (* p *) + (* u ?A *) Check @p. (* u *) Check u. (* u *) Check p 0 0. - (* p 0 0 *) + (* u nat 0 0 ?B *) Check u nat 0 0 bool. - (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *) + (* u nat 0 0 bool *) Check u nat 0 0. - (* @p nat 0 0 *) + (* u nat 0 0 *) Check @p nat 0 0. - (* @p nat 0 0 *) + (* u nat 0 0 *) End AtAbbreviationForApplicationHead. @@ -145,9 +145,9 @@ Module AppliedTermsPrinting. Check p. (* u *) Check @p. - (* u -- BUG *) + (* @u *) Check @u. - (* u -- BUG *) + (* @u *) Check u. (* u *) Check p 0 0. @@ -181,7 +181,7 @@ Module AppliedTermsPrinting. Check v 0. (* v 0 *) Check v 0 true. - (* v 0 (B:=bool) true -- BUG *) + (* v 0 true *) Check @p nat 0. (* v *) Check @p nat 0 0. @@ -209,7 +209,7 @@ Module AppliedTermsPrinting. Check v 0. (* v 0 *) Check v 0 true. - (* v 0 (B:=bool) true -- BUG *) + (* v 0 true *) Check @p nat 0. (* v *) Check @p nat 0 0. @@ -243,9 +243,9 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 (B:=bool). @@ -263,25 +263,25 @@ Module AppliedTermsPrinting. Notation "##" := @p (at level 0). Check p. - (* p *) + (* ## ?A *) Check @p. (* ## *) Check ##. (* ## *) Check p 0. - (* p 0 -- why not "## nat 0" *) + (* ## nat 0 *) Check ## nat 0. - (* p 0 *) + (* ## nat 0 *) Check ## nat 0 0. - (* @p nat 0 0 *) + (* ## nat 0 0 *) Check p 0 0. - (* p 0 0 *) + (* ## nat 0 0 ?B *) Check ## nat 0 0 _. - (* p 0 0 *) + (* ## nat 0 0 ?B *) Check ## nat 0 0 bool. - (* p 0 0 (B:=bool) *) + (* ## nat 0 0 bool *) Check ## nat 0 0 bool true. - (* p 0 0 true *) + (* ## nat 0 0 bool true *) End AtNotationForHeadApplication. @@ -298,16 +298,16 @@ Module AppliedTermsPrinting. (* ## 0 *) Check ## 0. (* ## 0 *) - (* Check ## 0 0. *) - (* Anomaly *) + Check ## 0 0. + (* ## 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) - Check ## 0 0 bool. - (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) - Check ## 0 0 bool true. - (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *) + (* ## 0 0 true *) + Check ## 0 0 true. + (* ## 0 0 true *) End NotationForPartialApplication. @@ -324,17 +324,75 @@ Module AppliedTermsPrinting. (* ## 0 *) Check ## 0. (* ## 0 *) - (* Check ## 0 0. *) - (* Anomaly *) + Check ## 0 0. + (* ## 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) - Check ## 0 0 bool. - (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) - Check ## 0 0 bool true. - (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *) + (* ## 0 0 true *) + Check ## 0 0 true. + (* ## 0 0 true *) End AtNotationForPartialApplication. End AppliedTermsPrinting. + +Module AppliedPatternsPrinting. + + (* Other tests testing inheritance of scope and implicit in + term and pattern for parsing and printing *) + + Inductive T := p (a:nat) (b:bool) {B} (b:B) : T. + Notation "0" := true : bool_scope. + + Module A. + Notation "#" := @p (at level 0). + Check # 0 0 _ true. + Check fun a => match a with # 0 0 _ _ => 1 | _ => 2 end. (* !! *) + End A. + + Module B. + Notation "#'" := p (at level 0). + Check #' 0 0 true. + Check fun a => match a with #' 0 0 _ => 1 | _ => 2 end. + End B. + + Module C. + Notation "## q" := (@p q) (at level 0, q at level 0). + Check ## 0 0 true. + Check fun a => match a with ## 0 0 _ => 1 | _ => 2 end. + End C. + + Module D. + Notation "##' q" := (p q) (at level 0, q at level 0). + Check ##' 0 0 true. + Check fun a => match a with ##' 0 0 _ => 1 | _ => 2 end. + End D. + + Module E. + Notation P := @ p. + Check P 0 0 _ true. + Check fun a => match a with P 0 0 _ _ => 1 | _ => 2 end. + End E. + + Module F. + Notation P' := p. + Check P' 0 0 true. + Check fun a => match a with P' 0 0 _ => 1 | _ => 2 end. + End F. + + Module G. + Notation Q q := (@p q). + Check Q 0 0 true. + Check fun a => match a with Q 0 0 _ => 1 | _ => 2 end. + End G. + + Module H. + Notation Q' q := (p q). + Check Q' 0 0 true. + Check fun a => match a with Q' 0 0 _ => 1 | _ => 2 end. + End H. + +End AppliedPatternsPrinting. diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index d9a649fadc..71a8afa131 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,6 +20,8 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. +Set Printing Records. + Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 525ca48bee..04514c15cb 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -67,9 +67,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.34} in -let ff := Type@{UnivBinders.36} in tt -> ff - : Type@{max(UnivBinders.33,UnivBinders.35)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -142,16 +142,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.59 UnivBinders.60} : -Type@{UnivBinders.59} -> Type@{i} -(* i UnivBinders.59 UnivBinders.60 |= *) +axfoo@{i UnivBinders.58 UnivBinders.59} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.58 UnivBinders.59 |= *) axfoo is universe polymorphic Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.59 UnivBinders.60} : -Type@{UnivBinders.60} -> Type@{i} -(* i UnivBinders.59 UnivBinders.60 |= *) +axbar@{i UnivBinders.58 UnivBinders.59} : +Type@{UnivBinders.59} -> Type@{i} +(* i UnivBinders.58 UnivBinders.59 |= *) axbar is universe polymorphic Arguments axbar _%type_scope diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index aa439fae12..f166a53256 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -7,21 +7,21 @@ The convention is: Constant foo with implicit arguments and scopes used in a term or a pattern: foo do not deactivate further arguments and scopes - @foo deactivates further arguments and scopes - (foo x) deactivates further arguments and scopes - (@foo x) deactivates further arguments and scopes + @foo deactivate further arguments and scopes + (foo x) deactivate further arguments and scopes + (@foo x) deactivate further arguments and scopes Notations binding to foo: # := foo do not deactivate further arguments and scopes -# := @foo deactivates further arguments and scopes -# x := foo x deactivates further arguments and scopes -# x := @foo x deactivates further arguments and scopes +# := @foo deactivate further arguments and scopes +# x := foo x do not deactivate further arguments and scopes +# x := @foo x do not deactivate further arguments and scopes Abbreviations binding to foo: f := foo do not deactivate further arguments and scopes -f := @foo deactivates further arguments and scopes +f := @foo deactivate further arguments and scopes f x := foo x do not deactivate further arguments and scopes f x := @foo x do not deactivate further arguments and scopes *) @@ -62,18 +62,18 @@ Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end. Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end. -(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *) +(* 5. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *) Notation "# x" := (pair' x) (at level 0, x at level 1). Check pair' 0 0 0 : prod' bool bool. -Check # 0 _ 0%bool 0%bool : prod' bool bool. -Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end. +Check # 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with # 0 y 0 => 2 | _ => 1 end. -(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *) +(* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *) Notation "## x" := ((@pair') _ x) (at level 0, x at level 1). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. -Check ## 0%bool _ 0%bool 0%bool : prod' bool bool. -Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end. +Check ## 0%bool 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ## 0%bool y 0 => 2 | _ => 1 end. (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *) Notation "###" := (@pair') (at level 0). @@ -86,10 +86,10 @@ Notation "####" := pair' (at level 0). Check #### 0 0 0 : prod' bool bool. Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. -(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *) +(* 9. Non-@id notations inherit implicit arguments and scopes *) Notation "##### x" := (pair' x) (at level 0, x at level 1). -Check ##### 0 _ 0%bool 0%bool : prod' bool bool. -Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. +Check ##### 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ##### 0 y 0 => 2 | _ => 1 end. (* 10. Check computation of binding variable through other notations *) (* it should be detected as binding variable and the scopes not being checked *) @@ -172,3 +172,25 @@ Notation "#" := 0 (only printing). Print Visibility. End Bug10750. + +Module M18. + + Module A. + Module B. + Infix "+++" := Nat.add (at level 70). + End B. + End A. +Import A. +(* Check that the notation in module B is not visible *) +Infix "+++" := Nat.add (at level 80). + +End M18. + +Module InheritanceArgumentScopes. + +Axiom p : forall (A:Type) (b:nat), A = A /\ b = b. +Check fun A n => p (A * A) (n * n). (* safety check *) +Notation q := @p. +Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *) + +End InheritanceArgumentScopes. diff --git a/test-suite/success/NotationsAndLtac.v b/test-suite/success/NotationsAndLtac.v new file mode 100644 index 0000000000..f3ec1916dc --- /dev/null +++ b/test-suite/success/NotationsAndLtac.v @@ -0,0 +1,52 @@ +(* Test that adding notations that overlap with the tactic grammar does not +* interfere with Ltac parsing. *) + +Module test1. + Notation "x [ y ]" := (fst (id x, id y)) (at level 11). + + Goal True \/ (exists x : nat, True /\ True) -> True. + Proof. + intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]]. + Qed. +End test1. + +Module test2. + Notation "x [ y ]" := (fst (id x, id y)) (at level 100). + Goal True \/ (exists x : nat, True /\ True) -> True. + Proof. + intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]]. + Qed. +End test2. + +Module test3. + Notation "x [ y ]" := (fst (id x, id y)) (at level 1). + Goal True \/ (exists x : nat, True /\ True) -> True. + Proof. + intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]]. + Qed. +End test3. + +Module test1'. + Notation "x [ [ y ] ] " := (fst (id x, id y)) (at level 11). + + Goal True \/ (exists x : nat, True /\ True) -> True. + Proof. + intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]]. + Qed. +End test1'. + +Module test2'. + Notation "x [ [ y ] ]" := (fst (id x, id y)) (at level 100). + Goal True \/ (exists x : nat, True /\ True) -> True. + Proof. + intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]]. + Qed. +End test2'. + +Module test3'. + Notation "x [ [ y ] ]" := (fst (id x, id y)) (at level 1). + Goal True \/ (exists x : nat, True /\ True) -> True. + Proof. + intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]]. + Qed. +End test3'. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index c1bd585f3f..d05640f22d 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -948,6 +948,12 @@ VERNAC { tac2mode } EXTEND VernacLtac2 fun ~pstate -> Tac2entries.call ~pstate ~default t } END +GRAMMAR EXTEND Gram + GLOBAL: tac2mode; + tac2mode: + [ [ tac = G_vernac.query_command -> { tac None } ] ]; +END + { open Stdarg diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 85f2bf3708..edb03a5c89 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -433,26 +433,17 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not then user_err (str "Inductives with uniform parameters may not have attached notations."); let indnames = List.map (fun ind -> ind.ind_name) indl in - let sigma, env_params, infos = + + (* In case of template polymorphism, we need to compute more constraints *) + let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in + + let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) = interp_params env0 udecl uparamsl paramsl in (* Interpret the arities *) let arities = List.map (intern_ind_arity env_params sigma) indl in - let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template = - let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in - if not poly && is_template then - (* In case of template polymorphism, we need to compute more constraints *) - let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in - let sigma, env_params, infos = - interp_params env0 udecl uparamsl paramsl - in - let arities = List.map (intern_ind_arity env_params sigma) indl in - sigma, env_params, infos, arities, is_template - else sigma, env_params, infos, arities, is_template - in - let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in let arities, relevances, arityconcl, indimpls = List.split4 arities in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d597707d12..def4ed942a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,7 +402,7 @@ GRAMMAR EXTEND Gram ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } - | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { Constructors ((c id)::l) } | id = identref ; c = constructor_type -> { Constructors [ c id ] } | cstr = identref; "{"; fs = record_fields; "}" -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index dfc4631572..f6f6c4f1eb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -324,11 +324,8 @@ let explain_unification_error env sigma p1 p2 = function strbrk ": cannot ensure that " ++ t ++ strbrk " is a subtype of " ++ u] | UnifUnivInconsistency p -> - if !Constrextern.print_universes then - [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] - else - [str "universe inconsistency"] + [str "universe inconsistency: " ++ + Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] | CannotSolveConstraint ((pb,env,t,u),e) -> let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ @@ -1375,13 +1372,8 @@ let _ = CErrors.register_handler explain_exn_default let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> - let msg = - if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i - else - mt() in - str "Universe inconsistency" ++ msg ++ str "." + str "Universe inconsistency." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 69d9bd4c41..afff0347f5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -286,32 +286,30 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = let open Gramlib.Gramext in function - | RightA -> (L,E) - | LeftA -> (E,L) - | NonA -> (L,L) - let precedence_of_position_and_level from_level = function - | NumLevel n, BorderProd (_,None) -> n, Prec n | NumLevel n, BorderProd (b,Some a) -> - n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp - | NumLevel n, InternalProd -> n, Prec n - | NextLevel, _ -> from_level, L - | DefaultLevel, _ -> - (* Fake value, waiting for PR#5 at herbelin's fork *) 200, - Any + (let open Gramlib.Gramext in + match a, b with + | RightA, Left -> LevelLt n + | RightA, Right -> LevelLe n + | LeftA, Left -> LevelLe n + | LeftA, Right -> LevelLt n + | NonA, _ -> LevelLt n) + | NumLevel n, _ -> LevelLe n + | NextLevel, _ -> LevelLt from_level + | DefaultLevel, _ -> LevelSome (** Computing precedences of subentries for parsing *) let precedence_of_entry_type (from_custom,from_level) = function | ETConstr (custom,_,x) when notation_entry_eq custom from_custom -> precedence_of_position_and_level from_level x - | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n + | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n | ETConstr (custom,_,(NextLevel,_)) -> user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++ quote (pr_notation_entry custom) ++ strbrk " is different from " ++ quote (pr_notation_entry from_custom) ++ str ").") - | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n - | _ -> 0, E (* should not matter *) + | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n + | _ -> LevelSome (* should not matter *) (** Computing precedences for future insertion of parentheses at the time of printing using hard-wired constr levels *) @@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function (* Possible insertion of parentheses at printing time to deal with precedence in a constr entry is managed using [prec_less] in [ppconstr.ml] *) - snd (precedence_of_position_and_level from_level x) + precedence_of_position_and_level from_level x | ETConstr (custom,_,_) -> (* Precedence of printing for a custom entry is managed using explicit insertion of entry coercions at the time of building a [constr_expr] *) - Any - | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0) - | _ -> Any (* should not matter *) + LevelSome + | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0) + | _ -> LevelSome (* should not matter *) (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) @@ -397,11 +395,11 @@ let unparsing_metavar i from typs = let prec = unparsing_precedence_of_entry_type from x in match x with | ETConstr _ | ETGlobal | ETBigint -> - UnpMetaVar (i,prec) + UnpMetaVar prec | ETPattern _ -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETIdent -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETBinder isopen -> assert false @@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level = (* We add NonTerminal for simulation but remove it afterwards *) else make true sl in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl') + | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl') | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,List.map snd sl') + UnpBinderListMetaVar (isopen,List.map snd sl') | _ -> assert false in (None, hunk) :: make_with_space b prods @@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt = if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); let symbs, l = aux (symbs,rfmt) in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) + | ETConstr _ -> UnpListMetaVar (prec,slfmt) | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,slfmt) + UnpBinderListMetaVar (isopen,slfmt) | _ -> assert false in symbs, hunk :: l | symbs, (_,UnpBox (a,b)) :: fmt -> @@ -745,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in let pr_arg_level from (lev,typ) = let pplev = function - | (n,L) when Int.equal n from -> str "at next level" - | (n,E) -> str "at level " ++ int n - | (n,L) -> str "at level below " ++ int n - | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" in - Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ - (match typ with - | ETConstr _ | ETPattern _ -> spc () ++ pplev lev - | _ -> mt ()) + | LevelLt n when Int.equal n from -> spc () ++ str "at next level" + | LevelLe n -> spc () ++ str "at level " ++ int n + | LevelLt n -> spc () ++ str "at level below " ++ int n + | LevelSome -> mt () in + Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev let pr_level ntn (from,fromlevel,args,typs) = (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++ @@ -788,7 +782,7 @@ let warn_incompatible_format = type syntax_parsing_extension = { synext_level : Notation_gram.level; synext_notation : notation; - synext_notgram : notation_grammar; + synext_notgram : notation_grammar option; } type syntax_printing_extension = { @@ -833,29 +827,30 @@ let check_and_extend_constr_grammar ntn rule = let ntn_for_grammar = rule.notgram_notation in if notation_eq ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in - let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in - if not (Notgram_ops.level_eq prec oldprec) && not oldonlyprint then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; - if oldonlyprint then raise Not_found + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in + if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + if oldparsing = None then raise Not_found with Not_found -> Egramcoq.extend_constr_grammar rule let cache_one_syntax_extension (pa_se,pp_se) = let ntn = pa_se.synext_notation in let prec = pa_se.synext_level in - let onlyprint = pa_se.synext_notgram.notgram_onlyprinting in (* Check and ensure that the level and the precomputed parsing rule is declared *) - let parsing_to_activate = + let oldparsing = try - let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn in - if not (Notgram_ops.level_eq prec oldprec) && (not oldonlyprint || onlyprint) then error_incompatible_level ntn oldprec prec; - oldonlyprint && not onlyprint + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in + if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec; + oldparsing with Not_found -> (* Declare the level and the precomputed parsing rule *) - let _ = Notgram_ops.declare_notation_level ntn ~onlyprint pa_se.synext_notgram prec in - not onlyprint in + let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in + None in (* Declare the parsing rule *) - if parsing_to_activate then - List.iter (check_and_extend_constr_grammar ntn) pa_se.synext_notgram.notgram_rules; + begin match oldparsing, pa_se.synext_notgram with + | None, Some grams -> List.iter (check_and_extend_constr_grammar ntn) grams + | _ -> (* The grammars rules are canonically derived from the string and the precedence*) () + end; (* Printing *) match pp_se with | None -> () @@ -875,7 +870,7 @@ let subst_printing_rule subst x = x let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) = (local, ({ pa_sy with - synext_notgram = { pa_sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) pa_sy.synext_notgram.notgram_rules }}, + synext_notgram = Option.map (List.map (subst_parsing_rule subst)) pa_sy.synext_notgram }, Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy) ) @@ -1416,34 +1411,36 @@ let load_notation = load_notation_common true let open_notation i (_, nobj) = - let scope = nobj.notobj_scope in - let (ntn, df) = nobj.notobj_notation in - let pat = nobj.notobj_interp in - let onlyprint = nobj.notobj_onlyprint in - let deprecation = nobj.notobj_deprecation in - let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in - let specific_ntn = (specific,ntn) in - let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - if Int.equal i 1 && fresh then begin - (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in - (* Declare the uninterpretation *) - if not nobj.notobj_onlyparse then - Notation.declare_uninterpretation (NotationRule specific_ntn) pat; - (* Declare a possible coercion *) - (match nobj.notobj_coercion with - | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry - | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n - | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n - | None -> ()) - end; - (* Declare specific format if any *) - match nobj.notobj_specific_pp_rules with - | Some pp_sy -> - if specific_format_to_declare specific_ntn pp_sy then - Ppextend.declare_specific_notation_printing_rules - specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing - | None -> () + if Int.equal i 1 then begin + let scope = nobj.notobj_scope in + let (ntn, df) = nobj.notobj_notation in + let pat = nobj.notobj_interp in + let onlyprint = nobj.notobj_onlyprint in + let deprecation = nobj.notobj_deprecation in + let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + let specific_ntn = (specific,ntn) in + let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in + if fresh then begin + (* Declare the interpretation *) + let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in + (* Declare the uninterpretation *) + if not nobj.notobj_onlyparse then + Notation.declare_uninterpretation (NotationRule specific_ntn) pat; + (* Declare a possible coercion *) + (match nobj.notobj_coercion with + | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry + | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n + | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n + | None -> ()) + end; + (* Declare specific format if any *) + match nobj.notobj_specific_pp_rules with + | Some pp_sy -> + if specific_format_to_declare specific_ntn pp_sy then + Ppextend.declare_specific_notation_printing_rules + specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing + | None -> () + end let cache_notation o = load_notation_common false 1 o; @@ -1486,7 +1483,7 @@ exception NoSyntaxRule let recover_notation_syntax ntn = let pa = try - let _,pa_rule,prec = Notgram_ops.level_of_notation ntn in + let pa_rule,prec = Notgram_ops.level_of_notation ntn in { synext_level = prec; synext_notation = ntn; synext_notgram = pa_rule } @@ -1505,7 +1502,9 @@ let recover_notation_syntax ntn = let recover_squash_syntax sy = let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in - sy :: sq.synext_notgram.notgram_rules + match sq.synext_notgram with + | Some gram -> sy :: gram + | None -> raise NoSyntaxRule (**********************************************************************) (* Main entry point for building parsing and printing rules *) @@ -1538,10 +1537,13 @@ let make_pp_rule level (typs,symbols) fmt = let make_parsing_rules (sd : SynData.syn_data) = let open SynData in let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in - let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in { + let pa_rule = + if sd.only_printing then None + else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash) + in { synext_level = sd.level; synext_notation = fst sd.info; - synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; + synext_notgram = pa_rule; } let warn_irrelevant_format = @@ -1610,7 +1612,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in (* If the only printing flag has been explicitly requested, put it back *) - let onlyprint = onlyprint || pa_sy.synext_notgram.notgram_onlyprinting in + let onlyprint = onlyprint || pa_sy.synext_notgram = None in let _,_,_,typs = pa_sy.synext_level in Some pa_sy.synext_level, typs, onlyprint, pp_sy end else None, [], false, None in |