1 2open HolKernel Parse boolLib bossLib; 3open arithmeticTheory listTheory pairTheory finite_mapTheory stringTheory; 4open source_valuesTheory; 5 6val _ = new_theory "source_syntax"; 7 8 9(* abstract syntax *) 10 11Type name = ���:num��� 12 13Datatype: 14 op = Add | Sub | Div | Cons | Head | Tail | Read | Write 15End 16 17Datatype: 18 test = Less | Equal 19End 20 21Datatype: 22 exp = Const num (* constant number *) 23 | Var name (* local variable *) 24 | Op op (exp list) (* primitive operations *) 25 | If test (exp list) exp exp (* if test .. then .. else .. *) 26 | Let name exp exp (* let name = .. in .. *) 27 | Call name (exp list) (* call a function *) 28End 29 30Datatype: 31 dec = Defun name (name list) exp (* func name, formal params, body *) 32End 33 34Datatype: (* a complete program is a list of *) 35 prog = Program (dec list) exp (* function declarations followed by *) 36End (* an expression to evaluate *) 37 38 39val _ = export_theory(); 40