1(*---------------------------------------------------------------------------* 2 * This example defines the abstract syntax for a simple ML-like language, * 3 * and a simple mutually-recursive function for computing the variables * 4 * in a program. It exercises the type definition package on a mutually * 5 * recursive concrete type. * 6 * * 7 * The example is also a demonstration of how Holmake works. Just invoke * 8 * * 9 * Holmake * 10 * * 11 * and wait. When Holmake is done, a compiled theory corresponding to this * 12 * file is found in MLSyntaxTheory.u{i,o}. It can be loaded into an * 13 * interactive session by * 14 * * 15 * load "MLTheory"; * 16 * * 17 * Loading the theory can take a little while - about 5 seconds on my * 18 * machine. * 19 * * 20 * If you are working interactively, i.e., you don't want to pay any * 21 * attention to this Holmake stuff, do the following: * 22 * * 23 app load ["bossLib", "stringTheory", "setTheory"]; 24 * * 25 * and then proceed with cut-and-paste. * 26 * * 27 * * 28 * * 29 * GRAMMAR * 30 * --------- * 31 * * 32 * atexp ::= <var> * 33 * | "let" <dec> "in" <exp> "end" * 34 * * 35 * exp ::= <atexp> * 36 * | <exp> <atexp> * 37 * | "fn" <match> * 38 * * 39 * match ::= <rule> * 40 * | <rule> "|" <match> * 41 * * 42 * rule ::= <pat> "=>" <exp> * 43 * * 44 * dec ::= "val" <valbind> * 45 * | "local" <dec> "in" <dec> "end" * 46 * | <dec> ";" <dec> * 47 * * 48 * valbind ::= <pat> "=" <exp> * 49 * | <pat> "=" <exp> "and" <valbind> * 50 * | "valrec" <valbind> * 51 * * 52 * pat ::= "_" (* wildcard *) * 53 * | <var> * 54 * * 55 *---------------------------------------------------------------------------*) 56 57 58open bossLib Theory Parse ; 59 60local open stringTheory pred_setTheory (* Make strings and sets be present *) 61in end; 62 63val _ = new_theory "ML"; 64 65 66(*--------------------------------------------------------------------------- 67 Define the type of variables. 68 ---------------------------------------------------------------------------*) 69 70val _ = Datatype `var = VAR string`; 71 72 73(*--------------------------------------------------------------------------- 74 Define the datatype of ML syntax trees. 75 ---------------------------------------------------------------------------*) 76 77val _ = Datatype 78 `atexp = var_exp var 79 | let_exp dec exp ; 80 81 exp = aexp atexp 82 | app_exp exp atexp 83 | fn_exp match ; 84 85 match = match rule 86 | matchl rule match ; 87 88 rule = rule pat exp ; 89 90 dec = val_dec valbind 91 | local_dec dec dec 92 | seq_dec dec dec ; 93 94 valbind = bind pat exp 95 | bindl pat exp valbind 96 | rec_bind valbind ; 97 98 pat = wild_pat 99 | var_pat var`; 100 101 102(*--------------------------------------------------------------------------- 103 A simple collection of functions for finding the variables 104 in a program. 105 ----------------------------------------------------------------------------*) 106 107val Vars_def = 108 Define 109 `(atexpV (var_exp v) = {v}) /\ 110 (atexpV (let_exp d e) = (decV d) UNION (expV e)) 111 /\ 112 (expV (aexp a) = atexpV a) /\ 113 (expV (app_exp e a) = (expV e) UNION (atexpV a)) /\ 114 (expV (fn_exp m) = matchV m) 115 /\ 116 (matchV (match r) = ruleV r) /\ 117 (matchV (matchl r mrst) = (ruleV r) UNION (matchV mrst)) 118 /\ 119 (ruleV (rule p e) = (patV p) UNION (expV e)) 120 /\ 121 (decV (val_dec b) = valbindV b) /\ 122 (decV (local_dec d1 d2) = (decV d1) UNION (decV d2)) /\ 123 (decV (seq_dec d1 d2) = (decV d1) UNION (decV d2)) 124 /\ 125 (valbindV (bind p e) = (patV p) UNION (expV e)) /\ 126 (valbindV (bindl p e vb) = (patV p) UNION (expV e) UNION (valbindV vb)) /\ 127 (valbindV (rec_bind vb) = (valbindV vb)) 128 /\ 129 (patV wild_pat = {}) /\ 130 (patV (var_pat v) = {v})`; 131 132val _ = export_theory(); 133