diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 10:55:32 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 10:55:32 +0000 |
commit | 8659ff43db85c43df644da6ac08509374aabcad4 (patch) | |
tree | 83b7e6318a45245bac501f14c4ea01dfc7b99e3a /interp | |
parent | dbd84fb57142a15b11a2ead23ed651ae8b2382a8 (diff) |
Improving abbreviations/notations + backtrack of semantic change in r12439
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrextern.ml | 39 | ||||
-rw-r--r-- | interp/constrintern.ml | 52 | ||||
-rw-r--r-- | interp/constrintern.mli | 6 | ||||
-rw-r--r-- | interp/smartlocate.ml | 6 | ||||
-rw-r--r-- | interp/syntax_def.ml | 24 | ||||
-rw-r--r-- | interp/syntax_def.mli | 2 |
6 files changed, 83 insertions, 46 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e948dc6b4..60960754b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -351,7 +351,6 @@ let bind_env (sigma,sigmalist as fullsigma) var v = let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 | PatVar (_,Anonymous), AHole _ -> sigma - | a, AHole _ -> sigma | PatCstr (loc,(ind,_ as r1),args1,_), _ -> let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in @@ -361,7 +360,10 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | AApp (ARef (ConstructRef r2),l2) when r1 = r2 -> l2 | _ -> raise No_match in if List.length l2 <> nparams + List.length args1 - then raise No_match + then + (* TODO: revert partially applied notations of the form + "Notation P x := (@pair _ _ x)." *) + raise No_match else let (p2,args2) = list_chop nparams l2 in (* All parameters must be _ *) @@ -425,13 +427,26 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> - try - (* Check the number of arguments expected by the notation *) - let loc,na = match t,n with - | PatCstr (_,f,l,_), Some n when List.length l > n -> - raise No_match - | PatCstr (loc,_,_,na),_ -> loc,na - | PatVar (loc,na),_ -> loc,na in + try + match t,n with + | PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or + n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams -> + (* Abbreviation for the constructor name only *) + (match keyrule with + | NotationRule (sc,ntn) -> raise No_match + | SynDefRule kn -> + let p = + let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in + if l = [] then + CPatAtom (loc,Some qid) + else + let l = + List.map (extern_cases_pattern_in_scope allscopes vars) l in + CPatCstr (loc,qid,l) in + insert_pat_alias loc p na) + | PatCstr (_,f,l,_), Some n when List.length l > n -> + raise No_match + | PatCstr (loc,_,_,na),_ -> (* Try matching ... *) let subst,substlist = match_aconstr_cases_pattern t pat in (* Try availability of interpretation ... *) @@ -458,8 +473,10 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function let qid = shortest_qualid_of_syndef vars kn in CPatAtom (loc,Some (Qualid (loc, qid))) in insert_pat_alias loc p na - with - No_match -> extern_symbol_pattern allscopes vars t rules + | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None) + | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id))) + with + No_match -> extern_symbol_pattern allscopes vars t rules let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d8cb8c715..cfce96521 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -68,12 +68,7 @@ let for_grammar f x = (* Locating reference, possibly via an abbreviation *) let locate_reference qid = - match Nametab.locate_extended qid with - | TrueGlobal ref -> ref - | SynDef kn -> - match Syntax_def.search_syntactic_definition dummy_loc kn with - | [],ARef ref -> ref - | _ -> raise Not_found + Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let is_global id = try @@ -429,25 +424,31 @@ let check_no_explicitation l = user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") +let dump_extended_global loc = function + | TrueGlobal ref -> Dumpglob.add_glob loc ref + | SynDef sp -> Dumpglob.add_glob_kn loc sp + +let intern_extended_global_of_qualid (loc,qid) = + try let r = Nametab.locate_extended qid in dump_extended_global loc r; r + with Not_found -> error_global_not_found_loc loc qid + +let intern_reference ref = + Smartlocate.global_of_extended_global + (intern_extended_global_of_qualid (qualid_of_reference ref)) + (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env args = - try match Nametab.locate_extended qid with + match intern_extended_global_of_qualid (loc,qid) with | TrueGlobal ref -> - Dumpglob.add_glob loc ref; RRef (loc, ref), args | SynDef sp -> - Dumpglob.add_glob_kn loc sp; - match Syntax_def.search_syntactic_definition loc sp with - | [],ARef ref -> RRef (loc, ref), args - | (ids,c) -> + let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments loc; let args1,args2 = list_chop nids args in check_no_explicitation args1; let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2 - with Not_found -> - error_global_not_found_loc loc qid (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env args = @@ -489,8 +490,8 @@ let rec simple_adjust_scopes n = function let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in let npar = mib.Declarations.mind_nparams in - snd (list_chop (List.length pl1 + npar) - (simple_adjust_scopes (npar + List.length pl2) + snd (list_chop (npar + List.length pl1) + (simple_adjust_scopes (npar + List.length pl1 + List.length pl2) (find_arguments_scope (ConstructRef cstr)))) (**********************************************************************) @@ -564,11 +565,16 @@ let error_invalid_pattern_notation loc = user_err_loc (loc,"",str "Invalid notation for pattern.") let chop_aconstr_constructor loc (ind,k) args = - let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in - let params,args = list_chop nparams args in - List.iter (function AHole _ -> () - | _ -> error_invalid_pattern_notation loc) params; - args + if List.length args = 0 then (* Tolerance for a @id notation *) args else + begin + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then error_invalid_pattern_notation loc; + let params,args = list_chop nparams args in + List.iter (function AHole _ -> () + | _ -> error_invalid_pattern_notation loc) params; + args + end let rec subst_pat_iterator y t (subst,p) = match p with | PatVar (_,id) as x -> @@ -637,7 +643,7 @@ let find_constructor ref f aliases pats scopes = with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in match gref with | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition loc sp in + let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with | ARef (ConstructRef cstr) -> assert (vars=[]); @@ -1123,7 +1129,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let args = List.map (fun a -> (a,None)) args in intern_applied_reference intern env lvar args ref in check_projection isproj (List.length args) f; - if args = [] then f else + (* Rem: RApp(_,f,[]) stands for @f *) RApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b08b8dd1f..ee677e80a 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -144,6 +144,10 @@ val intern_constr_pattern : evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern +(* Raise Not_found if syndef not bound to a name and error if unexisting ref *) +val intern_reference : reference -> global_reference + +(* Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> reference -> rawconstr (* Interpret binders *) @@ -161,8 +165,8 @@ val interp_context_evars : ?fail_anonymous:bool -> evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) +(* (these functions do not modify the glob file) *) -val locate_reference : qualid -> global_reference val is_global : identifier -> bool val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 9b4ff860c..faad3c50a 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -25,7 +25,7 @@ open Topconstr let global_of_extended_global = function | TrueGlobal ref -> ref | SynDef kn -> - match search_syntactic_definition dummy_loc kn with + match search_syntactic_definition kn with | [],ARef ref -> ref | _ -> raise Not_found @@ -34,7 +34,7 @@ let locate_global_with_alias (loc,qid) = try global_of_extended_global ref with Not_found -> user_err_loc (loc,"",pr_qualid qid ++ - str " is bound to a notation that does not denote a reference") + str " is bound to a notation that does not denote a reference.") let global_inductive_with_alias r = let (loc,qid as lqid) = qualid_of_reference r in @@ -42,7 +42,7 @@ let global_inductive_with_alias r = | IndRef ind -> ind | ref -> user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") + pr_reference r ++ spc () ++ str "is not an inductive type.") with Not_found -> Nametab.error_global_not_found_loc loc qid let global_with_alias r = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b0e27f04e..245ed0f50 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -38,15 +38,25 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = add_syntax_constant kn pat; Nametab.push_syndef (Nametab.Until i) sp kn +let is_alias_of_already_visible_name sp = function + | _,ARef ref -> + let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in + dir = empty_dirpath && id = basename sp + | _ -> + false + let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = - Nametab.push_syndef (Nametab.Exactly i) sp kn; - if not onlyparse 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 + if not (is_alias_of_already_visible_name sp pat) then begin + Nametab.push_syndef (Nametab.Exactly i) sp kn; + if not onlyparse 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 + end let cache_syntax_constant d = - load_syntax_constant 1 d + load_syntax_constant 1 d; + open_syntax_constant 1 d let subst_syntax_constant (subst,(local,pat,onlyparse)) = (local,subst_interpretation subst pat,onlyparse) @@ -72,5 +82,5 @@ let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let search_syntactic_definition loc kn = +let search_syntactic_definition kn = out_pat (KNmap.find kn !syntax_table) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 747f7b9da..b4da6dd7a 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -24,4 +24,4 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr val declare_syntactic_definition : bool -> identifier -> bool -> syndef_interpretation -> unit -val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation +val search_syntactic_definition : kernel_name -> syndef_interpretation |