diff -r 77daf1b85cf0 -r a5f5b9336007 thys2/Term_pat.thy --- /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