1open Theory Datatype Drule Thm Term Lib listTheory ratTheory; 2 3val types = ref ([] : hol_type list); 4 5fun DataType t def = 6let val _ = (Parse.Type t ; ()) handle _ => Hol_datatype def 7in 8 (types := Parse.Type t :: (!types)) 9end; 10 11fun AddType t = (types := Parse.Type t :: (!types)); 12 13val _ = new_theory "testTypes"; 14 15(*****************************************************************************) 16(* Simple Types *) 17(*****************************************************************************) 18 19val _ = DataType `:'a List` `List = LNil | LCons of 'a => List`; 20val _ = DataType `:'a Tree` `Tree = TLeaf of 'a | TBranch of Tree => Tree`; 21val _ = DataType `:'a Tre` `Tre = TNil | TNode of 'a => Tre => Tre`; 22val _ = DataType `:Label` `Label = L0 | L1 | L2 | L3 | L4`; 23val _ = DataType `:'a + 'b` `'a + 'b = Left of 'a | Right of 'b`; 24val _ = DataType `:unit` `unit = ()`; 25val _ = DataType `:'a BList` `BList = BL of unit + 'a # BList`; 26val _ = DataType `:'a CList` `CList = CLL of 'a # CList + unit`; 27val _ = DataType `:'a BTree` `BTree = BT of 'a + BTree # BTree`; 28 29(*****************************************************************************) 30(* Types using recursive functions for their nested recursion *) 31(*****************************************************************************) 32 33val _ = DataType `:'a RoseTree` `RoseTree = RTBranch of ('a # RoseTree) List`; 34val _ = DataType `:'a BRoseTree` 35 `BRoseTree = BRTBranch of ('a # BRoseTree) BList`; 36val _ = DataType `:RoseBush` `RoseBush = RBush of RoseBush RoseTree`; 37val _ = DataType `:BRoseBush` `BRoseBush = BBush of BRoseBush BRoseTree`; 38val _ = DataType `:Thicket` `Thicket = TStalk of Thicket Tre`; 39 40(*****************************************************************************) 41(* Connected single constructors *) 42(*****************************************************************************) 43 44val _ = DataType `:'a CS4` `CS4 = CS4C of 'a`; 45val _ = DataType `:'a CS3` `CS3 = CS3C of 'a CS4`; 46val _ = DataType `:'a CS2` `CS2 = CS2C of 'a CS3 => 'a CS4`; 47val _ = DataType `:'a CS1` `CS1 = CS1C of 'a CS2 => 'a CS4`; 48 49 50val _ = DataType `:'a DListL` 51 `DListL = DLR of DListR ; DListR = DLRNil | DLRCons of 'a => DListL`; 52(* val _ = DataType `:'a DLTree` 53 `DLTree = DLBranch of ('a # DLTree DListR)` --> Fails!! *) 54val _ = DataType `:'a CSList` `CSList = CSNil | CSCons of 'a => CSList CS1`; 55 56(*****************************************************************************) 57(* Types with products as sub-types, since products are used heavily *) 58(*****************************************************************************) 59 60val _ = DataType `:NumProdList` 61 `NumProdList = NPLNull | NPLCons of num # num => NumProdList`; 62 63val _ = DataType `:UncurriedNPL` 64 `UncurriedNPL = UNPLNull | 65 UNPLCons of num # num # UncurriedNPL`; 66 67(*****************************************************************************) 68(* Previous types from earlier incarnations *) 69(*****************************************************************************) 70 71val _ = DataType `:('a,'b) test1` `test1 = Pair of 'a # 'b`; 72val _ = DataType `:('a,'b)test2` `test2 = Curry of 'a => 'b`; 73val _ = DataType `:('a,'b,'c) test2b` `test2b = Curry3 of 'a => 'b => 'c`; 74val _ = DataType `:('a,'b,'c) test2c` `test2c = Curry2 of 'a => 'b # 'c`; 75val _ = DataType `:('a,'b) test3` `test3 = Sum1 of 'a | Sum2 of 'b`; 76val _ = DataType `:test4` `test4 = Recursive of test4 | End`; 77val _ = DataType `:test5` `test5 = RecursiveList of test5 list | EndList`; 78val _ = DataType `:test6` 79 `test6 = DoubleList of test6 list => test6 list | EndD`; 80val _ = DataType `:'a test7` `test7 = Node of test7 # test7 | Leaf of 'a`; 81val _ = DataType `:test8` `test8 = Double of test8 test7 # test8 list | End8`; 82val _ = DataType `:test9l` 83 `test9l = R9 of test9r | EndL ; test9r = L9 of test9l | EndR`; 84val _ = DataType `:testA` 85 `testA = <| Reg1 : num; Reg2 : num; Waiting : bool |>`; 86val _ = DataType `:testBa` 87 `testBa = Aa of num | Ba of testBb | Ca of testBc ; 88 testBb = Bb of int | Ab of testBa | Cb of testBc ; 89 testBc = Cc of rat | Bc of testBb | Ac of testBa`; 90val _ = DataType `:('a,'b) testCR` 91 `testCR = CR of ('a # testCL) list ; 92 testCL = CL of ('b # testCR) list`; 93val _ = DataType `:testDX` 94 `testDX = dL of testDZ => testDY | DeL ; 95 testDY = dR of testDX ; testDZ = dRec of testDX`; 96val _ = DataType `:testEX` 97 `testEX = eL of testEZ => testEY | EeL ; 98 testEY = eR of testEZ => testEX | EeR ; 99 testEZ = twoRec of testEX => testEY`; 100val _ = DataType `:('a,'b) testFX` 101 `testFX = fL of testFZ => testFY | FeL ; 102 testFY = fR of testFZ => testFX | FeR ; 103 testFZ = fRec of testFX => 'a => 'b => testFY`; 104val _ = DataType `:('a,'b) state_out` 105 `state_out = <| state : 'a; out : 'b |>`; 106val _ = DataType `:register` 107`register = 108 r0 | r1 | r2 | r3 | r4 | r5 | r6 | r7 | 109 r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | 110 r8_fiq | r9_fiq | r10_fiq | r11_fiq | r12_fiq | r13_fiq | r14_fiq | 111 r13_irq | r14_irq | 112 r13_svc | r14_svc | 113 r13_abt | r14_abt | 114 r13_und | r14_und`; 115val _ = DataType `:psr` 116 `psr = CPSR | SPSR_fiq | SPSR_irq | SPSR_svc | SPSR_abt | SPSR_und`; 117val _ = DataType `:exceptions` 118 `exceptions = reset | undefined | software | pabort | 119 dabort | address |interrupt | fast`; 120val _ = DataType `:('a,'b,'c) sumpair` `sumpair = Lsp of 'a | Rsp of 'b => 'c`; 121val _ = DataType `:'a my_tree` 122 `my_tree = Branch of ('a,my_tree,my_tree) sumpair`; 123 124(*****************************************************************************) 125(* Red-Black trees *) 126(*****************************************************************************) 127 128val _ = DataType `colour = R | B`; 129val _ = DataType `tree = LEAF | NODE of colour => num => tree => tree`; 130 131(*****************************************************************************) 132(* Some examples from src/datatype/jrh.test *) 133(*****************************************************************************) 134 135val _ = DataType `:One` `One = Single_contructor`; 136 137val _ = DataType 138 `:('A,'B) Term` 139 `Term = Var of 'A => 'B 140 | App of bool => Termlist; 141 Termlist = Emp 142 | Consp of Term => Termlist`; 143 144val _ = DataType 145 `:('A,'B) Btree` 146 `Btree = Lf of 'A 147 | Nd of 'B => Btree => Btree`;; 148 149val _ = DataType 150 `:Express` 151 `Command = Assign of num => Express 152 | If of Express => Command 153 | Ite of Express => Command => Command 154 | While of Express => Command 155 | Do of Command => Express; 156 157 Express = Constant of num 158 | Variable of num 159 | Summ of Express => Express 160 | Product of Express => Express`; 161 162val _ = AddType `:Command`; 163 164val _ = DataType 165 `:pat` 166 `atexp = Varb of num 167 | Let of dec => exp; 168 169 exp = Exp1 of atexp 170 | Exp2 of exp => atexp 171 | Exp3 of match; 172 173 match = Match1 of rule 174 | Matches of rule => match; 175 176 rule = Rule of pat => exp; 177 dec = Val of valbind 178 | Local of dec => dec 179 | Decs of dec => dec; 180 181 valbind = Single of pat => exp 182 | Multi of pat => exp => valbind 183 | Rec of valbind; 184 185 pat = Wild 186 | Varpat of num`; 187 188val _ = AddType `:atexp`; 189 190val _ = DataType 191 `:tri` 192 `tri = ONE | TWO | THREE`; 193 194val _ = DataType 195 `:Steve0` 196 `Steve0 = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | 197 X11 | X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | 198 X21 | X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | 199 X31 | X32 | X33 | X34`;; 200 201val _ = DataType 202 `:('A,'B,'C) TY1` 203 `TY1 = NoF__ 204 | Fk__ of 'A => TY2; 205 206 TY2 = Ta__ of bool 207 | Td__ of bool 208 | Tf__ of TY1 209 | Tk__ of bool 210 | Tp__ of bool 211 | App__ of 'A => TY1 => TY2 => TY3 212 | Pair__ of TY2 => TY2; 213 214 TY3 = NoS__ 215 | Fresh__ of TY2 216 | Trustworthy__ of 'A 217 | PrivateKey__ of 'A => 'B => 'C 218 | PublicKey__ of 'A => 'B => 'C 219 | Conveyed__ of 'A => TY2 220 | Possesses__ of 'A => TY2 221 | Received__ of 'A => TY2 222 | Recognizes__ of 'A => TY2 223 | Sends__ of 'A => TY2 => 'B 224 | SharedSecret__ of 'A => TY2 => 'B 225 | Believes__ of 'A => TY3 226 | And__ of TY3 => TY3 227 | NeverMalFromSelf__ of 'A => 'B => TY2`;; 228 229(*****************************************************************************) 230(* Example from Myra: part of the syntax of SML. *) 231(*****************************************************************************) 232 233val _ = DataType 234 `:String` 235 `String = EMPTY_STRING 236 | CONS_STRING of num => String`; 237 238val _ = DataType 239 `:strid` 240 `strid = STRID of String; 241 var = VAR of String; 242 con = CON of String; 243 scon = SCINT of num (* was int *) 244 | SCSTR of String; 245 excon = EXCON of String; 246 label = LABEL of String`;; 247 248val _ = AddType `:var`; 249val _ = AddType `:con`; 250val _ = AddType `:scon`; 251val _ = AddType `:excon`; 252 253val _ = DataType 254 `:'A nonemptylist` 255 `nonemptylist = Head_and_tail of 'A => 'A list`;; 256 257val _ = DataType 258 `:'A long` 259 `long = BASE of 'A | QUALIFIED of strid => long`;; 260 261val _ = DataType 262 `:'a option` 263 `option = SOME of 'a | NONE`; 264 265val _ = DataType 266 `:atpat_e` 267 `atpat_e = WILDCARDatpat_e 268 | SCONatpat_e of scon 269 | VARatpat_e of var 270 | CONatpat_e of con long 271 | EXCONatpat_e of excon long 272 | RECORDatpat_e of patrow_e option 273 | PARatpat_e of pat_e; 274 275 patrow_e = DOTDOTDOT_e 276 | PATROW_e of num => pat_e => patrow_e option; 277 278 pat_e = ATPATpat_e of atpat_e 279 | CONpat_e of con long => atpat_e 280 | EXCONpat_e of excon long => atpat_e 281 | LAYEREDpat_e of var => pat_e; 282 283 conbind_e = CONBIND_e of con => conbind_e option; 284 285 datbind_e = DATBIND_e of conbind_e => datbind_e option; 286 287 exbind_e = EXBIND1_e of excon => exbind_e option 288 | EXBIND2_e of excon => excon long => exbind_e option; 289 290 atexp_e = SCONatexp_e of scon 291 | VARatexp_e of var long 292 | CONatexp_e of con long 293 | EXCONatexp_e of excon long 294 | RECORDatexp_e of exprow_e option 295 | LETatexp_e of dec_e => exp_e 296 | PARatexp_e of exp_e; 297 298 exprow_e = EXPROW_e of num => exp_e => exprow_e option; 299 300 exp_e = ATEXPexp_e of atexp_e 301 | APPexp_e of exp_e => atexp_e 302 | HANDLEexp_e of exp_e => match_e 303 | RAISEexp_e of exp_e 304 | FNexp_e of match_e; 305 306 match_e = MATCH_e of mrule_e => match_e option; 307 308 mrule_e = MRULE_e of pat_e => exp_e; 309 310 dec_e = VALdec_e of valbind_e 311 | DATATYPEdec_e of datbind_e 312 | ABSTYPEdec_e of datbind_e => dec_e 313 | EXCEPTdec_e of exbind_e 314 | LOCALdec_e of dec_e => dec_e 315 | OPENdec_e of (strid long) nonemptylist 316 | EMPTYdec_e 317 | SEQdec_e of dec_e => dec_e; 318 319 valbind_e = PLAINvalbind_e of pat_e => exp_e => valbind_e option 320 | RECvalbind_e of valbind_e`;; 321 322val _ = save_thm("LIST",LIST_CONJ (map (REFL o curry mk_var "a") 323 (rev (!types)))); 324 325val _ = export_theory(); 326