wneuper@59276
|
1 |
(* Title: generate specific entries into Ctree
|
wneuper@59276
|
2 |
Author: Walther Neuper
|
wneuper@59276
|
3 |
(c) due to copyright terms
|
wneuper@59276
|
4 |
*)
|
wneuper@59276
|
5 |
|
wneuper@59271
|
6 |
signature GENERATE_CALC_TREE =
|
wneuper@59276
|
7 |
sig
|
walther@59903
|
8 |
datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
|
wneuper@59268
|
9 |
datatype mout =
|
wneuper@59268
|
10 |
EmptyMout
|
wneuper@59268
|
11 |
| Error' of string
|
walther@59865
|
12 |
| FormKF of TermC.as_string
|
wneuper@59316
|
13 |
| PpcKF of pblmet * Model.item Model.ppc
|
walther@59939
|
14 |
| RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
|
walther@59931
|
15 |
|
walther@59931
|
16 |
type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree
|
walther@59931
|
17 |
|
walther@59939
|
18 |
val init_pbl: (string * (term * 'a)) list -> I_Model.T
|
walther@59939
|
19 |
val init_pbl': (string * (term * term)) list -> I_Model.T
|
walther@59931
|
20 |
val generate_inconsistent_rew: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
|
walther@59908
|
21 |
Pos.pos' -> Ctree.ctree -> Calc.T
|
wneuper@59310
|
22 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59931
|
23 |
val mout2str: mout -> string
|
walther@59886
|
24 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59908
|
25 |
(* NONE *)
|
walther@59886
|
26 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59266
|
27 |
end
|
neuper@37906
|
28 |
|
walther@59908
|
29 |
(**)
|
wneuper@59271
|
30 |
structure Generate(**): GENERATE_CALC_TREE(**) =
|
wneuper@59266
|
31 |
struct
|
walther@59908
|
32 |
(**)
|
wneuper@59276
|
33 |
open Ctree
|
walther@59695
|
34 |
open Pos
|
wneuper@59312
|
35 |
|
wneuper@59405
|
36 |
datatype pblmet = (*%^%*)
|
wneuper@59405
|
37 |
Upblmet (*undefined*)
|
walther@59903
|
38 |
| Problem of Problem.id (*%^%*)
|
walther@59903
|
39 |
| Method of Method.id; (*%^%*)
|
wneuper@59266
|
40 |
fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
|
walther@59903
|
41 |
| pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)
|
wneuper@59266
|
42 |
| pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
|
neuper@37906
|
43 |
|
neuper@37906
|
44 |
(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
|
neuper@37906
|
45 |
datatype foppFK = (* in DG cases div 2 *)
|
neuper@37906
|
46 |
EmptyFoppFK (*DG internal*)
|
walther@59865
|
47 |
| FormFK of TermC.as_string
|
walther@59865
|
48 |
| PpcFK of TermC.as_string Model.ppc
|
wneuper@59266
|
49 |
fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
|
wneuper@59316
|
50 |
| foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc
|
wneuper@59266
|
51 |
| foppFK2str EmptyFoppFK ="EmptyFoppFK"
|
neuper@37906
|
52 |
|
neuper@37906
|
53 |
datatype nest = Open | Closed | Nundef;
|
neuper@37906
|
54 |
fun nest2str Open = "Open"
|
neuper@37906
|
55 |
| nest2str Closed = "Closed"
|
wneuper@59266
|
56 |
| nest2str Nundef = "Nundef"
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
type indent = int;
|
neuper@37906
|
59 |
datatype edit = EdUndef | Write | Protect;
|
neuper@37906
|
60 |
(* bridge --> kernel *)
|
neuper@37906
|
61 |
(* bridge <-> kernel *)
|
neuper@37906
|
62 |
(* needed in dialog.sml *) (* bridge <-- kernel *)
|
neuper@37906
|
63 |
fun edit2str EdUndef = "EdUndef"
|
neuper@37906
|
64 |
| edit2str Write = "Write"
|
neuper@37906
|
65 |
| edit2str Protect = "Protect";
|
neuper@37906
|
66 |
|
neuper@42023
|
67 |
datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
|
wneuper@59405
|
68 |
Error_ of string (*<--*)
|
walther@59865
|
69 |
| FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*)
|
wneuper@59316
|
70 |
| PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
|
wneuper@59405
|
71 |
| RefineKF of Stool.match list (*<--*)
|
walther@59939
|
72 |
| RefinedKF of (Problem.id * ((I_Model.T) * ((bool * term) list))) (*<--*)
|
neuper@37906
|
73 |
|
walther@59931
|
74 |
(*
|
wneuper@59267
|
75 |
datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
|
wneuper@59267
|
76 |
*)
|
neuper@37906
|
77 |
datatype mout =
|
walther@59865
|
78 |
FormKF of TermC.as_string
|
wneuper@59316
|
79 |
| PpcKF of (pblmet * Model.item Model.ppc)
|
walther@59939
|
80 |
| RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
|
wneuper@59267
|
81 |
| Error' of string
|
wneuper@59267
|
82 |
| EmptyMout
|
neuper@37906
|
83 |
|
wneuper@59267
|
84 |
fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
|
wneuper@59316
|
85 |
| mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Model.itemppc2str itemppc ^ ")"
|
wneuper@59312
|
86 |
| mout2str (RefinedKF (_, _)) = "mout2str: RefinedKF not impl."
|
wneuper@59267
|
87 |
| mout2str (Error' str) = "Error' " ^ str
|
wneuper@59267
|
88 |
| mout2str (EmptyMout ) = "EmptyMout"
|
neuper@37906
|
89 |
|
walther@59931
|
90 |
type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree;
|
walther@59931
|
91 |
|
neuper@37906
|
92 |
(* init pbl with ...,dsc,empty | [] *)
|
neuper@37906
|
93 |
fun init_pbl pbt =
|
wneuper@59266
|
94 |
let
|
walther@59861
|
95 |
fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (TermC.empty, [])))
|
wneuper@59266
|
96 |
in map pbt2itm pbt end
|
wneuper@59266
|
97 |
|
wneuper@59266
|
98 |
(* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)
|
neuper@37906
|
99 |
fun init_pbl' pbt =
|
neuper@37906
|
100 |
let
|
walther@59861
|
101 |
fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (TermC.empty, [])))
|
wneuper@59266
|
102 |
in map pbt2itm pbt end
|
bonzai@41951
|
103 |
|
neuper@42437
|
104 |
fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
|
neuper@42434
|
105 |
let
|
wneuper@59266
|
106 |
val f = get_curr_formula (pt, pos)
|
wneuper@59266
|
107 |
val pos' as (p', _) = (lev_on p, Res)
|
wneuper@59266
|
108 |
val (pt, _) = case subs_opt of
|
walther@59828
|
109 |
NONE => cappend_atomic pt p' (is, ctxt) f
|
wneuper@59571
|
110 |
(Tactic.Rewrite thm') (f', []) Inconsistent
|
walther@59828
|
111 |
| SOME subs => cappend_atomic pt p' (is, ctxt) f
|
wneuper@59571
|
112 |
(Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent
|
wneuper@59266
|
113 |
val pt = update_branch pt p' TransitiveB
|
neuper@42437
|
114 |
in (pt, pos') end
|
neuper@42432
|
115 |
|
walther@59932
|
116 |
(**)end(**) |