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