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