
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




