(* Title:  BaseDefinitions/substitution.sml

   Author: Walther Neuper

   (c) due to copyright terms

The variety of substitutions is required by various presentations to the front end;

this shall be simplified during the shift to Isabelle/PIDE.

Two different formats shall remain, probably:

# type input: is what the user sees (pairs of terms)

# type as_eqs: a format useful for handling results of equation solving

*)

signature SUBSTITUTION =

sig

  type T = LibraryC.subst;

  val to_string: T -> string

  type as_eqs = term list                   (* for Tactic.Substitute: [@{term "bdv = x"}, ...] *)

  type program = term                      (* in programs: @{term "[(''bdv_1'', x::real), ..]} *)

  type input = TermC.as_string list                        (* by student: ["(''bdv'', x)", ..] *)

  val input_empty: input

  type as_string_eqs                               (* for Tactic.Substitute ["bdv_1 = x", ...] *)

  val string_eqs_to_string: as_string_eqs -> string

  val T_to_string_eqs: T -> as_string_eqs

  val T_to_input: T -> input

  val T_from_string_eqs: theory -> as_string_eqs -> T

  val T_from_input: Proof.context -> input -> T

  val input_to_terms: Proof.context -> input -> as_eqs

  val eqs_to_input: as_eqs -> as_string_eqs

  val program_to_input: program -> input

  val for_bdv: program -> T -> input option * T

\<^isac_test>\<open>

  val string_eqs_empty: as_string_eqs

  val T_from_program: program -> T

\<close>

end

(**)

structure Subst(**): SUBSTITUTION(**) =

struct

(**)

type T = LibraryC.subst;

fun to_string s =

    (strs2str o

      (map (

        linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;

type input = TermC.as_string list;

val input_empty = [];

type as_string_eqs = TermC.as_string list;

\<^isac_test>\<open>

val string_eqs_empty = []: TermC.as_string list;

\<close>

fun string_eqs_to_string s = strs2str s;

type as_eqs = term list;

type program = term;

fun T_to_string_eqs subst = map UnparseC.term (map HOLogic.mk_eq subst)

fun T_to_input subst_rew = (subst_rew

  |> map (apsnd UnparseC.term)

  |> map (apfst UnparseC.term)

  |> map (apfst (enclose "''" "''")))

  |> map pair2str

  handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, [])

fun T_from_string_eqs thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;

(*TODO: input requires parse _: _ -> _ option*)

fun T_from_input ctxt input = (input

  |> map (TermC.parse_patt (Proof_Context.theory_of ctxt))

  |> map TermC.isapair2pair

  |> map (apfst HOLogic.dest_string)

  |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))

  handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])

val eqs_to_input = map UnparseC.term;

(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)

fun input_to_terms ctxt strs = strs

  |> map (TermC.parse ctxt)

  |> map (Model_Pattern.adapt_term_to_type ctxt)

fun program_to_input sub = (sub 

  |> HOLogic.dest_list 

  |> map HOLogic.dest_prod 

  |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))

  |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)

  handle TERM _ => raise TERM ("program_to_input: wrong argument ", [sub])

fun T_from_program t = (t 

  |> HOLogic.dest_list 

  |> map HOLogic.dest_prod 

  |> map (apfst HOLogic.dest_string))

  |> map (apfst (fn e1 => (TermC.mk_Free (e1, HOLogic.realT))))

  handle TERM _ => raise TERM ("T_from_program: wrong argument ", [t])

(* get a substitution for "bdv*" from the current program and environment.

    returns a substitution: as_string_eqs for tac, subst for tac_, i.e. for rewriting *)

fun for_bdv prog env =

  let

    fun scan (Const _) = NONE

      | scan (Free _) = NONE

      | scan (Var _) = NONE

      | scan (Bound _) = NONE

      | scan (t as Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ _) $ _) =

        if TermC.is_bdv_subst t then SOME t else NONE

      | scan (Abs (_, _, body)) = scan body

      | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

  in

    case scan prog of

      NONE => (NONE: input option, []: subst)

    | SOME tm =>

        let val subst = subst_atomic env tm

        in (SOME (program_to_input subst), T_from_program subst) end

  end

(**)end(**)