1.1 --- a/src/Tools/isac/Specify/specification.sml Mon May 18 11:58:55 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/specification.sml Mon May 18 14:02:54 2020 +0200
1.3 @@ -60,68 +60,80 @@
1.4
1.5 type T = Specification_Def.T
1.6
1.7 -(*val reset: Calc.T -> Calc.T*)
1.8 - val reset_calchead: Calc.T -> Calc.T
1.9 -(*val get: Calc.T -> T*)
1.10 - val get_ocalhd: Calc.T -> T
1.11 -(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
1.12 - val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
1.13 -(*val is_complete: Calc.T -> bool*)
1.14 - val is_complete_mod: Calc.T -> bool
1.15 +(*val reset_calchead: Calc.T -> Calc.T*)
1.16 + val reset: Calc.T -> Calc.T
1.17 +(*val get_ocalhd: Calc.T -> T*)
1.18 + val get: Calc.T -> T
1.19 +(*val get: Calc.T ->
1.20 + I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context*)
1.21 + val get_data: Calc.T ->
1.22 + I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
1.23 +
1.24 +(*/----- delete -----\* )
1.25 + val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
1.26 +( *\----- delete -----/*)
1.27 +
1.28 +(*val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
1.29 + val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
1.30 +(*val is_complete_mod: Calc.T -> bool*)
1.31 + val is_complete: Calc.T -> bool
1.32
1.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.34 (*NONE*)
1.35 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.36 - val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
1.37 - val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
1.38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.39 end
1.40
1.41 (**)
1.42 -structure Specification(** ): SPECIFICATION( **) =
1.43 +structure Specification(**): SPECIFICATION(**) =
1.44 struct
1.45 (**)
1.46
1.47 type T = Specification_Def.T;
1.48
1.49 (* is the calchead complete ? *)
1.50 -fun ocalhd_complete its pre (dI, pI, mI) =
1.51 +fun complete its pre (dI, pI, mI) =
1.52 foldl and_ (true, map #3 (its: I_Model.T)) andalso
1.53 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
1.54 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
1.55
1.56 +(*/----- delete -----\* )
1.57 fun is_parsed (I_Model.Syn _) = false
1.58 | is_parsed _ = true
1.59
1.60 -(* get the first term in ts from ori *)
1.61 -fun getr_ct thy (_, _, fd, d, ts) =
1.62 - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
1.63 -
1.64 (* get a term from ori, notyet input in itm.
1.65 the term from ori is thrown back to a string in order to reuse
1.66 machinery for immediate input by the user. *)
1.67 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
1.68 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
1.69 +( *\----- delete -----/*)
1.70
1.71 +(*/----- delete -----\* )
1.72 (* output the headline to a ppc *)
1.73 fun header p_ pI mI =
1.74 case p_ of
1.75 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
1.76 | Pos.Met => Test_Out.Method mI
1.77 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
1.78 +( *\----- delete -----/*)
1.79
1.80 +(** )
1.81 fun make m_field (term_as_string, i_model) =
1.82 case m_field of
1.83 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
1.84 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
1.85 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
1.86 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
1.87 -fun get (pt, (p, _)) =
1.88 +( **)
1.89 +
1.90 +fun get_data (pt, (p, _)) =
1.91 case Ctree.get_obj I pt p of
1.92 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
1.93 => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
1.94 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
1.95
1.96 +
1.97 +(*/----- delete -----\* )
1.98 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1.99 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1.100 fun tag_form thy (formal, given) =
1.101 @@ -131,18 +143,20 @@
1.102 in gf end)
1.103 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
1.104 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
1.105 +( *\----- delete -----/*)
1.106
1.107 -fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
1.108 +fun is_complete (pt, pos as (p, Pos.Pbl)) =
1.109 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
1.110 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
1.111 - else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
1.112 - | is_complete_mod (pt, pos as (p, Pos.Met)) =
1.113 + else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
1.114 + | is_complete (pt, pos as (p, Pos.Met)) =
1.115 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
1.116 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
1.117 - else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
1.118 - | is_complete_mod (_, pos) =
1.119 - raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
1.120 + else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
1.121 + | is_complete (_, pos) =
1.122 + raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
1.123
1.124 +(*/----- delete -----\* )
1.125 (** get the formula from a ctree-node **)
1.126 (*
1.127 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1.128 @@ -157,38 +171,39 @@
1.129 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
1.130 [("stepform", (p, Pos.Res), r)]
1.131 | form _ _ = raise ERROR "form: uncovered definition"
1.132 +( *\----- delete -----/*)
1.133
1.134 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
1.135 -fun get_ocalhd (pt, (p, Pos.Pbl)) =
1.136 +fun get (pt, (p, Pos.Pbl)) =
1.137 let
1.138 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
1.139 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1.140 - | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
1.141 + | _ => raise ERROR "get Pbl: uncovered case get_obj"
1.142 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
1.143 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
1.144 in
1.145 - (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
1.146 + (complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
1.147 end
1.148 - | get_ocalhd (pt, (p, Pos.Met)) =
1.149 + | get (pt, (p, Pos.Met)) =
1.150 let
1.151 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
1.152 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1.153 - | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
1.154 + | _ => raise ERROR "get Met: uncovered case get_obj"
1.155 val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
1.156 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
1.157 in
1.158 - (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
1.159 + (complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
1.160 end
1.161 - | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
1.162 + | get _ = raise ERROR "get: uncovered definition"
1.163
1.164 (* at the activeFormula set the Specification
1.165 to empty and return a CalcHead;
1.166 the 'origin' remains (for reconstructing all that) *)
1.167 -fun reset_calchead (pt, (p,_)) =
1.168 +fun reset (pt, (p,_)) =
1.169 let
1.170 val () = case Ctree.get_obj I pt p of
1.171 Ctree.PblObj _ => ()
1.172 - | _ => raise ERROR "reset_calchead: uncovered case get_obj"
1.173 + | _ => raise ERROR "reset: uncovered case get_obj"
1.174 val pt = Ctree.update_pbl pt p []
1.175 val pt = Ctree.update_met pt p []
1.176 val pt = Ctree.update_spec pt p References.empty