From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- parsing/argextend.ml4 | 145 ++++++++------- parsing/egrammar.ml | 100 +++++------ parsing/egrammar.mli | 23 ++- parsing/extend.ml | 45 ++--- parsing/extend.mli | 44 ++--- parsing/extrawit.ml | 4 +- parsing/extrawit.mli | 8 +- parsing/g_constr.ml4 | 97 +++++----- parsing/g_decl_mode.ml4 | 252 -------------------------- parsing/g_intsyntax.mli | 13 -- parsing/g_ltac.ml4 | 26 ++- parsing/g_natsyntax.mli | 15 -- parsing/g_prim.ml4 | 12 +- parsing/g_proofs.ml4 | 55 +++--- parsing/g_tactic.ml4 | 148 +++++++--------- parsing/g_vernac.ml4 | 370 ++++++++++++++++++++++++-------------- parsing/g_xml.ml4 | 68 ++++--- parsing/g_zsyntax.mli | 11 -- parsing/grammar.mllib | 6 +- parsing/highparsing.mllib | 1 - parsing/lexer.ml4 | 322 ++++++++++++++++++--------------- parsing/lexer.mli | 24 +-- parsing/parsing.mllib | 1 - parsing/pcoq.ml4 | 432 +++++++++++++++++++++++++-------------------- parsing/pcoq.mli | 263 +++++++++++++-------------- parsing/ppconstr.ml | 157 ++-------------- parsing/ppconstr.mli | 15 +- parsing/ppdecl_proof.ml | 190 -------------------- parsing/ppdecl_proof.mli | 2 - parsing/pptactic.ml | 113 ++++-------- parsing/pptactic.mli | 18 +- parsing/ppvernac.ml | 204 +++++++++++---------- parsing/ppvernac.mli | 6 +- parsing/prettyp.ml | 228 +++++++++--------------- parsing/prettyp.mli | 19 +- parsing/printer.ml | 317 ++++++++++++++++++++++----------- parsing/printer.mli | 74 ++++---- parsing/printmod.ml | 242 +++++++++++++++++-------- parsing/printmod.mli | 4 +- parsing/q_constr.ml4 | 52 +++--- parsing/q_coqast.ml4 | 189 +++++++++++--------- parsing/q_util.ml4 | 56 ++---- parsing/q_util.mli | 8 +- parsing/tacextend.ml4 | 59 +++---- parsing/tactic_printer.ml | 95 +++------- parsing/tactic_printer.mli | 9 +- parsing/tok.ml | 90 ++++++++++ parsing/tok.mli | 29 +++ parsing/vernacextend.ml4 | 60 ++++--- 49 files changed, 2194 insertions(+), 2527 deletions(-) delete mode 100644 parsing/g_decl_mode.ml4 delete mode 100644 parsing/g_intsyntax.mli delete mode 100644 parsing/g_natsyntax.mli delete mode 100644 parsing/g_zsyntax.mli delete mode 100644 parsing/ppdecl_proof.ml delete mode 100644 parsing/ppdecl_proof.mli create mode 100644 parsing/tok.ml create mode 100644 parsing/tok.mli (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 848223a0..3266fcf9 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -1,21 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* > @@ -42,7 +40,12 @@ let rec make_rawwit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> + | ExtraArgType s -> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"rawwit_"^s$; + end in WIT.wit >> let rec make_globwit loc = function | BoolArgType -> <:expr< Genarg.globwit_bool >> @@ -67,7 +70,12 @@ let rec make_globwit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"globwit_"^s$ >> + | ExtraArgType s -> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"globwit_"^s$; + end in WIT.wit >> let rec make_wit loc = function | BoolArgType -> <:expr< Genarg.wit_bool >> @@ -92,48 +100,51 @@ let rec make_wit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >> + | ExtraArgType s -> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"wit_"^s$; + end in WIT.wit >> let make_act loc act pil = let rec make = function - | [] -> <:expr< Gramext.action (fun loc -> ($act$ : 'a)) >> + | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> | GramNonTerminal (_,t,_,Some p) :: tl -> let p = Names.string_of_id p in <:expr< - Gramext.action + Pcoq.Gram.action (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) >> | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl -> - <:expr< Gramext.action (fun _ -> $make tl$) >> in + <:expr< Pcoq.Gram.action (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function - | GramTerminal s -> <:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >> + | GramTerminal s -> <:expr< Pcoq.gram_token_of_string $str:s$ >> | GramNonTerminal (_,_,g,_) -> <:expr< Pcoq.symbol_of_prod_entry_key $mlexpr_of_prod_entry_key g$ >> let make_rule loc (prods,act) = <:expr< ($mlexpr_of_list make_prod_item prods$,$make_act loc act prods$) >> -let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = - let rawtyp, rawpr = match rawtyppr with - | None -> typ,pr - | Some (t,p) -> t,p in - let globtyp, globpr = match globtyppr with - | None -> typ,pr - | Some (t,p) -> t,p in +let declare_tactic_argument loc s (typ, pr, f, g, h) cl = + let rawtyp, rawpr, globtyp, globpr = match typ with + | `Uniform typ -> typ, pr, typ, pr + | `Specialized (a, b, c, d) -> a, b, c, d + in let glob = match g with | None -> <:expr< fun e x -> - out_gen $make_globwit loc typ$ + out_gen $make_globwit loc rawtyp$ (Tacinterp.intern_genarg e (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in let interp = match f with | None -> <:expr< fun ist gl x -> - out_gen $make_wit loc typ$ + out_gen $make_wit loc globtyp$ (Tacinterp.interp_genarg ist gl (Genarg.in_gen $make_globwit loc globtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in @@ -149,13 +160,13 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = let rawwit = <:expr< $lid:"rawwit_"^s$ >> in let globwit = <:expr< $lid:"globwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in - <:str_item< - declare - open Pcoq; - open Extrawit; + declare_str_items loc + [ <:str_item< value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) = - Genarg.create_arg $se$; - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; + Genarg.create_arg $se$ >>; + <:str_item< + value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + <:str_item< do { Tacinterp.add_interp_genarg $se$ ((fun e x -> (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))), @@ -163,14 +174,13 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))), (fun subst x -> (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))))); - Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None - [(None, None, $rules$)]; + Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) + (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $lid:rawpr$) ($globwit$, $lid:globpr$) - ($wit$, $lid:pr$); - end - >> + ($wit$, $lid:pr$) } + >> ] let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in @@ -181,56 +191,58 @@ let declare_vernac_argument loc s pr cl = let pr_rules = match pr with | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in - <:str_item< - declare - open Pcoq; - open Extrawit; + declare_str_items loc + [ <:str_item< value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel), ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel), - $lid:"rawwit_"^s$) = Genarg.create_arg $se$; - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; - Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None - [(None, None, $rules$)]; + $lid:"rawwit_"^s$) = Genarg.create_arg $se$ >>; + <:str_item< + value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + <:str_item< do { + Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) + (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $pr_rules$) ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer") - ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer"); - end - >> + ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer") } + >> ] open Vernacexpr open Pcoq open Pcaml +open PcamlSig EXTEND GLOBAL: str_item; str_item: - [ [ "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; - "TYPED"; "AS"; typ = argtype; - "PRINTED"; "BY"; pr = LIDENT; - f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; - g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; - h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; - rawtyppr = - (* Necessary if the globalized type is different from the final type *) - OPT [ "RAW_TYPED"; "AS"; t = argtype; - "RAW_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; - globtyppr = - OPT [ "GLOB_TYPED"; "AS"; t = argtype; - "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + [ [ "ARGUMENT"; "EXTEND"; s = entry_name; + header = argextend_header; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> - if String.capitalize s = s then - failwith "Argument entry names must be lowercase"; - declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l - | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; + declare_tactic_argument loc s header l + | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name; pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> - if String.capitalize s = s then - failwith "Argument entry names must be lowercase"; declare_vernac_argument loc s pr l ] ] ; + argextend_header: + [ [ "TYPED"; "AS"; typ = argtype; + "PRINTED"; "BY"; pr = LIDENT; + f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ] -> + (`Uniform typ, pr, f, g, h) + | "PRINTED"; "BY"; pr = LIDENT; + f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; + "RAW_TYPED"; "AS"; rawtyp = argtype; + "RAW_PRINTED"; "BY"; rawpr = LIDENT; + "GLOB_TYPED"; "AS"; globtyp = argtype; + "GLOB_PRINTED"; "BY"; globpr = LIDENT -> + (`Specialized (rawtyp, rawpr, globtyp, globpr), pr, f, g, h) ] ] + ; argtype: [ "2" [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] @@ -253,9 +265,14 @@ EXTEND GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then - Lexer.add_token ("", s); + Lexer.add_keyword s; GramTerminal s ] ] ; + entry_name: + [ [ s = LIDENT -> s + | UIDENT -> failwith "Argument entry names must be lowercase" + ] ] + ; END diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index ba965a54..4418a45f 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -1,14 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CPatAtom (loc,Some (Ident (loc,id))) type grammar_constr_prod_item = - | GramConstrTerminal of Token.pattern + | GramConstrTerminal of Tok.t | GramConstrNonTerminal of constr_prod_entry_key * identifier option | GramConstrListMark of int * bool (* tells action rule to make a list of the n previous parsed items; concat with last parsed list if true *) -type 'a action_env = 'a list * 'a list list - let make_constr_action (f : loc -> constr_notation_substitution -> constr_expr) pil = let rec make (constrs,constrlists,binders as fullsubst) = function | [] -> - Gramext.action (fun loc -> f loc fullsubst) + Gram.action (fun loc -> f loc fullsubst) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullsubst tl) + Gram.action (fun _ -> make fullsubst tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) - (match typ with - | (ETConstr _| ETOther _) -> - Gramext.action (fun (v:constr_expr) -> + (match typ with + | (ETConstr _| ETOther _) -> + Gram.action (fun (v:constr_expr) -> make (v :: constrs, constrlists, binders) tl) - | ETReference -> - Gramext.action (fun (v:reference) -> + | ETReference -> + Gram.action (fun (v:reference) -> make (CRef v :: constrs, constrlists, binders) tl) - | ETName -> - Gramext.action (fun (na:name located) -> + | ETName -> + Gram.action (fun (na:name located) -> make (constr_expr_of_name na :: constrs, constrlists, binders) tl) - | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> + | ETBigint -> + Gram.action (fun (v:Bigint.bigint) -> make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl) - | ETConstrList (_,n) -> - Gramext.action (fun (v:constr_expr list) -> + | ETConstrList (_,n) -> + Gram.action (fun (v:constr_expr list) -> make (constrs, v::constrlists, binders) tl) | ETBinder _ | ETBinderList (true,_) -> - Gramext.action (fun (v:local_binder list) -> + Gram.action (fun (v:local_binder list) -> make (constrs, constrlists, v::binders) tl) | ETBinderList (false,_) -> - Gramext.action (fun (v:local_binder list list) -> + Gram.action (fun (v:local_binder list list) -> make (constrs, constrlists, List.flatten v::binders) tl) | ETPattern -> failwith "Unexpected entry of type cases pattern") @@ -113,26 +110,26 @@ let make_cases_pattern_action (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = let rec make (env,envlist as fullenv) = function | [] -> - Gramext.action (fun loc -> f loc fullenv) + Gram.action (fun loc -> f loc fullenv) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullenv tl) + Gram.action (fun _ -> make fullenv tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) (match typ with | ETConstr _ -> (* pattern non-terminal *) - Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) + Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) | ETReference -> - Gramext.action (fun (v:reference) -> + Gram.action (fun (v:reference) -> make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl) | ETName -> - Gramext.action (fun (na:name located) -> + Gram.action (fun (na:name located) -> make (cases_pattern_expr_of_name na :: env, envlist) tl) | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> + Gram.action (fun (v:Bigint.bigint) -> make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl) | ETConstrList (_,_) -> - Gramext.action (fun (vl:cases_pattern_expr list) -> + Gram.action (fun (vl:cases_pattern_expr list) -> make (env, vl :: envlist) tl) | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) -> failwith "Unexpected entry of type cases pattern or other") @@ -146,7 +143,7 @@ let make_cases_pattern_action let rec make_constr_prod_item assoc from forpat = function | GramConstrTerminal tok :: l -> - Gramext.Stoken tok :: make_constr_prod_item assoc from forpat l + gram_token_of_token tok :: make_constr_prod_item assoc from forpat l | GramConstrNonTerminal (nt, ovar) :: l -> symbol_of_constr_prod_entry_key assoc from forpat nt :: make_constr_prod_item assoc from forpat l @@ -156,17 +153,18 @@ let rec make_constr_prod_item assoc from forpat = function [] let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = - let entry = + let entry = if forpat then weaken_entry Constr.pattern else weaken_entry Constr.operconstr in - grammar_extend entry pos reinit [(name, p4assoc, [])] + grammar_extend entry reinit (pos,[(name, p4assoc, [])]) let pure_sublevels level symbs = - map_succeed (function - | Gramext.Snterml (_,n) when Some (int_of_string n) <> level -> - int_of_string n - | _ -> - failwith "") symbs + map_succeed + (function s -> + let i = level_of_snterml s in + if level = Some i then failwith ""; + i) + symbs let extend_constr (entry,level) (n,assoc) mkact forpat rules = List.fold_left (fun nb pt -> @@ -176,7 +174,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = let pos,p4assoc,name,reinit = find_position forpat assoc level in let nb_decls = List.length needed_levels + 1 in List.iter (prepare_empty_levels forpat) needed_levels; - grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]; + grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])]); nb_decls) 0 rules let extend_constr_notation (n,assoc,ntn,rules) = @@ -187,8 +185,8 @@ let extend_constr_notation (n,assoc,ntn,rules) = (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,env) in let e = interp_constr_entry_key true (ETConstr (n,())) in - let nb' = - extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rules in + let nb' = extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) + true rules in nb+nb' (**********************************************************************) @@ -198,11 +196,11 @@ let make_generic_action (f:loc -> ('b * raw_generic_argument) list -> 'a) pil = let rec make env = function | [] -> - Gramext.action (fun loc -> f loc env) + Gram.action (fun loc -> f loc env) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gram.action (fun _ -> make env tl) | Some (p, t) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in + Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) let make_rule univ f g pt = @@ -216,10 +214,10 @@ let make_rule univ f g pt = type grammar_prod_item = | GramTerminal of string | GramNonTerminal of - loc * argument_type * Gram.te prod_entry_key * identifier option + loc * argument_type * prod_entry_key * identifier option let make_prod_item = function - | GramTerminal s -> (Gramext.Stoken (Lexer.terminal s), None) + | GramTerminal s -> (gram_token_of_string s, None) | GramNonTerminal (_,t,e,po) -> (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po) @@ -229,19 +227,21 @@ let extend_tactic_grammar s gl = let univ = get_univ "tactic" in let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in let rules = List.map (make_rule univ mkact make_prod_item) gl in - Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)] + maybe_uncurry (Gram.extend Tactic.simple_tactic) + (None,[(None, None, List.rev rules)]) (* Vernac grammar extensions *) let vernac_exts = ref [] let get_extend_vernac_grammars () = !vernac_exts -let extend_vernac_command_grammar s gl = +let extend_vernac_command_grammar s nt gl = + let nt = Option.default Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; let univ = get_univ "vernac" in let mkact loc l = VernacExtend (s,List.map snd l) in let rules = List.map (make_rule univ mkact make_prod_item) gl in - Gram.extend Vernac_.command None [(None, None, List.rev rules)] + maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)]) (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) @@ -252,7 +252,7 @@ let get_tactic_entry n = else if n = 5 then weaken_entry Tactic.binder_tactic, None else if 1<=n && n<5 then - weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) + weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -276,14 +276,14 @@ let add_tactic_entry (key,lev,prods,tac) = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule univ (mkact key tac) make_prod_item prods in synchronize_level_positions (); - grammar_extend entry pos None [(None, None, List.rev [rules])]; + grammar_extend entry None (pos,[(None, None, List.rev [rules])]); 1 (**********************************************************************) (** State of the grammar extensions *) type notation_grammar = - int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list + int * gram_assoc option * notation * grammar_constr_prod_item list list type all_grammar_command = | Notation of diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 8554c9be..1d85c74e 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* grammar_prod_item list list -> unit val extend_vernac_command_grammar : - string -> grammar_prod_item list list -> unit + string -> vernac_expr Gram.entry option -> grammar_prod_item list list -> unit val get_extend_vernac_grammars : unit -> (string * grammar_prod_item list list) list diff --git a/parsing/extend.ml b/parsing/extend.ml index 9b85ada5..fca24ed5 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -1,42 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Lexer.add_token("",s)) constr_kw +let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c @@ -36,7 +33,7 @@ let mk_cast = function let binders_of_lidents l = List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, + LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, CHole (loc, Some (Evd.BinderType (Name id))))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = @@ -66,60 +63,49 @@ let mk_fix(loc,kw,id,dcls) = let mk_single_fix (loc,kw,dcl) = let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) +let err () = raise Stream.Failure + (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let lpar_id_coloneq = Gram.Entry.of_parser "test_lpar_id_coloneq" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("IDENT",s)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":=")] -> - Stream.junk strm; Stream.junk strm; Stream.junk strm; + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT s -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":=" -> + stream_njunk 3 strm; Names.id_of_string s - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) let impl_ident_head = Gram.Entry.of_parser "impl_ident_head" (fun strm -> - match Stream.npeek 1 strm with - | [(_,"{")] -> - (match Stream.npeek 2 strm with - | [_;("IDENT",("wf"|"struct"|"measure"))] -> - raise Stream.Failure - | [_;("IDENT",s)] -> - Stream.junk strm; Stream.junk strm; + match get_tok (stream_nth 0 strm) with + | KEYWORD "{" -> + (match get_tok (stream_nth 1 strm) with + | IDENT ("wf"|"struct"|"measure") -> err () + | IDENT s -> + stream_njunk 2 strm; Names.id_of_string s - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + | _ -> err ()) + | _ -> err ()) let ident_colon = Gram.Entry.of_parser "ident_colon" (fun strm -> - match Stream.npeek 1 strm with - | [("IDENT",s)] -> - (match Stream.npeek 2 strm with - | [_; ("", ":")] -> - Stream.junk strm; Stream.junk strm; + match get_tok (stream_nth 0 strm) with + | IDENT s -> + (match get_tok (stream_nth 1 strm) with + | KEYWORD ":" -> + stream_njunk 2 strm; Names.id_of_string s - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - -let ident_with = - Gram.Entry.of_parser "ident_with" - (fun strm -> - match Stream.npeek 1 strm with - | [("IDENT",s)] -> - (match Stream.npeek 2 strm with - | [_; ("", "with")] -> - Stream.junk strm; Stream.junk strm; - Names.id_of_string s - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + | _ -> err ()) + | _ -> err ()) let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None @@ -147,9 +133,9 @@ GEXTEND Gram [ [ c = lconstr -> c ] ] ; sort: - [ [ "Set" -> RProp Pos - | "Prop" -> RProp Null - | "Type" -> RType None ] ] + [ [ "Set" -> GProp Pos + | "Prop" -> GProp Null + | "Type" -> GType None ] ] ; lconstr: [ [ c = operconstr LEVEL "200" -> c ] ] @@ -215,7 +201,7 @@ GEXTEND Gram [ [ "fun" -> () ] ] ; record_declaration: - [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs) + [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) (* CRecord (loc, Some c, fs) *) ] ] @@ -227,7 +213,7 @@ GEXTEND Gram binder_constr: [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> mkCProdN loc bl c - | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" -> + | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> mkCLambdaN loc bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> @@ -334,14 +320,17 @@ GEXTEND Gram [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] | "99" RIGHTA [ ] | "10" LEFTA + [ p = pattern; "as"; id = ident -> + CPatAlias (loc, p, id) ] + | "9" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected.")) - | p = pattern; "as"; id = ident -> - CPatAlias (loc, p, id) ] + |"@"; r = Prim.reference; lp = LIST1 NEXT -> + CPatCstrExpl (loc, r, lp) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ] | "0" diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 deleted file mode 100644 index 8893ebcc..00000000 --- a/parsing/g_decl_mode.ml4 +++ /dev/null @@ -1,252 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] - | Some l -> l - -GEXTEND Gram -GLOBAL: proof_instr; - thesis : - [[ "thesis" -> Plain - | "thesis"; "for"; i=ident -> (For i) - ]]; - statement : - [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} - | i=ident -> {st_label=Anonymous; - st_it=Topconstr.CRef (Libnames.Ident (loc, i))} - | c=constr -> {st_label=Anonymous;st_it=c} - ]]; - constr_or_thesis : - [[ t=thesis -> Thesis t ] | - [ c=constr -> This c - ]]; - statement_or_thesis : - [ - [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] - | - [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} - | i=ident -> {st_label=Anonymous; - st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} - | c=constr -> {st_label=Anonymous;st_it=This c} - ] - ]; - justification_items : - [[ -> Some [] - | "by"; l=LIST1 constr SEP "," -> Some l - | "by"; "*" -> None ]] - ; - justification_method : - [[ -> None - | "using"; tac = tactic -> Some tac ]] - ; - simple_cut_or_thesis : - [[ ls = statement_or_thesis; - j = justification_items; - taco = justification_method - -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] - ; - simple_cut : - [[ ls = statement; - j = justification_items; - taco = justification_method - -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] - ; - elim_type: - [[ IDENT "induction" -> ET_Induction - | IDENT "cases" -> ET_Case_analysis ]] - ; - block_type : - [[ IDENT "claim" -> B_claim - | IDENT "focus" -> B_focus - | IDENT "proof" -> B_proof - | et=elim_type -> B_elim et ]] - ; - elim_obj: - [[ IDENT "on"; c=constr -> Real c - | IDENT "of"; c=simple_cut -> Virtual c ]] - ; - elim_step: - [[ IDENT "consider" ; - h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h) - | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj) - | IDENT "suffices"; ls=suff_clause; - j = justification_items; - taco = justification_method - -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] - ; - rew_step : - [[ "~=" ; c=simple_cut -> (Rhs,c) - | "=~" ; c=simple_cut -> (Lhs,c)]] - ; - cut_step: - [[ "then"; tt=elim_step -> Pthen tt - | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c) - | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) - | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c) - | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c) - | tt=elim_step -> tt - | tt=rew_step -> let s,c=tt in Prew (s,c); - | IDENT "have"; c=simple_cut_or_thesis -> Pcut c; - | IDENT "claim"; c=statement -> Pclaim c; - | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; - | "end"; bt = block_type -> Pend bt; - | IDENT "escape" -> Pescape ]] - ; - (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) - loc_id: - [[ id=ident -> fun x -> (loc,(id,x)) ]]; - hyp: - [[ id=loc_id -> id None ; - | id=loc_id ; ":" ; c=constr -> id (Some c)]] - ; - consider_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=consider_vars -> (Hvar name) :: v - | name=hyp; - IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h - ]] - ; - consider_hyps: - [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h - | st=statement; IDENT "and"; - IDENT "consider" ; v=consider_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]] - ; - assume_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=assume_vars -> (Hvar name) :: v - | name=hyp; - IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h - ]] - ; - assume_hyps: - [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h - | st=statement; IDENT "and"; - IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]] - ; - assume_clause: - [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v - | h=assume_hyps -> h ]] - ; - suff_vars: - [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> - [Hvar name],c - | name=hyp; ","; v=suff_vars -> - let (q,c) = v in ((Hvar name) :: q),c - | name=hyp; - IDENT "such"; IDENT "that"; h=suff_hyps -> - let (q,c) = h in ((Hvar name) :: q),c - ]]; - suff_hyps: - [[ st=statement; IDENT "and"; h=suff_hyps -> - let (q,c) = h in (Hprop st::q),c - | st=statement; IDENT "and"; - IDENT "to" ; IDENT "have" ; v=suff_vars -> - let (q,c) = v in (Hprop st::q),c - | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> - [Hprop st],c - ]] - ; - suff_clause: - [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v - | h=suff_hyps -> h ]] - ; - let_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=let_vars -> (Hvar name) :: v - | name=hyp; IDENT "be"; - IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h - ]] - ; - let_hyps: - [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h - | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]]; - given_vars: - [[ name=hyp -> [Hvar name] - | name=hyp; ","; v=given_vars -> (Hvar name) :: v - | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h - ]] - ; - given_hyps: - [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h - | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v - | st=statement -> [Hprop st] - ]]; - suppose_vars: - [[name=hyp -> [Hvar name] - |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v - |name=hyp; OPT[IDENT "be"]; - IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h - ]] - ; - suppose_hyps: - [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h - | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have"; - v=suppose_vars -> Hprop st::v - | st=statement_or_thesis -> [Hprop st] - ]] - ; - suppose_clause: - [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v; - | h=suppose_hyps -> h ]] - ; - intro_step: - [[ IDENT "suppose" ; h=assume_clause -> Psuppose h - | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; - po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ; - ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> - Pcase (none_is_empty po,c,none_is_empty ho) - | "let" ; v=let_vars -> Plet v - | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses - | IDENT "assume"; h=assume_clause -> Passume h - | IDENT "given"; h=given_vars -> Pgiven h - | IDENT "define"; id=ident; args=LIST0 hyp; - "as"; body=constr -> Pdefine(id,args,body) - | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ) - | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ) - ]] - ; - emphasis : - [[ -> 0 - | "*" -> 1 - | "**" -> 2 - | "***" -> 3 - ]] - ; - bare_proof_instr: - [[ c = cut_step -> c ; - | i = intro_step -> i ]] - ; - proof_instr : - [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]] - ; -END;; - - diff --git a/parsing/g_intsyntax.mli b/parsing/g_intsyntax.mli deleted file mode 100644 index de85b6af..00000000 --- a/parsing/g_intsyntax.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* a + TacArg (loc,a) -> a | e -> Tacexp (e:raw_tactic_expr) (* Tactics grammar rules *) @@ -60,6 +57,7 @@ GEXTEND Gram | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta (*To do: put Abstract in Refiner*) @@ -87,20 +85,20 @@ GEXTEND Gram | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> - TacArg (TacExternal (loc,com,req,la)) + TacArg (loc,TacExternal (loc,com,req,la)) | st = simple_tactic -> TacAtom (loc,st) - | a = may_eval_arg -> TacArg(a) + | a = may_eval_arg -> TacArg(loc,a) | IDENT "constr"; ":"; id = METAIDENT -> - TacArg(MetaIdArg (loc,false,id)) + TacArg(loc,MetaIdArg (loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(ConstrMayEval(ConstrTerm c)) + TacArg(loc,ConstrMayEval(ConstrTerm c)) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacArg(IntroPattern ipat) + TacArg(loc,IntroPattern ipat) | r = reference; la = LIST0 tactic_arg -> - TacArg(TacCall (loc,r,la)) ] + TacArg(loc,TacCall (loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a - | a = tactic_atom -> TacArg a ] ] + | a = tactic_atom -> TacArg (loc,a) ] ] ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli deleted file mode 100644 index d3f12bed..00000000 --- a/parsing/g_natsyntax.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Lexer.add_token("",s)) prim_kw +let _ = List.iter Lexer.add_keyword prim_kw open Prim open Nametab @@ -45,7 +43,7 @@ GEXTEND Gram [ [ s = IDENT -> id_of_string s ] ] ; pattern_ident: - [ [ s = LEFTQMARK; id = ident -> id ] ] + [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: [ [ id = pattern_ident -> (loc, id) ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f1dad3b2..9abb8cd1 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,16 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] - | ":"; l = LIST1 IDENT -> l ] ] + | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (Tacexpr.TacId []) - | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta + | IDENT "Proof" -> VernacProof (None,None) + | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn + | IDENT "Proof"; "with"; ta = tactic; + l = OPT [ "using"; l = LIST0 identref -> l ] -> + VernacProof (Some ta, l) + | IDENT "Proof"; "using"; l = LIST0 identref; + ta = OPT [ "with"; ta = tactic -> ta ] -> + VernacProof (ta,Some l) + | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll | IDENT "Abort"; id = identref -> VernacAbort (Some id) @@ -59,15 +62,19 @@ GEXTEND Gram | IDENT "Resume" -> VernacResume None | IDENT "Resume"; id = identref -> VernacResume (Some id) | IDENT "Restart" -> VernacRestart - | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n | IDENT "Focus" -> VernacFocus None | IDENT "Focus"; n = natural -> VernacFocus (Some n) | IDENT "Unfocus" -> VernacUnfocus - | IDENT "Show" -> VernacShow (ShowGoal None) - | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n)) + | IDENT "BeginSubproof" -> VernacSubproof None + | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n) + | IDENT "EndSubproof" -> VernacEndSubproof + | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) + | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) + | IDENT "Show"; IDENT "Goal"; n = string -> + VernacShow (ShowGoal (GoalId n)) | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode @@ -80,34 +87,22 @@ GEXTEND Gram | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis - | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer -> - VernacShow (ExplainProof l) - | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> - VernacShow (ExplainTree l) - | IDENT "Go"; n = natural -> VernacGo (GoTo n) - | IDENT "Go"; IDENT "top" -> VernacGo GoTop - | IDENT "Go"; IDENT "prev" -> VernacGo GoPrev - | IDENT "Go"; IDENT "next" -> VernacGo GoNext | IDENT "Guarded" -> VernacCheckGuard -(* Hints for Auto and EAuto *) + (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ "discriminated" -> true | -> false ] -> VernacCreateHintDb (use_module_locality (), id, b) + | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> + VernacRemoveHints (use_module_locality (), dbnames, ids) | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> VernacHints (enforce_module_locality local,dbnames, h) - -(* Declare "Resolve" directly so as to be able to later extend with - "Resolve ->" and "Resolve <-" *) + (* Declare "Resolve" explicitly so as to be able to later extend with + "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; dbnames = opt_hintbases -> VernacHints (use_module_locality (),dbnames, HintsResolve (List.map (fun x -> (n, true, x)) lc)) - -(*This entry is not commented, only for debug*) - | IDENT "PrintConstr"; c = constr -> - VernacExtend ("PrintConstr", - [Genarg.in_gen Genarg.rawwit_constr c]) ] ]; obsolete_locality: @@ -134,6 +129,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index be20f891..f1b3ffed 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -1,122 +1,104 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "; "<-" ; "by" ] -let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw +let _ = List.iter Lexer.add_keyword tactic_kw + +let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let test_lpar_id_coloneq = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("IDENT",s)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":=")] -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; (("IDENT"|"INT"),_)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":=")] -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ | INT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) (* idem for (x:t) *) let test_lpar_id_colon = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("IDENT",id)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":")] -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = - match list_last (Stream.npeek n strm) with - | ("","(") -> skip_to_rpar (p+1) (n+1) - | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1) - | ("",".") -> raise Stream.Failure + match get_tok (list_last (Stream.npeek n strm)) with + | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) + | KEYWORD ")" -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1) + | KEYWORD "." -> err () | _ -> skip_to_rpar p (n+1) in let rec skip_names n = - match list_last (Stream.npeek n strm) with - | ("IDENT",_) | ("","_") -> skip_names (n+1) - | ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *) - | _ -> raise Stream.Failure in + match get_tok (list_last (Stream.npeek n strm)) with + | IDENT _ | KEYWORD "_" -> skip_names (n+1) + | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) + | _ -> err () in let rec skip_binders n = - match list_last (Stream.npeek n strm) with - | ("","(") -> skip_binders (skip_names (n+1)) - | ("IDENT",_) | ("","_") -> skip_binders (n+1) - | ("",":=") -> () - | _ -> raise Stream.Failure in - match Stream.npeek 1 strm with - | [("","(")] -> skip_binders 2 - | _ -> raise Stream.Failure) - -let guess_lpar_ipat s strm = - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("",("("|"["))] -> () - | [_; ("IDENT",_)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", s')] when s = s' -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure - -let guess_lpar_coloneq = - Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=") - -let guess_lpar_colon = - Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":") + match get_tok (list_last (Stream.npeek n strm)) with + | KEYWORD "(" -> skip_binders (skip_names (n+1)) + | IDENT _ | KEYWORD "_" -> skip_binders (n+1) + | KEYWORD ":=" -> () + | _ -> err () in + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> skip_binders 2 + | _ -> err ()) let lookup_at_as_coma = Gram.Entry.of_parser "lookup_at_as_coma" (fun strm -> - match Stream.npeek 1 strm with - | [("",(","|"at"|"as"))] -> () - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD (","|"at"|"as") -> () + | _ -> err ()) open Constr open Prim @@ -183,8 +165,8 @@ let mkCLambdaN_simple bl c = let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) let map_int_or_var f = function - | Rawterm.ArgArg x -> Rawterm.ArgArg (f x) - | Rawterm.ArgVar _ as y -> y + | Glob_term.ArgArg x -> Glob_term.ArgArg (f x) + | Glob_term.ArgVar _ as y -> y let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr } @@ -222,12 +204,12 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Rawterm.ArgArg n - | id = identref -> Rawterm.ArgVar id ] ] + [ [ n = integer -> Glob_term.ArgArg n + | id = identref -> Glob_term.ArgVar id ] ] ; nat_or_var: - [ [ n = natural -> Rawterm.ArgArg n - | id = identref -> Rawterm.ArgVar id ] ] + [ [ n = natural -> Glob_term.ArgArg n + | id = identref -> Glob_term.ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -236,12 +218,6 @@ GEXTEND Gram (* This is used in quotations *) | id = METAIDENT -> MetaId (loc,id) ] ] ; - (* A number or a quotation meta-variable *) - num_or_meta: - [ [ n = integer -> AI n - | id = METAIDENT -> MetaId (loc,id) - ] ] - ; open_constr: [ [ c = constr -> ((),c) ] ] ; @@ -451,7 +427,7 @@ GEXTEND Gram ; hintbases: [ [ "with"; "*" -> None - | "with"; l = LIST1 IDENT -> Some l + | "with"; l = LIST1 [ x = IDENT -> x] -> Some l | -> Some [] ] ] ; auto_using: @@ -656,9 +632,9 @@ GEXTEND Gram | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll) | IDENT "eexists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (true,true,bll) - | IDENT "constructor"; n = num_or_meta; l = with_bindings -> + | IDENT "constructor"; n = nat_or_var; l = with_bindings -> TacConstructor (false,n,l) - | IDENT "econstructor"; n = num_or_meta; l = with_bindings -> + | IDENT "econstructor"; n = nat_or_var; l = with_bindings -> TacConstructor (true,n,l) | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor (false,t) | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d761ed64..ac81786b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1,30 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw +let _ = List.iter Lexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -let check_command = Gram.Entry.create "vernac:check_command" +let check_command = Gram.entry_create "vernac:check_command" -let tactic_mode = Gram.Entry.create "vernac:tactic_command" -let proof_mode = Gram.Entry.create "vernac:proof_command" -let noedit_mode = Gram.Entry.create "vernac:noedit_command" +let tactic_mode = Gram.entry_create "vernac:tactic_command" +let noedit_mode = Gram.entry_create "vernac:noedit_command" +let subprf = Gram.entry_create "vernac:subprf" -let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" -let thm_token = Gram.Entry.create "vernac:thm_token" -let def_body = Gram.Entry.create "vernac:def_body" -let decl_notation = Gram.Entry.create "vernac:decl_notation" -let typeclass_context = Gram.Entry.create "vernac:typeclass_context" -let record_field = Gram.Entry.create "vernac:record_field" -let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion" -let instance_name = Gram.Entry.create "vernac:instance_name" +let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" +let thm_token = Gram.entry_create "vernac:thm_token" +let def_body = Gram.entry_create "vernac:def_body" +let decl_notation = Gram.entry_create "vernac:decl_notation" +let record_field = Gram.entry_create "vernac:record_field" +let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" +let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" +let instance_name = Gram.entry_create "vernac:instance_name" -let get_command_entry () = - match Decl_mode.get_current_mode () with - Mode_proof -> proof_mode - | Mode_tactic -> tactic_mode - | Mode_none -> noedit_mode +let command_entry = ref noedit_mode +let set_command_entry e = command_entry := e +let get_command_entry () = !command_entry + + +(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for + proof editing and changes nothing else). Then sets it as the default proof mode. *) +let set_tactic_mode () = set_command_entry tactic_mode +let set_noedit_mode () = set_command_entry noedit_mode +let _ = Proof_global.register_proof_mode {Proof_global. + name = "Classic" ; + set = set_tactic_mode ; + reset = set_noedit_mode + } let default_command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm) + (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) let no_hook _ _ = () GEXTEND Gram - GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode; + GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) @@ -79,6 +84,7 @@ GEXTEND Gram | c = command; "." -> c | c = syntax; "." -> c | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l + | c = subprf -> c ] ] ; vernac_aux: LAST @@ -96,20 +102,27 @@ GEXTEND Gram [ [ gln = OPT[n=natural; ":" -> n]; tac = subgoal_command -> tac gln ] ] ; - subgoal_command: - [ [ c = check_command; "." -> c + + subprf: + [ [ + "-" -> VernacBullet Dash + | "*" -> VernacBullet Star + | "+" -> VernacBullet Plus + | "{" -> VernacSubproof None + | "}" -> VernacEndSubproof + ] ] + ; + + + + subgoal_command: + [ [ c = check_command; "." -> fun g -> c g | tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] -> (fun g -> - let g = match g with Some gl -> gl | _ -> 1 in + let g = Option.default 1 g in VernacSolve(g,tac,use_dft_tac)) ] ] ; - proof_mode: - [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] - ; - proof_mode: LAST - [ [ c=subgoal_command -> c (Some 1) ] ] - ; located_vernac: [ [ v = vernac -> loc, v ] ] ; @@ -117,20 +130,20 @@ END let test_plurial_form = function | [(_,([_],_))] -> - Flags.if_verbose warning - "Keywords Variables/Hypotheses/Parameters expect more than one assumption" + Flags.if_verbose msg_warning + (str "Keywords Variables/Hypotheses/Parameters expect more than one assumption") | _ -> () let test_plurial_form_types = function | [([_],_)] -> - Flags.if_verbose warning - "Keywords Implicit Types expect more than one type" + Flags.if_verbose msg_warning + (str "Keywords Implicit Types expect more than one type") | _ -> () (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - typeclass_context typeclass_constraint record_field decl_notation; + typeclass_constraint record_field decl_notation rec_definition; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -144,10 +157,6 @@ GEXTEND Gram | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; VernacAssumption (stre, nl, bl) - | IDENT "Boxed";"Definition";id = identref; b = def_body -> - VernacDefinition ((Global,true,Definition), id, b, no_hook) - | IDENT "Unboxed";"Definition";id = identref; b = def_body -> - VernacDefinition ((Global,false,Definition), id, b, no_hook) | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) (* Gallina inductive declarations *) @@ -156,14 +165,10 @@ GEXTEND Gram let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,false,indl) - | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,true) - | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,false) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,Flags.boxed_definitions()) + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint recs | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (corecs,false) + VernacCoFixpoint corecs | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] @@ -178,10 +183,6 @@ GEXTEND Gram VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]]) ] ] ; - typeclass_context: - [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l - | -> [] ] ] - ; thm_token: [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma @@ -193,13 +194,13 @@ GEXTEND Gram ; def_token: [ [ "Definition" -> - no_hook, (Global, Flags.boxed_definitions(), Definition) + no_hook, (Global, Definition) | IDENT "Let" -> - no_hook, (Local, Flags.boxed_definitions(), Definition) + no_hook, (Local, Definition) | IDENT "Example" -> - no_hook, (Global, Flags.boxed_definitions(), Example) + no_hook, (Global, Example) | IDENT "SubClass" -> - Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] + Class.add_subclass_hook, (use_locality_exp (), SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) @@ -215,7 +216,9 @@ GEXTEND Gram | IDENT "Parameters" -> (Global, Definitional) ] ] ; inline: - [ ["Inline" -> true | -> false] ] + [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i) + | IDENT "Inline" -> Some (Flags.get_inline_level()) + | -> None] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) @@ -233,7 +236,7 @@ GEXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Rawterm.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -325,7 +328,8 @@ GEXTEND Gram *) (* ... with coercions *) record_field: - [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] + [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; + ntn = decl_notation -> (bd,pri),ntn ] ] ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; @@ -335,13 +339,13 @@ GEXTEND Gram (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with - | CCast(_,b, Rawterm.CastConv (_, t)) -> - (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) + | CCast(_,b, Glob_term.CastConv (_, t)) -> + (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | _ -> - (false,DefExpr(id,mkCLambdaN loc l b,None)) ] ] + (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ] ; record_binder: - [ [ id = name -> (false,AssumExpr(id,CHole (loc, None))) + [ [ id = name -> (None,AssumExpr(id,CHole (loc, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -352,13 +356,13 @@ GEXTEND Gram ; simple_assum_coe: [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> - (oc,(idl,c)) ] ] + (oc <> None,(idl,c)) ] ] ; constructor_type: [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> - fun l id -> (coe,(id,mkCProdN loc l c)) + fun l id -> (coe <> None,(id,mkCProdN loc l c)) | -> fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ] -> t l @@ -369,9 +373,12 @@ GEXTEND Gram [ [ id = identref; c=constructor_type -> c id ] ] ; of_type_with_opt_coercion: - [ [ ":>" -> true - | ":"; ">" -> true - | ":" -> false ] ] + [ [ ":>>" -> Some false + | ":>"; ">" -> Some false + | ":>" -> Some true + | ":"; ">"; ">" -> Some false + | ":"; ">" -> Some true + | ":" -> None ] ] ; END @@ -410,7 +417,8 @@ GEXTEND Gram | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - warning "Include Type is deprecated; use Include instead"; + Flags.if_verbose + msg_warning (str "Include Type is deprecated; use Include instead"); VernacInclude(e::l) ] ] ; export_token: @@ -442,13 +450,33 @@ GEXTEND Gram [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l) | -> [] ] ] ; + functor_app_annot: + [ [ IDENT "inline"; "at"; IDENT "level"; i = INT -> + [InlineAt (int_of_string i)], [] + | IDENT "no"; IDENT "inline" -> [NoInline], [] + | IDENT "scope"; sc1 = IDENT; IDENT "to"; sc2 = IDENT -> [], [sc1,sc2] + ] ] + ; + functor_app_annots: + [ [ "["; l = LIST1 functor_app_annot SEP ","; "]" -> + let inl,scs = List.split l in + let inl = match List.concat inl with + | [] -> DefaultInline + | [inl] -> inl + | _ -> error "Functor application with redundant inline annotations" + in { ann_inline = inl; ann_scope_subst = List.concat scs } + | -> { ann_inline = DefaultInline; ann_scope_subst = [] } + ] ] + ; module_expr_inl: - [ [ "!"; me = module_expr -> (me,false) - | me = module_expr -> (me,true) ] ] + [ [ "!"; me = module_expr -> + (me, { ann_inline = NoInline; ann_scope_subst = []}) + | me = module_expr; a = functor_app_annots -> (me,a) ] ] ; module_type_inl: - [ [ "!"; me = module_type -> (me,false) - | me = module_type -> (me,true) ] ] + [ [ "!"; me = module_type -> + (me, { ann_inline = NoInline; ann_scope_subst = []}) + | me = module_type; a = functor_app_annots -> (me,a) ] ] ; (* Module binder *) module_binder: @@ -458,7 +486,7 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CMapply (loc,me1,me2) ] ] ; module_expr_atom: @@ -474,8 +502,9 @@ GEXTEND Gram module_type: [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl) + | mty = module_type; me = module_expr_atom -> CMapply (loc,mty,me) + | mty = module_type; "with"; decl = with_declaration -> + CMwith (loc,mty,decl) ] ] ; END @@ -502,16 +531,16 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,false,CanonicalStructure),(dummy_loc,s),d, + ((Global,CanonicalStructure),(dummy_loc,s),d, (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((enforce_locality_exp true,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (enforce_locality_exp true, f, s, t) @@ -535,22 +564,75 @@ GEXTEND Gram VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; - props = [ ":="; "{"; r = record_declaration; "}" -> r | - ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> - VernacInstance (false, not (use_non_locality ()), + props = [ ":="; "{"; r = record_declaration; "}" -> Some r | + ":="; c = lconstr -> Some c | -> None ] -> + VernacInstance (false, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), props, pri) - | IDENT "Existing"; IDENT "Instance"; is = global -> - VernacDeclareInstance (not (use_section_locality ()), is) + | IDENT "Existing"; IDENT "Instance"; id = global -> + VernacDeclareInstances (not (use_section_locality ()), [id]) + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global -> + VernacDeclareInstances (not (use_section_locality ()), ids) | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is + (* Arguments *) + | IDENT "Arguments"; qid = smart_global; + impl = LIST1 [ l = LIST0 + [ item = argument_spec -> + let id, r, s = item in [`Id (id,r,s,false,false)] + | "/" -> [`Slash] + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items + ] -> l ] SEP ","; + mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> + let mods = match mods with None -> [] | Some l -> List.flatten l in + let impl = List.map List.flatten impl in + let rec aux n (narg, impl) = function + | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl + | `Slash :: tl -> aux (n+1) (n, impl) tl + | [] -> narg, impl in + let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in + let nargs, rest = List.hd nargs, List.tl nargs in + if List.exists ((<>) nargs) rest then + error "All arguments lists must have the same length"; + let err_incompat x y = + error ("Options \""^x^"\" and \""^y^"\" are incompatible") in + if nargs > 0 && List.mem `SimplNeverUnfold mods then + err_incompat "simpl never" "/"; + if List.mem `SimplNeverUnfold mods && + List.mem `SimplDontExposeCase mods then + err_incompat "simpl never" "simpl nomatch"; + VernacArguments (use_section_locality(), qid, impl, nargs, mods) + + (* moved there so that camlp5 factors it with the previous rule *) + | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; + "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> + Flags.if_verbose + msg_warning (str "Arguments Scope is deprecated; use Arguments instead"); + VernacArgumentsScope (use_section_locality (),qid,scl) + (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> + Flags.if_verbose + msg_warning (str "Implicit Arguments is deprecated; use Arguments instead"); VernacDeclareImplicits (use_section_locality (),qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> @@ -567,12 +649,33 @@ GEXTEND Gram idl = LIST1 identref -> Some idl ] -> VernacGeneralizable (use_non_locality (), gen) ] ] ; + arguments_modifier: + [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase] + | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold] + | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits] + | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] + | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] + | IDENT "rename" -> [`Rename] + | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> + [`ClearImplicits; `ClearScopes] + | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> + [`ClearImplicits; `ClearScopes] + ] ] + ; implicit_name: [ [ "!"; id = ident -> (id, false, true) | id = ident -> (id,false,false) | "["; "!"; id = ident; "]" -> (id,true,true) | "["; id = ident; "]" -> (id,true, false) ] ] ; + scope: + [ [ "%"; key = IDENT -> key ] ] + ; + argument_spec: [ + [ b = OPT "!"; id = name ; s = OPT scope -> + snd id, b <> None, Option.map (fun x -> loc, x) s + ] + ]; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque @@ -606,11 +709,11 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, not (use_non_locality ()), + VernacInstance (true, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), - CRecord (loc, None, []), pri) + None, pri) (* System directory *) | IDENT "Pwd" -> VernacChdir None @@ -627,9 +730,6 @@ GEXTEND Gram | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> VernacDeclareMLModule (use_locality (), l) - | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string -> - error "This command is deprecated, use Print Universes" - | IDENT "Locate"; l = locatable -> VernacLocate l (* Managing load paths *) @@ -668,18 +768,11 @@ GEXTEND Gram VernacSearch (SearchPattern c, l) | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchRewrite c, l) - | IDENT "SearchAbout"; - sl = [ "["; - l = LIST1 [ - b = positive_search_mark; s = ne_string; sc = OPT scope - -> b, SearchString (s,sc) - | b = positive_search_mark; p = constr_pattern - -> b, SearchSubPattern p - ]; "]" -> l - | p = constr_pattern -> [true,SearchSubPattern p] - | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ]; - l = in_or_out_modules -> - VernacSearch (SearchAbout sl, l) + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> + let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m) + (* compatibility format of SearchAbout, with "[ ... ]" *) + | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; + l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> VernacAddMLPath (false, dir) @@ -714,16 +807,13 @@ GEXTEND Gram | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption ([table;field], v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption ([table], v) - - | IDENT "proof" -> VernacDeclProof - | "return" -> VernacReturn ]] + VernacRemoveOption ([table], v) ]] ; check_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) | IDENT "Compute"; c = lconstr -> - fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c) + fun g -> VernacCheckMayEval (Some Glob_term.CbvVm, g, c) | IDENT "Check"; c = lconstr -> fun g -> VernacCheckMayEval (None, g, c) ] ] ; @@ -758,9 +848,10 @@ GEXTEND Gram | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s - | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s + | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid - | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt + | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt) + | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt) | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid) | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, qid) ] ] ; @@ -777,7 +868,7 @@ GEXTEND Gram | IDENT "Ltac"; qid = global -> LocateTactic qid ] ] ; option_value: - [ [ n = integer -> IntValue n + [ [ n = integer -> IntValue (Some n) | s = STRING -> StringValue s ] ] ; option_ref_value: @@ -785,14 +876,17 @@ GEXTEND Gram | s = STRING -> StringRefValue s ] ] ; option_table: - [ [ fl = LIST1 IDENT -> fl ]] + [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]] ; as_dirpath: [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] ; - in_or_out_modules: + ne_in_or_out_modules: [ [ IDENT "inside"; l = LIST1 global -> SearchInside l - | IDENT "outside"; l = LIST1 global -> SearchOutside l + | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ] + ; + in_or_out_modules: + [ [ m = ne_in_or_out_modules -> m | -> SearchOutside [] ] ] ; comment: @@ -806,6 +900,20 @@ GEXTEND Gram scope: [ [ "%"; key = IDENT -> key ] ] ; + searchabout_query: + [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> + (b, SearchString (s,sc)) + | b = positive_search_mark; p = constr_pattern -> + (b, SearchSubPattern p) + ] ] + ; + searchabout_queries: + [ [ m = ne_in_or_out_modules -> ([],m) + | s = searchabout_query; l = searchabout_queries -> + let (sl,m) = l in (s::sl,m) + | -> ([],SearchOutside []) + ] ] + ; END; GEXTEND Gram @@ -862,10 +970,6 @@ GEXTEND Gram | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 opt_scope; "]" -> - VernacArgumentsScope (use_section_locality (),qid,scl) - | IDENT "Infix"; local = obsolete_locality; op = ne_lstring; ":="; p = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; @@ -912,16 +1016,17 @@ GEXTEND Gram | IDENT "next"; IDENT "level" -> NextLevel ] ] ; syntax_modifier: - [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; + [ [ "at"; IDENT "level"; n = natural -> SetLevel n + | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA + | IDENT "right"; IDENT "associativity" -> SetAssoc RightA + | IDENT "no"; IDENT "associativity" -> SetAssoc NonA + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing + | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s + | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) - | "at"; IDENT "level"; n = natural -> SetLevel n - | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA - | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA - | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA + | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) - | IDENT "only"; IDENT "parsing" -> SetOnlyParsing - | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ] + ] ] ; syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference @@ -930,9 +1035,6 @@ GEXTEND Gram | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; - opt_scope: - [ [ "_" -> None | sc = IDENT -> Some sc ] ] - ; production_item: [ [ s = ne_string -> TacTerm s | nt = IDENT; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index b8fee3ff..c9e135ed 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -1,27 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* RProp Null - | "Set" -> RProp Pos - | "Type" -> RType None + | "Prop" -> GProp Null + | "Set" -> GProp Pos + | "Type" -> GType None | _ -> user_err_loc (loc,"",str "sort expected.") let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) @@ -138,63 +135,64 @@ let compute_branches_lengths ind = let compute_inductive_nargs ind = Inductiveops.inductive_nargs (Global.env()) ind -(* Interpreting constr as a rawconstr *) +(* Interpreting constr as a glob_constr *) let rec interp_xml_constr = function | XmlTag (loc,"REL",al,[]) -> - RVar (loc, get_xml_ident al) + GVar (loc, get_xml_ident al) | XmlTag (loc,"VAR",al,[]) -> error "XML parser: unable to interp free variables" | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) -> let body,decls = list_sep_last xl in let ctx = List.map interp_xml_decl decls in - List.fold_right (fun (na,t) b -> RLambda (loc, na, Explicit, t, b)) + List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b)) ctx (interp_xml_target body) | XmlTag (loc,"PROD",al,(_::_ as xl)) -> let body,decls = list_sep_last xl in let ctx = List.map interp_xml_decl decls in - List.fold_right (fun (na,t) b -> RProd (loc, na, Explicit, t, b)) + List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b)) ctx (interp_xml_target body) | XmlTag (loc,"LETIN",al,(_::_ as xl)) -> let body,defs = list_sep_last xl in let ctx = List.map interp_xml_def defs in - List.fold_right (fun (na,t) b -> RLetIn (loc, na, t, b)) + List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b)) ctx (interp_xml_target body) | XmlTag (loc,"APPLY",_,x::xl) -> - RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) + GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) | XmlTag (loc,"instantiate",_, (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) -> - RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl) + GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl) | XmlTag (loc,"META",al,xl) -> - REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl)) + GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl)) | XmlTag (loc,"CONST",al,[]) -> - RRef (loc, ConstRef (get_xml_constant al)) + GRef (loc, ConstRef (get_xml_constant al)) | XmlTag (loc,"MUTCASE",al,x::y::yl) -> let ind = get_xml_inductive al in let p = interp_xml_patternsType x in let tm = interp_xml_inductiveTerm y in - let brs = List.map interp_xml_pattern yl in - let brns = Array.to_list (compute_branches_lengths ind) in - let mat = simple_cases_matrix_of_branches ind brns brs in + let vars = compute_branches_lengths ind in + let brs = list_map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl + in + let mat = simple_cases_matrix_of_branches ind brs in let nparams,n = compute_inductive_nargs ind in let nal,rtn = return_type_of_predicate ind nparams n p in - RCases (loc,RegularStyle,rtn,[tm,nal],mat) + GCases (loc,RegularStyle,rtn,[tm,nal],mat) | XmlTag (loc,"MUTIND",al,[]) -> - RRef (loc, IndRef (get_xml_inductive al)) + GRef (loc, IndRef (get_xml_inductive al)) | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> - RRef (loc, ConstructRef (get_xml_constructor al)) + GRef (loc, ConstructRef (get_xml_constructor al)) | XmlTag (loc,"FIX",al,xl) -> let li,lnct = List.split (List.map interp_xml_FixFunction xl) in let ln,lc,lt = list_split3 lnct in let lctx = List.map (fun _ -> []) ln in - RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) + GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) | XmlTag (loc,"COFIX",al,xl) -> let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in - RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) + GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> - RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) + GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) | XmlTag (loc,"SORT",al,[]) -> - RSort (loc, get_xml_sort al) + GSort (loc, get_xml_sort al) | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") @@ -232,15 +230,15 @@ and interp_xml_recursionOrder x = let (locs, s) = get_xml_attr "type" al in match s with "Structural" -> - (match l with [] -> RStructRec + (match l with [] -> GStructRec | _ -> error_expect_no_argument loc) | "WellFounded" -> (match l with - [c] -> RWfRec (interp_xml_type c) + [c] -> GWfRec (interp_xml_type c) | _ -> error_expect_one_argument loc) | "Measure" -> (match l with - [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r)) + [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r)) | _ -> error_expect_two_arguments loc) | _ -> user_err_loc (locs,"",str "Invalid recursion order.") @@ -252,7 +250,7 @@ and interp_xml_FixFunction x = interp_xml_recursionOrder x1), (get_xml_name al, interp_xml_type x2, interp_xml_body x3)) | (loc,al,[x1;x2]) -> - ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec), + ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec), (get_xml_name al, interp_xml_type x1, interp_xml_body x2)) | (loc,_,_) -> error_expect_one_argument loc @@ -277,5 +275,5 @@ let rec interp_xml_tactic_arg = function let parse_tactic_arg ch = interp_xml_tactic_arg - (Pcoq.Gram.Entry.parse xml_eoi - (Pcoq.Gram.parsable (Stream.of_channel ch))) + (Pcoq.Gram.entry_parse xml_eoi + (Pcoq.Gram.parsable (Stream.of_channel ch))) diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli deleted file mode 100644 index 05c161c2..00000000 --- a/parsing/g_zsyntax.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* "Illegal character" + | Unterminated_comment -> "Unterminated comment" + | Unterminated_string -> "Unterminated string" + | Undefined_token -> "Undefined token" + | Bad_token tok -> Format.sprintf "Bad token %S" tok + | UnsupportedUnicode x -> + Printf.sprintf "Unsupported Unicode character (0x%x)" x) -exception Error of error + let print ppf x = Format.fprintf ppf "%s@." (to_string x) -let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str) +end +open Error -let bad_token str = raise (Error (Bad_token str)) +let err loc str = Loc.raise (make_loc loc) (Error.E str) + +let bad_token str = raise (Error.E (Bad_token str)) (* Lexer conventions on tokens *) @@ -96,9 +110,9 @@ type token_kind = | AsciiChar | EmptyStream -let error_unsupported_unicode_character n cs = +let error_unsupported_unicode_character n unicode cs = let bp = Stream.count cs in - err (bp,bp+n) (Bad_token "Unsupported Unicode character") + err (bp,bp+n) (UnsupportedUnicode unicode) let error_utf8 cs = let bp = Stream.count cs in @@ -147,7 +161,8 @@ let lookup_utf8_tail c cs = | _ -> error_utf8 cs in try classify_unicode unicode, n - with UnsupportedUtf8 -> njunk n cs; error_unsupported_unicode_character n cs + with UnsupportedUtf8 -> + njunk n cs; error_unsupported_unicode_character n unicode cs let lookup_utf8 cs = match Stream.peek cs with @@ -155,14 +170,26 @@ let lookup_utf8 cs = | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs) | None -> EmptyStream -let check_special_token str = +let unlocated f x = + try f x with Loc.Exc_located (_,exc) -> raise exc + +let check_keyword str = let rec loop_symb = parser | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str - | [< _ = Stream.empty >] -> () - | [< '_ ; s >] -> loop_symb s + | [< s >] -> + match unlocated lookup_utf8 s with + | Utf8Token (_,n) -> njunk n s; loop_symb s + | AsciiChar -> Stream.junk s; loop_symb s + | EmptyStream -> () in loop_symb (Stream.of_string str) +let check_keyword_to_add s = + try check_keyword s + with Error.E (UnsupportedUnicode unicode) -> + Flags.if_verbose msg_warning + (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x which will not be parsable." s unicode)) + let check_ident str = let rec loop_id intail = parser | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> @@ -170,7 +197,7 @@ let check_ident str = | [< ' ('0'..'9' | ''') when intail; s >] -> loop_id true s | [< s >] -> - match lookup_utf8 s with + match unlocated lookup_utf8 s with | Utf8Token (UnicodeLetter, n) -> njunk n s; loop_id true s | Utf8Token (UnicodeIdentPart, n) when intail -> njunk n s; loop_id true s | EmptyStream -> () @@ -178,9 +205,8 @@ let check_ident str = in loop_id false (Stream.of_string str) -let check_keyword str = - try check_special_token str - with Error _ -> check_ident str +let is_ident str = + try let _ = check_ident str in true with Error.E _ -> false (* Keyword and symbol dictionary *) let token_tree = ref empty_ttree @@ -190,22 +216,15 @@ let is_keyword s = with Not_found -> false let add_keyword str = - check_keyword str; - token_tree := ttree_add !token_tree str + if not (is_keyword str) then + begin + check_keyword_to_add str; + token_tree := ttree_add !token_tree str + end let remove_keyword str = token_tree := ttree_remove !token_tree str -(* Adding a new token (keyword or special token). *) -let add_token (con, str) = match con with - | "" -> add_keyword str - | "METAIDENT" | "LEFTQMARK" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI" - -> () - | _ -> - raise (Token.Error ("\ -the constructor \"" ^ con ^ "\" is not recognized by Lexer")) - - (* Freeze and unfreeze the state of the lexer *) type frozen_t = ttree @@ -249,17 +268,22 @@ let rec number len = parser | [< ' ('0'..'9' as c); s >] -> number (store len c) s | [< >] -> len -let escape len c = store len c - let rec string in_comments bp len = parser | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> if esc then string in_comments bp (store len '"') s else len + | [< ''('; s >] -> + (parser + | [< ''*'; s >] -> + string (Option.map succ in_comments) bp (store (store len '(') '*') s + | [< >] -> + string in_comments bp (store len '(') s) s | [< ''*'; s >] -> (parser | [< '')'; s >] -> - if in_comments then + if in_comments = Some 0 then msg_warning (str "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment."); - string in_comments bp (store (store len '*') ')') s + let in_comments = Option.map pred in_comments in + string in_comments bp (store (store len '*') ')') s | [< >] -> string in_comments bp (store len '*') s) s | [< 'c; s >] -> string in_comments bp (store len c) s @@ -348,7 +372,7 @@ let rec comment bp = parser bp2 | [< s >] -> real_push_char '*'; comment bp s >] -> () | [< ''"'; s >] -> if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) - else ignore (string true bp2 0 s); + else ignore (string (Some 0) bp2 0 s); comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment | [< 'z; s >] -> real_push_char z; comment bp s @@ -394,61 +418,68 @@ let find_keyword id s = let tt = ttree_find !token_tree id in match progress_further tt.node 0 tt s with | None -> raise Not_found - | Some c -> c + | Some c -> KEYWORD c (* Must be a special token *) let process_chars bp c cs = let t = progress_from_byte None (-1) !token_tree cs c in let ep = Stream.count cs in match t with - | Some t -> (("", t), (bp, ep)) + | Some t -> (KEYWORD t, (bp, ep)) | None -> let ep' = bp + utf8_char_size cs c in njunk (ep' - ep) cs; err (bp, ep') Undefined_token -let parse_after_dollar bp = - parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> - ("METAIDENT", get_buff len) - | [< s >] -> - match lookup_utf8 s with - | Utf8Token (UnicodeLetter, n) -> - ("METAIDENT", get_buff (ident_tail (nstore n 0 s) s)) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '$' s) +let token_of_special c s = match c with + | '$' -> METAIDENT s + | '.' -> FIELD s + | _ -> assert false -(* Parse what follows a dot *) -let parse_after_dot bp c = +(* Parse what follows a dot / a dollar *) + +let parse_after_special c bp = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> - ("FIELD", get_buff len) + | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] -> + token_of_special c (get_buff len) | [< s >] -> match lookup_utf8 s with | Utf8Token (UnicodeLetter, n) -> - ("FIELD", get_buff (ident_tail (nstore n 0 s) s)) - | AsciiChar | Utf8Token _ | EmptyStream -> - fst (process_chars bp c s) + token_of_special c (get_buff (ident_tail (nstore n 0 s) s)) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) (* Parse what follows a question mark *) + let parse_after_qmark bp s = match Stream.peek s with - |Some ('a'..'z' | 'A'..'Z' | '_') -> ("LEFTQMARK", "") - |None -> ("","?") + | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK + | None -> KEYWORD "?" | _ -> match lookup_utf8 s with - | Utf8Token (UnicodeLetter, _) -> ("LEFTQMARK", "") + | Utf8Token (UnicodeLetter, _) -> LEFTQMARK | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '?' s) +let blank_or_eof cs = + match Stream.peek cs with + | None -> true + | Some (' ' | '\t' | '\n' |'\r') -> true + | _ -> false (* Parse a token in a char stream *) + let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$'; t = parse_after_dollar bp >] ep -> + | [< ''$' as c; t = parse_after_special c bp >] ep -> comment_stop bp; (t, (ep, bp)) - | [< ''.' as c; t = parse_after_dot bp c >] ep -> + | [< ''.' as c; t = parse_after_special c bp; s >] ep -> comment_stop bp; - if Flags.do_beautify() & t=("",".") then between_com := true; + (* We enforce that "." should either be part of a larger keyword, + for instance ".(", or followed by a blank or eof. *) + if t = KEYWORD "." then begin + if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; + if Flags.do_beautify() then between_com := true; + end; (t, (bp,ep)) | [< ''?'; s >] ep -> let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) @@ -456,13 +487,13 @@ let rec next_token = parser bp len = ident_tail (store 0 c); s >] ep -> let id = get_buff len in comment_stop bp; - (try ("", find_keyword id s) with Not_found -> ("IDENT", id)), (bp, ep) + (try find_keyword id s with Not_found -> IDENT id), (bp, ep) | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> comment_stop bp; - (("INT", get_buff len), (bp, ep)) - | [< ''\"'; len = string false bp 0 >] ep -> + (INT (get_buff len), (bp, ep)) + | [< ''\"'; len = string None bp 0 >] ep -> comment_stop bp; - (("STRING", get_buff len), (bp, ep)) + (STRING (get_buff len), (bp, ep)) | [< ' ('(' as c); t = parser | [< ''*'; s >] -> @@ -479,62 +510,53 @@ let rec next_token = parser bp let id = get_buff len in let ep = Stream.count s in comment_stop bp; - (try ("",find_keyword id s) with Not_found -> ("IDENT",id)), (bp, ep) + (try find_keyword id s with Not_found -> IDENT id), (bp, ep) | AsciiChar | Utf8Token ((UnicodeSymbol | UnicodeIdentPart), _) -> let t = process_chars bp (Stream.next s) s in comment_stop bp; t | EmptyStream -> - comment_stop bp; (("EOI", ""), (bp, bp + 1)) + comment_stop bp; (EOI, (bp, bp + 1)) + +(* (* Debug: uncomment this for tracing tokens seen by coq...*) +let next_token s = + let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t); + (t,(bp,ep)) +*) (* Location table system for creating tables associating a token count to its location in a char stream (the source) *) let locerr () = invalid_arg "Lexer: location function" -let tsz = 256 (* up to 2^29 entries on a 32-bit machine, 2^61 on 64-bit *) - -let loct_create () = ref [| [| |] |] +let loct_create () = Hashtbl.create 207 let loct_func loct i = - match - if i < 0 || i/tsz >= Array.length !loct then None - else if !loct.(i/tsz) = [| |] then None - else !loct.(i/tsz).(i mod tsz) - with - | Some loc -> Util.make_loc loc - | _ -> locerr () - -let loct_add loct i loc = - while i/tsz >= Array.length !loct do - let new_tmax = Array.length !loct * 2 in - let new_loct = Array.make new_tmax [| |] in - Array.blit !loct 0 new_loct 0 (Array.length !loct); - loct := new_loct; - done; - if !loct.(i/tsz) = [| |] then !loct.(i/tsz) <- Array.make tsz None; - !loct.(i/tsz).(i mod tsz) <- Some loc - -let current_location_table = ref (ref [| [| |] |]) - -let location_function n = - loct_func !current_location_table n + try Hashtbl.find loct i with Not_found -> locerr () -let func cs = - let loct = loct_create () in - let ts = - Stream.from - (fun i -> - let (tok, loc) = next_token cs in - loct_add loct i loc; Some tok) - in - current_location_table := loct; - (ts, loct_func loct) +let loct_add loct i loc = Hashtbl.add loct i loc + +let current_location_table = ref (loct_create ()) -type location_table = (int * int) option array array ref +type location_table = (int, loc) Hashtbl.t let location_table () = !current_location_table let restore_location_table t = current_location_table := t +let location_function n = loct_func !current_location_table n -(* Names of tokens, for this lexer, used in Grammar error messages *) +(** {6 The lexer of Coq} *) + +(** Note: removing a token. + We do nothing because [remove_token] is called only when removing a grammar + rule with [Grammar.delete_rule]. The latter command is called only when + unfreezing the state of the grammar entries (see GRAMMAR summary, file + env/metasyntax.ml). Therefore, instead of removing tokens one by one, + we unfreeze the state of the lexer. This restores the behaviour of the + lexer. B.B. *) + +IFDEF CAMLP5 THEN + +type te = Tok.t + +(** Names of tokens, for this lexer, used in Grammar error messages *) let token_text = function | ("", t) -> "'" ^ t ^ "'" @@ -547,43 +569,65 @@ let token_text = function | (con, "") -> con | (con, prm) -> con ^ " \"" ^ prm ^ "\"" -(* The lexer of Coq *) - -(* Note: removing a token. - We do nothing because [remove_token] is called only when removing a grammar - rule with [Grammar.delete_rule]. The latter command is called only when - unfreezing the state of the grammar entries (see GRAMMAR summary, file - env/metasyntax.ml). Therefore, instead of removing tokens one by one, - we unfreeze the state of the lexer. This restores the behaviour of the - lexer. B.B. *) - -IFDEF CAMLP5 THEN +let func cs = + let loct = loct_create () in + let ts = + Stream.from + (fun i -> + let (tok, loc) = next_token cs in + loct_add loct i (make_loc loc); Some tok) + in + current_location_table := loct; + (ts, loct_func loct) let lexer = { Token.tok_func = func; - Token.tok_using = add_token; + Token.tok_using = + (fun pat -> match Tok.of_pattern pat with + | KEYWORD s -> add_keyword s + | _ -> ()); Token.tok_removing = (fun _ -> ()); - Token.tok_match = default_match; + Token.tok_match = Tok.match_pattern; Token.tok_comm = None; Token.tok_text = token_text } -ELSE - -let lexer = { - Token.func = func; - Token.using = add_token; - Token.removing = (fun _ -> ()); - Token.tparse = (fun _ -> None); - Token.text = token_text } +ELSE (* official camlp4 for ocaml >= 3.10 *) + +module M_ = Camlp4.ErrorHandler.Register (Error) + +module Loc = Loc +module Token = struct + include Tok (* Cf. tok.ml *) + module Loc = Loc + module Error = Camlp4.Struct.EmptyError + module Filter = struct + type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t + type t = unit + let mk _is_kwd = () + let keyword_added () kwd _ = add_keyword kwd + let keyword_removed () _ = () + let filter () x = x + let define_filter () _ = () + end +end + +let mk () _init_loc(*FIXME*) cs = + let loct = loct_create () in + let rec self = + parser i + [< (tok, loc) = next_token; s >] -> + let loc = make_loc loc in + loct_add loct i loc; + [< '(tok, loc); self s >] + | [< >] -> [< >] + in current_location_table := loct; self cs END -(* Terminal symbols interpretation *) +(** Terminal symbols interpretation *) let is_ident_not_keyword s = - match s.[0] with - | 'a'..'z' | 'A'..'Z' | '_' -> not (is_keyword s) - | _ -> false + is_ident s && not (is_keyword s) let is_number s = let rec aux i = @@ -613,6 +657,6 @@ let strip s = let terminal s = let s = strip s in if s = "" then failwith "empty token"; - if is_ident_not_keyword s then ("IDENT", s) - else if is_number s then ("INT", s) - else ("", s) + if is_ident_not_keyword s then IDENT s + else if is_number s then INT s + else KEYWORD s diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 93fc4231..1899f7f4 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -1,37 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit +val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool val location_function : int -> loc -(* for coqdoc *) +(** for coqdoc *) type location_table val location_table : unit -> location_table val restore_location_table : location_table -> unit val check_ident : string -> unit +val is_ident : string -> bool val check_keyword : string -> unit type frozen_t @@ -45,8 +35,8 @@ val restore_com_state: com_state -> unit val set_xml_output_comment : (string -> unit) -> unit -val terminal : string -> string * string +val terminal : string -> Tok.t -(* The lexer of Coq *) +(** The lexer of Coq: *) -val lexer : Compat.lexer +include Compat.LexerSig diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index c0c1817d..84a08d54 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -6,7 +6,6 @@ G_xml Ppconstr Printer Pptactic -Ppdecl_proof Tactic_printer Printmod Prettyp diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ff5213ef..075440f1 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -1,77 +1,96 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*