From 9bfb8b1262e3e833a2df9917c3b1d7a2775693a3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 2 Dec 2002 18:49:51 +0000 Subject: Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...). Diverses améliorations affichage et parsing. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3350 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.ml | 14 ++++++++------ interp/constrextern.mli | 3 ++- interp/constrintern.ml | 14 +++++++------- interp/constrintern.mli | 2 ++ interp/topconstr.ml | 4 ---- interp/topconstr.mli | 1 - parsing/extend.ml | 16 +++++++++++----- parsing/extend.mli | 7 ++++--- parsing/ppconstr.ml | 33 +++++++++++++++++++++++++++++---- 9 files changed, 63 insertions(+), 31 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 68bcd1235..1a398c665 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -100,7 +100,7 @@ let idopt_of_name = function let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n) -let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r) +let extern_reference loc r = Qualid (loc,shortest_qualid_of_global None r) (**********************************************************************) (* conversion of terms and cases patterns *) @@ -118,7 +118,7 @@ let rec extern_cases_pattern_in_scope scopes pat = | PatVar (_,Anonymous) -> CPatAtom (loc, None) | PatCstr(_,cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes) args in - let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in + let p = CPatCstr (loc,extern_reference loc (ConstructRef cstrsp),args) in (match na with | Name id -> CPatAlias (loc,p,id) | Anonymous -> p) @@ -186,7 +186,7 @@ let rec extern scopes r = extern_symbol scopes r (Symbols.uninterp_notations r) with No_match -> match r with - | RRef (_,ref) -> CRef (extern_ref ref) + | RRef (_,ref) -> CRef (extern_reference loc ref) | RVar (_,id) -> CRef (Ident (loc,id)) @@ -202,7 +202,8 @@ let rec extern scopes r = | RRef (loc,ref) -> let subscopes = Symbols.find_arguments_scope ref in let args = extern_args extern scopes args subscopes in - extern_app (implicits_of_global ref) (extern_ref ref) args + extern_app (implicits_of_global ref) (extern_reference loc ref) + args | _ -> explicitize [] (extern scopes f) (List.map (extern scopes) args)) @@ -333,7 +334,7 @@ let extern_constr at_top env t = (* Main translation function from pattern -> constr_expr *) let rec extern_pattern tenv env = function - | PRef ref -> CRef (extern_ref ref) + | PRef ref -> CRef (extern_reference loc ref) | PVar id -> CRef (Ident (loc,id)) @@ -359,7 +360,8 @@ let rec extern_pattern tenv env = function let args = List.map (extern_pattern tenv env) args in (match f with | PRef ref -> - extern_app (implicits_of_global ref) (extern_ref ref) args + extern_app (implicits_of_global ref) (extern_reference loc ref) + args | _ -> explicitize [] (extern_pattern tenv env f) args) | PSoApp (n,args) -> diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 614cbfdd4..d49b2b9a7 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -33,7 +33,7 @@ val extern_pattern : env -> names_context -> constr_pattern -> constr_expr level of quantification clashing with the variables in [env] are renamed *) val extern_constr : bool -> env -> constr -> constr_expr -val extern_ref : global_reference -> reference +val extern_reference : loc -> global_reference -> reference (* For debugging *) val print_implicits : bool ref @@ -41,6 +41,7 @@ val print_arguments : bool ref val print_evar_arguments : bool ref val print_coercions : bool ref val print_universes : bool ref +val print_no_symbol : bool ref (* This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e8e42a7b4..3d5526d39 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -134,7 +134,7 @@ let intern_var (env,impls,_) (vars1,vars2) loc id = RRef (loc, VarRef id), imps, args_scopes (* Is it a global reference or a syntactic definition? *) -let intern_qualid env vars loc qid = +let intern_qualid loc qid = try match Nametab.extended_locate qid with | TrueGlobal ref -> if !dump then add_glob loc ref; @@ -146,14 +146,14 @@ let intern_qualid env vars loc qid = let intern_reference env lvar = function | Qualid (loc, qid) -> - intern_qualid env lvar loc qid + intern_qualid loc qid | Ident (loc, id) -> (* For old ast syntax compatibility *) if (string_of_id id).[0] = '$' then RVar (loc,id),[],[] else (* End old ast syntax compatibility *) try intern_var env lvar loc id with Not_found -> - try intern_qualid env lvar loc (make_short_qualid id) + try intern_qualid loc (make_short_qualid id) with e -> (* Extra allowance for grammars *) if !interning_grammar then begin @@ -162,6 +162,9 @@ let intern_reference env lvar = function end else raise e +let interp_reference vars r = + let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[]) r in r + let apply_scope_env (ids,impls,scopes as env) = function | [] -> env, [] | (Some sc)::scl -> (ids,impls,sc::scopes), scl @@ -338,7 +341,7 @@ let traverse_binder id (subst,(ids,impls,scopes as env)) = let rec subst_rawconstr loc interp (subst,env as senv) = function | AVar id -> let a = try List.assoc id subst - with Not_found -> CRef (Ident (dummy_loc,id)) in + with Not_found -> CRef (Ident (loc,id)) in interp env a | t -> map_aconstr_with_binders_loc loc traverse_binder @@ -426,9 +429,6 @@ let internalise sigma env allow_soapp lvar c = | CCast (loc, c1, c2) -> RCast (loc,intern env c1,intern env c2) - | CGrammar (loc,c,subst) -> - subst_rawconstr loc intern (subst,env) c - | CDynamic (loc,d) -> RDynamic (loc,d) and intern_eqn n (ids,impls,scopes as env) (loc,lhs,rhs) = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ce8c6f5ee..8666db633 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -80,6 +80,8 @@ val interp_constrpattern_gen : val interp_constrpattern : evar_map -> env -> constr_expr -> int list * constr_pattern +val interp_reference : identifier list -> reference -> rawconstr + (* Interprets into a abbreviatable constr *) val interp_aconstr : constr_expr -> aconstr diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 2028d6de8..bce7772b4 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -262,7 +262,6 @@ type constr_expr = | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr | CNotation of loc * notation * (identifier * constr_expr) list - | CGrammar of loc * aconstr * (identifier * constr_expr) list | CNumeral of loc * Bignat.bigint | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t @@ -299,7 +298,6 @@ let constr_loc = function | CSort (loc,_) -> loc | CCast (loc,_,_) -> loc | CNotation (loc,_,_) -> loc - | CGrammar (loc,_,_) -> loc | CNumeral (loc,_) -> loc | CDelimiters (loc,_,_) -> loc | CDynamic _ -> dummy_loc @@ -328,7 +326,6 @@ let rec occur_var_constr_expr id = function | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a] | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b | CNotation (_,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x) l - | CGrammar (loc,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x)l | CDelimiters (loc,_,a) -> occur_var_constr_expr id a | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false | CCases (loc,_,_,_) @@ -371,7 +368,6 @@ let map_constr_expr_with_binders f g e = function | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) | CCast (loc,a,b) -> CCast (loc,f e a,f e b) | CNotation (loc,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,f e t)) l) - | CGrammar (loc,r,l) -> CGrammar (loc,r,List.map (fun (x,t) ->(x,f e t)) l) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x | CCases (loc,po,a,bl) -> diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 272b5391b..38c39fc9b 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -85,7 +85,6 @@ type constr_expr = | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr | CNotation of loc * notation * (identifier * constr_expr) list - | CGrammar of loc * aconstr * (identifier * constr_expr) list | CNumeral of loc * Bignat.bigint | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t diff --git a/parsing/extend.ml b/parsing/extend.ml index c7ea8737f..64d8cc7cd 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -47,7 +47,7 @@ type prod_item = type grammar_rule = { gr_name : string; gr_production : prod_item list; - gr_action : aconstr } + gr_action : constr_expr } type grammar_entry = { ge_name : string; @@ -65,11 +65,14 @@ type grammar_associativity = Gramext.g_assoc option type entry_context = identifier list -let ast_to_rawconstr = ref (fun _ _ -> AVar (id_of_string "Z")) -let set_ast_to_rawconstr f = ast_to_rawconstr := f +open Rawterm +open Libnames + +let globalizer = ref (fun _ _ -> CHole dummy_loc) +let set_constr_globalizer f = globalizer := f let act_of_ast vars = function - | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a + | SimpleAction (loc,ConstrNode a) -> !globalizer vars a | SimpleAction (loc,CasesPatternNode a) -> failwith "TODO:act_of_ast: cases_pattern" | CaseAction _ -> failwith "case/let not supported" @@ -92,8 +95,11 @@ type grammar_production = type raw_grammar_rule = string * grammar_production list * grammar_action type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list +(* No kernel names in Grammar's *) +let subst_constr_expr _ a = a + let subst_grammar_rule subst gr = - { gr with gr_action = subst_aconstr subst gr.gr_action } + { gr with gr_action = subst_constr_expr subst gr.gr_action } let subst_grammar_entry subst ge = { ge with gl_rules = List.map (subst_grammar_rule subst) ge.gl_rules } diff --git a/parsing/extend.mli b/parsing/extend.mli index 12d2ecc62..7398c7903 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -48,7 +48,7 @@ type prod_item = type grammar_rule = { gr_name : string; gr_production : prod_item list; - gr_action : aconstr } + gr_action : constr_expr } type grammar_entry = { ge_name : string; @@ -63,8 +63,9 @@ type grammar_associativity = Gramext.g_assoc option (* Globalisation and type-checking of Grammar actions *) type entry_context = identifier list -val to_act_check_vars : entry_context -> grammar_action -> aconstr -val set_ast_to_rawconstr : (entry_context -> constr_expr -> aconstr) -> unit + +val set_constr_globalizer : + (entry_context -> constr_expr -> constr_expr) -> unit type syntax_modifier = | SetItemLevel of string list * int diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index e177bb621..cea099da7 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -214,7 +214,33 @@ let rec pr_arrow pr = function let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">" -let pr_cases _ _ _ = str "" +let rec pr_pat = function + | CPatAlias (_,p,x) -> pr_pat p ++ spc () ++ str "as" ++ spc () ++ pr_id x + | CPatCstr (_,c,[]) -> pr_reference c + | CPatCstr (_,c,pl) -> + hov 0 ( + str "(" ++ pr_reference c ++ spc () ++ + prlist_with_sep spc pr_pat pl ++ str ")") + | CPatAtom (_,Some c) -> pr_reference c + | CPatAtom (_,None) -> str "_" + | CPatNumeral (_,n) -> Bignat.pr_bigint n + | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_pat p) + +let pr_eqn pr (_,patl,rhs) = + hov 0 ( + prlist_with_sep spc pr_pat patl ++ + str "=>" ++ + brk (1,1) ++ pr ltop rhs) + +let pr_cases pr po tml eqns = + hov 0 ( + pr_opt (pr_annotation pr) po ++ + hv 0 ( + hv 0 ( + str "Cases" ++ brk (1,2) ++ + prlist_with_sep spc (pr ltop) tml ++ spc() ++ str "of") ++ + prlist_with_sep pr_bar (pr_eqn pr) eqns ++ spc () ++ + str "end")) let rec pr inherited a = let (strm,prec) = match a with @@ -239,8 +265,8 @@ let rec pr inherited a = hov 0 ( pr (latom,E) a ++ prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp - | CCases (_,po,c,eqns) -> - pr_cases po c eqns, lcases + | CCases (_,po,tml,eqns) -> + pr_cases pr po tml eqns, lcases | COrderedCase (_,IfStyle,po,c,[b1;b2]) -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) @@ -278,7 +304,6 @@ let rec pr inherited a = | CCast (_,a,b) -> hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast | CNotation (_,s,env) -> pr_notation pr s env - | CGrammar _ -> failwith "CGrammar: TODO" | CNumeral (_,p) -> Bignat.pr_bigint p, latom | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom | CDynamic _ -> str "", latom -- cgit v1.2.3