diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 289 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 54 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 597 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 101 | ||||
| -rw-r--r-- | grammar/q_util.mli | 35 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 204 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 94 |
7 files changed, 328 insertions, 1046 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index b3c71a703..0e52dc948 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -8,150 +8,105 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) -open Genarg open Q_util -open Egramml open Compat -open Pcoq let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> -let qualified_name loc s = - let path = CString.split '.' s in - let (name, path) = CList.sep_last path in - qualified_name loc path name - -let mk_extraarg loc s = - try - let name = Genarg.get_name0 s in - qualified_name loc name - with Not_found -> - <:expr< $lid:"wit_"^s$ >> +let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function - | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> - | IdentArgType -> <:expr< Constrarg.wit_ident >> - | VarArgType -> <:expr< Constrarg.wit_var >> - | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >> - | GenArgType -> <:expr< Constrarg.wit_genarg >> - | ConstrArgType -> <:expr< Constrarg.wit_constr >> - | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >> - | RedExprArgType -> <:expr< Constrarg.wit_red_expr >> - | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >> - | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >> - | BindingsArgType -> <:expr< Constrarg.wit_bindings >> | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> | 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 -> mk_extraarg loc s +let is_self s = function +| ExtraArgType s' -> s = s' +| _ -> false + let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> -let has_extraarg = - List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false) +let make_act loc act pil = + let rec make = function + | [] -> <:expr< (fun loc -> $act$) >> + | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtTerminal _ :: tl -> + <:expr< (fun _ -> $make tl$) >> in + make (List.rev pil) -let rec is_possibly_empty = function -| Aopt _ | Alist0 _ | Alist0sep _ | Amodifiers _ -> true -| Alist1 t | Alist1sep (t, _) -> is_possibly_empty t -| _ -> false +let make_prod_item = function + | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> + | ExtNonTerminal (g, _) -> + let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in + mlexpr_of_prod_entry_key base g -let rec get_empty_entry = function -| Aopt _ -> <:expr< None >> -| Alist0 _ | Alist0sep _ | Amodifiers _ -> <:expr< [] >> -| Alist1 t | Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >> -| _ -> assert false +let rec make_prod = function +| [] -> <:expr< Extend.Stop >> +| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> -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(_,_,e,_) -> - is_possibly_empty e - | GramTerminal _ -> - (* This consumes a token for sure *) false) - prods +let make_rule loc (prods,act) = + <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> -let possibly_empty_subentries loc (prods,act) = - let bind_name p v e = match p with - | None -> e - | Some id -> - let s = Names.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in - let rec aux = function - | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >> - | GramNonTerminal(_,_,e,p) :: tl when is_possibly_empty e -> - bind_name p (get_empty_entry e) (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.Id.to_string id in - <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit 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 [ Exit -> None ] >>) - else - (* Static optimisation *) - (false, aux prods) +let is_ident x = function +| <:expr< $lid:s$ >> -> (s : string) = x +| _ -> false -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_extend loc s cl wit = match cl with +| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act -> + (** Special handling of identity arguments by not redeclaring an entry *) + <:str_item< + value $lid:s$ = + let () = Pcoq.register_grammar $wit$ $lid:e$ in + $lid:e$ + >> +| _ -> + let se = mlexpr_of_string s in + let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in + <:str_item< + value $lid:s$ = + let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + $lid:s$ >> -let make_act loc act pil = - let rec make = function - | [] -> <:expr< Pcoq.Gram.action (fun loc -> let loc = Compat.to_coqloc loc in ($act$ : 'a)) >> - | GramNonTerminal (_,t,_,Some p) :: tl -> - let p = Names.Id.to_string p in - <:expr< - Pcoq.Gram.action - (fun $lid:p$ -> - let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) - >> - | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl -> - <:expr< Pcoq.Gram.action (fun _ -> $make tl$) >> in - make (List.rev pil) +let warning_redundant prefix s = + Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s -let make_prod_item = function - | 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 get_type prefix s = function +| None -> None +| Some typ -> + if is_self s typ then + let () = warning_redundant prefix s in None + else Some typ -let make_rule loc (prods,act) = - <:expr< ($mlexpr_of_list make_prod_item prods$,$make_act loc act prods$) >> +let check_type prefix s = function +| None -> () +| Some _ -> warning_redundant prefix s -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 +let declare_tactic_argument loc s (typ, f, g, h) cl = + let se = mlexpr_of_string s in + let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with + | `Uniform (typ, pr) -> + let typ = get_type "" s typ in + typ, pr, typ, pr, typ, pr + | `Specialized (a, rpr, c, gpr, e, tpr) -> + (** Check that we actually need the TYPED AS arguments *) + let rawtyp = get_type "RAW_" s a in + let glbtyp = get_type "GLOB_" s c in + let toptyp = get_type "" s e in + let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in + let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in + rawtyp, rpr, glbtyp, gpr, toptyp, tpr in let glob = match g with | None -> begin match rawtyp with - | Genarg.ExtraArgType s' when CString.equal s s' -> - <:expr< fun ist v -> (ist, v) >> - | _ -> + | None -> <:expr< fun ist v -> (ist, v) >> + | Some rawtyp -> <:expr< fun ist v -> let ans = out_gen $make_globwit loc rawtyp$ (Tacintern.intern_genarg ist @@ -164,73 +119,73 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let interp = match f with | None -> begin match globtyp with - | Genarg.ExtraArgType s' when CString.equal s s' -> - <:expr< fun ist gl v -> (gl.Evd.sigma, v) >> - | _ -> - <:expr< fun ist gl x -> - let (sigma,a_interp) = - Tacinterp.interp_genarg ist - (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it - (Genarg.in_gen $make_globwit loc globtyp$ x) - in - (sigma , out_gen $make_topwit loc globtyp$ a_interp)>> + | None -> + let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in + <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> + | Some globtyp -> + <:expr< fun ist x -> + Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> end - | Some f -> <:expr< $lid:f$>> in + | Some f -> + (** Compatibility layer, TODO: remove me *) + let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in + <:expr< + let f = $lid:f$ in + fun ist v -> Ftactic.nf_s_enter { Proofview.Goal.s_enter = fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in + Sigma.Unsafe.of_pair (Ftactic.return v, sigma) + } + >> in let subst = match h with | None -> begin match globtyp with - | Genarg.ExtraArgType s' when CString.equal s s' -> - <:expr< fun s v -> v >> - | _ -> + | None -> <:expr< fun s v -> v >> + | Some globtyp -> <:expr< fun s x -> out_gen $make_globwit loc globtyp$ (Tacsubst.subst_genarg s (Genarg.in_gen $make_globwit loc globtyp$ x)) >> end | Some f -> <:expr< $lid:f$>> in - let se = mlexpr_of_string s in + let dyn = match typ with + | None -> <:expr< None >> + | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> + in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> 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$) = Genarg.make0 $default_value$ $se$ >>; + [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; + make_extend loc s cl wit; <:str_item< do { - Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) - (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule - $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$ } - >> ] + $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; + Tacentries.create_ltac_quotation $se$ + (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v)) + ($lid:s$, None) + } >> ] let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in let pr_rules = match pr with | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = - Genarg.create_arg None $se$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; + Genarg.create_arg $se$ >>; + make_extend loc s cl wit; <:str_item< do { - Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) - (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $pr_rules$ (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } >> ] -open Pcoq open Pcaml open PcamlSig (* necessary for camlp4 *) @@ -248,22 +203,25 @@ EXTEND "END" -> declare_vernac_argument loc s pr l ] ] ; + argextend_specialized: + [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ]; + "RAW_PRINTED"; "BY"; rawpr = LIDENT; + globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ]; + "GLOB_PRINTED"; "BY"; globpr = LIDENT -> + (rawtyp, rawpr, globtyp, globpr) ] ] + ; argextend_header: - [ [ "TYPED"; "AS"; typ = argtype; + [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; "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) ] ] + special = OPT argextend_specialized -> + let repr = match special with + | None -> `Uniform (typ, pr) + | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) + in + (repr, f, g, h) ] ] ; argtype: [ "2" @@ -272,7 +230,9 @@ EXTEND [ e = argtype; LIDENT "list" -> ListArgType e | e = argtype; LIDENT "option" -> OptArgType e ] | "0" - [ e = LIDENT -> fst (interp_entry_name false None e "") + [ e = LIDENT -> + let e = parse_user_entry e "" in + type_of_user_symbol e | "("; e = argtype; ")" -> e ] ] ; argrule: @@ -280,15 +240,12 @@ EXTEND ; genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name false None e "" in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name false None e sep in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) - | s = STRING -> - if String.length s > 0 && Util.is_letter s.[0] then - CLexer.add_keyword s; - GramTerminal s + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) + | s = STRING -> ExtTerminal s ] ] ; entry_name: diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 1864fae5f..9b24c9797 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,65 +1,13 @@ Coq_config -Hook -Terminal -Canary -Hashset -Hashcons -CSet -CMap -Int -HMap -Option Store Exninfo -Backtrace -Pp_control -Flags Loc -CList -CString -Serialize -Stateid -Feedback -Pp -CArray -CStack -Util -Ppstyle -Errors -Bigint -Predicate -Segmenttree -Unicodetable -Unicode -Genarg - -Evar -Names - -Libnames - -Redops -Miscops -Locusops - -Stdarg -Constrarg -Constrexpr_ops - -Compat Tok -CLexer -Pcoq -G_prim -G_tactic -G_ltac -G_constr +Compat Q_util -Q_coqast -Egramml Argextend Tacextend Vernacextend diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 deleted file mode 100644 index 304e49923..000000000 --- a/grammar/q_coqast.ml4 +++ /dev/null @@ -1,597 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Q_util -open Compat - -let is_meta s = String.length s > 0 && s.[0] == '$' - -let purge_str s = - if String.length s == 0 || s.[0] <> '$' then s - else String.sub s 1 (String.length s - 1) - -let anti loc x = - expl_anti loc <:expr< $lid:purge_str x$ >> - -(* We don't give location for tactic quotation! *) -let loc = CompatLoc.ghost - -let dloc = <:expr< Loc.ghost >> - -let mlexpr_of_ident id = - <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >> - -let mlexpr_of_name = function - | Names.Anonymous -> <:expr< Names.Anonymous >> - | Names.Name id -> - <:expr< Names.Name (Names.Id.of_string $str:Names.Id.to_string id$) >> - -let mlexpr_of_dirpath dir = - let l = Names.DirPath.repr dir in - <:expr< Names.DirPath.make $mlexpr_of_list mlexpr_of_ident l$ >> - -let mlexpr_of_qualid qid = - let (dir, id) = Libnames.repr_qualid qid in - <:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> - -let mlexpr_of_reference = function - | Libnames.Qualid (loc,qid) -> - let loc = of_coqloc loc in <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> - | Libnames.Ident (loc,id) -> - let loc = of_coqloc loc in <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> - -let mlexpr_of_union f g = function - | Util.Inl a -> <:expr< Util.Inl $f a$ >> - | Util.Inr b -> <:expr< Util.Inr $g b$ >> - -let mlexpr_of_located f (loc,x) = - let loc = of_coqloc loc in - <:expr< ($dloc$, $f x$) >> - -let mlexpr_of_loc loc = <:expr< $dloc$ >> - -let mlexpr_of_by_notation f = function - | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >> - | Misctypes.ByNotation (loc,s,sco) -> - let loc = of_coqloc loc in - <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> - -let mlexpr_of_global_flag = function - | Tacexpr.TacGlobal -> <:expr<Tacexpr.TacGlobal>> - | Tacexpr.TacLocal -> <:expr<Tacexpr.TacLocal>> - -let mlexpr_of_intro_pattern_disjunctive = function - _ -> failwith "mlexpr_of_intro_pattern_disjunctive: TODO" - -let mlexpr_of_intro_pattern_naming = function - | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >> - | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >> - | Misctypes.IntroIdentifier id -> - <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> - -let mlexpr_of_intro_pattern = function - | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> - | Misctypes.IntroNaming pat -> - <:expr< Misctypes.IntroNaming $mlexpr_of_intro_pattern_naming pat$ >> - | Misctypes.IntroAction _ -> - failwith "mlexpr_of_intro_pattern: TODO" - -let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) - -let mlexpr_of_quantified_hypothesis = function - | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> - | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> - -let mlexpr_of_or_var f = function - | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >> - | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> - -let mlexpr_of_hyp = (mlexpr_of_located mlexpr_of_ident) - -let mlexpr_of_occs = function - | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >> - | Locus.AllOccurrencesBut l -> - <:expr< Locus.AllOccurrencesBut - $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> - | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >> - | Locus.OnlyOccurrences l -> - <:expr< Locus.OnlyOccurrences - $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> - -let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f - -let mlexpr_of_hyp_location = function - | occs, Locus.InHyp -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >> - | occs, Locus.InHypTypeOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >> - | occs, Locus.InHypValueOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >> - -let mlexpr_of_clause cl = - <:expr< {Locus.onhyps= - $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location) - cl.Locus.onhyps$; - Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >> - -let mlexpr_of_red_flags { - Genredexpr.rBeta = bb; - Genredexpr.rIota = bi; - Genredexpr.rZeta = bz; - Genredexpr.rDelta = bd; - Genredexpr.rConst = l -} = <:expr< { - Genredexpr.rBeta = $mlexpr_of_bool bb$; - Genredexpr.rIota = $mlexpr_of_bool bi$; - Genredexpr.rZeta = $mlexpr_of_bool bz$; - Genredexpr.rDelta = $mlexpr_of_bool bd$; - Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$ -} >> - -let mlexpr_of_instance c = <:expr< None >> - -let mlexpr_of_explicitation = function - | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >> - | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >> - -let mlexpr_of_binding_kind = function - | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >> - | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >> - -let mlexpr_of_binder_kind = function - | Constrexpr.Default b -> <:expr< Constrexpr.Default $mlexpr_of_binding_kind b$ >> - | Constrexpr.Generalized (b,b',b'') -> - <:expr< Constrexpr.TypeClass $mlexpr_of_binding_kind b$ - $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >> - -let rec mlexpr_of_constr = function - | Constrexpr.CRef (Libnames.Ident (loc,id),_) when is_meta (Id.to_string id) -> - let loc = of_coqloc loc in - anti loc (Id.to_string id) - | Constrexpr.CRef (r,n) -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ None >> - | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CProdN (loc,l,a) -> - let loc = of_coqloc loc in - <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list - (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> - | Constrexpr.CLambdaN (loc,l,a) -> - let loc = of_coqloc loc in - <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> - | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CAppExpl (loc,(p,r,us),l) -> - let loc = of_coqloc loc in - let a = (p,r,us) in - <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_triple (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference mlexpr_of_instance a$ $mlexpr_of_list mlexpr_of_constr l$ >> - | Constrexpr.CApp (loc,a,l) -> - let loc = of_coqloc loc in - <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >> - | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CHole (loc, None, ipat, None) -> - let loc = of_coqloc loc in - <:expr< Constrexpr.CHole $dloc$ None $mlexpr_of_intro_pattern_naming ipat$ None >> - | Constrexpr.CHole (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" - | Constrexpr.CNotation(_,ntn,(subst,substl,[])) -> - <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$ - ($mlexpr_of_list mlexpr_of_constr subst$, - $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >> - | Constrexpr.CPatVar (loc,n) -> - let loc = of_coqloc loc in - <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_ident n$ >> - | Constrexpr.CEvar (loc,n,[]) -> - let loc = of_coqloc loc in - <:expr< Constrexpr.CEvar $dloc$ $mlexpr_of_ident n$ [] >> - | _ -> failwith "mlexpr_of_constr: TODO" - -let mlexpr_of_occ_constr = - mlexpr_of_occurrences mlexpr_of_constr - -let mlexpr_of_occ_ref_or_constr = - mlexpr_of_occurrences - (mlexpr_of_union - (mlexpr_of_by_notation mlexpr_of_reference) mlexpr_of_constr) - -let mlexpr_of_red_expr = function - | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >> - | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >> - | Genredexpr.Simpl (f,o) -> - <:expr< Genredexpr.Simpl $mlexpr_of_red_flags f$ $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >> - | Genredexpr.Cbv f -> - <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >> - | Genredexpr.Cbn f -> - <:expr< Genredexpr.Cbn $mlexpr_of_red_flags f$ >> - | Genredexpr.Lazy f -> - <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >> - | Genredexpr.Unfold l -> - let f1 = mlexpr_of_by_notation mlexpr_of_reference in - let f = mlexpr_of_list (mlexpr_of_occurrences f1) in - <:expr< Genredexpr.Unfold $f l$ >> - | Genredexpr.Fold l -> - <:expr< Genredexpr.Fold $mlexpr_of_list mlexpr_of_constr l$ >> - | Genredexpr.Pattern l -> - let f = mlexpr_of_list mlexpr_of_occ_constr in - <:expr< Genredexpr.Pattern $f l$ >> - | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >> - | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >> - | Genredexpr.ExtraRedExpr s -> - <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> - -let rec mlexpr_of_argtype loc = function - | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> - | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >> - | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> - | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >> - | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> - | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> - | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> - | Genarg.GenArgType -> <:expr< Genarg.GenArgType >> - | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> - | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> - | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >> - | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >> - | Genarg.PairArgType (t1,t2) -> - let t1 = mlexpr_of_argtype loc t1 in - let t2 = mlexpr_of_argtype loc t2 in - <:expr< Genarg.PairArgType $t1$ $t2$ >> - | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> - -let mlexpr_of_may_eval f = function - | Genredexpr.ConstrEval (r,c) -> - <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >> - | Genredexpr.ConstrContext ((loc,id),c) -> - let loc = of_coqloc loc in - let id = mlexpr_of_ident id in - <:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >> - | Genredexpr.ConstrTypeOf c -> - <:expr< Genredexpr.ConstrTypeOf $mlexpr_of_constr c$ >> - | Genredexpr.ConstrTerm c -> - <:expr< Genredexpr.ConstrTerm $mlexpr_of_constr c$ >> - -let mlexpr_of_binding_kind = function - | Misctypes.ExplicitBindings l -> - let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in - <:expr< Misctypes.ExplicitBindings $l$ >> - | Misctypes.ImplicitBindings l -> - let l = mlexpr_of_list mlexpr_of_constr l in - <:expr< Misctypes.ImplicitBindings $l$ >> - | Misctypes.NoBindings -> - <:expr< Misctypes.NoBindings >> - -let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr - -let mlexpr_of_constr_with_binding = - mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind - -let mlexpr_of_constr_with_binding_arg = - mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) mlexpr_of_constr_with_binding - -let mlexpr_of_move_location f = function - | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >> - | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >> - | Misctypes.MoveFirst -> <:expr< Misctypes.MoveFirst >> - | Misctypes.MoveLast -> <:expr< Misctypes.MoveLast >> - -let mlexpr_of_induction_arg = function - | Tacexpr.ElimOnConstr c -> - <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >> - | Tacexpr.ElimOnIdent (_,id) -> - <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >> - | Tacexpr.ElimOnAnonHyp n -> - <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >> - -let mlexpr_of_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO" - -let mlexpr_of_pattern_ast = mlexpr_of_constr - -let mlexpr_of_entry_type = function - _ -> failwith "mlexpr_of_entry_type: TODO" - -let mlexpr_of_match_lazy_flag = function - | Tacexpr.General -> <:expr<Tacexpr.General>> - | Tacexpr.Select -> <:expr<Tacexpr.Select>> - | Tacexpr.Once -> <:expr<Tacexpr.Once>> - -let mlexpr_of_match_pattern = function - | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >> - | Tacexpr.Subterm (b,ido,t) -> - <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >> - -let mlexpr_of_match_context_hyps = function - | Tacexpr.Hyp (id,l) -> - let f = mlexpr_of_located mlexpr_of_name in - <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >> - | Tacexpr.Def (id,v,l) -> - let f = mlexpr_of_located mlexpr_of_name in - <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >> - -let mlexpr_of_match_rule f = function - | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >> - | Tacexpr.All t -> <:expr< Tacexpr.All $f t$ >> - -let mlexpr_of_message_token = function - | Tacexpr.MsgString s -> <:expr< Tacexpr.MsgString $str:s$ >> - | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >> - | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >> - -let mlexpr_of_debug = function - | Tacexpr.Off -> <:expr< Tacexpr.Off >> - | Tacexpr.Debug -> <:expr< Tacexpr.Debug >> - | Tacexpr.Info -> <:expr< Tacexpr.Info >> - -let rec mlexpr_of_atomic_tactic = function - (* Basic tactics *) - | Tacexpr.TacIntroPattern pl -> - let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in - <:expr< Tacexpr.TacIntroPattern $pl$ >> - | Tacexpr.TacIntroMove (idopt,idopt') -> - let idopt = mlexpr_of_ident_option idopt in - let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in - <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> - | Tacexpr.TacExact c -> - <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> - | Tacexpr.TacApply (b,false,cb,None) -> - <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding_arg cb$ None >> - | Tacexpr.TacElim (false,cb,cbo) -> - let cb = mlexpr_of_constr_with_binding_arg cb in - let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> - | Tacexpr.TacCase (false,cb) -> - let cb = mlexpr_of_constr_with_binding_arg cb in - <:expr< Tacexpr.TacCase False $cb$ >> - | Tacexpr.TacFix (ido,n) -> - let ido = mlexpr_of_ident_option ido in - let n = mlexpr_of_int n in - <:expr< Tacexpr.TacFix $ido$ $n$ >> - | Tacexpr.TacMutualFix (id,n,l) -> - let id = mlexpr_of_ident id in - let n = mlexpr_of_int n in - let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in - let l = mlexpr_of_list f l in - <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >> - | Tacexpr.TacCofix ido -> - let ido = mlexpr_of_ident_option ido in - <:expr< Tacexpr.TacCofix $ido$ >> - | Tacexpr.TacMutualCofix (id,l) -> - let id = mlexpr_of_ident id in - let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in - let l = mlexpr_of_list f l in - <:expr< Tacexpr.TacMutualCofix $id$ $l$ >> - - | Tacexpr.TacAssert (b,t,ipat,c) -> - let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in - <:expr< Tacexpr.TacAssert $mlexpr_of_bool b$ - $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ - $mlexpr_of_constr c$ >> - | Tacexpr.TacGeneralize cl -> - <:expr< Tacexpr.TacGeneralize - $mlexpr_of_list - (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >> - | Tacexpr.TacGeneralizeDep c -> - <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> - | Tacexpr.TacLetTac (na,c,cl,b,e) -> - let na = mlexpr_of_name na in - let cl = mlexpr_of_clause_pattern cl in - <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ - $mlexpr_of_bool b$ - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) e) - >> - - (* Derived basic tactics *) - | Tacexpr.TacInductionDestruct (isrec,ev,l) -> - <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ - $mlexpr_of_pair - (mlexpr_of_list - (mlexpr_of_triple - (mlexpr_of_pair - (mlexpr_of_option mlexpr_of_bool) - mlexpr_of_induction_arg) - (mlexpr_of_pair - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern_naming)) - (mlexpr_of_option (mlexpr_of_intro_pattern_disjunctive))) - (mlexpr_of_option mlexpr_of_clause))) - (mlexpr_of_option mlexpr_of_constr_with_binding) - l$ >> - - (* Context management *) - | Tacexpr.TacClear (b,l) -> - let l = mlexpr_of_list (mlexpr_of_hyp) l in - <:expr< Tacexpr.TacClear $mlexpr_of_bool b$ $l$ >> - | Tacexpr.TacClearBody l -> - let l = mlexpr_of_list (mlexpr_of_hyp) l in - <:expr< Tacexpr.TacClearBody $l$ >> - | Tacexpr.TacMove (id1,id2) -> - <:expr< Tacexpr.TacMove - $mlexpr_of_hyp id1$ - $mlexpr_of_move_location mlexpr_of_hyp id2$ >> - - (* Constructors *) - | Tacexpr.TacSplit (ev,l) -> - <:expr< Tacexpr.TacSplit - ($mlexpr_of_bool ev$, $mlexpr_of_list mlexpr_of_binding_kind l$)>> - (* Conversion *) - | Tacexpr.TacReduce (r,cl) -> - let l = mlexpr_of_clause cl in - <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >> - | Tacexpr.TacChange (p,c,cl) -> - let l = mlexpr_of_clause cl in - let g = mlexpr_of_option mlexpr_of_constr in - <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >> - - (* Equivalence relations *) - | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> - - (* Automation tactics *) - | Tacexpr.TacAuto (debug,n,lems,l) -> - let d = mlexpr_of_debug debug in - let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in - let lems = mlexpr_of_list mlexpr_of_constr lems in - let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in - <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >> - | Tacexpr.TacTrivial (debug,lems,l) -> - let d = mlexpr_of_debug debug in - let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in - let lems = mlexpr_of_list mlexpr_of_constr lems in - <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >> - - | _ -> failwith "Quotation of atomic tactic expressions: TODO" - -and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function - | Tacexpr.TacAtom (loc,t) -> - let loc = of_coqloc loc in - <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >> - | Tacexpr.TacThen (t1,t2) -> - <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$>> - | Tacexpr.TacThens (t,tl) -> - <:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>> - | Tacexpr.TacFirst tl -> - <:expr< Tacexpr.TacFirst $mlexpr_of_list mlexpr_of_tactic tl$ >> - | Tacexpr.TacSolve tl -> - <:expr< Tacexpr.TacSolve $mlexpr_of_list mlexpr_of_tactic tl$ >> - | Tacexpr.TacTry t -> - <:expr< Tacexpr.TacTry $mlexpr_of_tactic t$ >> - | Tacexpr.TacOr (t1,t2) -> - <:expr< Tacexpr.TacOr $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >> - | Tacexpr.TacOrelse (t1,t2) -> - <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >> - | Tacexpr.TacDo (n,t) -> - <:expr< Tacexpr.TacDo $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >> - | Tacexpr.TacTimeout (n,t) -> - <:expr< Tacexpr.TacTimeout $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >> - | Tacexpr.TacRepeat t -> - <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >> - | Tacexpr.TacProgress t -> - <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >> - | Tacexpr.TacShowHyps t -> - <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >> - | Tacexpr.TacId l -> - <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> - | Tacexpr.TacFail (g,n,l) -> - <:expr< Tacexpr.TacFail $mlexpr_of_global_flag g$ $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >> -(* - | Tacexpr.TacInfo t -> TacInfo (loc,f t) - - | Tacexpr.TacRec (id,(idl,t)) -> TacRec (loc,(id,(idl,f t))) - | Tacexpr.TacRecIn (l,t) -> TacRecIn(loc,List.map (fun (id,t) -> (id,f t)) l,f t) -*) - | Tacexpr.TacLetIn (isrec,l,t) -> - let f = - mlexpr_of_pair - (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident) - mlexpr_of_tactic_arg in - <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >> - | Tacexpr.TacMatch (lz,t,l) -> - <:expr< Tacexpr.TacMatch - $mlexpr_of_match_lazy_flag lz$ - $mlexpr_of_tactic t$ - $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> - | Tacexpr.TacMatchGoal (lz,lr,l) -> - <:expr< Tacexpr.TacMatchGoal - $mlexpr_of_match_lazy_flag lz$ - $mlexpr_of_bool lr$ - $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> - - | Tacexpr.TacFun (idol,body) -> - <:expr< Tacexpr.TacFun - ($mlexpr_of_list mlexpr_of_ident_option idol$, - $mlexpr_of_tactic body$) >> - | Tacexpr.TacArg (_,Tacexpr.MetaIdArg (_,true,id)) -> anti loc id - | Tacexpr.TacArg (_,t) -> - <:expr< Tacexpr.TacArg $dloc$ $mlexpr_of_tactic_arg t$ >> - | Tacexpr.TacComplete t -> - <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >> - | _ -> failwith "Quotation of tactic expressions: TODO" - -and mlexpr_of_tactic_arg = function - | Tacexpr.MetaIdArg (loc,true,id) -> - let loc = of_coqloc loc in - anti loc id - | Tacexpr.MetaIdArg (loc,false,id) -> - let loc = of_coqloc loc in - <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >> - | Tacexpr.TacCall (loc,t,tl) -> - let loc = of_coqloc loc in - <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> - | Tacexpr.Tacexp t -> - <:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >> - | Tacexpr.ConstrMayEval c -> - <:expr< Tacexpr.ConstrMayEval $mlexpr_of_may_eval mlexpr_of_constr c$ >> - | Tacexpr.Reference r -> - <:expr< Tacexpr.Reference $mlexpr_of_reference r$ >> - | _ -> failwith "mlexpr_of_tactic_arg: TODO" - - -IFDEF CAMLP5 THEN - -let not_impl x = - let desc = - if Obj.is_block (Obj.repr x) then - "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) - else "int_val = " ^ string_of_int (Obj.magic x) - in - failwith ("<Q_coqast.patt_of_expt, not impl: " ^ desc) - -(* The following function is written without quotation - in order to be parsable even by camlp4. The version with - quotation can be found in revision <= 12972 of [q_util.ml4] *) - -open MLast - -let rec patt_of_expr e = - let loc = loc_of_expr e in - match e with - | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2) - | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2) - | ExLid (_, x) when x = vala "loc" -> PaAny loc - | ExLid (_, s) -> PaLid (loc, s) - | ExUid (_, s) -> PaUid (loc, s) - | ExStr (_, s) -> PaStr (loc, s) - | ExAnt (_, e) -> PaAnt (loc, patt_of_expr e) - | _ -> not_impl e - -let fconstr e = - let ee s = - mlexpr_of_constr (Pcoq.Gram.entry_parse e - (Pcoq.Gram.parsable (Stream.of_string s))) - in - let ep s = patt_of_expr (ee s) in - Quotation.ExAst (ee, ep) - -let ftac e = - let ee s = - mlexpr_of_tactic (Pcoq.Gram.entry_parse e - (Pcoq.Gram.parsable (Stream.of_string s))) - in - let ep s = patt_of_expr (ee s) in - Quotation.ExAst (ee, ep) - -let _ = - Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi); - Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi); - Quotation.default := "constr" - -ELSE - -open Pcaml - -let expand_constr_quot_expr loc _loc_name_opt contents = - mlexpr_of_constr - (Pcoq.Gram.parse_string Pcoq.Constr.constr_eoi loc contents) - -let expand_tactic_quot_expr loc _loc_name_opt contents = - mlexpr_of_tactic - (Pcoq.Gram.parse_string Pcoq.Tactic.tactic_eoi loc contents) - -let _ = - (* FIXME: for the moment, we add quotations in expressions only, not pattern *) - Quotation.add "constr" Quotation.DynAst.expr_tag expand_constr_quot_expr; - Quotation.add "tactic" Quotation.DynAst.expr_tag expand_tactic_quot_expr; - Quotation.default := "constr" - -END diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index a116b1e8b..c529260e9 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -10,6 +10,25 @@ open Compat +type argument_type = +| ListArgType of argument_type +| OptArgType of argument_type +| PairArgType of argument_type * argument_type +| ExtraArgType of string + +type user_symbol = +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Uentry of string +| Uentryl of string * int + +type extend_token = +| ExtTerminal of string +| ExtNonTerminal of user_symbol * string + let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> @@ -23,16 +42,6 @@ let mlexpr_of_pair m1 m2 (a1,a2) = let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> -let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= - let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in - <:expr< ($e1$, $e2$, $e3$) >> - -let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)= - let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in - <:expr< ($e1$, $e2$, $e3$, $e4$) >> - (* We don't give location for tactic quotation! *) let loc = CompatLoc.ghost @@ -49,16 +58,62 @@ let mlexpr_of_option f = function | None -> <:expr< None >> | Some e -> <:expr< Some $f e$ >> -let rec mlexpr_of_prod_entry_key = function - | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Aself -> <:expr< Pcoq.Aself >> - | Pcoq.Anext -> <:expr< Pcoq.Anext >> - | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> - | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported") - | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.name $lid:s$) >> - | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> +let mlexpr_of_ident id = + <:expr< Names.Id.of_string $str:id$ >> + +let rec mlexpr_of_prod_entry_key f = function + | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Uentry e -> <:expr< Extend.Aentry $f e$ >> + | Uentryl (e, l) -> + (** Keep in sync with Pcoq! *) + assert (e = "tactic"); + if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> + else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + +let rec type_of_user_symbol = function +| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> + ListArgType (type_of_user_symbol s) +| Uopt s -> + OptArgType (type_of_user_symbol s) +| Uentry e | Uentryl (e, _) -> ExtraArgType e + +let coincide s pat off = + let len = String.length pat in + let break = ref true in + let i = ref 0 in + while !break && !i < len do + let c = Char.code s.[off + !i] in + let d = Char.code pat.[!i] in + break := Int.equal c d; + incr i + done; + !break + +let rec parse_user_entry s sep = + let l = String.length s in + if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then + let entry = parse_user_entry (String.sub s 3 (l-8)) "" in + Ulist1 entry + else if l > 12 && coincide s "ne_" 0 && + coincide s "_list_sep" (l-9) then + let entry = parse_user_entry (String.sub s 3 (l-12)) "" in + Ulist1sep (entry, sep) + else if l > 5 && coincide s "_list" (l-5) then + let entry = parse_user_entry (String.sub s 0 (l-5)) "" in + Ulist0 entry + else if l > 9 && coincide s "_list_sep" (l-9) then + let entry = parse_user_entry (String.sub s 0 (l-9)) "" in + Ulist0sep (entry, sep) + else if l > 4 && coincide s "_opt" (l-4) then + let entry = parse_user_entry (String.sub s 0 (l-4)) "" in + Uopt entry + else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then + let n = Char.code s.[6] - 48 in + Uentryl ("tactic", n) + else + let s = match s with "hyp" -> "var" | _ -> s in + Uentry s diff --git a/grammar/q_util.mli b/grammar/q_util.mli index a85ad2f6a..a34fc0bcb 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -8,20 +8,31 @@ open Compat (* necessary for camlp4 *) +type argument_type = +| ListArgType of argument_type +| OptArgType of argument_type +| PairArgType of argument_type * argument_type +| ExtraArgType of string + +type user_symbol = +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Uentry of string +| Uentryl of string * int + +type extend_token = +| ExtTerminal of string +| ExtNonTerminal of user_symbol * string + val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr val mlexpr_of_pair : ('a -> MLast.expr) -> ('b -> MLast.expr) -> 'a * 'b -> MLast.expr -val mlexpr_of_triple : - ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr) - -> 'a * 'b * 'c -> MLast.expr - -val mlexpr_of_quadruple : - ('a -> MLast.expr) -> ('b -> MLast.expr) -> - ('c -> MLast.expr) -> ('d -> MLast.expr) -> 'a * 'b * 'c * 'd -> MLast.expr - val mlexpr_of_bool : bool -> MLast.expr val mlexpr_of_int : int -> MLast.expr @@ -30,4 +41,10 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr -val mlexpr_of_prod_entry_key : Pcoq.prod_entry_key -> MLast.expr +val mlexpr_of_ident : string -> MLast.expr + +val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr + +val type_of_user_symbol : user_symbol -> argument_type + +val parse_user_entry : string -> string -> user_symbol diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 39f605e29..19b6e1b5f 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -10,15 +10,8 @@ (** Implementation of the TACTIC EXTEND macro. *) -open Util -open Pp -open Names -open Genarg open Q_util -open Q_coqast open Argextend -open Pcoq -open Egramml open Compat let dloc = <:expr< Loc.ghost >> @@ -27,160 +20,67 @@ let plugin_name = <:expr< __coq_plugin_name >> let rec make_patt = function | [] -> <:patt< [] >> - | GramNonTerminal(loc',_,_,Some p)::l -> - let p = Names.Id.to_string p in + | ExtNonTerminal (_, p) :: l -> <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l -let rec make_when loc = function - | [] -> <:expr< True >> - | GramNonTerminal(loc',t,_,Some p)::l -> - let loc' = of_coqloc loc' in - let p = Names.Id.to_string p in - let l = make_when loc l in - let loc = CompatLoc.merge loc' loc in - let t = mlexpr_of_argtype loc' t in - <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >> - | _::l -> make_when loc l - let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | GramNonTerminal(loc,t,_,Some p)::l -> - let loc = of_coqloc loc in - let p = Names.Id.to_string p in - let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g in + let loc = MLast.loc_of_expr e in let e = make_let raw e l in let v = if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in + else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l -let rec extract_signature = function - | [] -> [] - | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l - | _::l -> extract_signature l - - - -let check_unicity s l = - let l' = List.map (fun (l,_,_) -> extract_signature l) l in - if not (Util.List.distinct l') then - Pp.msg_warning - (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^ - "non-terminals in the same order: put them in distinct tactic entries")) - let make_clause (pt,_,e) = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let false e pt) let make_fun_clauses loc s l = - check_unicity s l; - Compat.make_fun loc (List.map make_clause l) - -let rec make_args = function - | [] -> <:expr< [] >> - | GramNonTerminal(loc,t,_,Some p)::l -> - let loc = of_coqloc loc in - let p = Names.Id.to_string p in - <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >> - | _::l -> make_args l - -let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function - | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >> - | GramNonTerminal (loc,nt,_,sopt) -> - let loc = of_coqloc loc in <:expr< None >> + let map c = Compat.make_fun loc [make_clause c] in + mlexpr_of_list map l + +let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> + +let rec mlexpr_of_symbol = function +| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Uentry e -> + let arg = get_argt <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let arg = get_argt <:expr< Constrarg.wit_tactic >> in + <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> let make_prod_item = function - | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | GramNonTerminal (loc,nt,g,sopt) -> - let loc = of_coqloc loc in - <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ - $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> + | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> + | ExtNonTerminal (g, id) -> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> -let mlexpr_of_clause = - mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) - -let rec make_tags loc = function - | [] -> <:expr< [] >> - | GramNonTerminal(loc',t,_,Some p)::l -> - let loc' = of_coqloc loc' in - let l = make_tags loc l in - let loc = CompatLoc.merge loc' loc in - let t = mlexpr_of_argtype loc' t in - <:expr< [ $t$ :: $l$ ] >> - | _::l -> make_tags loc l - -let make_one_printing_rule se (pt,_,e) = - let level = mlexpr_of_int 0 in (* only level 0 supported here *) - let loc = MLast.loc_of_expr e in - let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in - <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$; - pptac_prods = ($level$, $prods$) }) >> - -let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) - -let make_empty_check = function -| GramNonTerminal(_, t, e, _)-> - let is_extra = match t with ExtraArgType _ -> true | _ -> false in - if is_possibly_empty e || is_extra then - (* This possibly parses epsilon *) - let wit = make_wit loc t in - let rawwit = make_rawwit loc t in - <:expr< - match Genarg.default_empty_value $wit$ with - [ None -> raise Exit - | Some v -> - Tacintern.intern_genarg Tacintern.fully_empty_glob_sign - (Genarg.in_gen $rawwit$ v) ] >> - else - (* This does not parse epsilon (this Exit is static time) *) - raise Exit -| GramTerminal _ -> - (* Idem *) - raise Exit - -let rec possibly_empty_subentries loc = function - | [] -> [] - | (s,prodsl) :: l -> - let rec aux = function - | [] -> (false,<:expr< None >>) - | prods :: rest -> - try - let l = List.map make_empty_check prods in - if has_extraarg prods then - (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ - with [ Exit -> $snd (aux rest)$ ] >>) - else - (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) - with Exit -> aux rest in - let (nonempty,v) = aux prodsl in - if nonempty then (s,v) :: possibly_empty_subentries loc l - else possibly_empty_subentries loc l - -let possibly_atomic loc prods = - let l = List.map_filter (function - | GramTerminal s :: l, _, _ -> Some (s,l) - | _ -> None) prods - in - possibly_empty_subentries loc (List.factorize_left String.equal l) +let mlexpr_of_clause cl = + mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl (** Special treatment of constr entries *) let is_constr_gram = function -| GramTerminal _ -> false -| GramNonTerminal (_, _, e, _) -> - match e with - | Aentry ("constr", "constr") -> true - | _ -> false +| ExtTerminal _ -> false +| ExtNonTerminal (Uentry "constr", _) -> true +| _ -> false let make_var = function - | GramNonTerminal(loc',_,_,Some p) -> Some p - | GramNonTerminal(loc',_,_,None) -> Some (Id.of_string "_") + | ExtNonTerminal (_, p) -> Some p | _ -> assert false let declare_tactic loc s c cl = match cl with -| [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> +| [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in @@ -188,27 +88,28 @@ let declare_tactic loc s c cl = match cl with let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in + let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in let name = mlexpr_of_string name in - let tac = + let tac = match rem with + | [] -> (** Special handling of tactics without arguments: such tactics do not do a Proofview.Goal.nf_enter to compute their arguments. It matters for some whole-prof tactics like [shelve_unifiable]. *) - if List.is_empty rem then <:expr< fun _ $lid:"ist"$ -> $tac$ >> - else + | _ -> let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> in (** Arguments are not passed directly to the ML tactic in the TacML node, the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in + let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $ml$, [])) >> in let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in try do { - Tacenv.register_ml_tactic $se$ $tac$; + Tacenv.register_ml_tactic $se$ [|$tac$|]; Mltop.declare_cache_obj obj $plugin_name$; } with [ e when Errors.noncritical e -> Pp.msg_warning @@ -221,18 +122,13 @@ let declare_tactic loc s c cl = match cl with TacML tactic. *) let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let pp = make_printing_rule se cl in let gl = mlexpr_of_clause cl in - let atom = - mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) - (possibly_atomic loc cl) in - let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ $atom$ >> in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in declare_str_items loc [ <:str_item< do { try do { - Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$; - Mltop.declare_cache_obj $obj$ $plugin_name$; - List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } + Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); + Mltop.declare_cache_obj $obj$ $plugin_name$; } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app @@ -257,7 +153,7 @@ EXTEND c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ]; "->"; "["; e = Pcaml.expr; "]" -> (match l with - | GramNonTerminal _ :: _ -> + | ExtNonTerminal _ :: _ -> (* En attendant la syntaxe de tacticielles *) failwith "Tactic syntax must start with an identifier" | _ -> (l,c,e)) @@ -265,14 +161,14 @@ EXTEND ; tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name false None e "" in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name false None e sep in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) | s = STRING -> - if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); - GramTerminal s + let () = if s = "" then failwith "Empty terminal." in + ExtTerminal s ] ] ; tac_name: diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index d789a6c1f..0d4bec69d 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -10,19 +10,15 @@ (** Implementation of the VERNAC EXTEND macro. *) -open Pp -open Util open Q_util open Argextend open Tacextend -open Pcoq -open Egramml open Compat type rule = { r_head : string option; (** The first terminal grammar token *) - r_patt : grammar_prod_item list; + r_patt : extend_token list; (** The remaining tokens of the parsing rule *) r_class : MLast.expr option; (** An optional classifier for the STM *) @@ -34,24 +30,25 @@ type rule = { let rec make_let e = function | [] -> e - | GramNonTerminal(loc,t,_,Some p)::l -> - let loc = of_coqloc loc in - let p = Names.Id.to_string p in - let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g in + let loc = MLast.loc_of_expr e in let e = make_let e l in <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> | _::l -> make_let e l let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let e pt) (* To avoid warnings *) let mk_ignore c pt = - let names = CList.map_filter (function - | GramNonTerminal(_,_,_,Some p) -> Some (Names.Id.to_string p) - | _ -> None) pt in + let fold accu = function + | ExtNonTerminal (_, p) -> p :: accu + | _ -> accu + in + let names = List.fold_left fold [] pt in let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in let names = List.fold_left fold <:expr< () >> names in <:expr< do { let _ = $names$ in $c$ } >> @@ -60,34 +57,34 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr c) pt)), + vala None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr cg) pt)), + vala None, <:expr< fun () -> $cg$ $str:s$ >>) - | None, None -> msg_warning - (strbrk("Vernac entry \""^s^"\" misses a classifier. "^ + | None, None -> prerr_endline + (("Vernac entry \""^s^"\" misses a classifier. "^ "A classifier is a function that returns an expression "^ - "of type vernac_classification (see Vernacexpr). You can: ")++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ - "new vernacular command does not alter the system state;"))++fnl()++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ + "of type vernac_classification (see Vernacexpr). You can: ") ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ + "new vernacular command does not alter the system state;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ "new vernacular command alters the system state but not the "^ - "parser nor it starts a proof or ends one;"))++fnl()++ - str"- "++hov 0 ( - strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ + "parser nor it starts a proof or ends one;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ "a global function f. The function f will be called passing "^ - "\""^s^"\" as the only argument;")) ++fnl()++ - str"- "++hov 0 ( - strbrk"Add a specific classifier in each clause using the syntax:" - ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++ - strbrk("Specific classifiers have precedence over global "^ - "classifiers. Only one classifier is called.")++fnl()); + "\""^s^"\" as the only argument;")) ^ "\n" ^ + "- " ^ ( + "Add a specific classifier in each clause using the syntax:" + ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^ + ("Specific classifiers have precedence over global "^ + "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, - vala (Some (make_when loc pt)), + vala None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = @@ -105,10 +102,20 @@ let make_fun_classifiers loc s c l = let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl -let mlexpr_of_clause = - mlexpr_of_list - (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item - (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) +let make_prod_item = function + | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtNonTerminal (g, id) -> + let nt = type_of_user_symbol g in + let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in + <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ + $mlexpr_of_prod_entry_key base g$ >> + +let mlexpr_of_clause cl = + let mkexpr { r_head = a; r_patt = b; } = match a with + | None -> mlexpr_of_list make_prod_item b + | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) + in + mlexpr_of_list mkexpr cl let declare_command loc s c nt cl = let se = mlexpr_of_string s in @@ -166,8 +173,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - if String.is_empty s then - Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty."); + let () = if s = "" then failwith "Command name is empty." in let b = <:expr< fun () -> $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; @@ -181,13 +187,13 @@ EXTEND ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name false None e "" in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name false None e sep in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) | s = STRING -> - GramTerminal s + ExtTerminal s ] ] ; END |