1.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Dec 14 09:37:01 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Dec 14 10:45:41 2016 +0100
1.3 @@ -10,10 +10,12 @@
1.4 eqtype indent
1.5 datatype nest = Closed | Nundef | Open
1.6 datatype pblmet = Method of metID | Problem of pblID | Upblmet
1.7 - datatype inout
1.8 - = Error_ of string | FormKF of cellID * edit * indent * nest * cterm'
1.9 - | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) | RefineKF of match list
1.10 - | RefinedKF of pblID * (itm list * (bool * term) list)
1.11 + datatype inout =
1.12 + Error_ of string
1.13 + | FormKF of cellID * edit * indent * nest * cterm'
1.14 + | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc)
1.15 + | RefineKF of match list
1.16 + | RefinedKF of pblID * (itm list * (bool * term) list)
1.17 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
1.18 val generate1 : theory -> tac_ -> istate * Proof.context ->
1.19 posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
1.20 @@ -38,7 +40,7 @@
1.21 end
1.22
1.23 (**)
1.24 -structure Ctree(**): CALC_TREE(**) =
1.25 +structure Ctree(*: CALC_TREE*) =
1.26 (**)
1.27 struct
1.28 (* initialize istate for Detail_Set *)
1.29 @@ -153,16 +155,21 @@
1.30 | inout2str _ = error "inout2str: uncovered definition"
1.31 fun inouts2str ios = (strs2str' o (map inout2str)) ios
1.32
1.33 +(*
1.34 + datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
1.35 +*)
1.36 datatype mout =
1.37 - Form' of inout (* packing cterm' | cterm' ppc *)
1.38 -| Problems of inout (* passes specify (and solve) *)
1.39 -| Error' of inout
1.40 -| EmptyMout;
1.41 + FormKF of cterm'
1.42 +| PpcKF of (pblmet * item ppc)
1.43 +| RefinedKF of pblID * (itm list * (bool * term) list)
1.44 +| Error' of string
1.45 +| EmptyMout
1.46
1.47 -fun mout2str (Form' inout) ="Form' "^(inout2str inout)
1.48 - | mout2str (Error' inout) ="Error' "^(inout2str inout)
1.49 - | mout2str (EmptyMout ) ="EmptyMout"
1.50 - | mout2str _ = error "mout2str: uncovered definition"
1.51 +fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
1.52 + | mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ itemppc2str itemppc ^ ")"
1.53 + | mout2str (RefinedKF (pblID, ls)) = "mout2str: RefinedKF not impl."
1.54 + | mout2str (Error' str) = "Error' " ^ str
1.55 + | mout2str (EmptyMout ) = "EmptyMout"
1.56
1.57 (* init pbl with ...,dsc,empty | [] *)
1.58 fun init_pbl pbt =
1.59 @@ -179,7 +186,7 @@
1.60 (*generate 1 ppobj in ptree*)
1.61 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
1.62 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
1.63 - (pos:pos',[],Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [][]))),
1.64 + (pos: pos', [], PpcKF (Upblmet, itms2itemppc thy [][]),
1.65 case p_ of
1.66 Pbl => update_pbl pt p itmlist
1.67 | Met => update_met pt p itmlist
1.68 @@ -187,27 +194,27 @@
1.69 (* WN110515 probably declare_constraints with input item (without dsc) --
1.70 -- important when specifying without formalisation *)
1.71 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
1.72 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
1.73 + (pos, [], (PpcKF (Upblmet, itms2itemppc thy [] [])),
1.74 case p_ of
1.75 Pbl => update_pbl pt p itmlist
1.76 | Met => update_met pt p itmlist
1.77 | _ => error ("uncovered case " ^ pos_2str p_))
1.78 (*WN110515 probably declare_constraints with input item (without dsc)*)
1.79 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
1.80 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
1.81 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []),
1.82 case p_ of
1.83 Pbl => update_pbl pt p itmlist
1.84 | Met => update_met pt p itmlist
1.85 | _ => error ("uncovered case " ^ pos_2str p_))
1.86 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
1.87 - (pos, [] ,Form' (PpcKF (0 ,EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
1.88 + (pos, [] , PpcKF (Upblmet, itms2itemppc thy [] []),
1.89 update_domID pt p domID)
1.90 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
1.91 let
1.92 val pt = update_pbl pt p itms
1.93 val pt = update_pblID pt p pI
1.94 in
1.95 - ((p, Pbl), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.96 + ((p, Pbl), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.97 end
1.98 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
1.99 let
1.100 @@ -215,28 +222,28 @@
1.101 val pt = update_met pt p itms
1.102 val pt = update_metID pt p mID
1.103 in
1.104 - ((p, Met), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.105 + ((p, Met), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.106 end
1.107 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
1.108 let
1.109 val pt = update_pbl pt p itms
1.110 val pt = update_met pt p met
1.111 in
1.112 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.113 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.114 end
1.115 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
1.116 let
1.117 val pt = update_pbl pt p pbl
1.118 val pt = update_orispec pt p (domID, pIre, metID)
1.119 in
1.120 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.121 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.122 end
1.123 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
1.124 let
1.125 val (dI, _, mI) = get_obj g_spec pt p
1.126 val pt = update_spec pt p (dI, pI, mI)
1.127 in
1.128 - (pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
1.129 + (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.130 end
1.131 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
1.132 (case topt of
1.133 @@ -251,7 +258,7 @@
1.134 in if p' = 0 then ps @ [1] else p end
1.135 val (pt, c) = cappend_form pt p l t
1.136 in
1.137 - ((p, Frm): pos', c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
1.138 + ((p, Frm): pos', c, FormKF (term2str t), pt)
1.139 end
1.140 | generate1 _ (Begin_Trans' t) l (p, Frm) pt =
1.141 let
1.142 @@ -261,7 +268,7 @@
1.143 val p = (lev_on o lev_dn (* starts with [...,0] *)) p
1.144 val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
1.145 in
1.146 - ((p, Frm), c @ c', Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
1.147 + ((p, Frm), c @ c', FormKF (term2str t), pt)
1.148 end
1.149 | generate1 thy (Begin_Trans' t) l (p, Res) pt =
1.150 (*append after existing PrfObj vvvvvvvvvvvvv*)
1.151 @@ -271,21 +278,23 @@
1.152 val p' = lev_up p
1.153 val (pt, c) = append_result pt p' l tasm Complete
1.154 in
1.155 - ((p', Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
1.156 + ((p', Res), c, FormKF (term2str t), pt)
1.157 end
1.158 | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
1.159 let
1.160 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.161 (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
1.162 val pt = update_branch pt p TransitiveB
1.163 - in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt) end
1.164 + in
1.165 + ((p, Res), c, FormKF (term2str f'), pt)
1.166 + end
1.167 | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
1.168 let
1.169 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.170 (Rewrite thm') (f', asm) Complete
1.171 val pt = update_branch pt p TransitiveB
1.172 in
1.173 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.174 + ((p, Res), c, FormKF (term2str f'), pt)
1.175 end
1.176 | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
1.177 | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
1.178 @@ -294,7 +303,7 @@
1.179 (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete
1.180 val pt = update_branch pt p TransitiveB
1.181 in
1.182 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.183 + ((p, Res), c, FormKF (term2str f'), pt)
1.184 end
1.185 | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
1.186 let
1.187 @@ -313,7 +322,7 @@
1.188 (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.189 val pt = update_branch pt p TransitiveB
1.190 in
1.191 - ((p, Res), c, Form' (FormKF (~1 ,EdUndef, length p, Nundef, term2str f')), pt)
1.192 + ((p, Res), c, FormKF (term2str f'), pt)
1.193 end
1.194 | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
1.195 let
1.196 @@ -330,37 +339,37 @@
1.197 let
1.198 val (pt, c) = append_result pt p l (scval, asm) Complete
1.199 in
1.200 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str scval)), pt)
1.201 + ((p, Res), c, FormKF (term2str scval), pt)
1.202 end
1.203 | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt =
1.204 let
1.205 val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete
1.206 in
1.207 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.208 + ((p, Res), c, FormKF (term2str f'), pt)
1.209 end
1.210 | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
1.211 let
1.212 val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete
1.213 in
1.214 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
1.215 + ((p, Res), c, FormKF (term2str f'), pt)
1.216 end
1.217 | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt =
1.218 let
1.219 val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete
1.220 in
1.221 - ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str list)), pt)
1.222 + ((p, Res), c, FormKF (term2str list), pt)
1.223 end
1.224 | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt =
1.225 let
1.226 val (pt,c) =
1.227 cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete
1.228 - in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t')), pt)
1.229 + in ((p, Res), c, FormKF (term2str t'), pt)
1.230 end
1.231 | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt =
1.232 let
1.233 val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete
1.234 in
1.235 - ((p,Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f')), pt)
1.236 + ((p,Res), c, FormKF f', pt)
1.237 end
1.238 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
1.239 let
1.240 @@ -368,7 +377,7 @@
1.241 val pt = update_ctxt pt p ctxt
1.242 val f = Syntax.string_of_term (thy2ctxt thy) f
1.243 in
1.244 - ((p, Pbl), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f)), pt)
1.245 + ((p, Pbl), c, FormKF f, pt)
1.246 end
1.247 | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m')
1.248