1.1 --- a/src/Tools/isac/Specify/specification.sml Sat May 16 14:04:35 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/specification.sml Sat May 16 16:23:24 2020 +0200
1.3 @@ -86,17 +86,6 @@
1.4 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
1.5 ( *\------- to Specify from Specification -------/*)
1.6
1.7 -(*/------- to I_Model from Specification -------\*)
1.8 - val complete_metitms: O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
1.9 - val insert_ppc': I_Model.single -> I_Model.T -> I_Model.T
1.10 - val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
1.11 - I_Model.T * I_Model.T
1.12 - val is_error: I_Model.feedback -> bool
1.13 - val itm_out: theory -> I_Model.feedback -> string
1.14 - val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool
1.15 - val ori2Coritm: Model_Pattern.T -> O_Model.single -> I_Model.single
1.16 -(*\------- to I_Model from Specification -------/*)
1.17 -
1.18 (*/------- to P_Model from Specification -------\*)
1.19 val ppc2list: 'a P_Model.ppc -> 'a list
1.20 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
1.21 @@ -176,12 +165,6 @@
1.22 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
1.23 in (flat o (map d_in)) itm_s end;
1.24
1.25 -fun is_error (I_Model.Cor _) = false
1.26 - | is_error (I_Model.Sup _) = false
1.27 - | is_error (I_Model.Inc _) = false
1.28 - | is_error (I_Model.Mis _) = false
1.29 - | is_error _ = true
1.30 -
1.31 (* get the first term in ts from ori *)
1.32 fun getr_ct thy (_, _, fd, d, ts) =
1.33 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
1.34 @@ -242,18 +225,9 @@
1.35 | SOME ori => SOME (geti_ct thy ori (hd icl))
1.36 end
1.37
1.38 -(*create output-string for itm_*)
1.39 -fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
1.40 - | itm_out _ (I_Model.Syn c) = c
1.41 - | itm_out _ (I_Model.Typ c) = c
1.42 - | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
1.43 - | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
1.44 - | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
1.45 - | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
1.46 -
1.47 -fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (itm_out thy itm_)
1.48 - | mk_delete thy "#Find" itm_ = Tactic.Del_Find (itm_out thy itm_)
1.49 - | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (itm_out thy itm_)
1.50 +fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
1.51 + | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
1.52 + | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
1.53 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
1.54 fun mk_additem "#Given" ct = Tactic.Add_Given ct
1.55 | mk_additem "#Find" ct = Tactic.Add_Find ct
1.56 @@ -280,7 +254,7 @@
1.57 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
1.58 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
1.59 else
1.60 - case find_first (is_error o #5) pbl of
1.61 + case find_first (I_Model.is_error o #5) pbl of
1.62 SOME (_, _, _, fd, itm_) =>
1.63 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
1.64 | NONE =>
1.65 @@ -292,14 +266,14 @@
1.66 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
1.67 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
1.68 else
1.69 - case find_first (is_error o #5) met of
1.70 + case find_first (I_Model.is_error o #5) met of
1.71 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
1.72 | NONE =>
1.73 (case nxt_add (ThyC.get_theory dI) oris mpc met of
1.74 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
1.75 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
1.76 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
1.77 - (case find_first (is_error o #5) met of
1.78 + (case find_first (I_Model.is_error o #5) met of
1.79 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
1.80 | NONE =>
1.81 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
1.82 @@ -312,13 +286,6 @@
1.83 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
1.84 (*\------- to Specify from Specification -------/*)
1.85
1.86 -
1.87 -fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
1.88 -
1.89 -(* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1.90 - handles superfluous items carelessly *)
1.91 -fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.92 -
1.93 (* output the headline to a ppc *)
1.94 fun header p_ pI mI =
1.95 case p_ of
1.96 @@ -469,54 +436,6 @@
1.97 end
1.98 | nxt_specif_additem _ _ (_, p) = raise ERROR ("nxt_specif_additem not impl. for" ^ Pos.pos'2str p)
1.99
1.100 -(*/------- to I_Model from Specification -------\*)
1.101 -fun ori2Coritm pbt (i, v, f, d, ts) =
1.102 - (i, v, true, f, I_Model.Cor ((d, ts), ((snd o snd o the o (find_first (I_Model.eq1 d))) pbt, ts)))
1.103 - handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
1.104 - (*dsc in oris, but not in pbl pat list: keep this dsc*)
1.105 -(*\------- to I_Model from Specification -------/*)
1.106 -
1.107 -(* filter out oris which have same description in itms *)
1.108 -fun filter_outs oris [] = oris
1.109 - | filter_outs oris (i::itms) =
1.110 - let
1.111 - val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
1.112 - in
1.113 - filter_outs ors itms
1.114 - end
1.115 -
1.116 -(* filter oris which are in pbt, too *)
1.117 -fun filter_pbt oris pbt =
1.118 - let
1.119 - val dscs = map (fst o snd) pbt
1.120 - in
1.121 - filter ((member op= dscs) o (#4)) oris
1.122 - end
1.123 -
1.124 -(* combine itms from pbl + met and complete them wrt. pbt *)
1.125 -(* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1.126 -fun complete_metitms oris pits mits met =
1.127 - let
1.128 - val vat = I_Model.max_vt pits;
1.129 - val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
1.130 - val ors = filter ((member_swap op= vat) o (#2)) oris
1.131 - val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
1.132 - in
1.133 - itms @ (map (ori2Coritm met) os)
1.134 - end
1.135 -
1.136 -(* complete model and guard of a calc-head *)
1.137 -fun complete_mod_ (oris, mpc, ppc, probl) =
1.138 - let
1.139 - val pits = filter_out ((curry op= false) o (#3)) probl
1.140 - val vat = if probl = [] then 1 else I_Model.max_vt probl
1.141 - val pors = filter ((member_swap op = vat) o (#2)) oris
1.142 - val pors = filter_outs pors pits (*which are in pbl already*)
1.143 - val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1.144 - val pits = pits @ (map (ori2Coritm ppc) pors)
1.145 - val mits = complete_metitms oris pits [] mpc
1.146 - in (pits, mits) end
1.147 -
1.148 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1.149 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1.150 fun tag_form thy (formal, given) =
1.151 @@ -542,7 +461,7 @@
1.152 val (_, pI, mI) = References.select ospec spec
1.153 val mpc = (#ppc o Method.from_store) mI
1.154 val ppc = (#ppc o Problem.from_store) pI
1.155 - val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1.156 + val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
1.157 val pt = Ctree.update_pblppc pt p pits
1.158 val pt = Ctree.update_metppc pt p mits
1.159 in (pt, (p, Pos.Met)) end
1.160 @@ -561,22 +480,24 @@
1.161 val (_, vals) = O_Model.values' pors
1.162 val ctxt = ContextC.initialise dI vals
1.163 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
1.164 - map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
1.165 + map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)
1.166 in
1.167 (pt, (p, Pos.Met))
1.168 end
1.169
1.170 +(*/------- to I_Model from Specification -------\* )
1.171 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
1.172 fun is_complete_mod_ [] = false
1.173 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
1.174 +( *\------- to I_Model from Specification -------/*)
1.175
1.176 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
1.177 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
1.178 - then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p
1.179 + then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
1.180 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
1.181 | is_complete_mod (pt, pos as (p, Pos.Met)) =
1.182 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
1.183 - then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p
1.184 + then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
1.185 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
1.186 | is_complete_mod (_, pos) =
1.187 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")