src/Tools/Compute_Oracle/am.ML
author wenzelm
Fri, 02 Oct 2009 22:15:08 +0200
changeset 32861 105f40051387
parent 25520 e123c81257a5
child 32960 69916a850301
permissions -rw-r--r--
eliminated dead code;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     1
signature ABSTRACT_MACHINE =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     2
sig
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     3
25217
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
     4
datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     5
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     6
datatype pattern = PVar | PConst of int * (pattern list)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     7
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     8
datatype guard = Guard of term * term
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     9
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    10
type program
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    11
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    12
exception Compile of string;
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    13
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    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,
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    15
   1 to the second last, and so on. *)
25520
e123c81257a5 improvements
obua
parents: 25217
diff changeset
    16
val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    17
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    18
val discard : program -> unit
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    19
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    20
exception Run of string;
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    21
val run : program -> term -> term
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    22
25217
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    23
(* Utilities *)
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    24
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    25
val check_freevars : int -> term -> bool
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    26
val forall_consts : (int -> bool) -> term -> bool
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    27
val closed : term -> bool
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    28
val erase_Computed : term -> term
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    29
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    30
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    31
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    32
structure AbstractMachine : ABSTRACT_MACHINE = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    33
struct
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    34
25217
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    35
datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    36
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    37
datatype pattern = PVar | PConst of int * (pattern list)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    38
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    39
datatype guard = Guard of term * term
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    40
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    41
type program = unit
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    42
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    43
exception Compile of string;
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    44
25217
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    45
fun erase_Computed (Computed t) = erase_Computed t
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    46
  | erase_Computed (App (t1, t2)) = App (erase_Computed t1, erase_Computed t2)
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    47
  | erase_Computed (Abs t) = Abs (erase_Computed t)
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    48
  | erase_Computed t = t
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    49
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    50
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    51
  check_freevars 0 t iff t is closed*)
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    52
fun check_freevars free (Var x) = x < free
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    53
  | check_freevars free (Const c) = true
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    54
  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    55
  | check_freevars free (Abs m) = check_freevars (free+1) m
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    56
  | check_freevars free (Computed t) = check_freevars free t
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    57
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    58
fun forall_consts pred (Const c) = pred c
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    59
  | forall_consts pred (Var x) = true
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    60
  | forall_consts pred (App (u,v)) = forall_consts pred u 
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    61
				     andalso forall_consts pred v
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    62
  | forall_consts pred (Abs m) = forall_consts pred m
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    63
  | forall_consts pred (Computed t) = forall_consts pred t
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    64
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    65
fun closed t = check_freevars 0 t
3224db6415ae better compute oracle
obua
parents: 23663
diff changeset
    66
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    67
fun compile _ = raise Compile "abstract machine stub"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    68
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    69
fun discard _ = raise Compile "abstract machine stub"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    70
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    71
exception Run of string;
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    72
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    73
fun run p t = raise Run "abstract machine stub"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    74
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    75
end