wneuper/isa: comparison src/Tools/isac/Interpret/generate.sml

equal deleted inserted replaced

-:56762e8a672e
+:aab874fdd910
 val e_taci : taci
 datatype edit = EdUndef | Protect | Write
 eqtype indent
 datatype nest = Closed | Nundef | Open
 datatype pblmet = Method of metID | Problem of pblID | Upblmet
-datatype inout
+datatype inout =
-= Error_ of string | FormKF of cellID * edit * indent * nest * cterm'
+Error_ of string
-| PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) | RefineKF of match list
+| FormKF of cellID * edit * indent * nest * cterm'
-| RefinedKF of pblID * (itm list * (bool * term) list)
+| PpcKF of cellID * edit * indent * nest * (pblmet * item ppc)
+| RefineKF of match list
+| RefinedKF of pblID * (itm list * (bool * term) list)
 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
 val generate1 : theory -> tac_ -> istate * Proof.context ->
 posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
 val init_pbl : (string * (term * 'a)) list -> itm list
 val init_pbl' : (string * (term * term)) list -> itm list
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end
 (**)
-structure Ctree(**): CALC_TREE(**) =
+structure Ctree(*: CALC_TREE*) =
 (**)
 struct
 (* initialize istate for Detail_Set *)
 fun init_istate (Rewrite_Set rls) t =
 (case assoc_rls rls of
 	       ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"
 | inout2str (RefineKF ms)  = "RefineKF "^(matchs2str ms)
 | inout2str _ = error "inout2str: uncovered definition"
 fun inouts2str ios = (strs2str' o (map inout2str)) ios
+(*
+datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
+*)
 datatype mout =
-Form' of inout         (* packing cterm' | cterm' ppc *)
+FormKF of cterm'
-| Problems of inout      (* passes specify (and solve)  *)
+| PpcKF of (pblmet * item ppc)
-| Error' of inout
+| RefinedKF of pblID * (itm list * (bool * term) list)
-| EmptyMout;
+| Error' of string
+| EmptyMout
-fun mout2str (Form' inout) ="Form' "^(inout2str inout)
-| mout2str (Error'  inout) ="Error' "^(inout2str inout)
+fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
-| mout2str (EmptyMout    ) ="EmptyMout"
+| mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ itemppc2str itemppc ^ ")"
-| mout2str _ = error "mout2str: uncovered definition"
+| mout2str (RefinedKF  (pblID, ls)) = "mout2str: RefinedKF not impl."
+| mout2str (Error'  str) = "Error' " ^ str
+| mout2str (EmptyMout    ) = "EmptyMout"
 (* init pbl with ...,dsc,empty | [] *)
 fun init_pbl pbt =
 let
 fun pbt2itm (f, (d, _)) = ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm)
 in map pbt2itm pbt end
 (*generate 1 ppobj in ptree*)
 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
-(pos:pos',[],Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [][]))),
+(pos: pos', [], PpcKF (Upblmet, itms2itemppc thy [][]),
 case p_ of
 Pbl => update_pbl pt p itmlist
 	     | Met => update_met pt p itmlist
 | _ => error ("uncovered case " ^ pos_2str p_))
 (* WN110515 probably declare_constraints with input item (without dsc) --
 -- important when specifying without formalisation *)
 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
-(pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
+(pos, [], (PpcKF (Upblmet, itms2itemppc thy [] [])),
 case p_ of
 Pbl => update_pbl pt p itmlist
 	     | Met => update_met pt p itmlist
 | _ => error ("uncovered case " ^ pos_2str p_))
 (*WN110515 probably declare_constraints with input item (without dsc)*)
 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
-(pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
+(pos, [],  PpcKF (Upblmet, itms2itemppc thy [] []),
 case p_ of
 Pbl => update_pbl pt p itmlist
 	     | Met => update_met pt p itmlist
 | _ => error ("uncovered case " ^ pos_2str p_))
 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
-(pos, [] ,Form' (PpcKF (0 ,EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))),
+(pos, [] , PpcKF  (Upblmet, itms2itemppc thy [] []),
 update_domID pt p domID)
 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
 let
 val pt = update_pbl pt p itms
 val pt = update_pblID pt p pI
 in
-((p, Pbl), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
+((p, Pbl), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
 end
 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
 let
 val pt = update_oris pt p oris
 val pt = update_met pt p itms
 val pt = update_metID pt p mID
 in
-((p, Met), [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
+((p, Met), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
 end
 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
 let
 val pt = update_pbl pt p itms
 	    val pt = update_met pt p met
 in
-(pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
+(pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
 end
 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
 let
 val pt = update_pbl pt p pbl
 val pt = update_orispec pt p (domID, pIre, metID)
 in
-(pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
+(pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
 end
 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
 let
 val (dI, _, mI) = get_obj g_spec pt p
 val pt = update_spec pt p (dI, pI, mI)
 in
-(pos, [], Form' (PpcKF (0, EdUndef, 0, Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
+(pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
 end
 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
 (case topt of
 SOME t =>
 let val (pt, c) = cappend_form pt p (is, ctxt) t
 val p =
 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
 	      in if p' = 0 then ps @ [1] else p end
 val (pt, c) = cappend_form pt p l t
 in
-((p, Frm): pos', c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
+((p, Frm): pos', c, FormKF (term2str t), pt)
 end
 | generate1 _ (Begin_Trans' t) l (p, Frm) pt =
 let
 val (pt, c) = cappend_form pt p l t
 val pt = update_branch pt p TransitiveB (*040312*)
 (* replace the old PrfOjb ~~~~~ *)
 val p = (lev_on o lev_dn (* starts with [...,0] *)) p
 val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
 in
-((p, Frm), c @ c', Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
+((p, Frm), c @ c', FormKF (term2str t), pt)
 end
 | generate1 thy (Begin_Trans' t) l (p, Res) pt =
 (*append after existing PrfObj    vvvvvvvvvvvvv*)
 generate1 thy (Begin_Trans' t) l (lev_on p, Frm) pt
 | generate1 _ (End_Trans' tasm) l (p, _) pt =
 let
 val p' = lev_up p
 val (pt, c) = append_result pt p' l tasm Complete
 in
-((p', Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t)), pt)
+((p', Res), c, FormKF (term2str t), pt)
 end
 | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
 let
 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
 (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
 val pt = update_branch pt p TransitiveB
-in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt) end
+in
+((p, Res), c, FormKF (term2str f'), pt)
+end
 | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
 let
 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
 (Rewrite thm') (f', asm) Complete
 val pt = update_branch pt p TransitiveB
 in
-((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
+((p, Res), c, FormKF (term2str f'), pt)
 end
 | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
 | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
 let
 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
 (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete
 val pt = update_branch pt p TransitiveB
 in
-((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
+((p, Res), c, FormKF (term2str f'), pt)
 end
 | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
 let
 val ctxt' = insert_assumptions asm ctxt
 val (pt, _) = cappend_form pt p (is, ctxt') f
 let
 val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
 (Rewrite_Set (id_rls rls')) (f',asm) Complete
 val pt = update_branch pt p TransitiveB
 in
-((p, Res), c, Form' (FormKF (~1 ,EdUndef, length p, Nundef, term2str f')), pt)
+((p, Res), c, FormKF (term2str f'), pt)
 end
 | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
 let
 val ctxt' = insert_assumptions asm ctxt
 val (pt, _) = cappend_form pt p (is, ctxt') f
 end
 | generate1 _ (Check_Postcond' (_, (scval, asm))) l (p, _) pt =
 let
 val (pt, c) = append_result pt p l (scval, asm) Complete
 in
-((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str scval)), pt)
+((p, Res), c, FormKF (term2str scval), pt)
 end
 | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt =
 let
 val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete
 in
-((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
+((p, Res), c, FormKF (term2str f'), pt)
 end
 | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt =
 let
 val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete
 in
-((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str f')), pt)
+((p, Res), c, FormKF (term2str f'), pt)
 end
 | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt =
 let
 val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete
 in
-((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str list)), pt)
+((p, Res), c, FormKF (term2str list), pt)
 end
 | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt =
 let
 val (pt,c) =
 cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete
-in ((p, Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, term2str t')), pt)
+in ((p, Res), c, FormKF (term2str t'), pt)
 end
 | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt =
 let
 val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete
 in
-((p,Res), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f')), pt)
+((p,Res), c, FormKF f', pt)
 end
 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt =
 let
 	    val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl)
 val pt = update_ctxt pt p ctxt
 	    val f = Syntax.string_of_term (thy2ctxt thy) f
 in
-((p, Pbl), c, Form' (FormKF (~1, EdUndef, length p, Nundef, f)), pt)
+((p, Pbl), c, FormKF f, pt)
 end
 | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m')
 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
 let

changeset 59267	aab874fdd910
parent 59266	56762e8a672e
child 59268	c988bdecd7be