1 signature ABSTRACT_MACHINE = |
|
2 sig |
|
3 |
|
4 datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term |
|
5 |
|
6 datatype pattern = PVar | PConst of int * (pattern list) |
|
7 |
|
8 datatype guard = Guard of term * term |
|
9 |
|
10 type program |
|
11 |
|
12 exception Compile of string; |
|
13 |
|
14 (* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right, |
|
15 1 to the second last, and so on. *) |
|
16 val compile : (guard list * pattern * term) list -> program |
|
17 |
|
18 exception Run of string; |
|
19 val run : program -> term -> term |
|
20 |
|
21 (* Utilities *) |
|
22 |
|
23 val check_freevars : int -> term -> bool |
|
24 val forall_consts : (int -> bool) -> term -> bool |
|
25 val closed : term -> bool |
|
26 val erase_Computed : term -> term |
|
27 |
|
28 end |
|
29 |
|
30 structure AbstractMachine : ABSTRACT_MACHINE = |
|
31 struct |
|
32 |
|
33 datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term |
|
34 |
|
35 datatype pattern = PVar | PConst of int * (pattern list) |
|
36 |
|
37 datatype guard = Guard of term * term |
|
38 |
|
39 type program = unit |
|
40 |
|
41 exception Compile of string; |
|
42 |
|
43 fun erase_Computed (Computed t) = erase_Computed t |
|
44 | erase_Computed (App (t1, t2)) = App (erase_Computed t1, erase_Computed t2) |
|
45 | erase_Computed (Abs t) = Abs (erase_Computed t) |
|
46 | erase_Computed t = t |
|
47 |
|
48 (*Returns true iff at most 0 .. (free-1) occur unbound. therefore |
|
49 check_freevars 0 t iff t is closed*) |
|
50 fun check_freevars free (Var x) = x < free |
|
51 | check_freevars free (Const _) = true |
|
52 | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v |
|
53 | check_freevars free (Abs m) = check_freevars (free+1) m |
|
54 | check_freevars free (Computed t) = check_freevars free t |
|
55 |
|
56 fun forall_consts pred (Const c) = pred c |
|
57 | forall_consts pred (Var _) = true |
|
58 | forall_consts pred (App (u,v)) = forall_consts pred u |
|
59 andalso forall_consts pred v |
|
60 | forall_consts pred (Abs m) = forall_consts pred m |
|
61 | forall_consts pred (Computed t) = forall_consts pred t |
|
62 |
|
63 fun closed t = check_freevars 0 t |
|
64 |
|
65 fun compile _ = raise Compile "abstract machine stub" |
|
66 |
|
67 exception Run of string; |
|
68 |
|
69 fun run _ _ = raise Run "abstract machine stub" |
|
70 |
|
71 end |
|