diff options
-rw-r--r-- | .gitignore | 1 | ||||
-rw-r--r-- | Makefile.build | 5 | ||||
-rw-r--r-- | _tags | 2 | ||||
-rw-r--r-- | grammar/q_constr.mlp | 112 | ||||
-rw-r--r-- | myocamlbuild.ml | 1 | ||||
-rw-r--r-- | tactics/hipattern.ml | 2 |
6 files changed, 2 insertions, 121 deletions
diff --git a/.gitignore b/.gitignore index 55df76e30..116f88dd7 100644 --- a/.gitignore +++ b/.gitignore @@ -121,7 +121,6 @@ g_*.ml ide/project_file.ml parsing/compat.ml grammar/q_util.ml -grammar/q_constr.ml grammar/tacextend.ml grammar/vernacextend.ml grammar/argextend.ml diff --git a/Makefile.build b/Makefile.build index 4fac65df7..fc92507e6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -110,7 +110,7 @@ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cm $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef -CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma grammar/q_constr.cmo +CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) else @@ -200,7 +200,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h # grammar/grammar.cma ########################################################################### -## In this part, we compile grammar/grammar.cma (and grammar/q_constr.cmo) +## In this part, we compile grammar/grammar.cma ## without relying on .d dependency files, for bootstraping the creation ## and inclusion of these .d files @@ -213,7 +213,6 @@ GRAMCMO := \ grammar/q_util.cmi : grammar/gramCompat.cmo grammar/argextend.cmo : $(GRAMBASEDEPS) -grammar/q_constr.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ @@ -35,12 +35,10 @@ "parsing/g_obligations.ml4": use_grammar "grammar/argextend.ml4": use_compat5b -"grammar/q_constr.ml4": use_compat5b "grammar/tacextend.ml4": use_compat5b "grammar/vernacextend.ml4": use_compat5b <tactics/*.ml4>: use_grammar -"tactics/hipattern.ml4": use_constr <plugins/**/*.ml4>: use_grammar "plugins/decl_mode/g_decl_mode.ml4": use_compat5 diff --git a/grammar/q_constr.mlp b/grammar/q_constr.mlp deleted file mode 100644 index 8e1587ec3..000000000 --- a/grammar/q_constr.mlp +++ /dev/null @@ -1,112 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Q_util -open GramCompat -open Pcaml -open PcamlSig (* necessary for camlp4 *) - -let loc = CompatLoc.ghost -let dloc = <:expr< Loc.ghost >> - -let apply_ref f l = - <:expr< - Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$) - >> - -EXTEND - GLOBAL: expr; - expr: - [ [ "PATTERN"; "["; c = constr; "]" -> - <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] - ; - 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" - [ id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),Misctypes.IntroAnonymous,None) >> - | "?"; 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$, None) >> - | 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/myocamlbuild.ml b/myocamlbuild.ml index 90df4f00c..b81b280ff 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -277,7 +277,6 @@ let extra_rules () = begin A"-o"; Px ml; A"-impl"; P ml4])); 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/tactics/hipattern.ml b/tactics/hipattern.ml index 51d4c1635..fded54fcb 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma grammar/q_constr.cmo" i*) - open Pp open Errors open Util |