(* 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(**)