From 463e46425b56360a158b44c61208060c64eb2ff5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:09:25 +0000 Subject: place all files specific to camlp4 syntax extensions in grammar/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .gitignore | 11 +- Makefile.build | 4 +- Makefile.common | 4 +- _tags | 11 +- doc/faq/FAQ.tex | 2 +- grammar/argextend.ml4 | 339 +++++++++++++++++++++ grammar/grammar.mllib | 37 +++ grammar/q_constr.ml4 | 126 ++++++++ grammar/q_coqast.ml4 | 568 ++++++++++++++++++++++++++++++++++++ grammar/q_util.ml4 | 69 +++++ grammar/q_util.mli | 33 +++ grammar/tacextend.ml4 | 234 +++++++++++++++ grammar/vernacextend.ml4 | 101 +++++++ myocamlbuild.ml | 4 +- parsing/argextend.ml4 | 340 --------------------- parsing/g_obligations.ml4 | 2 +- parsing/grammar.mllib | 38 --- parsing/highparsing.mllib | 2 +- parsing/q_constr.ml4 | 127 -------- parsing/q_coqast.ml4 | 568 ------------------------------------ parsing/q_util.ml4 | 69 ----- parsing/q_util.mli | 33 --- parsing/tacextend.ml4 | 235 --------------- parsing/vernacextend.ml4 | 101 ------- plugins/btauto/g_btauto.ml4 | 2 +- plugins/cc/cctac.ml | 2 - plugins/cc/g_congruence.ml4 | 2 +- plugins/decl_mode/g_decl_mode.ml4 | 2 +- plugins/extraction/g_extraction.ml4 | 2 +- plugins/field/field.ml4 | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/recdef.ml | 1 - plugins/micromega/g_micromega.ml4 | 2 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/omega/g_omega.ml4 | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/ring/g_ring.ml4 | 2 +- plugins/romega/g_romega.ml4 | 2 +- plugins/rtauto/g_rtauto.ml4 | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- plugins/xml/dumptree.ml4 | 2 +- plugins/xml/xmlentries.ml4 | 2 +- tactics/class_tactics.ml4 | 2 +- tactics/eauto.ml4 | 2 +- tactics/eqdecide.ml4 | 2 +- tactics/extraargs.ml4 | 2 +- tactics/extratactics.ml4 | 2 +- tactics/hipattern.ml4 | 2 +- tactics/rewrite.ml4 | 2 +- tactics/tauto.ml4 | 2 +- toplevel/whelp.ml4 | 2 +- 53 files changed, 1555 insertions(+), 1560 deletions(-) create mode 100644 grammar/argextend.ml4 create mode 100644 grammar/grammar.mllib create mode 100644 grammar/q_constr.ml4 create mode 100644 grammar/q_coqast.ml4 create mode 100644 grammar/q_util.ml4 create mode 100644 grammar/q_util.mli create mode 100644 grammar/tacextend.ml4 create mode 100644 grammar/vernacextend.ml4 delete mode 100644 parsing/argextend.ml4 delete mode 100644 parsing/grammar.mllib delete mode 100644 parsing/q_constr.ml4 delete mode 100644 parsing/q_coqast.ml4 delete mode 100644 parsing/q_util.ml4 delete mode 100644 parsing/q_util.mli delete mode 100644 parsing/tacextend.ml4 delete mode 100644 parsing/vernacextend.ml4 diff --git a/.gitignore b/.gitignore index 8c14100cd3..0cbb48297a 100644 --- a/.gitignore +++ b/.gitignore @@ -111,12 +111,13 @@ g_*.ml ide/project_file.ml lib/pp.ml lib/compat.ml -parsing/q_util.ml -parsing/tacextend.ml -parsing/q_constr.ml +grammar/q_util.ml +grammar/q_constr.ml +grammar/q_coqast.ml +grammar/tacextend.ml +grammar/vernacextend.ml +grammar/argextend.ml parsing/pcoq.ml -parsing/vernacextend.ml -parsing/argextend.ml parsing/lexer.ml plugins/xml/proofTree2Xml.ml plugins/xml/acic2Xml.ml diff --git a/Makefile.build b/Makefile.build index da5e8e694b..2aa4ca6d73 100644 --- a/Makefile.build +++ b/Makefile.build @@ -701,7 +701,7 @@ ml-doc: parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) -parsing/grammar.dot : | parsing/grammar.mllib.d +grammar/grammar.dot : | grammar/grammar.mllib.d $(OCAMLDOC_MLLIBD) tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d @@ -724,7 +724,7 @@ dev/printers.cma: | dev/printers.mllib.d $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ -parsing/grammar.cma: | parsing/grammar.mllib.d +grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar diff --git a/Makefile.common b/Makefile.common index d5b152432d..d7325bcbb9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ SRCDIRS:=\ config tools tools/coqdoc scripts lib \ kernel kernel/byterun library proofs tactics \ pretyping interp toplevel/utils toplevel parsing \ - intf ide/utils ide \ + grammar intf ide/utils ide \ $(addprefix plugins/, \ omega romega micromega quote ring \ setoid_ring xml extraction fourier \ @@ -160,7 +160,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ parsing/highparsing.cma tactics/hightactics.cma -GRAMMARCMA:=parsing/grammar.cma +GRAMMARCMA:=grammar/grammar.cma OMEGACMA:=plugins/omega/omega_plugin.cma ROMEGACMA:=plugins/romega/romega_plugin.cma diff --git a/_tags b/_tags index 08dc9f1af6..19dfff544d 100644 --- a/_tags +++ b/_tags @@ -20,7 +20,7 @@ ## tags for grammar.cm* - : use_unix + : use_unix ## tags for camlp4 files @@ -48,10 +48,10 @@ "plugins/decl_mode/g_decl_mode.ml4": use_compat5 "plugins/funind/g_indfun.ml4": use_compat5 -"parsing/argextend.ml4": use_compat5b -"parsing/q_constr.ml4": use_compat5b -"parsing/tacextend.ml4": use_compat5b -"parsing/vernacextend.ml4": use_compat5b +"grammar/argextend.ml4": use_compat5b +"grammar/q_constr.ml4": use_compat5b +"grammar/tacextend.ml4": use_compat5b +"grammar/vernacextend.ml4": use_compat5b : use_grammar @@ -65,6 +65,7 @@ "ide/utils": include "interp": include "intf": include +"grammar": include "kernel": include "kernel/byterun": include "lib": include diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 80da0c8b01..b63f3ee26c 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2013,7 +2013,7 @@ containing: \begin{itemize} \item in \verb+g_hello.ml4+: \begin{verbatim} -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND Hello | [ "hello" ] -> [ Coq_hello.printHello ] END diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 new file mode 100644 index 0000000000..a130597990 --- /dev/null +++ b/grammar/argextend.ml4 @@ -0,0 +1,339 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > + +let rec make_rawwit loc = function + | BoolArgType -> <:expr< Genarg.rawwit_bool >> + | IntArgType -> <:expr< Genarg.rawwit_int >> + | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >> + | StringArgType -> <:expr< Genarg.rawwit_string >> + | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> + | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >> + | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >> + | VarArgType -> <:expr< Genarg.rawwit_var >> + | RefArgType -> <:expr< Genarg.rawwit_ref >> + | SortArgType -> <:expr< Genarg.rawwit_sort >> + | ConstrArgType -> <:expr< Genarg.rawwit_constr >> + | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >> + | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> + | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> + | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >> + | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> + | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> + | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> + | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >> + | 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< + 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 >> + | IntArgType -> <:expr< Genarg.globwit_int >> + | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >> + | StringArgType -> <:expr< Genarg.globwit_string >> + | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> + | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >> + | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >> + | VarArgType -> <:expr< Genarg.globwit_var >> + | RefArgType -> <:expr< Genarg.globwit_ref >> + | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> + | SortArgType -> <:expr< Genarg.globwit_sort >> + | ConstrArgType -> <:expr< Genarg.globwit_constr >> + | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> + | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> + | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >> + | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> + | BindingsArgType -> <:expr< Genarg.globwit_bindings >> + | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> + | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >> + | 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< + 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 >> + | IntArgType -> <:expr< Genarg.wit_int >> + | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> + | StringArgType -> <:expr< Genarg.wit_string >> + | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> + | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> + | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> + | VarArgType -> <:expr< Genarg.wit_var >> + | RefArgType -> <:expr< Genarg.wit_ref >> + | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> + | SortArgType -> <:expr< Genarg.wit_sort >> + | ConstrArgType -> <:expr< Genarg.wit_constr >> + | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> + | RedExprArgType -> <:expr< Genarg.wit_red_expr >> + | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> + | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> + | BindingsArgType -> <:expr< Genarg.wit_bindings >> + | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> + | List1ArgType t -> <:expr< Genarg.wit_list1 $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 -> + <: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 [ _ -> 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)) >> + | GramNonTerminal (_,t,_,Some p) :: tl -> + let p = Names.string_of_id 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 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 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) 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 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 -> + 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 -> + <:expr< fun s x -> + out_gen $make_globwit loc globtyp$ + (Tacinterp.subst_genarg s + (Genarg.in_gen $make_globwit loc globtyp$ x)) >> + | Some f -> <:expr< $lid:f$>> in + let se = mlexpr_of_string s in + let wit = <:expr< $lid:"wit_"^s$ >> in + 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 $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 -> + 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)) + (None, [(None, None, $rules$)]); + Pptactic.declare_extra_genarg_pprule + ($rawwit$, $lid:rawpr$) + ($globwit$, $lid:globpr$) + ($wit$, $lid:pr$) } + >> ] + +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< $lid:"rawwit_"^s$ >> in + let globwit = <:expr< $lid:"globwit_"^s$ >> 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.abstract_argument_type unit Genarg.tlevel), + ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel), + $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 _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer") + ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } + >> ] + +open Vernacexpr +open Pcoq +open Pcaml +open PcamlSig + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "ARGUMENT"; "EXTEND"; s = entry_name; + header = argextend_header; + OPT "|"; l = LIST1 argrule SEP "|"; + "END" -> + 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" -> + 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) ] + | "1" + [ e = argtype; LIDENT "list" -> List0ArgType e + | e = argtype; LIDENT "option" -> OptArgType e ] + | "0" + [ e = LIDENT -> fst (interp_entry_name false None e "") + | "("; e = argtype; ")" -> e ] ] + ; + argrule: + [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] + ; + 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)) + | 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 + Lexer.add_keyword s; + GramTerminal s + ] ] + ; + entry_name: + [ [ s = LIDENT -> s + | UIDENT -> failwith "Argument entry names must be lowercase" + ] ] + ; + END diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib new file mode 100644 index 0000000000..195ad38c02 --- /dev/null +++ b/grammar/grammar.mllib @@ -0,0 +1,37 @@ +Coq_config + +Pp_control +Compat +Flags +Pp +Segmenttree +Unicodetable +Errors +Util +Bigint +Hashcons +Predicate +Option + +Names +Libnames +Genarg +Tok +Lexer +Extend +Extrawit +Pcoq +Q_util +Q_coqast +Egramml +Argextend +Tacextend +Vernacextend + +Redops +Constrexpr_ops +Locusops +G_prim +G_tactic +G_ltac +G_constr diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 new file mode 100644 index 0000000000..fe4ccc53d5 --- /dev/null +++ b/grammar/q_constr.ml4 @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > + +let apply_ref f l = + <:expr< + Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) + >> + +EXTEND + GLOBAL: expr; + expr: + [ [ "PATTERN"; "["; c = constr; "]" -> + <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] + ; + sort: + [ [ "Set" -> GSet + | "Prop" -> GProp + | "Type" -> GType None ] ] + ; + ident: + [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] + ; + name: + [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] + ; + string: + [ [ s = UIDENT -> s | s = LIDENT -> s ] ] + ; + constr: + [ "200" RIGHTA + [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> + <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> + | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> + <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> + | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> + <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> + (* fix todo *) + ] + | "100" RIGHTA + [ c1 = constr; ":"; c2 = SELF -> + <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] + | "90" RIGHTA + [ c1 = constr; "->"; c2 = SELF -> + <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] + | "75" RIGHTA + [ "~"; c = constr -> + apply_ref <:expr< coq_not_ref >> [c] ] + | "70" RIGHTA + [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT -> + apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ] + | "10" LEFTA + [ f = constr; args = LIST1 NEXT -> + let args = mlexpr_of_list (fun x -> x) args in + <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ] + | "0" + [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> + | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False)) >> + | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> + | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> + apply_ref <:expr< coq_sumbool_ref >> [c1;c2] + | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >> + | c = match_constr -> c + | "("; c = constr LEVEL "200"; ")" -> c ] ] + ; + match_constr: + [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; + "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> + let br = mlexpr_of_list (fun x -> x) br in + <:expr< Glob_term.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> + ] ] + ; + match_type: + [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; + "return"; ty = constr LEVEL "100" -> + let nal = mlexpr_of_list (fun x -> x) nal in + <:expr< Some $ty$ >>, + <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> + | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ] + ; + eqn: + [ [ (lid,pl) = pattern; "=>"; rhs = constr -> + let lid = mlexpr_of_list (fun x -> x) lid in + <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> + ] ] + ; + pattern: + [ [ "%"; e = string; lip = LIST0 patvar -> + let lp = mlexpr_of_list (fun (_,x) -> x) lip in + let lid = List.flatten (List.map fst lip) in + lid, <:expr< Glob_term.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> + | p = patvar -> p + | "("; p = pattern; ")" -> p ] ] + ; + patvar: + [ [ "_" -> [], <:expr< Glob_term.PatVar ($dloc$,Anonymous) >> + | id = ident -> [id], <:expr< Glob_term.PatVar ($dloc$,Name $id$) >> + ] ] + ; + END;; + +(* Example +open Coqlib +let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] +*) diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 new file mode 100644 index 0000000000..7467a32f0d --- /dev/null +++ b/grammar/q_coqast.ml4 @@ -0,0 +1,568 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 = dummy_loc + +let dloc = <:expr< Pp.dummy_loc >> + +let mlexpr_of_ident id = + <:expr< Names.id_of_string $str:Names.string_of_id id$ >> + +let mlexpr_of_name = function + | Names.Anonymous -> <:expr< Names.Anonymous >> + | Names.Name id -> + <:expr< Names.Name (Names.id_of_string $str:Names.string_of_id id$) >> + +let mlexpr_of_dirpath dir = + let l = Names.repr_dirpath dir in + <:expr< Names.make_dirpath $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) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> + | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> + +let mlexpr_of_located f (loc,x) = <: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) -> + <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> + +let mlexpr_of_intro_pattern = function + | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >> + | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >> + | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> + | Misctypes.IntroIdentifier id -> + <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ -> + failwith "mlexpr_of_intro_pattern: TODO" + +let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) + +let mlexpr_of_or_metaid f = function + | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> + | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> + +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_or_metaid (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_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 (string_of_id id) -> + anti loc (string_of_id id) + | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >> + | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" + | Constrexpr.CProdN (loc,l,a) -> <: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) -> <: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,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> + | Constrexpr.CApp (loc,a,l) -> <: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) -> <:expr< Constrexpr.CHole $dloc$ None >> + | Constrexpr.CHole (loc, Some _) -> 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) -> + <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> + | _ -> failwith "mlexpr_of_constr: TODO" + +let mlexpr_of_occ_constr = + mlexpr_of_occurrences 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 o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >> + | Genredexpr.Cbv f -> + <:expr< Genredexpr.Cbv $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_constr o$ >> + | Genredexpr.ExtraRedExpr s -> + <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> + +let rec mlexpr_of_argtype loc = function + | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> + | Genarg.IntArgType -> <:expr< Genarg.IntArgType >> + | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> + | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> + | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> + | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> + | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> + | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> + | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> + | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> + | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> + | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> + | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> + | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> + | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> + | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> + | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> + | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >> + | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $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 rec 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 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_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_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.TacIntrosUntil h -> + <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >> + | 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.TacAssumption -> + <:expr< Tacexpr.TacAssumption >> + | Tacexpr.TacExact c -> + <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> + | Tacexpr.TacExactNoCheck c -> + <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> + | Tacexpr.TacVmCastNoCheck c -> + <:expr< Tacexpr.TacVmCastNoCheck $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 cb$ None >> + | Tacexpr.TacElim (false,cb,cbo) -> + let cb = mlexpr_of_constr_with_binding cb in + let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in + <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> + | Tacexpr.TacElimType c -> + <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >> + | Tacexpr.TacCase (false,cb) -> + let cb = mlexpr_of_constr_with_binding cb in + <:expr< Tacexpr.TacCase False $cb$ >> + | Tacexpr.TacCaseType c -> + <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >> + | 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 (b,id,n,l) -> + let b = mlexpr_of_bool b in + 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 $b$ $id$ $n$ $l$ >> + | Tacexpr.TacCofix ido -> + let ido = mlexpr_of_ident_option ido in + <:expr< Tacexpr.TacCofix $ido$ >> + | Tacexpr.TacMutualCofix (b,id,l) -> + let b = mlexpr_of_bool b in + 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 $b$ $id$ $l$ >> + + | Tacexpr.TacCut c -> + <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> + | Tacexpr.TacAssert (t,ipat,c) -> + let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in + <:expr< Tacexpr.TacAssert $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) -> + 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$ >> + + (* Derived basic tactics *) + | Tacexpr.TacSimpleInductionDestruct (isrec,h) -> + <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$ + $mlexpr_of_quantified_hypothesis h$ >> + | 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_list mlexpr_of_induction_arg) + (mlexpr_of_option mlexpr_of_constr_with_binding) + (mlexpr_of_pair + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) + (mlexpr_of_option mlexpr_of_clause) 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 (dep,id1,id2) -> + <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ + $mlexpr_of_hyp id1$ + $mlexpr_of_move_location mlexpr_of_hyp id2$ >> + + (* Constructors *) + | Tacexpr.TacLeft (ev,l) -> + <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> + | Tacexpr.TacRight (ev,l) -> + <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> + | Tacexpr.TacSplit (ev,b,l) -> + <:expr< Tacexpr.TacSplit + ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>> + | Tacexpr.TacAnyConstructor (ev,t) -> + <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>> + | Tacexpr.TacConstructor (ev,n,l) -> + let n = mlexpr_of_or_var mlexpr_of_int n in + <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $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.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> + | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> + | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> + + (* 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) -> + <: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.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.TacId l -> + <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> + | Tacexpr.TacFail (n,l) -> + <:expr< Tacexpr.TacFail $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_bool 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_bool 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) -> anti loc id + | Tacexpr.MetaIdArg (loc,false,id) -> + <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >> + | Tacexpr.TacCall (loc,t,tl) -> + <: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 (" 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 new file mode 100644 index 0000000000..cfaa2a654a --- /dev/null +++ b/grammar/q_util.ml4 @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let e1 = f e1 in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + <:expr< [$e1$ :: $e2$] >>) + l (let loc = dummy_loc in <:expr< [] >>) + +let mlexpr_of_pair m1 m2 (a1,a2) = + let e1 = m1 a1 and e2 = m2 a2 in + let loc = join_loc (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 = join_loc (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 = join_loc (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 = dummy_loc + + +let mlexpr_of_bool = function + | true -> <:expr< True >> + | false -> <:expr< False >> + +let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> + +let mlexpr_of_string s = <:expr< $str:s$ >> + +let mlexpr_of_option f = function + | None -> <:expr< None >> + | Some e -> <:expr< Some $f e$ >> + +open Vernacexpr +open Genarg + +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 "Agram not supported" + | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> + | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> diff --git a/grammar/q_util.mli b/grammar/q_util.mli new file mode 100644 index 0000000000..5d56c456f5 --- /dev/null +++ b/grammar/q_util.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + +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 diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 new file mode 100644 index 0000000000..3a47ade0df --- /dev/null +++ b/grammar/tacextend.ml4 @@ -0,0 +1,234 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <:patt< [] >> + | GramNonTerminal(loc',_,_,Some p)::l -> + let p = Names.string_of_id p in + <: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 p = Names.string_of_id p in + let l = make_when loc l in + let loc = join_loc loc' loc in + let t = mlexpr_of_argtype loc' t in + <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> + | _::l -> make_when loc l + +let rec make_let e = function + | [] -> e + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in + let loc = join_loc loc (MLast.loc_of_expr e) in + let e = make_let e l in + let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in + <:expr< let $lid:p$ = $v$ in $e$ >> + | _::l -> make_let 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.warning_with !Pp_control.err_ft + ("Two distinct rules of tactic entry "^s^" have the same\n"^ + "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)), + make_let 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 p = Names.string_of_id p in + <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >> + | _::l -> make_args l + +let rec make_eval_tactic e = function + | [] -> e + | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag -> + let p = Names.string_of_id p in + let loc = join_loc loc (MLast.loc_of_expr e) in + let e = make_eval_tactic e l in + <:expr< let $lid:p$ = $lid:p$ in $e$ >> + | _::l -> make_eval_tactic e l + +let rec make_fun e = function + | [] -> e + | GramNonTerminal(loc,_,_,Some p)::l -> + let p = Names.string_of_id p in + <:expr< fun $lid:p$ -> $make_fun e l$ >> + | _::l -> make_fun e l + +let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function + | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >> + | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >> + +let make_prod_item = function + | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | GramNonTerminal (loc,nt,g,sopt) -> + <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ + $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> + +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 l = make_tags loc l in + let loc = join_loc 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$, $make_tags loc pt$, ($level$, $prods$)) >> + +let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) + +let rec possibly_empty_subentries loc = function + | [] -> [] + | (s,prodsl) :: l -> + let rec aux = function + | [] -> (false,<:expr< None >>) + | prods :: rest -> + try + let l = List.map (function + | GramNonTerminal(_,(List0ArgType _| + OptArgType _| + ExtraArgType _ as t),_,_)-> + (* This possibly parses epsilon *) + let rawwit = make_rawwit loc t in + <:expr< match Genarg.default_empty_value $rawwit$ with + [ None -> failwith "" + | Some v -> + Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign + (Genarg.in_gen $rawwit$ v) ] >> + | GramTerminal _ | GramNonTerminal(_,_,_,_) -> + (* This does not parse epsilon (this Exit is static time) *) + raise Exit) prods in + if has_extraarg prods then + (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ + with [ Failure "" -> $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 l) + +let declare_tactic loc s cl = + let se = mlexpr_of_string s in + let pp = make_printing_rule se cl in + let gl = mlexpr_of_clause cl in + let hide_tac (p,e) = + (* reste a definir les fonctions cachees avec des noms frais *) + let stac = "h_"^s in + let e = + make_fun + <:expr< + Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ + >> + p in + <:str_item< value $lid:stac$ = $e$ >> + in + let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in + let atomic_tactics = + mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) + (possibly_atomic loc cl) in + declare_str_items loc + (hidden @ + [ <:str_item< do { + try + let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in + List.iter + (fun (s,l) -> match l with + [ Some l -> + Tacinterp.add_primitive_tactic s + (Tacexpr.TacAtom($default_loc$, + Tacexpr.TacExtend($default_loc$,$se$,l))) + | None -> () ]) + $atomic_tactics$ + with e -> Pp.pp (Errors.print e); + Egramml.extend_tactic_grammar $se$ $gl$; + List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> + ]) + +open Pcaml +open PcamlSig + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "TACTIC"; "EXTEND"; s = tac_name; + OPT "|"; l = LIST1 tacrule SEP "|"; + "END" -> + declare_tactic loc s l ] ] + ; + tacrule: + [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" + -> + if match List.hd l with GramNonTerminal _ -> true | _ -> false then + (* En attendant la syntaxe de tacticielles *) + failwith "Tactic syntax must start with an identifier"; + (l,e) + ] ] + ; + 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)) + | 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 s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal."); + GramTerminal s + ] ] + ; + tac_name: + [ [ s = LIDENT -> s + | s = UIDENT -> s + ] ] + ; + END diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 new file mode 100644 index 0000000000..af7ee7d169 --- /dev/null +++ b/grammar/vernacextend.ml4 @@ -0,0 +1,101 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* e + | GramNonTerminal(loc,t,_,Some p)::l -> + let p = Names.string_of_id p in + let loc = join_loc 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 check_unicity s l = + let l' = List.map (fun (_,l,_) -> extract_signature l) l in + if not (Util.list_distinct l') then + Pp.warning_with !Pp_control.err_ft + ("Two distinct rules of entry "^s^" have the same\n"^ + "non-terminals in the same order: put them in distinct vernac entries") + +let make_clause (_,pt,e) = + (make_patt pt, + vala (Some (make_when (MLast.loc_of_expr e) pt)), + make_let e pt) + +let make_fun_clauses loc s l = + check_unicity s l; + Compat.make_fun loc (List.map make_clause l) + +let mlexpr_of_clause = + mlexpr_of_list + (fun (a,b,c) -> mlexpr_of_list make_prod_item + (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) + +let declare_command loc s nt cl = + let gl = mlexpr_of_clause cl in + let funcl = make_fun_clauses loc s cl in + declare_str_items loc + [ <:str_item< do { + try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ + with e -> Pp.pp (Errors.print e); + Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + } >> ] + +open Pcaml +open PcamlSig + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; + OPT "|"; l = LIST1 rule SEP "|"; + "END" -> + declare_command loc s <:expr> l + | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; + OPT "|"; l = LIST1 rule SEP "|"; + "END" -> + declare_command loc s <:expr> l ] ] + ; + (* spiwack: comment-by-guessing: it seems that the isolated string (which + otherwise could have been another argument) is not passed to the + VernacExtend interpreter function to discriminate between the clauses. *) + rule: + [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]" + -> + if s = "" then Errors.user_err_loc (loc,"",Pp.str"Command name is empty."); + (Some s,l,<:expr< fun () -> $e$ >>) + | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" -> + (None,l,<:expr< fun () -> $e$ >>) + ] ] + ; + 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)) + | 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 -> + GramTerminal s + ] ] + ; + END +;; diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 7700d9959f..966eb6c1c0 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -278,8 +278,8 @@ let extra_rules () = begin T(tags_of_pathname ml4 ++ "p4option"); camlp4compat; A"-o"; Px ml; A"-impl"; P ml4])); - flag_and_dep ["p4mod"; "use_grammar"] (P "parsing/grammar.cma"); - flag_and_dep ["p4mod"; "use_constr"] (P "parsing/q_constr.cmo"); + flag_and_dep ["p4mod"; "use_grammar"] (P "grammar/grammar.cma"); + flag_and_dep ["p4mod"; "use_constr"] (P "grammar/q_constr.cmo"); flag_and_dep ["p4mod"; "use_compat5"] (P "tools/compat5.cmo"); flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo"); diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 deleted file mode 100644 index 5a64580d22..0000000000 --- a/parsing/argextend.ml4 +++ /dev/null @@ -1,340 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > - -let rec make_rawwit loc = function - | BoolArgType -> <:expr< Genarg.rawwit_bool >> - | IntArgType -> <:expr< Genarg.rawwit_int >> - | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >> - | StringArgType -> <:expr< Genarg.rawwit_string >> - | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> - | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >> - | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >> - | VarArgType -> <:expr< Genarg.rawwit_var >> - | RefArgType -> <:expr< Genarg.rawwit_ref >> - | SortArgType -> <:expr< Genarg.rawwit_sort >> - | ConstrArgType -> <:expr< Genarg.rawwit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >> - | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> - | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >> - | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> - | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >> - | 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< - 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 >> - | IntArgType -> <:expr< Genarg.globwit_int >> - | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >> - | StringArgType -> <:expr< Genarg.globwit_string >> - | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> - | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >> - | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >> - | VarArgType -> <:expr< Genarg.globwit_var >> - | RefArgType -> <:expr< Genarg.globwit_ref >> - | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> - | SortArgType -> <:expr< Genarg.globwit_sort >> - | ConstrArgType -> <:expr< Genarg.globwit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> - | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >> - | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> - | BindingsArgType -> <:expr< Genarg.globwit_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >> - | 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< - 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 >> - | IntArgType -> <:expr< Genarg.wit_int >> - | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> - | StringArgType -> <:expr< Genarg.wit_string >> - | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> - | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> - | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> - | VarArgType -> <:expr< Genarg.wit_var >> - | RefArgType -> <:expr< Genarg.wit_ref >> - | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> - | SortArgType -> <:expr< Genarg.wit_sort >> - | ConstrArgType -> <:expr< Genarg.wit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> - | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> - | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> - | BindingsArgType -> <:expr< Genarg.wit_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $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 -> - <: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 [ _ -> 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)) >> - | GramNonTerminal (_,t,_,Some p) :: tl -> - let p = Names.string_of_id 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 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 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) 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 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 -> - 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 -> - <:expr< fun s x -> - out_gen $make_globwit loc globtyp$ - (Tacinterp.subst_genarg s - (Genarg.in_gen $make_globwit loc globtyp$ x)) >> - | Some f -> <:expr< $lid:f$>> in - let se = mlexpr_of_string s in - let wit = <:expr< $lid:"wit_"^s$ >> in - 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 $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 -> - 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)) - (None, [(None, None, $rules$)]); - Pptactic.declare_extra_genarg_pprule - ($rawwit$, $lid:rawpr$) - ($globwit$, $lid:globpr$) - ($wit$, $lid:pr$) } - >> ] - -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< $lid:"rawwit_"^s$ >> in - let globwit = <:expr< $lid:"globwit_"^s$ >> 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.abstract_argument_type unit Genarg.tlevel), - ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel), - $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 _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer") - ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } - >> ] - -open Vernacexpr -open Pcoq -open Pcaml -open PcamlSig - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "ARGUMENT"; "EXTEND"; s = entry_name; - header = argextend_header; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - 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" -> - 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) ] - | "1" - [ e = argtype; LIDENT "list" -> List0ArgType e - | e = argtype; LIDENT "option" -> OptArgType e ] - | "0" - [ e = LIDENT -> fst (interp_entry_name false None e "") - | "("; e = argtype; ")" -> e ] ] - ; - argrule: - [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] - ; - 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)) - | 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 - Lexer.add_keyword s; - GramTerminal s - ] ] - ; - entry_name: - [ [ s = LIDENT -> s - | UIDENT -> failwith "Argument entry names must be lowercase" - ] ] - ; - END - diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index d763a1cabf..d4229ff0b0 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) (* Syntax for the subtac terms and types. diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib deleted file mode 100644 index 313676c969..0000000000 --- a/parsing/grammar.mllib +++ /dev/null @@ -1,38 +0,0 @@ -Coq_config - -Pp_control -Compat -Flags -Pp -Segmenttree -Unicodetable -Errors -Util -Bigint -Hashcons -Predicate -Option - -Names -Libnames -Genarg -Tok -Lexer -Extend -Extrawit -Pcoq -Q_util -Q_coqast - -Egramml -Argextend -Tacextend -Vernacextend - -Redops -Constrexpr_ops -Locusops -G_prim -G_tactic -G_ltac -G_constr diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 6ccbdb7523..13ed804641 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,4 +4,4 @@ G_prim G_proofs G_tactic G_ltac -G_obligations \ No newline at end of file +G_obligations diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 deleted file mode 100644 index d78b6c8c01..0000000000 --- a/parsing/q_constr.ml4 +++ /dev/null @@ -1,127 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > - -let apply_ref f l = - <:expr< - Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) - >> - -EXTEND - GLOBAL: expr; - expr: - [ [ "PATTERN"; "["; c = constr; "]" -> - <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] - ; - sort: - [ [ "Set" -> GSet - | "Prop" -> GProp - | "Type" -> GType None ] ] - ; - ident: - [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] - ; - name: - [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] - ; - string: - [ [ s = UIDENT -> s | s = LIDENT -> s ] ] - ; - constr: - [ "200" RIGHTA - [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> - | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> - | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> - <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> - (* fix todo *) - ] - | "100" RIGHTA - [ c1 = constr; ":"; c2 = SELF -> - <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] - | "90" RIGHTA - [ c1 = constr; "->"; c2 = SELF -> - <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] - | "75" RIGHTA - [ "~"; c = constr -> - apply_ref <:expr< coq_not_ref >> [c] ] - | "70" RIGHTA - [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT -> - apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ] - | "10" LEFTA - [ f = constr; args = LIST1 NEXT -> - let args = mlexpr_of_list (fun x -> x) args in - <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ] - | "0" - [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> - | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False)) >> - | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> - | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> - apply_ref <:expr< coq_sumbool_ref >> [c1;c2] - | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >> - | c = match_constr -> c - | "("; c = constr LEVEL "200"; ")" -> c ] ] - ; - match_constr: - [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; - "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> - let br = mlexpr_of_list (fun x -> x) br in - <:expr< Glob_term.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> - ] ] - ; - match_type: - [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; - "return"; ty = constr LEVEL "100" -> - let nal = mlexpr_of_list (fun x -> x) nal in - <:expr< Some $ty$ >>, - <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> - | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ] - ; - eqn: - [ [ (lid,pl) = pattern; "=>"; rhs = constr -> - let lid = mlexpr_of_list (fun x -> x) lid in - <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> - ] ] - ; - pattern: - [ [ "%"; e = string; lip = LIST0 patvar -> - let lp = mlexpr_of_list (fun (_,x) -> x) lip in - let lid = List.flatten (List.map fst lip) in - lid, <:expr< Glob_term.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> - | p = patvar -> p - | "("; p = pattern; ")" -> p ] ] - ; - patvar: - [ [ "_" -> [], <:expr< Glob_term.PatVar ($dloc$,Anonymous) >> - | id = ident -> [id], <:expr< Glob_term.PatVar ($dloc$,Name $id$) >> - ] ] - ; - END;; - -(* Example -open Coqlib -let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] -*) - diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 deleted file mode 100644 index 7467a32f0d..0000000000 --- a/parsing/q_coqast.ml4 +++ /dev/null @@ -1,568 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 = dummy_loc - -let dloc = <:expr< Pp.dummy_loc >> - -let mlexpr_of_ident id = - <:expr< Names.id_of_string $str:Names.string_of_id id$ >> - -let mlexpr_of_name = function - | Names.Anonymous -> <:expr< Names.Anonymous >> - | Names.Name id -> - <:expr< Names.Name (Names.id_of_string $str:Names.string_of_id id$) >> - -let mlexpr_of_dirpath dir = - let l = Names.repr_dirpath dir in - <:expr< Names.make_dirpath $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) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> - | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> - -let mlexpr_of_located f (loc,x) = <: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) -> - <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> - -let mlexpr_of_intro_pattern = function - | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >> - | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >> - | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >> - | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> - | Misctypes.IntroIdentifier id -> - <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> - | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ -> - failwith "mlexpr_of_intro_pattern: TODO" - -let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) - -let mlexpr_of_or_metaid f = function - | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> - | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> - -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_or_metaid (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_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 (string_of_id id) -> - anti loc (string_of_id id) - | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >> - | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Constrexpr.CProdN (loc,l,a) -> <: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) -> <: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,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> - | Constrexpr.CApp (loc,a,l) -> <: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) -> <:expr< Constrexpr.CHole $dloc$ None >> - | Constrexpr.CHole (loc, Some _) -> 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) -> - <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> - | _ -> failwith "mlexpr_of_constr: TODO" - -let mlexpr_of_occ_constr = - mlexpr_of_occurrences 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 o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >> - | Genredexpr.Cbv f -> - <:expr< Genredexpr.Cbv $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_constr o$ >> - | Genredexpr.ExtraRedExpr s -> - <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> - -let rec mlexpr_of_argtype loc = function - | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> - | Genarg.IntArgType -> <:expr< Genarg.IntArgType >> - | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> - | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> - | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> - | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> - | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> - | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> - | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> - | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> - | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> - | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> - | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> - | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> - | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> - | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> - | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >> - | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $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 rec 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 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_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_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.TacIntrosUntil h -> - <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >> - | 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.TacAssumption -> - <:expr< Tacexpr.TacAssumption >> - | Tacexpr.TacExact c -> - <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> - | Tacexpr.TacExactNoCheck c -> - <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> - | Tacexpr.TacVmCastNoCheck c -> - <:expr< Tacexpr.TacVmCastNoCheck $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 cb$ None >> - | Tacexpr.TacElim (false,cb,cbo) -> - let cb = mlexpr_of_constr_with_binding cb in - let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> - | Tacexpr.TacElimType c -> - <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >> - | Tacexpr.TacCase (false,cb) -> - let cb = mlexpr_of_constr_with_binding cb in - <:expr< Tacexpr.TacCase False $cb$ >> - | Tacexpr.TacCaseType c -> - <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >> - | 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 (b,id,n,l) -> - let b = mlexpr_of_bool b in - 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 $b$ $id$ $n$ $l$ >> - | Tacexpr.TacCofix ido -> - let ido = mlexpr_of_ident_option ido in - <:expr< Tacexpr.TacCofix $ido$ >> - | Tacexpr.TacMutualCofix (b,id,l) -> - let b = mlexpr_of_bool b in - 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 $b$ $id$ $l$ >> - - | Tacexpr.TacCut c -> - <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> - | Tacexpr.TacAssert (t,ipat,c) -> - let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in - <:expr< Tacexpr.TacAssert $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) -> - 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$ >> - - (* Derived basic tactics *) - | Tacexpr.TacSimpleInductionDestruct (isrec,h) -> - <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$ - $mlexpr_of_quantified_hypothesis h$ >> - | 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_list mlexpr_of_induction_arg) - (mlexpr_of_option mlexpr_of_constr_with_binding) - (mlexpr_of_pair - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) - (mlexpr_of_option mlexpr_of_clause) 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 (dep,id1,id2) -> - <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ - $mlexpr_of_hyp id1$ - $mlexpr_of_move_location mlexpr_of_hyp id2$ >> - - (* Constructors *) - | Tacexpr.TacLeft (ev,l) -> - <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> - | Tacexpr.TacRight (ev,l) -> - <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> - | Tacexpr.TacSplit (ev,b,l) -> - <:expr< Tacexpr.TacSplit - ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>> - | Tacexpr.TacAnyConstructor (ev,t) -> - <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>> - | Tacexpr.TacConstructor (ev,n,l) -> - let n = mlexpr_of_or_var mlexpr_of_int n in - <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $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.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> - | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> - | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> - - (* 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) -> - <: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.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.TacId l -> - <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> - | Tacexpr.TacFail (n,l) -> - <:expr< Tacexpr.TacFail $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_bool 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_bool 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) -> anti loc id - | Tacexpr.MetaIdArg (loc,false,id) -> - <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >> - | Tacexpr.TacCall (loc,t,tl) -> - <: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 (" 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/parsing/q_util.ml4 b/parsing/q_util.ml4 deleted file mode 100644 index cfaa2a654a..0000000000 --- a/parsing/q_util.ml4 +++ /dev/null @@ -1,69 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let e1 = f e1 in - let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< [$e1$ :: $e2$] >>) - l (let loc = dummy_loc in <:expr< [] >>) - -let mlexpr_of_pair m1 m2 (a1,a2) = - let e1 = m1 a1 and e2 = m2 a2 in - let loc = join_loc (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 = join_loc (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 = join_loc (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 = dummy_loc - - -let mlexpr_of_bool = function - | true -> <:expr< True >> - | false -> <:expr< False >> - -let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> - -let mlexpr_of_string s = <:expr< $str:s$ >> - -let mlexpr_of_option f = function - | None -> <:expr< None >> - | Some e -> <:expr< Some $f e$ >> - -open Vernacexpr -open Genarg - -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 "Agram not supported" - | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> - | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> diff --git a/parsing/q_util.mli b/parsing/q_util.mli deleted file mode 100644 index 5d56c456f5..0000000000 --- a/parsing/q_util.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 - -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 diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 deleted file mode 100644 index ec0784c529..0000000000 --- a/parsing/tacextend.ml4 +++ /dev/null @@ -1,235 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <:patt< [] >> - | GramNonTerminal(loc',_,_,Some p)::l -> - let p = Names.string_of_id p in - <: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 p = Names.string_of_id p in - let l = make_when loc l in - let loc = join_loc loc' loc in - let t = mlexpr_of_argtype loc' t in - <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> - | _::l -> make_when loc l - -let rec make_let e = function - | [] -> e - | GramNonTerminal(loc,t,_,Some p)::l -> - let p = Names.string_of_id p in - let loc = join_loc loc (MLast.loc_of_expr e) in - let e = make_let e l in - let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in - <:expr< let $lid:p$ = $v$ in $e$ >> - | _::l -> make_let 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.warning_with !Pp_control.err_ft - ("Two distinct rules of tactic entry "^s^" have the same\n"^ - "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)), - make_let 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 p = Names.string_of_id p in - <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >> - | _::l -> make_args l - -let rec make_eval_tactic e = function - | [] -> e - | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag -> - let p = Names.string_of_id p in - let loc = join_loc loc (MLast.loc_of_expr e) in - let e = make_eval_tactic e l in - <:expr< let $lid:p$ = $lid:p$ in $e$ >> - | _::l -> make_eval_tactic e l - -let rec make_fun e = function - | [] -> e - | GramNonTerminal(loc,_,_,Some p)::l -> - let p = Names.string_of_id p in - <:expr< fun $lid:p$ -> $make_fun e l$ >> - | _::l -> make_fun e l - -let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function - | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >> - | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >> - -let make_prod_item = function - | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | GramNonTerminal (loc,nt,g,sopt) -> - <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$ - $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> - -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 l = make_tags loc l in - let loc = join_loc 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$, $make_tags loc pt$, ($level$, $prods$)) >> - -let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) - -let rec possibly_empty_subentries loc = function - | [] -> [] - | (s,prodsl) :: l -> - let rec aux = function - | [] -> (false,<:expr< None >>) - | prods :: rest -> - try - let l = List.map (function - | GramNonTerminal(_,(List0ArgType _| - OptArgType _| - ExtraArgType _ as t),_,_)-> - (* This possibly parses epsilon *) - let rawwit = make_rawwit loc t in - <:expr< match Genarg.default_empty_value $rawwit$ with - [ None -> failwith "" - | Some v -> - Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign - (Genarg.in_gen $rawwit$ v) ] >> - | GramTerminal _ | GramNonTerminal(_,_,_,_) -> - (* This does not parse epsilon (this Exit is static time) *) - raise Exit) prods in - if has_extraarg prods then - (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ - with [ Failure "" -> $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 l) - -let declare_tactic loc s cl = - let se = mlexpr_of_string s in - let pp = make_printing_rule se cl in - let gl = mlexpr_of_clause cl in - let hide_tac (p,e) = - (* reste a definir les fonctions cachees avec des noms frais *) - let stac = "h_"^s in - let e = - make_fun - <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ - >> - p in - <:str_item< value $lid:stac$ = $e$ >> - in - let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in - let atomic_tactics = - mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) - (possibly_atomic loc cl) in - declare_str_items loc - (hidden @ - [ <:str_item< do { - try - let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in - List.iter - (fun (s,l) -> match l with - [ Some l -> - Tacinterp.add_primitive_tactic s - (Tacexpr.TacAtom($default_loc$, - Tacexpr.TacExtend($default_loc$,$se$,l))) - | None -> () ]) - $atomic_tactics$ - with e -> Pp.pp (Errors.print e); - Egramml.extend_tactic_grammar $se$ $gl$; - List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> - ]) - -open Pcaml -open PcamlSig - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "TACTIC"; "EXTEND"; s = tac_name; - OPT "|"; l = LIST1 tacrule SEP "|"; - "END" -> - declare_tactic loc s l ] ] - ; - tacrule: - [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" - -> - if match List.hd l with GramNonTerminal _ -> true | _ -> false then - (* En attendant la syntaxe de tacticielles *) - failwith "Tactic syntax must start with an identifier"; - (l,e) - ] ] - ; - 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)) - | 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 s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal."); - GramTerminal s - ] ] - ; - tac_name: - [ [ s = LIDENT -> s - | s = UIDENT -> s - ] ] - ; - END - diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 deleted file mode 100644 index 94135d1211..0000000000 --- a/parsing/vernacextend.ml4 +++ /dev/null @@ -1,101 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* e - | GramNonTerminal(loc,t,_,Some p)::l -> - let p = Names.string_of_id p in - let loc = join_loc 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 check_unicity s l = - let l' = List.map (fun (_,l,_) -> extract_signature l) l in - if not (Util.list_distinct l') then - Pp.warning_with !Pp_control.err_ft - ("Two distinct rules of entry "^s^" have the same\n"^ - "non-terminals in the same order: put them in distinct vernac entries") - -let make_clause (_,pt,e) = - (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), - make_let e pt) - -let make_fun_clauses loc s l = - check_unicity s l; - Compat.make_fun loc (List.map make_clause l) - -let mlexpr_of_clause = - mlexpr_of_list - (fun (a,b,c) -> mlexpr_of_list make_prod_item - (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) - -let declare_command loc s nt cl = - let gl = mlexpr_of_clause cl in - let funcl = make_fun_clauses loc s cl in - declare_str_items loc - [ <:str_item< do { - try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ - with e -> Pp.pp (Errors.print e); - Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ - } >> ] - -open Pcaml -open PcamlSig - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s <:expr> l - | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s <:expr> l ] ] - ; - (* spiwack: comment-by-guessing: it seems that the isolated string (which - otherwise could have been another argument) is not passed to the - VernacExtend interpreter function to discriminate between the clauses. *) - rule: - [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]" - -> - if s = "" then Errors.user_err_loc (loc,"",Pp.str"Command name is empty."); - (Some s,l,<:expr< fun () -> $e$ >>) - | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" -> - (None,l,<:expr< fun () -> $e$ >>) - ] ] - ; - 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)) - | 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 -> - GramTerminal s - ] ] - ; - END -;; diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index a7171b6bd6..14d23a82a2 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND btauto | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0a3697e2a7..7940009c6e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) - (* This file is the interface between the c-c algorithm and Coq *) open Evd diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 881b9beeba..e4428f4664 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Cctac open Tactics diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 83beece261..9a8682891c 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) (* arnaud: veiller à l'aspect tutorial des commentaires *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 11a2d0e0de..4438c5897a 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) (* ML names *) diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 15c495ae72..988e56af58 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Names open Pp diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index a5ee551a52..b6a0ef4c33 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Formula open Sequent diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 9276eda1b9..039d7a499f 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open FourierR diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index eb90c05492..169f4d1204 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Util open Term open Names diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2005a90e31..5fcd495ef9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) open Tacexpr open Term open Namegen diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index cd87e93ec0..19af8d57e4 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -14,7 +14,7 @@ (* *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Quote open Ring diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index c6d23afa68..b5c8502af5 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 4aad8e7383..0b070dbc87 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Coq_omega open Refiner diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 4b3385677d..9698ca73a8 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Tacexpr diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index e306a5319b..758de80ba5 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Quote open Ring diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 87e42354b0..a548d4d4a7 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -6,7 +6,7 @@ *************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Refl_omega open Refiner diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 8d103d1ba5..cab5a00199 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND rtauto [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ] diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index c2815aafaf..783aebafd4 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 8415bbd10d..d0b694d975 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -11,7 +11,7 @@ (** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Tacexpr;; open Decl_mode;; open Printer;; diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index d65a1bd331..597190d3e9 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -12,7 +12,7 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Util;; open Vernacinterp;; diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index a749ba8ab5..d62320e769 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fb692873e1..1cde368a11 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 1a65f62780..6a88843555 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -12,7 +12,7 @@ (* by Eduardo Gimenez *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Errors open Util diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4677d87ef1..bff4f47601 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Pcoq diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index db55f6434a..82b08289da 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Pcoq diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 5abbe7ae98..bc91219112 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) +(*i camlp4deps: "grammar/grammar.cma grammar/q_constr.cmo" i*) open Pp open Errors diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 004599f455..16eb595eaf 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 79c1797e41..0ab78fcd6c 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Term open Hipattern diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index d869e88544..71c17b9acc 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Flags open Pp -- cgit v1.2.3