23663
|
1 |
signature ABSTRACT_MACHINE =
|
|
2 |
sig
|
|
3 |
|
25217
|
4 |
datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term
|
23663
|
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. *)
|
25520
|
16 |
val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
|
23663
|
17 |
|
|
18 |
val discard : program -> unit
|
|
19 |
|
|
20 |
exception Run of string;
|
|
21 |
val run : program -> term -> term
|
|
22 |
|
25217
|
23 |
(* Utilities *)
|
|
24 |
|
|
25 |
val check_freevars : int -> term -> bool
|
|
26 |
val forall_consts : (int -> bool) -> term -> bool
|
|
27 |
val closed : term -> bool
|
|
28 |
val erase_Computed : term -> term
|
|
29 |
|
23663
|
30 |
end
|
|
31 |
|
|
32 |
structure AbstractMachine : ABSTRACT_MACHINE =
|
|
33 |
struct
|
|
34 |
|
25217
|
35 |
datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term
|
23663
|
36 |
|
|
37 |
datatype pattern = PVar | PConst of int * (pattern list)
|
|
38 |
|
|
39 |
datatype guard = Guard of term * term
|
|
40 |
|
|
41 |
type program = unit
|
|
42 |
|
|
43 |
exception Compile of string;
|
|
44 |
|
25217
|
45 |
fun erase_Computed (Computed t) = erase_Computed t
|
|
46 |
| erase_Computed (App (t1, t2)) = App (erase_Computed t1, erase_Computed t2)
|
|
47 |
| erase_Computed (Abs t) = Abs (erase_Computed t)
|
|
48 |
| erase_Computed t = t
|
|
49 |
|
|
50 |
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
|
|
51 |
check_freevars 0 t iff t is closed*)
|
|
52 |
fun check_freevars free (Var x) = x < free
|
|
53 |
| check_freevars free (Const c) = true
|
|
54 |
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
|
|
55 |
| check_freevars free (Abs m) = check_freevars (free+1) m
|
|
56 |
| check_freevars free (Computed t) = check_freevars free t
|
|
57 |
|
|
58 |
fun forall_consts pred (Const c) = pred c
|
|
59 |
| forall_consts pred (Var x) = true
|
|
60 |
| forall_consts pred (App (u,v)) = forall_consts pred u
|
|
61 |
andalso forall_consts pred v
|
|
62 |
| forall_consts pred (Abs m) = forall_consts pred m
|
|
63 |
| forall_consts pred (Computed t) = forall_consts pred t
|
|
64 |
|
|
65 |
fun closed t = check_freevars 0 t
|
|
66 |
|
23663
|
67 |
fun compile _ = raise Compile "abstract machine stub"
|
|
68 |
|
|
69 |
fun discard _ = raise Compile "abstract machine stub"
|
|
70 |
|
|
71 |
exception Run of string;
|
|
72 |
|
|
73 |
fun run p t = raise Run "abstract machine stub"
|
|
74 |
|
|
75 |
end
|