author | Walther Neuper <walther.neuper@jku.at> |
Wed, 03 Feb 2021 16:39:44 +0100 | |
changeset 60154 | 2ab0d1523731 |
parent 60111 | 2e996663e5a7 |
child 60223 | 740ebee5948b |
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@59963 | 16 |
| RefinedKF of Problem.id * (I_Model.T * 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@59310 | 20 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
walther@59959 | 21 |
(* NONE *) |
walther@59886 | 22 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
walther@59908 | 23 |
(* NONE *) |
walther@59886 | 24 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
wneuper@59266 | 25 |
end |
neuper@37906 | 26 |
|
walther@59959 | 27 |
(**) (*Generate*) |
walther@59959 | 28 |
structure Test_Out(**): TEST_OUTPUT(**) = |
wneuper@59266 | 29 |
struct |
walther@59908 | 30 |
(**) |
wneuper@59276 | 31 |
open Ctree |
walther@59695 | 32 |
open Pos |
wneuper@59312 | 33 |
|
walther@59959 | 34 |
datatype pblmet = |
walther@59959 | 35 |
Upblmet |
walther@59959 | 36 |
| Problem of Problem.id |
walther@60154 | 37 |
| MethodC of MethodC.id; |
wneuper@59266 | 38 |
fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*) |
walther@60154 | 39 |
| pblmet2str (MethodC metID) = "MethodC " ^ MethodC.id_to_string metID (*%^%*) |
walther@59962 | 40 |
| pblmet2str x = raise ERROR ("pblmet2str: uncovered definition " ^ pblmet2str x) |
neuper@37906 | 41 |
|
neuper@37906 | 42 |
(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) |
neuper@37906 | 43 |
datatype foppFK = (* in DG cases div 2 *) |
neuper@37906 | 44 |
EmptyFoppFK (*DG internal*) |
walther@59865 | 45 |
| FormFK of TermC.as_string |
walther@59959 | 46 |
| PpcFK of TermC.as_string P_Model.ppc |
neuper@37906 | 47 |
|
neuper@37906 | 48 |
datatype nest = Open | Closed | Nundef; |
neuper@37906 | 49 |
|
neuper@37906 | 50 |
type indent = int; |
neuper@37906 | 51 |
datatype edit = EdUndef | Write | Protect; |
neuper@37906 | 52 |
|
neuper@42023 | 53 |
datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*) |
wneuper@59405 | 54 |
Error_ of string (*<--*) |
walther@59865 | 55 |
| FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*) |
walther@59969 | 56 |
| PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.T) (*<--*) |
walther@59984 | 57 |
| RefineKF of M_Match.T list (*<--*) |
walther@59963 | 58 |
| RefinedKF of (Problem.id * ((I_Model.T) * (Pre_Conds.T))) (*<--*) |
neuper@37906 | 59 |
|
neuper@37906 | 60 |
datatype mout = |
walther@59865 | 61 |
FormKF of TermC.as_string |
walther@59969 | 62 |
| PpcKF of (pblmet * P_Model.T) |
walther@59963 | 63 |
| RefinedKF of Problem.id * (I_Model.T * Pre_Conds.T) |
wneuper@59267 | 64 |
| Error' of string |
wneuper@59267 | 65 |
| EmptyMout |
neuper@37906 | 66 |
|
wneuper@59267 | 67 |
fun mout2str (FormKF cterm') = "FormKF " ^ cterm' |
walther@59997 | 68 |
| mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ ", " ^ P_Model.to_string itemppc ^ ")" |
wneuper@59312 | 69 |
| mout2str (RefinedKF (_, _)) = "mout2str: RefinedKF not impl." |
wneuper@59267 | 70 |
| mout2str (Error' str) = "Error' " ^ str |
wneuper@59267 | 71 |
| mout2str (EmptyMout ) = "EmptyMout" |
neuper@37906 | 72 |
|
walther@59959 | 73 |
type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree; |
neuper@42432 | 74 |
|
walther@59932 | 75 |
(**)end(**) |