1.1 --- a/src/Tools/isac/Specify/input-calchead.sml Thu May 14 09:30:40 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Thu May 14 13:33:47 2020 +0200
1.3 @@ -5,46 +5,58 @@
1.4 This will be dropped at switch to Isabelle/PIDE.
1.5 *)
1.6
1.7 -signature INPUT_CALCHEAD =
1.8 +signature INPUT_SPECIFICATION =
1.9 sig
1.10 - type pbt_ = string * (term * term)
1.11 -
1.12 datatype iitem =
1.13 Find of TermC.as_string list
1.14 | Given of TermC.as_string list
1.15 | Relate of TermC.as_string list
1.16 type imodel = iitem list
1.17 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
1.18 - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
1.19 - val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
1.20 + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
1.21 + val cas_input : term -> (Ctree.ctree * Specification.T) option
1.22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.23 (* NONE *)
1.24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.25 - (* NONE *)
1.26 + val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
1.27 + string * TermC.as_string -> I_Model.single
1.28 + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
1.29 + (string * TermC.as_string) list -> I_Model.T
1.30 + val cas_input_: References.T -> (term * term list) list ->
1.31 + Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context
1.32 + val dtss2itm_: Model_Pattern.single list -> term * term list ->
1.33 + int list * bool * string * I_Model.feedback (*I_Model.single'*)
1.34 + val e_icalhd: icalhd
1.35 + val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
1.36 + val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
1.37 + val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
1.38 + val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
1.39 + int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
1.40 + val imodel2fstr: iitem list -> (string * TermC.as_string) list
1.41 + val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
1.42 + val is_casinput: TermC.as_string -> Formalise.T -> bool
1.43 + val is_e_ts: term list -> bool
1.44 + val itms2fstr: I_Model.single -> string * string
1.45 + val par2fstr: I_Model.single -> string * TermC.as_string
1.46 + val parsitm: theory -> I_Model.single -> I_Model.single
1.47 + val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
1.48 + (''a * string) list ->
1.49 + (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
1.50 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.51 -
1.52 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.53 - val e_icalhd : icalhd
1.54 - val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->
1.55 - ('c * ''b * bool * 'd * I_Model.feedback) list
1.56 end
1.57
1.58 -structure In_Chead(**): INPUT_CALCHEAD(**) =
1.59 +(**)
1.60 +structure In_Chead(**): INPUT_SPECIFICATION(**) =
1.61 struct
1.62 +(**)
1.63
1.64 -(* types for problems models (TODO rename to specification models) *)
1.65 -type pbt_ =
1.66 - (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
1.67 - (term * (* description *)
1.68 - term)); (* id | struct-var *)
1.69 -
1.70 -(*** handle an input by CAS-command ***)
1.71 +(** handle input **)
1.72
1.73 fun dtss2itm_ ppc (d, ts) =
1.74 let
1.75 val (f, (d, id)) = the (find_first ((curry op= d) o
1.76 (#1: (term * term) -> term) o
1.77 - (#2: pbt_ -> (term * term))) ppc)
1.78 + (#2: Model_Pattern.single -> (term * term))) ppc)
1.79 in
1.80 ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
1.81 end
1.82 @@ -92,28 +104,27 @@
1.83 val pt = Ctree.update_pbl pt [] pits
1.84 val pt = Ctree.update_met pt [] mits
1.85 in
1.86 - SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
1.87 + SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T)
1.88 end
1.89 end
1.90
1.91
1.92 -(*** handle an input calc-head ***)
1.93 +(** handle an input calc-head **)
1.94
1.95 datatype iitem =
1.96 Given of TermC.as_string list
1.97 -(*Where is never input*)
1.98 +(*Where is still not input*)
1.99 | Find of TermC.as_string list
1.100 | Relate of TermC.as_string list
1.101
1.102 type imodel = iitem list
1.103
1.104 -(*calc-head as input*)
1.105 type icalhd =
1.106 - Pos.pos' * (*the position of the calc-head in the calc-tree*)
1.107 - TermC.as_string * (*the headline*)
1.108 - imodel * (*the model (without Find) of the calc-head*)
1.109 - Pos.pos_ * (*model belongs to Pbl or Met*)
1.110 - References.T; (*specification: domID, pblID, metID*)
1.111 + Pos.pos' * (* the position in Ctree *)
1.112 + TermC.as_string * (* the headline shown on Calc.T *)
1.113 + imodel * (* the model *)
1.114 + Pos.pos_ * (* model belongs to Problem or Method *)
1.115 + References.T; (* into Know_Store *)
1.116 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
1.117
1.118 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
1.119 @@ -228,13 +239,7 @@
1.120 | appl_adds _ _ ppc _ [] = ppc
1.121 | appl_adds dI oris ppc pbt (selct :: ss) =
1.122 let val itm = appl_add' dI oris ppc pbt selct;
1.123 - in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
1.124 -
1.125 -fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
1.126 - | oris2itms pbt vat ((i, v, f, d, ts) :: os) =
1.127 - if member op = vat v
1.128 - then (i, v, true, f, I_Model.Cor ((d, ts), (TermC.empty, []))) :: (oris2itms pbt vat os)
1.129 - else oris2itms pbt vat os
1.130 + in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
1.131
1.132 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
1.133 | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
1.134 @@ -269,38 +274,38 @@
1.135 if dI <> sdI
1.136 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
1.137 val (its, trms) = filter_sep is_Par its;
1.138 - val pbt = (#ppc o Problem.from_store) (#2 (Chead.some_spec ospec sspec))
1.139 + val pbt = (#ppc o Problem.from_store) (#2 (Specification.some_spec ospec sspec))
1.140 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.141 else
1.142 if pI <> spI
1.143 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
1.144 else
1.145 let val pbt = (#ppc o Problem.from_store) pI
1.146 - val dI' = #1 (Chead.some_spec ospec spec)
1.147 + val dI' = #1 (Specification.some_spec ospec spec)
1.148 val oris = if pI = #2 ospec then oris
1.149 else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
1.150 in (Pos.Pbl, appl_adds dI' oris probl pbt
1.151 (map itms2fstr probl), meth) end
1.152 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.153 then let val met = (#ppc o Method.from_store) mI
1.154 - val mits = Chead.complete_metitms oris probl meth met
1.155 + val mits = Specification.complete_metitms oris probl meth met
1.156 in if foldl and_ (true, map #3 mits)
1.157 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
1.158 end
1.159 - else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
1.160 - ((#ppc o Problem.from_store) (#2 (Chead.some_spec ospec spec)))
1.161 + else (Pos.Pbl, appl_adds (#1 (Specification.some_spec ospec spec)) oris [(*!!!*)]
1.162 + ((#ppc o Problem.from_store) (#2 (Specification.some_spec ospec spec)))
1.163 (imodel2fstr imodel), meth)
1.164 val pt = Ctree.update_spec pt p spec;
1.165 in if pos_ = Pos.Pbl
1.166 - then let val {prls,where_,...} = Problem.from_store (#2 (Chead.some_spec ospec spec))
1.167 + then let val {prls,where_,...} = Problem.from_store (#2 (Specification.some_spec ospec spec))
1.168 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
1.169 in (Ctree.update_pbl pt p pits,
1.170 - (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
1.171 + (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
1.172 end
1.173 - else let val {prls,pre,...} = Method.from_store (#3 (Chead.some_spec ospec spec))
1.174 + else let val {prls,pre,...} = Method.from_store (#3 (Specification.some_spec ospec spec))
1.175 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
1.176 in (Ctree.update_met pt p mits,
1.177 - (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
1.178 + (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
1.179 end
1.180 end
1.181 end