--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Term_pat.thy Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,244 @@
+theory Term_pat
+imports Main
+begin
+
+text {*
+ @{text "trace_match"} is the flag to control the tracing of matching activities.
+*}
+
+ML {*
+ val trace_match = Attrib.setup_config_bool @{binding trace_match} (K false)
+*}
+
+section {* Monad with support of excepion *}
+
+ML {*
+
+structure Exceptional =
+struct
+ datatype ('a, 'b) Exceptional =
+ Exception of 'a | Success of 'b
+ fun (scan1 :|-- scan2) st =
+ case scan1 st of
+ Success (v, st') => scan2 v st'
+ | Exception e => Exception e
+ fun returnM v = (fn st => Success (v, st))
+ fun (scan1 |-- scan2) = scan1 :|-- (K scan2)
+ fun (scan1 -- scan2) = scan1 :|-- (fn v1 => scan2 :|-- (fn v2 => returnM (v1, v2)))
+ fun liftE scan st = let
+ val (v, st') = scan st
+ in Success (v, st') end
+ fun getM y = Success (y, y)
+ fun setM v = (fn _ => Success (v, v))
+ fun failM x = (fn _ => raise (Scan.fail x))
+ fun m0M f = getM :|-- f
+ fun pushM x = (m0M (fn (top::rest) => setM (top::top::rest) |-- returnM top)) x
+ fun popM x = (m0M (fn (top::rest) => setM rest |-- returnM top)) x
+ (* [f] is assumed to be a monad valued function, so that it can be constructed using monad combinators.
+ For this reason, [f] is assumed to take two arguments.
+ *)
+ fun topM f = m0M (fn (top::rest) =>
+ case f top top of
+ Success (v, top') => (setM (top'::rest) |-- returnM v)
+ | Exception e => (K (Exception e)))
+ (* all the [f] in the following are monad or moand function on stack element (not on stack itself )*)
+ (* [f] in the following is assumed to be plain monad on stack element, not a monad valued function *)
+ fun liftM f = topM (K f)
+ (* [f] in the following is a monad valued funtion depending only on the first component *)
+ fun m1M f = m0M (fn (st1, st2) => f st1)
+ (* [f] in the following is a monad valued funtion depending only on the second component *)
+ fun m2M f = m0M (fn (st1, st2) => f st2)
+ fun localM f = pushM |-- f :|-- (fn res => popM |-- returnM res)
+ fun s1M n1 = m0M (fn (_, st2) => setM (n1, st2))
+ fun s2M n2 = m0M (fn (st1, _) => setM (st1, n2))
+ (* The flowing primed version is meant to substitute the unprimed version *)
+ fun m0M' f = liftM (m0M f)
+ fun m1M' f = liftM (m1M f)
+ fun m2M' f = liftM (m2M f)
+ fun lift scan = (fn (d, a) =>
+ case scan a of
+ Success (v, b) => Success (v, (d, b))
+ | Exception e => Exception e
+ )
+ fun normVal (Success v) = v
+ fun normExcp (Exception e) = e
+ fun (scan >> f) = scan :|-- (fn v => returnM (f v))
+ fun raiseM v = K (Exception v)
+end
+*}
+
+(* ccc *)
+
+section {* State monad with stack *}
+
+ML {*
+structure StackMonad = struct
+ (* getM fetches the underlying state *)
+ fun getM y = (y, y)
+ (* setM sets the underlying state *)
+ fun setM v = (fn _ => (v, v))
+ (* returnM retruns any value *)
+ fun returnM v = (fn st => (v, st))
+ (* failM failes the current process *)
+ fun failM x = (fn _ => raise (Scan.fail x))
+ (* [m0M f] applies function f to the underlying state *)
+ fun m0M f = getM :|-- f
+ fun pushM x = (m0M (fn (top::rest) => setM (top::top::rest) |-- returnM top)) x
+ fun popM x = (m0M (fn (top::rest) => setM rest |-- returnM top)) x
+ (* [f] is assumed to be a monad valued function, so that it can be constructed using monad combinators.
+ For this reason, [f] is assumed to take two arguments.
+ *)
+ fun topM f = m0M (fn (top::rest) => let val (v, top') = f top top in
+ setM (top'::rest) |-- returnM v
+ end)
+ (* all the [f] in the following are monad or moand function on stack element (not on stack itself )*)
+ (* [f] in the following is assumed to be plain monad on stack element, not a monad valued function *)
+ fun liftM f = topM (K f)
+ (* [f] in the following is a monad valued funtion depending only on the first component *)
+ fun m1M f = m0M (fn (st1, st2) => f st1)
+ (* [f] in the following is a monad valued funtion depending only on the second component *)
+ fun m2M f = m0M (fn (st1, st2) => f st2)
+ fun localM f = pushM |-- f :|-- (fn res => popM |-- returnM res)
+ fun s1M n1 = m0M (fn (_, st2) => setM (n1, st2))
+ fun s2M n2 = m0M (fn (st1, _) => setM (st1, n2))
+ fun dgM scan arg = let val (v, [arg']) = scan [arg] in (v, arg') end
+ (* The flowing primed version is meant to substitute the unprimed version *)
+ fun m0M' f = liftM (m0M f)
+ fun m1M' f = liftM (m1M f)
+ fun m2M' f = liftM (m2M f)
+ val liftE = I
+ val lift = Scan.lift
+ val :|-- = Scan.:|--
+ val |-- = Scan.|--
+ val -- = Scan.--
+ val >> = Scan.>>
+ val normVal = I
+end
+*}
+
+ML {*
+ open StackMonad
+ open Exceptional
+*}
+
+section {* State monad with stack *}
+
+ML {*
+local
+ val tracing = (fn ctxt => fn str =>
+ if (Config.get ctxt trace_match) then tracing str else ())
+ fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of
+ fun pterm ctxt t =
+ t |> string_of_term ctxt |> tracing ctxt
+in
+ fun tracingM s = liftM (m2M (fn ctxt => returnM (tracing ctxt s)))
+ fun ptermM t = liftM (m2M (fn ctxt => returnM (pterm ctxt t)))
+ fun presultM tag scan = scan :|-- (fn res =>
+ tracingM tag |--
+ ptermM res |--
+ returnM res
+ )
+end
+*}
+
+ML {*
+local
+ val tracing = (fn ctxt => fn str =>
+ if (Config.get ctxt trace_match) then tracing str else ())
+ fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of
+ fun pterm ctxt t =
+ t |> string_of_term ctxt |> tracing ctxt
+ fun match_fun1 pat term (st, ctxt) = let
+ val _ = tracing ctxt "match_fun on:"
+ val _ = tracing ctxt pat
+ val _ = pterm ctxt term
+ in
+ (Proof_Context.match_bind_i true
+ [([Proof_Context.read_term_pattern ctxt pat], term)] ctxt |>
+ (fn (_, ctxt) => (term, (st, ctxt))))
+ handle (ERROR x) =>
+ raise (Scan.fail x)
+ end
+in
+ fun match_fun pat term = liftE (match_fun1 pat term)
+end
+*}
+
+ML {*
+ fun err_trans (ERROR x) = raise (Scan.fail x)
+ | err_trans e = e
+*}
+
+ML {*
+ fun exnM f monad = (fn inp => monad inp handle e => raise (f e))
+*}
+
+ML {*
+ fun match_fun pat term =
+ tracingM "match_fun on:" |--
+ tracingM pat |--
+ ptermM term |--
+ liftM (lift (m0M (fn ctxt => (* setM (Variable.auto_fixes term ctxt) |-- *)
+ (liftE (Proof_Context.match_bind_i true [([Proof_Context.read_term_pattern ctxt pat], term)])) |--
+ returnM term
+ )) |> exnM err_trans)
+*}
+
+ML {*
+local
+ val >> = Scan.>>
+in
+ val match_parser =
+ (Args.name_source) >> (fn s => "(match_fun "^ML_Syntax.print_string s^")")
+end
+*}
+
+ML {*
+local
+ val >> = Scan.>>
+in
+ val fterm_parser =
+ Args.name_source >>
+ (fn term => "liftM (exnM err_trans (lift (m0M (fn ctxt => returnM ((Syntax.read_term ctxt) "^ML_Syntax.print_string term ^")))))")
+end
+*}
+
+setup {*
+ ML_Antiquote.inline @{binding match} (Scan.lift match_parser) #>
+ ML_Antiquote.inline @{binding fterm} (Scan.lift fterm_parser)
+*}
+
+ML {*
+ infixr 0 |||
+ fun (scan1 ||| scan2) xs = scan1 xs handle _ => scan2 xs
+*}
+
+declare [[trace_match = false]]
+
+ML {*
+ val t = [((), @{context})] |>
+ (@{match "(?x::nat) + ?y"} @{term "(1::nat) + 2"} |--
+ @{fterm "?x"})
+*}
+
+
+ML {* (* testings and examples *)
+ fun trans t = (@{match "(?x ::nat) + ?y"} t |--
+ (@{fterm "?x"} :|-- trans) :|-- @{match "?u"} |--
+ (@{fterm "?y"} :|-- trans) :|-- @{match "?v"} |--
+ @{fterm "?v * ?v * ?u"}
+ ||
+ @{match "(?x ::nat) - ?y"} t |--
+ (@{fterm "?x"} :|-- trans) :|-- @{match "?u"} |--
+ (@{fterm "?y"} :|-- trans) :|-- @{match "v"} |--
+ @{fterm "?v - ?v * ?u"}
+ ||
+ (returnM t))
+*}
+
+ML {*
+ val t = trans @{term "(u - (x::nat) + y)"} [((), @{context})] |> normVal |>
+ apfst (cterm_of @{theory}) |> fst
+ *}
+
+end
\ No newline at end of file