|
1 theory Term_pat |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 text {* |
|
6 @{text "trace_match"} is the flag to control the tracing of matching activities. |
|
7 *} |
|
8 |
|
9 ML {* |
|
10 val trace_match = Attrib.setup_config_bool @{binding trace_match} (K false) |
|
11 *} |
|
12 |
|
13 section {* Monad with support of excepion *} |
|
14 |
|
15 ML {* |
|
16 |
|
17 structure Exceptional = |
|
18 struct |
|
19 datatype ('a, 'b) Exceptional = |
|
20 Exception of 'a | Success of 'b |
|
21 fun (scan1 :|-- scan2) st = |
|
22 case scan1 st of |
|
23 Success (v, st') => scan2 v st' |
|
24 | Exception e => Exception e |
|
25 fun returnM v = (fn st => Success (v, st)) |
|
26 fun (scan1 |-- scan2) = scan1 :|-- (K scan2) |
|
27 fun (scan1 -- scan2) = scan1 :|-- (fn v1 => scan2 :|-- (fn v2 => returnM (v1, v2))) |
|
28 fun liftE scan st = let |
|
29 val (v, st') = scan st |
|
30 in Success (v, st') end |
|
31 fun getM y = Success (y, y) |
|
32 fun setM v = (fn _ => Success (v, v)) |
|
33 fun failM x = (fn _ => raise (Scan.fail x)) |
|
34 fun m0M f = getM :|-- f |
|
35 fun pushM x = (m0M (fn (top::rest) => setM (top::top::rest) |-- returnM top)) x |
|
36 fun popM x = (m0M (fn (top::rest) => setM rest |-- returnM top)) x |
|
37 (* [f] is assumed to be a monad valued function, so that it can be constructed using monad combinators. |
|
38 For this reason, [f] is assumed to take two arguments. |
|
39 *) |
|
40 fun topM f = m0M (fn (top::rest) => |
|
41 case f top top of |
|
42 Success (v, top') => (setM (top'::rest) |-- returnM v) |
|
43 | Exception e => (K (Exception e))) |
|
44 (* all the [f] in the following are monad or moand function on stack element (not on stack itself )*) |
|
45 (* [f] in the following is assumed to be plain monad on stack element, not a monad valued function *) |
|
46 fun liftM f = topM (K f) |
|
47 (* [f] in the following is a monad valued funtion depending only on the first component *) |
|
48 fun m1M f = m0M (fn (st1, st2) => f st1) |
|
49 (* [f] in the following is a monad valued funtion depending only on the second component *) |
|
50 fun m2M f = m0M (fn (st1, st2) => f st2) |
|
51 fun localM f = pushM |-- f :|-- (fn res => popM |-- returnM res) |
|
52 fun s1M n1 = m0M (fn (_, st2) => setM (n1, st2)) |
|
53 fun s2M n2 = m0M (fn (st1, _) => setM (st1, n2)) |
|
54 (* The flowing primed version is meant to substitute the unprimed version *) |
|
55 fun m0M' f = liftM (m0M f) |
|
56 fun m1M' f = liftM (m1M f) |
|
57 fun m2M' f = liftM (m2M f) |
|
58 fun lift scan = (fn (d, a) => |
|
59 case scan a of |
|
60 Success (v, b) => Success (v, (d, b)) |
|
61 | Exception e => Exception e |
|
62 ) |
|
63 fun normVal (Success v) = v |
|
64 fun normExcp (Exception e) = e |
|
65 fun (scan >> f) = scan :|-- (fn v => returnM (f v)) |
|
66 fun raiseM v = K (Exception v) |
|
67 end |
|
68 *} |
|
69 |
|
70 (* ccc *) |
|
71 |
|
72 section {* State monad with stack *} |
|
73 |
|
74 ML {* |
|
75 structure StackMonad = struct |
|
76 (* getM fetches the underlying state *) |
|
77 fun getM y = (y, y) |
|
78 (* setM sets the underlying state *) |
|
79 fun setM v = (fn _ => (v, v)) |
|
80 (* returnM retruns any value *) |
|
81 fun returnM v = (fn st => (v, st)) |
|
82 (* failM failes the current process *) |
|
83 fun failM x = (fn _ => raise (Scan.fail x)) |
|
84 (* [m0M f] applies function f to the underlying state *) |
|
85 fun m0M f = getM :|-- f |
|
86 fun pushM x = (m0M (fn (top::rest) => setM (top::top::rest) |-- returnM top)) x |
|
87 fun popM x = (m0M (fn (top::rest) => setM rest |-- returnM top)) x |
|
88 (* [f] is assumed to be a monad valued function, so that it can be constructed using monad combinators. |
|
89 For this reason, [f] is assumed to take two arguments. |
|
90 *) |
|
91 fun topM f = m0M (fn (top::rest) => let val (v, top') = f top top in |
|
92 setM (top'::rest) |-- returnM v |
|
93 end) |
|
94 (* all the [f] in the following are monad or moand function on stack element (not on stack itself )*) |
|
95 (* [f] in the following is assumed to be plain monad on stack element, not a monad valued function *) |
|
96 fun liftM f = topM (K f) |
|
97 (* [f] in the following is a monad valued funtion depending only on the first component *) |
|
98 fun m1M f = m0M (fn (st1, st2) => f st1) |
|
99 (* [f] in the following is a monad valued funtion depending only on the second component *) |
|
100 fun m2M f = m0M (fn (st1, st2) => f st2) |
|
101 fun localM f = pushM |-- f :|-- (fn res => popM |-- returnM res) |
|
102 fun s1M n1 = m0M (fn (_, st2) => setM (n1, st2)) |
|
103 fun s2M n2 = m0M (fn (st1, _) => setM (st1, n2)) |
|
104 fun dgM scan arg = let val (v, [arg']) = scan [arg] in (v, arg') end |
|
105 (* The flowing primed version is meant to substitute the unprimed version *) |
|
106 fun m0M' f = liftM (m0M f) |
|
107 fun m1M' f = liftM (m1M f) |
|
108 fun m2M' f = liftM (m2M f) |
|
109 val liftE = I |
|
110 val lift = Scan.lift |
|
111 val :|-- = Scan.:|-- |
|
112 val |-- = Scan.|-- |
|
113 val -- = Scan.-- |
|
114 val >> = Scan.>> |
|
115 val normVal = I |
|
116 end |
|
117 *} |
|
118 |
|
119 ML {* |
|
120 open StackMonad |
|
121 open Exceptional |
|
122 *} |
|
123 |
|
124 section {* State monad with stack *} |
|
125 |
|
126 ML {* |
|
127 local |
|
128 val tracing = (fn ctxt => fn str => |
|
129 if (Config.get ctxt trace_match) then tracing str else ()) |
|
130 fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of |
|
131 fun pterm ctxt t = |
|
132 t |> string_of_term ctxt |> tracing ctxt |
|
133 in |
|
134 fun tracingM s = liftM (m2M (fn ctxt => returnM (tracing ctxt s))) |
|
135 fun ptermM t = liftM (m2M (fn ctxt => returnM (pterm ctxt t))) |
|
136 fun presultM tag scan = scan :|-- (fn res => |
|
137 tracingM tag |-- |
|
138 ptermM res |-- |
|
139 returnM res |
|
140 ) |
|
141 end |
|
142 *} |
|
143 |
|
144 ML {* |
|
145 local |
|
146 val tracing = (fn ctxt => fn str => |
|
147 if (Config.get ctxt trace_match) then tracing str else ()) |
|
148 fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of |
|
149 fun pterm ctxt t = |
|
150 t |> string_of_term ctxt |> tracing ctxt |
|
151 fun match_fun1 pat term (st, ctxt) = let |
|
152 val _ = tracing ctxt "match_fun on:" |
|
153 val _ = tracing ctxt pat |
|
154 val _ = pterm ctxt term |
|
155 in |
|
156 (Proof_Context.match_bind_i true |
|
157 [([Proof_Context.read_term_pattern ctxt pat], term)] ctxt |> |
|
158 (fn (_, ctxt) => (term, (st, ctxt)))) |
|
159 handle (ERROR x) => |
|
160 raise (Scan.fail x) |
|
161 end |
|
162 in |
|
163 fun match_fun pat term = liftE (match_fun1 pat term) |
|
164 end |
|
165 *} |
|
166 |
|
167 ML {* |
|
168 fun err_trans (ERROR x) = raise (Scan.fail x) |
|
169 | err_trans e = e |
|
170 *} |
|
171 |
|
172 ML {* |
|
173 fun exnM f monad = (fn inp => monad inp handle e => raise (f e)) |
|
174 *} |
|
175 |
|
176 ML {* |
|
177 fun match_fun pat term = |
|
178 tracingM "match_fun on:" |-- |
|
179 tracingM pat |-- |
|
180 ptermM term |-- |
|
181 liftM (lift (m0M (fn ctxt => (* setM (Variable.auto_fixes term ctxt) |-- *) |
|
182 (liftE (Proof_Context.match_bind_i true [([Proof_Context.read_term_pattern ctxt pat], term)])) |-- |
|
183 returnM term |
|
184 )) |> exnM err_trans) |
|
185 *} |
|
186 |
|
187 ML {* |
|
188 local |
|
189 val >> = Scan.>> |
|
190 in |
|
191 val match_parser = |
|
192 (Args.name_source) >> (fn s => "(match_fun "^ML_Syntax.print_string s^")") |
|
193 end |
|
194 *} |
|
195 |
|
196 ML {* |
|
197 local |
|
198 val >> = Scan.>> |
|
199 in |
|
200 val fterm_parser = |
|
201 Args.name_source >> |
|
202 (fn term => "liftM (exnM err_trans (lift (m0M (fn ctxt => returnM ((Syntax.read_term ctxt) "^ML_Syntax.print_string term ^")))))") |
|
203 end |
|
204 *} |
|
205 |
|
206 setup {* |
|
207 ML_Antiquote.inline @{binding match} (Scan.lift match_parser) #> |
|
208 ML_Antiquote.inline @{binding fterm} (Scan.lift fterm_parser) |
|
209 *} |
|
210 |
|
211 ML {* |
|
212 infixr 0 ||| |
|
213 fun (scan1 ||| scan2) xs = scan1 xs handle _ => scan2 xs |
|
214 *} |
|
215 |
|
216 declare [[trace_match = false]] |
|
217 |
|
218 ML {* |
|
219 val t = [((), @{context})] |> |
|
220 (@{match "(?x::nat) + ?y"} @{term "(1::nat) + 2"} |-- |
|
221 @{fterm "?x"}) |
|
222 *} |
|
223 |
|
224 |
|
225 ML {* (* testings and examples *) |
|
226 fun trans t = (@{match "(?x ::nat) + ?y"} t |-- |
|
227 (@{fterm "?x"} :|-- trans) :|-- @{match "?u"} |-- |
|
228 (@{fterm "?y"} :|-- trans) :|-- @{match "?v"} |-- |
|
229 @{fterm "?v * ?v * ?u"} |
|
230 || |
|
231 @{match "(?x ::nat) - ?y"} t |-- |
|
232 (@{fterm "?x"} :|-- trans) :|-- @{match "?u"} |-- |
|
233 (@{fterm "?y"} :|-- trans) :|-- @{match "v"} |-- |
|
234 @{fterm "?v - ?v * ?u"} |
|
235 || |
|
236 (returnM t)) |
|
237 *} |
|
238 |
|
239 ML {* |
|
240 val t = trans @{term "(u - (x::nat) + y)"} [((), @{context})] |> normVal |> |
|
241 apfst (cterm_of @{theory}) |> fst |
|
242 *} |
|
243 |
|
244 end |