blob: 256b48d6cb6a449721bc1afa07e6bdcff75a4939 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
(* $Id$ *)
let dummy_loc = (0,0)
let is_meta s = String.length s > 0 && s.[0] == '$'
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_coqast." ^ name ^ ", not impl: " ^ desc)
let purge_str s =
if String.length s == 0 || s.[0] <> '$' then s
else String.sub s 1 (String.length s - 1)
let anti loc x =
let e =
let loc = (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >>
in
<:expr< $anti:e$ >>
(* [expr_of_ast] contributes to translate g_*.ml4 files into g_*.ppo *)
(* This is where $id's (and macros) in ast are translated in ML variables *)
(* which will bind their actual ast value *)
let rec expr_of_ast = function
| Coqast.Nvar loc id when is_meta id -> anti loc id
| Coqast.Id loc id when is_meta id -> anti loc id
| Coqast.Node _ "$VAR" [Coqast.Nvar loc x] ->
<:expr< Coqast.Nvar loc $anti loc x$ >>
| Coqast.Node loc "$PATH" l ->
let extract_var = function
| Coqast.Nvar loc id -> id
| Coqast.Id loc id -> failwith ("Id"^id)
| Coqast.Node _ s _ -> failwith ("Node"^s)
| _ -> failwith "Path is not built from ast variables" in
let l = List.map extract_var l in
let l = expr_list_of_var_list l in
<:expr< Coqast.Path loc $l$ Names.CCI >>
| Coqast.Node _ "$ID" [Coqast.Nvar loc x] ->
<:expr< Coqast.Id loc $anti loc x$ >>
| Coqast.Node _ "$STR" [Coqast.Nvar loc x] ->
<:expr< Coqast.Str loc $anti loc x$ >>
| Coqast.Node _ "$SLAM" [Coqast.Nvar loc idl; y] ->
<:expr<
List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $expr_of_ast y$ >>
| Coqast.Node _ "$ABSTRACT" [Coqast.Str _ s;Coqast.Nvar loc idl; y] ->
<:expr<
Pcoq.abstract_binders_ast loc $str:s$ $anti loc idl$ $expr_of_ast y$ >>
| Coqast.Node loc nn al ->
let e = expr_list_of_ast_list al in
<:expr< Coqast.Node loc $str:nn$ $e$ >>
| Coqast.Nvar loc id -> <:expr< Coqast.Nvar loc $str:id$ >>
| Coqast.Slam loc None a ->
<:expr< Coqast.Slam loc None $expr_of_ast a$ >>
| Coqast.Slam loc (Some s) a ->
let se = if is_meta s then anti loc s else <:expr< $str:s$ >> in
<:expr< Coqast.Slam loc (Some $se$) $expr_of_ast a$ >>
| Coqast.Num loc i -> <:expr< Coqast.Num loc $int:string_of_int i$ >>
| Coqast.Id loc id -> <:expr< Coqast.Id loc $str:id$ >>
| Coqast.Str loc str -> <:expr< Coqast.Str loc $str:str$ >>
| Coqast.Path loc sl s ->
let e = expr_list_of_var_list sl in
<:expr< Coqast.Path loc $e$ $str:s$ >>
| Coqast.Dynamic _ _ ->
failwith "Q_Coqast: dynamic: not implemented"
and expr_list_of_ast_list al =
List.fold_right
(fun a e2 -> match a with
| (Coqast.Node _ "$LIST" [Coqast.Nvar locv pv]) ->
let e1 = anti locv pv in
let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
if e2 = (let loc = dummy_loc in <:expr< [] >>)
then <:expr< $e1$ >>
else <:expr< ( $lid:"@"$ $e1$ $e2$) >>
| _ ->
let e1 = expr_of_ast a in
let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
<:expr< [$e1$ :: $e2$] >> )
al (let loc = dummy_loc in <:expr< [] >>)
and expr_list_of_var_list sl =
let loc = dummy_loc in
List.fold_right
(fun s e2 ->
let e1 = if is_meta s then anti loc s else <:expr< $str:s$ >> in
let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
<:expr< [$e1$ :: $e2$] >>)
sl <:expr< [] >>
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 f e =
let ee s =
expr_of_ast (Pcoq.Gram.Entry.parse e
(Pcoq.Gram.parsable (Stream.of_string s)))
in
let ep s = patt_of_expr (ee s) in
Quotation.ExAst (ee, ep)
let _ =
Quotation.add "constr" (f Pcoq.Constr.constr_eoi);
Quotation.add "tactic" (f Pcoq.Tactic.tactic_eoi);
Quotation.add "vernac" (f Pcoq.Vernac.vernac_eoi);
Quotation.add "ast" (f Pcoq.Prim.ast_eoi);
Quotation.default := "constr"
|
