1.1 --- a/src/Tools/isac/Specify/p-model.sml Sat Nov 26 22:28:33 2022 +0100
1.2 +++ b/src/Tools/isac/Specify/p-model.sml Sat Dec 03 19:09:51 2022 +0100
1.3 @@ -9,9 +9,9 @@
1.4 sig
1.5 datatype switch_pbl_met = Model_For_Problem_Ref | Model_For_Method_Ref
1.6
1.7 - type field_out
1.8 + type model_out
1.9 val template_args: switch_pbl_met -> References.input -> Ctree.ctree ->
1.10 - (switch_pbl_met * field_out list) * References.input
1.11 + (switch_pbl_met * model_out) * References.input
1.12
1.13 (* for the OLD P_Model.T *)
1.14 type T
1.15 @@ -46,8 +46,22 @@
1.16
1.17 (** for the NEW template for Specification**)
1.18 datatype feedback = Cor | Inc | Sup | True | False
1.19 +(*
1.20 + legend:
1.21 + Cor correct: the default representation
1.22 + Inc incomplete list, (accessible) markup to be defined
1.23 + Sup superfluous within the current variant from Formalise.model;
1.24 + (accessible) markup to be defined
1.25 + True the default representation
1.26 + False (accessible) markup to be defined
1.27 +*)
1.28 type out_element = UnparseC.term_as_string * feedback
1.29 type field_out = Model_Pattern.m_field * out_element list
1.30 +type model_out =
1.31 + field_out (* "#Given", feedback: Cor | Inc | Sup *)
1.32 + * field_out (* "#Where", feedback: True | False *)
1.33 + * field_out (* "#Find", feedback: Cor | Inc | Sup *)
1.34 + * field_out (* "#Relate",feedback: Cor | Inc | Sup *)
1.35
1.36 (*val item_to_out: Proof.context -> I_Model.single -> out_element*)
1.37 fun item_to_out ctxt (_, _, _, _, I_Model.Cor (dsc_ts, _)) =
1.38 @@ -79,7 +93,7 @@
1.39 val where_ = wheres_to_out ctxt where_
1.40 val find = items_to_out ctxt "#Find" model
1.41 val relate = items_to_out ctxt "#Relate" model
1.42 - in given :: where_ :: find :: relate :: [] end
1.43 + in (given, where_, find, relate) end
1.44
1.45 fun template_args switch_pbl_met input_refs store =
1.46 if not (Ctree.is_pblnd store) then raise ERROR "update code w.r.t. to future design of Solution"