diff options
Diffstat (limited to 'parsing/argextend.ml4')
| -rw-r--r-- | parsing/argextend.ml4 | 74 |
1 files changed, 68 insertions, 6 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 3266fcf9..f554522a 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -107,6 +107,64 @@ let rec make_wit loc = function 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 [ _ -> 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< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> @@ -144,9 +202,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let interp = match f with | None -> <:expr< fun ist gl x -> - out_gen $make_wit loc globtyp$ - (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 -> @@ -160,10 +220,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) 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 + 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$ >>; + Genarg.create_arg $default_value$ $se$>>; <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { @@ -171,7 +232,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = ((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))))); Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) @@ -195,7 +257,7 @@ let declare_vernac_argument loc s pr cl = [ <: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$ >>; + $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>; <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { |