src/Tools/Compute_Oracle/am.ML

--- a/src/Tools/Compute_Oracle/am.ML	Sat Oct 27 18:37:06 2007 +0200
+++ b/src/Tools/Compute_Oracle/am.ML	Sat Oct 27 18:37:32 2007 +0200
@@ -1,7 +1,7 @@
 signature ABSTRACT_MACHINE =
 sig
 
-datatype term = Var of int | Const of int | App of term * term | Abs of term
+datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term
 
 datatype pattern = PVar | PConst of int * (pattern list)
 
@@ -20,12 +20,19 @@
 exception Run of string;
 val run : program -> term -> term
 
+(* Utilities *)
+
+val check_freevars : int -> term -> bool
+val forall_consts : (int -> bool) -> term -> bool
+val closed : term -> bool
+val erase_Computed : term -> term
+
 end
 
 structure AbstractMachine : ABSTRACT_MACHINE = 
 struct
 
-datatype term = Var of int | Const of int | App of term * term | Abs of term
+datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term
 
 datatype pattern = PVar | PConst of int * (pattern list)
 
@@ -35,6 +42,28 @@
 
 exception Compile of string;
 
+fun erase_Computed (Computed t) = erase_Computed t
+  | erase_Computed (App (t1, t2)) = App (erase_Computed t1, erase_Computed t2)
+  | erase_Computed (Abs t) = Abs (erase_Computed t)
+  | erase_Computed t = t
+
+(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
+  check_freevars 0 t iff t is closed*)
+fun check_freevars free (Var x) = x < free
+  | check_freevars free (Const c) = true
+  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
+  | check_freevars free (Abs m) = check_freevars (free+1) m
+  | check_freevars free (Computed t) = check_freevars free t
+
+fun forall_consts pred (Const c) = pred c
+  | forall_consts pred (Var x) = true
+  | forall_consts pred (App (u,v)) = forall_consts pred u 
+				     andalso forall_consts pred v
+  | forall_consts pred (Abs m) = forall_consts pred m
+  | forall_consts pred (Computed t) = forall_consts pred t
+
+fun closed t = check_freevars 0 t
+
 fun compile _ = raise Compile "abstract machine stub"
 
 fun discard _ = raise Compile "abstract machine stub"