src/Tools/isac/MathEngBasic/ctree-basic-TEST.sml
changeset 60771 1b072aab8f4e
parent 60704 af9ec1fc81b4
equal deleted inserted replaced
60770:365758b39d90 60771:1b072aab8f4e
     5 Definitions required for Ctree, renamed later appropriately
     5 Definitions required for Ctree, renamed later appropriately
     6 -------------------------vvvvv + I_Model.T-TEST are the only difference to 
     6 -------------------------vvvvv + I_Model.T-TEST are the only difference to 
     7           BASIC_CALC_TREE
     7           BASIC_CALC_TREE
     8 *)
     8 *)
     9 
     9 
    10 signature BASIC_CALC_TREE_TEST =
    10 signature BASIC_CALC_TREE_POS =
    11 sig
    11 sig
    12 (**** signature ****)
    12 (**** signature ****)
    13 (** the basic datatype **)
    13 (** the basic datatype **)
    14   type state
    14   type state
    15   val e_state: state
    15   val e_state: state
    44   val is_pblnd : ctree -> bool
    44   val is_pblnd : ctree -> bool
    45 
    45 
    46   val g_spec : ppobj -> References_Def.T
    46   val g_spec : ppobj -> References_Def.T
    47   val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
    47   val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
    48   val g_form : ppobj -> term
    48   val g_form : ppobj -> term
    49   val g_pbl : ppobj -> Model_Def.i_model_TEST
    49   val g_pbl : ppobj -> Model_Def.i_model_POS
    50   val g_met : ppobj -> Model_Def.i_model_TEST
    50   val g_met : ppobj -> Model_Def.i_model_POS
    51   val g_metID : ppobj -> MethodC.id
    51   val g_metID : ppobj -> MethodC.id
    52   val g_result : ppobj -> Celem.result
    52   val g_result : ppobj -> Celem.result
    53   val g_tac : ppobj -> Tactic.input
    53   val g_tac : ppobj -> Tactic.input
    54   val g_domID : ppobj -> ThyC.id
    54   val g_domID : ppobj -> ThyC.id
    55 
    55 
   104   val branch2str : branch -> string
   104   val branch2str : branch -> string
   105 \<close>
   105 \<close>
   106 end
   106 end
   107 
   107 
   108 (**)
   108 (**)
   109 structure CTbasic_TEST(**): BASIC_CALC_TREE_TEST(**) =
   109 structure CTbasic_POS(**): BASIC_CALC_TREE_POS(**) =
   110 struct
   110 struct
   111 (**)
   111 (**)
   112 open Pos
   112 open Pos
   113 
   113 
   114 (**** Ctree ****)
   114 (**** Ctree ****)
   179    {fmz   : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem            *)
   179    {fmz   : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem            *)
   180     origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model      *)
   180     origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model      *)
   181 	           References_Def.T *  (* updated by Refine_Tacitly                                  *)
   181 	           References_Def.T *  (* updated by Refine_Tacitly                                  *)
   182 	           term,            (* headline of calc-head, as calculated initially(!)             *)
   182 	           term,            (* headline of calc-head, as calculated initially(!)             *)
   183     spec  : References_Def.T, (* explicitly input                                              *)
   183     spec  : References_Def.T, (* explicitly input                                              *)
   184     probl : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a Problem                *)
   184     probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem                *)
   185     meth  : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a MethodC                *)
   185     meth  : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC                *)
   186     ctxt  : Proof.context,    (* used while specifying this (Sub-)Problem and MethodC          *)
   186     ctxt  : Proof.context,    (* used while specifying this (Sub-)Problem and MethodC          *)
   187     loc   : (Istate_Def.T * Proof.context) option  (* like in PrfObj, calling this SubProblem  *)
   187     loc   : (Istate_Def.T * Proof.context) option  (* like in PrfObj, calling this SubProblem  *)
   188           * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
   188           * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
   189     branch: branch,           (* like PrfObj                                                   *)
   189     branch: branch,           (* like PrfObj                                                   *)
   190     result: Celem.result,     (* like PrfObj                                                   *)
   190     result: Celem.result,     (* like PrfObj                                                   *)