From b3485ddc8c4f98743426bb58c8d49b76edd43d61 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 19:25:58 +0200 Subject: Making the grammar/ folder independent from the other ones. --- grammar/argextend.ml4 | 2 +- grammar/gramCompat.ml4 | 86 ++++++++++++++++++++++++++++++++++++++++++++++++ grammar/grammar.mllib | 10 +----- grammar/q_constr.ml4 | 10 ++---- grammar/q_util.ml4 | 6 ++-- grammar/q_util.mli | 2 +- grammar/tacextend.ml4 | 6 ++-- grammar/vernacextend.ml4 | 6 ++-- 8 files changed, 100 insertions(+), 28 deletions(-) create mode 100644 grammar/gramCompat.ml4 diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 9be6c6bc4..8e06adce9 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) open Q_util -open Compat +open GramCompat let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> diff --git a/grammar/gramCompat.ml4 b/grammar/gramCompat.ml4 new file mode 100644 index 000000000..6246da7bb --- /dev/null +++ b/grammar/gramCompat.ml4 @@ -0,0 +1,86 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > *) +ELSE + Ast.stSem_of_list l +END + +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) + +IFDEF CAMLP5 THEN + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) + +ELSE + +let make_fun loc cl = + let mk_when = function + | Some w -> w + | None -> Ast.ExNil loc + in + let mk_clause (patt,optwhen,expr) = + (* correspond to <:match_case< ... when ... -> ... >> *) + Ast.McArr (loc, patt, mk_when optwhen, expr) in + let init = mk_clause (default_patt loc) in + let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in + let l = List.fold_right add_clause cl init in + Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *) + +END diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 9b24c9797..6c3ce7f03 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,12 +1,4 @@ -Coq_config - -Store -Exninfo -Loc - -Tok -Compat - +GramCompat Q_util Argextend Tacextend diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index 40db81949..af90f5f2a 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) open Q_util -open Compat +open GramCompat open Pcaml open PcamlSig (* necessary for camlp4 *) @@ -27,11 +27,6 @@ EXTEND [ [ "PATTERN"; "["; c = constr; "]" -> <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] ; - sort: - [ [ "Set" -> Misctypes.GSet - | "Prop" -> Misctypes.GProp - | "Type" -> Misctypes.GType [] ] ] - ; ident: [ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ] ; @@ -68,8 +63,7 @@ EXTEND 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$) >> + [ 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; "}" -> diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index a9a339241..2d5c40894 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -8,7 +8,7 @@ (* This file defines standard combinators to build ml expressions *) -open Compat +open GramCompat type argument_type = | ListArgType of argument_type @@ -87,7 +87,7 @@ let coincide s pat off = while !break && !i < len do let c = Char.code s.[off + !i] in let d = Char.code pat.[!i] in - break := Int.equal c d; + break := c = d; incr i done; !break @@ -110,7 +110,7 @@ let rec parse_user_entry s sep = else if l > 4 && coincide s "_opt" (l-4) then let entry = parse_user_entry (String.sub s 0 (l-4)) "" in Uopt entry - else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then + else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in Uentryl ("tactic", n) else diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 9b6f11827..a5e36e47b 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat (* necessary for camlp4 *) +open GramCompat (* necessary for camlp4 *) type argument_type = | ListArgType of argument_type diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 4c4ecaf73..8593bad5d 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -12,7 +12,7 @@ open Q_util open Argextend -open Compat +open GramCompat let dloc = <:expr< Loc.ghost >> @@ -47,7 +47,7 @@ let make_clause (pt,_,e) = make_let false e pt) let make_fun_clauses loc s l = - let map c = Compat.make_fun loc [make_clause c] in + let map c = GramCompat.make_fun loc [make_clause c] in mlexpr_of_list map l let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> @@ -102,7 +102,7 @@ let declare_tactic loc s c cl = match cl with whole-prof tactics like [shelve_unifiable]. *) <:expr< fun _ $lid:"ist"$ -> $tac$ >> | _ -> - let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in + let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> in (** Arguments are not passed directly to the ML tactic in the TacML node, diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 904662ea1..1611de39c 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -13,7 +13,7 @@ open Q_util open Argextend open Tacextend -open Compat +open GramCompat type rule = { r_head : string option; @@ -93,13 +93,13 @@ let make_fun_clauses loc s l = | None -> false | Some () -> true in - let cl = Compat.make_fun loc [make_clause c] in + let cl = GramCompat.make_fun loc [make_clause c] in <:expr< ($mlexpr_of_bool depr$, $cl$)>> in mlexpr_of_list map l let make_fun_classifiers loc s c l = - let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in + let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl let make_prod_item = function -- cgit v1.2.3