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