author | wneuper <Walther.Neuper@jku.at> |
Sun, 10 Dec 2023 07:56:02 +0100 | |
changeset 60776 | c2e6848d3dce |
parent 60586 | 007ef64dbb08 |
child 60782 | e797d1bdfe37 |
permissions | -rw-r--r-- |
wneuper@59276 | 1 |
(* Title: generate specific entries into Ctree |
wneuper@59276 | 2 |
Author: Walther Neuper |
wneuper@59276 | 3 |
(c) due to copyright terms |
walther@59959 | 4 |
|
walther@60111 | 5 |
This will be dropped at switch to Isabelle/PIDE . |
wneuper@59276 | 6 |
*) |
wneuper@59276 | 7 |
|
walther@59959 | 8 |
signature TEST_OUTPUT = |
wneuper@59276 | 9 |
sig |
walther@60154 | 10 |
datatype pblmet = MethodC of MethodC.id | Problem of Problem.id | Upblmet |
wneuper@59268 | 11 |
datatype mout = |
wneuper@59268 | 12 |
EmptyMout |
wneuper@59268 | 13 |
| Error' of string |
walther@59865 | 14 |
| FormKF of TermC.as_string |
walther@59969 | 15 |
| PpcKF of pblmet * P_Model.T |
Walther@60776 | 16 |
| RefinedKF of Problem.id * (I_Model.T_POS * Pre_Conds.T) |
walther@59931 | 17 |
|
walther@59959 | 18 |
type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree |
walther@59959 | 19 |
val mout2str: mout -> string |
wneuper@59266 | 20 |
end |
neuper@37906 | 21 |
|
walther@59959 | 22 |
(**) (*Generate*) |
walther@59959 | 23 |
structure Test_Out(**): TEST_OUTPUT(**) = |
wneuper@59266 | 24 |
struct |
walther@59908 | 25 |
(**) |
wneuper@59276 | 26 |
open Ctree |
walther@59695 | 27 |
open Pos |
wneuper@59312 | 28 |
|
walther@59959 | 29 |
datatype pblmet = |
walther@59959 | 30 |
Upblmet |
walther@59959 | 31 |
| Problem of Problem.id |
walther@60154 | 32 |
| MethodC of MethodC.id; |
wneuper@59266 | 33 |
fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*) |
walther@60154 | 34 |
| pblmet2str (MethodC metID) = "MethodC " ^ MethodC.id_to_string metID (*%^%*) |
walther@59962 | 35 |
| pblmet2str x = raise ERROR ("pblmet2str: uncovered definition " ^ pblmet2str x) |
neuper@37906 | 36 |
|
neuper@37906 | 37 |
(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) |
neuper@37906 | 38 |
datatype foppFK = (* in DG cases div 2 *) |
neuper@37906 | 39 |
EmptyFoppFK (*DG internal*) |
walther@59865 | 40 |
| FormFK of TermC.as_string |
Walther@60586 | 41 |
| PpcFK of TermC.as_string P_Model.model |
neuper@37906 | 42 |
|
neuper@37906 | 43 |
datatype nest = Open | Closed | Nundef; |
neuper@37906 | 44 |
|
neuper@37906 | 45 |
type indent = int; |
neuper@37906 | 46 |
datatype edit = EdUndef | Write | Protect; |
neuper@37906 | 47 |
|
neuper@42023 | 48 |
datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*) |
wneuper@59405 | 49 |
Error_ of string (*<--*) |
walther@59865 | 50 |
| FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*) |
walther@59969 | 51 |
| PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.T) (*<--*) |
walther@59984 | 52 |
| RefineKF of M_Match.T list (*<--*) |
Walther@60776 | 53 |
| RefinedKF of (Problem.id * ((I_Model.T_POS) * (Pre_Conds.T))) (*<--*) |
neuper@37906 | 54 |
|
neuper@37906 | 55 |
datatype mout = |
walther@59865 | 56 |
FormKF of TermC.as_string |
walther@59969 | 57 |
| PpcKF of (pblmet * P_Model.T) |
Walther@60776 | 58 |
| RefinedKF of Problem.id * (I_Model.T_POS * Pre_Conds.T) |
wneuper@59267 | 59 |
| Error' of string |
wneuper@59267 | 60 |
| EmptyMout |
neuper@37906 | 61 |
|
wneuper@59267 | 62 |
fun mout2str (FormKF cterm') = "FormKF " ^ cterm' |
walther@59997 | 63 |
| mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ ", " ^ P_Model.to_string itemppc ^ ")" |
wneuper@59312 | 64 |
| mout2str (RefinedKF (_, _)) = "mout2str: RefinedKF not impl." |
wneuper@59267 | 65 |
| mout2str (Error' str) = "Error' " ^ str |
wneuper@59267 | 66 |
| mout2str (EmptyMout ) = "EmptyMout" |
neuper@37906 | 67 |
|
walther@59959 | 68 |
type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree; |
neuper@42432 | 69 |
|
walther@59932 | 70 |
(**)end(**) |