Remove Q_constr from grammar folder.

6 files changed, 61 insertions, 139 deletions

diff --git a/.gitignore b/.gitignore
index 06cac2fee6..116f88dd7e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -121,12 +121,10 @@ 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
 parsing/cLexer.ml
-tactics/hipattern.ml
 ltac/coretactics.ml
 ltac/extratactics.ml
 ltac/extraargs.ml
diff --git a/Makefile.build b/Makefile.build
index 4fac65df75..fc92507e69 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 \
diff --git a/_tags b/_tags
index e8317d6148..9f77416a02 100644
--- a/_tags
+++ b/_tags
@@ -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 8e1587ec34..0000000000
--- 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 90df4f00c6..b81b280fff 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.ml4 b/tactics/hipattern.ml
index bcec90f803..fded54fcb1 100644
--- a/tactics/hipattern.ml4
+++ 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
@@ -243,9 +241,36 @@ type equation_kind =
 
 exception NoEquationFound
 
-let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ]
-let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
-let coq_refl_jm_pattern       = PATTERN [ forall A:_, forall x:A, _ A x A x ]
+open Glob_term
+open Decl_kinds
+open Evar_kinds
+
+let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
+let mkGApp f args = GApp (Loc.ghost, f, args)
+let mkGHole =
+  GHole (Loc.ghost, QuestionMark (Define false), Misctypes.IntroAnonymous, None)
+let mkGProd id c1 c2 =
+  GProd (Loc.ghost, Name (Id.of_string id), Explicit, c1, c2)
+let mkGArrow c1 c2 =
+  GProd (Loc.ghost, Anonymous, Explicit, c1, c2)
+let mkGVar id = GVar (Loc.ghost, Id.of_string id)
+let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
+let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
+let mkGAppRef r args = mkGApp (mkGRef r) args
+
+(** forall x : _, _ x x *)
+let coq_refl_leibniz1_pattern =
+  mkPattern (mkGProd "x" mkGHole (mkGApp mkGHole [mkGVar "x"; mkGVar "x";]))
+
+(** forall A:_, forall x:A, _ A x x *)
+let coq_refl_leibniz2_pattern =
+  mkPattern (mkGProd "A" mkGHole (mkGProd "x" (mkGVar "A")
+    (mkGApp mkGHole [mkGVar "A"; mkGVar "x"; mkGVar "x";])))
+
+(** forall A:_, forall x:A, _ A x A x *)
+let coq_refl_jm_pattern       =
+  mkPattern (mkGProd "A" mkGHole (mkGProd "x" (mkGVar "A")
+    (mkGApp mkGHole [mkGVar "A"; mkGVar "x"; mkGVar "A"; mkGVar "x";])))
 
 open Globnames
 
@@ -301,7 +326,8 @@ let is_equality_type t = op2bool (match_with_equality_type t)
 
 (* Arrows/Implication/Negation *)
 
-let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
+(** X1 -> X2 **)
+let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2"))
 
 let match_arrow_pattern t =
   let result = matches coq_arrow_pattern t in
@@ -381,10 +407,15 @@ let rec first_match matcher = function
 (*** Equality *)
 
 (* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *)
-let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
+(** %eq ?X1 ?X2 ?X3 *)
+let coq_eq_pattern_gen eq =
+  lazy (mkPattern (mkGAppRef eq (List.map mkGPatVar ["X1"; "X2"; "X3";])))
 let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
 let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
-let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
+(** %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 *)
+let coq_jmeq_pattern =
+  lazy (mkPattern
+    (mkGAppRef coq_jmeq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"; "X4"])))
 
 let match_eq eqn eq_pat =
   let pat =
@@ -464,7 +495,8 @@ let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   match_sigma ex
 
 (* Pattern "(sig ?1 ?2)" *)
-let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
+let coq_sig_pattern =
+  lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"]))
 
 let match_sigma t =
   match Id.Map.bindings (matches (Lazy.force coq_sig_pattern) t) with
@@ -480,17 +512,25 @@ let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
 (* Pattern "{<?1>x=y}+{~(<?1>x=y)}" *)
 (* i.e. "(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
 
-let coq_eqdec_inf_pattern =
- lazy PATTERN [ { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } ]
+let coq_eqdec ~sum ~rev =
+  lazy (
+    let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
+    let args = [eqn; mkGAppRef coq_not_ref [eqn]] in
+    let args = if rev then List.rev args else args in
+    mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]])
+  )
+
+(** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *)
+let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false
 
-let coq_eqdec_inf_rev_pattern =
- lazy PATTERN [ { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } ]
+(** { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } *)
+let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true
 
-let coq_eqdec_pattern =
- lazy PATTERN [ %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) ]
+(** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *)
+let coq_eqdec_pattern = coq_eqdec ~sum:coq_or_ref ~rev:false
 
-let coq_eqdec_rev_pattern =
- lazy PATTERN [ %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) ]
+(** %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) *)
+let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true
 
 let op_or = coq_or_ref
 let op_sum = coq_sumbool_ref
@@ -510,8 +550,8 @@ let match_eqdec t =
   | _ -> anomaly (Pp.str "Unexpected pattern")
 
 (* Patterns "~ ?" and "? -> False" *)
-let coq_not_pattern = lazy PATTERN [ ~ _ ]
-let coq_imp_False_pattern = lazy PATTERN [ _ -> %coq_False_ref ]
+let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
+let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref)))
 
 let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t
 let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t