summaryrefslogtreecommitdiff
path: root/parsing/q_util.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/q_util.ml4')
-rw-r--r--parsing/q_util.ml456
1 files changed, 15 insertions, 41 deletions
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index a41824d0..91ab29f1 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -1,41 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4use: "q_MLast.cmo" i*)
-
-(* $Id: q_util.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* This file defines standard combinators to build ml expressions *)
-open Util
open Extrawit
-open Pcoq
-
-let not_impl name 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 ("<Q_util." ^ name ^ ", not impl: " ^ desc)
-
-let rec patt_of_expr e =
- let loc = MLast.loc_of_expr e in
- match e with
- | <:expr< $e1$.$e2$ >> -> <:patt< $patt_of_expr e1$.$patt_of_expr e2$ >>
- | <:expr< $e1$ $e2$ >> -> <:patt< $patt_of_expr e1$ $patt_of_expr e2$ >>
- | <:expr< loc >> -> <:patt< _ >>
- | <:expr< $lid:s$ >> -> <:patt< $lid:s$ >>
- | <:expr< $uid:s$ >> -> <:patt< $uid:s$ >>
- | <:expr< $str:s$ >> -> <:patt< $str:s$ >>
- | <:expr< $anti:e$ >> -> <:patt< $anti:patt_of_expr e$ >>
- | _ -> not_impl "patt_of_expr" e
+open Compat
+open Util
let mlexpr_of_list f l =
List.fold_right
@@ -77,19 +52,18 @@ let mlexpr_of_option f = function
| Some e -> <:expr< Some $f e$ >>
open Vernacexpr
-open Pcoq
open Genarg
let rec mlexpr_of_prod_entry_key = function
- | Extend.Alist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key s$ >>
- | Extend.Alist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
- | Extend.Alist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key s$ >>
- | Extend.Alist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
- | Extend.Aopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key s$ >>
- | Extend.Amodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key s$ >>
- | Extend.Aself -> <:expr< Extend.Aself >>
- | Extend.Anext -> <:expr< Extend.Anext >>
- | Extend.Atactic n -> <:expr< Extend.Atactic $mlexpr_of_int n$ >>
- | Extend.Agram s -> anomaly "Agram not supported"
- | Extend.Aentry ("",s) -> <:expr< Extend.Agram (Gram.Entry.obj $lid:s$) >>
- | Extend.Aentry (u,s) -> <:expr< Extend.Aentry $str:u$ $str:s$ >>
+ | 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 -> Util.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$ >>