From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- interp/constrextern.ml | 58 +++++++++++++++++------------------- interp/constrextern.mli | 4 +-- interp/constrintern.ml | 31 +++++++++---------- interp/constrintern.mli | 2 +- interp/coqlib.ml | 2 +- interp/coqlib.mli | 2 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 2 +- interp/genarg.ml | 2 +- interp/genarg.mli | 2 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- interp/modintern.ml | 2 +- interp/modintern.mli | 2 +- interp/notation.ml | 35 ++++++++++++++++------ interp/notation.mli | 2 +- interp/ppextend.ml | 2 +- interp/ppextend.mli | 2 +- interp/reserve.ml | 2 +- interp/reserve.mli | 2 +- interp/smartlocate.ml | 2 +- interp/smartlocate.mli | 2 +- interp/syntax_def.ml | 66 +++++++++++++++++++++++++++++++++++------ interp/syntax_def.mli | 12 ++++++-- interp/topconstr.ml | 2 +- interp/topconstr.mli | 2 +- 26 files changed, 157 insertions(+), 89 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 82e3cbe1..19e1fef5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* check_same_type a1 a2; check_same_type b1 b2 - | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 -> + | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when proj1=proj2 -> + check_same_ref r1 r2; List.iter2 check_same_type al1 al2 | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) -> check_same_type e1 e2; @@ -249,7 +250,7 @@ and check_same_fix_binder bl1 bl2 = check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2) | _ -> failwith "not same binder") bl1 bl2 -let same c d = try check_same_type c d; true with _ -> false +let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -293,7 +294,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn then expand_curly_brackets loc mknot ntn l else match ntn,List.map destprim l with - (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) + (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p -> mknot (loc,ntn,([mknot (loc,"( _ )",l)])) | _ -> @@ -662,12 +663,12 @@ let rec extern inctx scopes vars r = | GProd (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in - let (idl,c) = factorize_prod scopes (add_vname vars na) t c in + let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c) | GLambda (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in - let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in + let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) | GCases (loc,sty,rtntypopt,tml,eqns) -> @@ -753,30 +754,25 @@ and extern_typ (_,scopes) = and sub_extern inctx (_,scopes) = extern inctx (None,scopes) -and factorize_prod scopes vars aty c = - try - if !Flags.raw_print or !print_no_symbol then raise No_match; - ([],extern_symbol scopes vars c (uninterp_notations c)) - with No_match -> match c with - | GProd (loc,(Name id as na),bk,ty,c) - when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) - & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) - -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in - ((loc,Name id)::nal,c) - | c -> ([],extern_typ scopes vars c) - -and factorize_lambda inctx scopes vars aty c = - try - if !Flags.raw_print or !print_no_symbol then raise No_match; - ([],extern_symbol (Some Notation.type_scope,snd scopes) vars c (uninterp_notations c)) - with No_match -> match c with - | GLambda (loc,na,bk,ty,c) - when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) - & not (occur_name na aty) (* To avoid na in ty' escapes scope *) - -> let (nal,c) = - factorize_lambda inctx scopes (add_vname vars na) aty c in - ((loc,na)::nal,c) - | c -> ([],sub_extern inctx scopes vars c) +and factorize_prod scopes vars na bk aty c = + let c = extern_typ scopes vars c in + match na, c with + | Name id, CProdN (loc,[nal,Default bk',ty],c) + when bk = bk' && is_same_type aty ty + & not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> + nal,c + | _ -> + [],c + +and factorize_lambda inctx scopes vars na bk aty c = + let c = sub_extern inctx scopes vars c in + match c with + | CLambdaN (loc,[nal,Default bk',ty],c) + when bk = bk' && is_same_type aty ty + & not (occur_name na ty) (* avoid na in ty escapes scope *) -> + nal,c + | _ -> + [],c and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -790,7 +786,7 @@ and extern_local_binder scopes vars = function let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Idset.add na vars) l with (assums,ids,LocalRawAssum(nal,k,ty')::l) - when same ty ty' & + when is_same_type ty ty' & match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 2a53eb85..1a1560e5 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr_expr -> unit +val is_same_type : constr_expr -> constr_expr -> bool (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1dd735ad..45df005c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* None & - (* scopes have no effect on the interpretation of identifiers, hence - we can tolerate having a variable occurring several times in - different scopes: *) typ <> NtnInternTypeIdent & - make_current_scope (Option.get !idscopes) - <> make_current_scope (env.tmp_scope,env.scopes) then - error_inconsistent_scope loc id - (make_current_scope (Option.get !idscopes)) - (make_current_scope (env.tmp_scope,env.scopes)) - else - idscopes := Some (env.tmp_scope,env.scopes); + if istermvar then + (* scopes have no effect on the interpretation of identifiers *) + if !idscopes = None then + idscopes := Some (env.tmp_scope,env.scopes) + else + if make_current_scope (Option.get !idscopes) + <> make_current_scope (env.tmp_scope,env.scopes) + then + error_inconsistent_scope loc id + (make_current_scope (Option.get !idscopes)) + (make_current_scope (env.tmp_scope,env.scopes)); match typ with | NtnInternTypeBinder -> if istermvar then error_expect_binder_notation_type loc id @@ -1682,7 +1683,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_judgment env b in - let d = (na, Some c.uj_val, c.uj_type) in + let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in (push_rel d env, d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) in (env, par), impls diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 7d000902..7a4bba10 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* symbol_interpretation *) let scope_map = ref Gmap.empty +(* Delimiter table : delimiter -> scope_name *) +let delimiters_map = ref Gmap.empty + let empty_scope = { notations = Gmap.empty; delimiters = None @@ -74,12 +77,25 @@ let declare_scope scope = (* Flags.if_warn message ("Creating scope "^scope);*) scope_map := Gmap.add scope empty_scope !scope_map +let error_unknown_scope sc = error ("Scope "^sc^" is not declared.") + let find_scope scope = try Gmap.find scope !scope_map - with Not_found -> error ("Scope "^scope^" is not declared.") + with Not_found -> error_unknown_scope scope let check_scope sc = let _ = find_scope sc in () +(* [sc] might be here a [scope_name] or a [delimiter] + (now allowed after Open Scope) *) + +let normalize_scope sc = + try let _ = Gmap.find sc !scope_map in sc + with Not_found -> + try + let sc = Gmap.find sc !delimiters_map in + let _ = Gmap.find sc !scope_map in sc + with Not_found -> error_unknown_scope sc + (**********************************************************************) (* The global stack of scopes *) @@ -99,10 +115,13 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = - if i=1 then begin - (match sc with Scope sc -> check_scope sc | _ -> ()); - scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack - end + if i=1 then + let sc = match sc with + | Scope sc -> Scope (normalize_scope sc) + | _ -> sc + in + scope_stack := + if op then sc :: !scope_stack else list_except sc !scope_stack let cache_scope o = open_scope 1 o @@ -142,8 +161,6 @@ let make_current_scopes (tmp_scope,scopes) = (**********************************************************************) (* Delimiters *) -let delimiters_map = ref Gmap.empty - let declare_delimiters scope key = let sc = find_scope scope in let newsc = { sc with delimiters = Some key } in @@ -361,7 +378,7 @@ let interp_prim_token_gen g loc p local_scopes = with Not_found -> user_err_loc (loc,"interp_prim_token", (match p with - | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n + | Numeral n -> str "No interpretation for numeral " ++ str (to_string n) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token = diff --git a/interp/notation.mli b/interp/notation.mli index f429e377..2ecfbda7 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* syntax_table := ft); Summary.init_function = (fun () -> syntax_table := KNmap.empty) } -let add_syntax_constant kn c = - syntax_table := KNmap.add kn c !syntax_table +let add_syntax_constant kn c onlyparse = + syntax_table := KNmap.add kn (c,onlyparse) !syntax_table -let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = +let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); - add_syntax_constant kn pat; + add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function @@ -46,7 +48,7 @@ let is_alias_of_already_visible_name sp = function let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if not (is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; - if not onlyparse then + if onlyparse = None then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared inbetween *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat @@ -62,7 +64,8 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) = let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o -let in_syntax_constant : bool * interpretation * bool -> obj = +let in_syntax_constant + : bool * interpretation * Flags.compat_version option -> obj = declare_object {(default_object "SYNTAXCONSTANT") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; @@ -80,5 +83,50 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () +let pr_global r = pr_global_env Idset.empty r +let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Idset.empty kn) + +let allow_compat_notations = ref true +let verbose_compat_notations = ref false + +let is_verbose_compat () = + !verbose_compat_notations || not !allow_compat_notations + +let verbose_compat kn def = function + | Some v when is_verbose_compat () && Flags.version_strictly_greater v -> + let act = + if !verbose_compat_notations then msg_warning else errorlabstrm "" + in + let pp_def = match def with + | [], ARef r -> str " is " ++ pr_global_env Idset.empty r + | _ -> str " is a compatibility notation" + in + let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in + act (pr_syndef kn ++ pp_def ++ since) + | _ -> () + let search_syntactic_definition kn = - out_pat (KNmap.find kn !syntax_table) + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + verbose_compat kn def v; + def + +open Goptions + +let set_verbose_compat_notations = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "verbose compatibility notations"; + optkey = ["Verbose";"Compat";"Notations"]; + optread = (fun () -> !verbose_compat_notations); + optwrite = ((:=) verbose_compat_notations) } + +let set_compat_notations = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "accept compatibility notations"; + optkey = ["Compat"; "Notations"]; + optread = (fun () -> !allow_compat_notations); + optwrite = ((:=) allow_compat_notations) } diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index e4da52a3..036fe30a 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* identifier -> bool -> - syndef_interpretation -> unit +val declare_syntactic_definition : bool -> identifier -> + Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : kernel_name -> syndef_interpretation + +(** Options concerning verbose display of compatibility notations + or their deactivation *) + +val set_verbose_compat_notations : bool -> unit +val set_compat_notations : bool -> unit diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 04d39fbf..b02a67ea 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*