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 deBruijn 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 .. (free1) 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
