diff options
Diffstat (limited to 'parsing/argextend.ml4')
-rw-r--r-- | parsing/argextend.ml4 | 213 |
1 files changed, 146 insertions, 67 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 848223a0..214a6b98 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -1,21 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) - -(* $Id: argextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) +(*i camlp4deps: "tools/compat5b.cmo" i*) open Genarg open Q_util -open Q_coqast open Egrammar +open Pcoq +open Compat -let join_loc = Util.join_loc let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> @@ -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,50 +100,113 @@ 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 has_extraarg = + List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false) + +let statically_known_possibly_empty s (prods,_) = + List.for_all (function + | GramNonTerminal(_,ExtraArgType s',_,_) -> + (* For ExtraArg we don't know (we'll have to test dynamically) *) + (* unless it is a recursive call *) + s <> s' + | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) -> + (* Opt and List0 parses the empty string *) + true + | _ -> + (* This consumes a token for sure *) false) + prods + +let possibly_empty_subentries loc (prods,act) = + let bind_name p v e = match p with + | None -> e + | Some id -> + let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in + let rec aux = function + | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >> + | GramNonTerminal(_,OptArgType _,_,p) :: tl -> + bind_name p <:expr< None >> (aux tl) + | GramNonTerminal(_,List0ArgType _,_,p) :: tl -> + bind_name p <:expr< [] >> (aux tl) + | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl -> + (* We check at runtime if extraarg s parses "epsilon" *) + let s = match p with None -> "_" | Some id -> Names.string_of_id id in + <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit loc t$ with + [ None -> raise Exit + | Some v -> v ] in $aux tl$ >> + | _ -> assert false (* already filtered out *) in + if has_extraarg prods then + (* Needs a dynamic check; catch all exceptions if ever some rhs raises *) + (* an exception rather than returning a value; *) + (* declares loc because some code can refer to it; *) + (* ensures loc is used to avoid "unused variable" warning *) + (true, <:expr< try Some $aux prods$ with [ e when Errors.noncritical e -> None ] >>) + else + (* Static optimisation *) + (false, aux prods) + +let make_possibly_empty_subentries loc s cl = + let cl = List.filter (statically_known_possibly_empty s) cl in + if cl = [] then + <:expr< None >> + else + let rec aux = function + | (true, e) :: l -> + <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >> + | (false, e) :: _ -> + <:expr< Some $e$ >> + | [] -> + <:expr< None >> in + aux (List.map (possibly_empty_subentries loc) cl) 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$ - (Tacinterp.interp_genarg ist gl - (Genarg.in_gen $make_globwit loc globtyp$ x)) >> + let (sigma,a_interp) = + Tacinterp.interp_genarg ist gl + (Genarg.in_gen $make_globwit loc globtyp$ x) + in + (sigma , out_gen $make_wit loc globtyp$ a_interp)>> | Some f -> <:expr< $lid:f$>> in let substitute = match h with | None -> @@ -149,28 +220,29 @@ 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; + let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in + 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 $default_value$ $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)))), (fun ist gl x -> - (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))), + let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in + (sigma , Genarg.in_gen $wit$ a_interp)), (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 +253,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 None $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 +327,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 |