(* Title:  Interpret/Interpret.thy

    Author: Walther Neuper 110226

    (c) due to copyright terms

 Collect all defitions for the Lucas-Interpreter

 *)

 theory Interpret

 imports Specify.Specify

 begin

   ML_file istate.sml

   ML_file "sub-problem.sml"

   ML_file "thy-read.sml"

   ML_file "li-tool.sml"

   ML_file "solve-step.sml"

   ML_file "error-pattern.sml"

   ML_file derive.sml

   ML_file "lucas-interpreter.sml"

   ML_file "step-solve.sml"

 ML \<open>

 local

   val thys_known_sofar = Theory.nodes_of @{theory}

   val isac_thys_known_sofar = take (

     find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar,

     thys_known_sofar)

   val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar

 in

   val compare_dependencies__ThyC =

     if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()

     else raise ERROR "theory dependencies not as anticipated in ThyC"

 end

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =

     let

       val tid = HOLogic.dest_string thmID

       val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub

     in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end

   | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =

      (Tactic.Rewrite_Set (HOLogic.dest_string rls))

   | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =

     let

       val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub

     in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end