diff options
Diffstat (limited to 'parsing/q_util.ml4')
-rw-r--r-- | parsing/q_util.ml4 | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 new file mode 100644 index 00000000..b3f5393c --- /dev/null +++ b/parsing/q_util.ml4 @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: q_util.ml4,v 1.2.2.2 2004/07/16 19:30:41 herbelin Exp $ *) + +(* This file defines standard combinators to build ml expressions *) + +open Util + +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 + +let mlexpr_of_list f l = + List.fold_right + (fun e1 e2 -> + let e1 = f e1 in + let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in + <:expr< [$e1$ :: $e2$] >>) + l (let loc = dummy_loc in <:expr< [] >>) + +let mlexpr_of_pair m1 m2 (a1,a2) = + let e1 = m1 a1 and e2 = m2 a2 in + let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in + <:expr< ($e1$, $e2$) >> + +let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= + let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in + let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in + <:expr< ($e1$, $e2$, $e3$) >> + +(* We don't give location for tactic quotation! *) +let loc = dummy_loc + + +let mlexpr_of_bool = function + | true -> <:expr< True >> + | false -> <:expr< False >> + +let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> + +let mlexpr_of_string s = <:expr< $str:s$ >> + +let mlexpr_of_option f = function + | None -> <:expr< None >> + | Some e -> <:expr< Some $f e$ >> |