diff options
Diffstat (limited to 'grammar/gramCompat.mlp')
-rw-r--r-- | grammar/gramCompat.mlp | 86 |
1 files changed, 86 insertions, 0 deletions
diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp new file mode 100644 index 00000000..6246da7b --- /dev/null +++ b/grammar/gramCompat.mlp @@ -0,0 +1,86 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Compatibility file depending on ocaml/camlp4 version *) + +(** Misc module emulation *) + +IFDEF CAMLP5 THEN + +module CompatLoc = struct + include Ploc + let ghost = dummy + let merge = encl +end + +ELSE + +module CompatLoc = Camlp4.PreCast.Loc + +END + +IFDEF CAMLP5 THEN + +module PcamlSig = struct end + +ELSE + +module PcamlSig = Camlp4.Sig +module Ast = Camlp4.PreCast.Ast +module Pcaml = Camlp4.PreCast.Syntax +module MLast = Ast + +END + +(** Compatibility with camlp5 strict mode *) +IFDEF CAMLP5 THEN + IFDEF STRICT THEN + let vala x = Ploc.VaVal x + ELSE + let vala x = x + END +ELSE + let vala x = x +END + +(** Fix a quotation difference in [str_item] *) + +let declare_str_items loc l = +IFDEF CAMLP5 THEN + MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *) +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 |