1 (* Title: generate specific entries into Ctree
3 (c) due to copyright terms
6 signature GENERATE_CALC_TREE =
8 datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
12 | FormKF of TermC.as_string
13 | PpcKF of pblmet * Model.item Model.ppc
14 | RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
16 type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree
18 val init_pbl: (string * (term * 'a)) list -> I_Model.T
19 val init_pbl': (string * (term * term)) list -> I_Model.T
20 val generate_inconsistent_rew: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
21 Pos.pos' -> Ctree.ctree -> Calc.T
22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
23 val mout2str: mout -> string
24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
26 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30 structure Generate(**): GENERATE_CALC_TREE(**) =
36 datatype pblmet = (*%^%*)
38 | Problem of Problem.id (*%^%*)
39 | Method of Method.id; (*%^%*)
40 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
41 | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)
42 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
44 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
45 datatype foppFK = (* in DG cases div 2 *)
46 EmptyFoppFK (*DG internal*)
47 | FormFK of TermC.as_string
48 | PpcFK of TermC.as_string Model.ppc
49 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
50 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc
51 | foppFK2str EmptyFoppFK ="EmptyFoppFK"
53 datatype nest = Open | Closed | Nundef;
54 fun nest2str Open = "Open"
55 | nest2str Closed = "Closed"
56 | nest2str Nundef = "Nundef"
59 datatype edit = EdUndef | Write | Protect;
60 (* bridge --> kernel *)
61 (* bridge <-> kernel *)
62 (* needed in dialog.sml *) (* bridge <-- kernel *)
63 fun edit2str EdUndef = "EdUndef"
64 | edit2str Write = "Write"
65 | edit2str Protect = "Protect";
67 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
68 Error_ of string (*<--*)
69 | FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*)
70 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
71 | RefineKF of Stool.match list (*<--*)
72 | RefinedKF of (Problem.id * ((I_Model.T) * ((bool * term) list))) (*<--*)
75 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
78 FormKF of TermC.as_string
79 | PpcKF of (pblmet * Model.item Model.ppc)
80 | RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
84 fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
85 | mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Model.itemppc2str itemppc ^ ")"
86 | mout2str (RefinedKF (_, _)) = "mout2str: RefinedKF not impl."
87 | mout2str (Error' str) = "Error' " ^ str
88 | mout2str (EmptyMout ) = "EmptyMout"
90 type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree;
92 (* init pbl with ...,dsc,empty | [] *)
95 fun pbt2itm (f, (d, _)) = (0, [], false, f, I_Model.Inc ((d, []), (TermC.empty, [])))
96 in map pbt2itm pbt end
98 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
101 fun pbt2itm (f, (d, t)) = (0, [], false, f, I_Model.Inc((d, [t]), (TermC.empty, [])))
102 in map pbt2itm pbt end
104 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
106 val f = get_curr_formula (pt, pos)
107 val pos' as (p', _) = (lev_on p, Res)
108 val (pt, _) = case subs_opt of
109 NONE => cappend_atomic pt p' (is, ctxt) f
110 (Tactic.Rewrite thm') (f', []) Inconsistent
111 | SOME subs => cappend_atomic pt p' (is, ctxt) f
112 (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent
113 val pt = update_branch pt p' TransitiveB