src/Tools/Compute_Oracle/am_interpreter.ML
author obua
Thu, 20 Sep 2007 12:10:23 +0200
changeset 24654 329f1b4d9d16
parent 24584 01e83ffa6c54
child 25217 3224db6415ae
permissions -rw-r--r--
improved computing
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 23663
diff changeset
     1
(*  Title:      Tools/Compute_Oracle/am_interpreter.ML
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     3
    Author:     Steven Obua
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     4
*)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     5
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
     6
signature AM_BARRAS = 
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
     7
sig
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
     8
  include ABSTRACT_MACHINE
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
     9
  val max_reductions : int option ref
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    10
end
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    11
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    12
structure AM_Interpreter : AM_BARRAS = struct
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    13
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    14
open AbstractMachine;
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    15
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    16
datatype closure = CDummy | CVar of int | CConst of int
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    17
                 | CApp of closure * closure | CAbs of closure
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    18
                 | Closure of (closure list) * closure
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    19
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    20
structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    21
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    22
datatype program = Program of ((pattern * closure) list) prog_struct.table
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    23
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    24
datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    25
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    26
fun clos_of_term (Var x) = CVar x
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    27
  | clos_of_term (Const c) = CConst c
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    28
  | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    29
  | clos_of_term (Abs u) = CAbs (clos_of_term u)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    30
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    31
fun term_of_clos (CVar x) = Var x
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    32
  | term_of_clos (CConst c) = Const c
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    33
  | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    34
  | term_of_clos (CAbs u) = Abs (term_of_clos u)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    35
  | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    36
  | term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found")
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    37
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    38
fun resolve_closure closures (CVar x) = (case List.nth (closures, x) of CDummy => CVar x | r => r)
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    39
  | resolve_closure closures (CConst c) = CConst c
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    40
  | resolve_closure closures (CApp (u, v)) = CApp (resolve_closure closures u, resolve_closure closures v)
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    41
  | resolve_closure closures (CAbs u) = CAbs (resolve_closure (CDummy::closures) u)
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    42
  | resolve_closure closures (CDummy) = raise (Run "internal error: resolve_closure applied to CDummy")
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    43
  | resolve_closure closures (Closure (e, u)) = resolve_closure e u
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    44
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    45
fun resolve_closure' c = resolve_closure [] c
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    46
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    47
fun resolve_stack tm SEmpty = tm
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    48
  | resolve_stack tm (SAppL (c, s)) = resolve_stack (CApp (tm, resolve_closure' c)) s
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    49
  | resolve_stack tm (SAppR (c, s)) = resolve_stack (CApp (resolve_closure' c, tm)) s
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    50
  | resolve_stack tm (SAbs s) = resolve_stack (CAbs tm) s
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    51
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    52
fun resolve (stack, closure) = 
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    53
    let
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    54
	val _ = writeln "start resolving"
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    55
	val t =	resolve_stack (resolve_closure' closure) stack
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    56
	val _ = writeln "finished resolving"
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    57
    in
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    58
	t
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    59
    end
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
    60
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    61
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    62
  | strip_closure args x = (x, args)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    63
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    64
fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    65
  | len_head_of_closure n x = (n, x)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    66
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    67
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    68
(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    69
fun pattern_match args PVar clos = SOME (clos::args)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    70
  | pattern_match args (PConst (c, patterns)) clos =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    71
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    72
        val (f, closargs) = strip_closure [] clos
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    73
    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    74
        case f of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    75
            CConst d =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    76
            if c = d then
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    77
                pattern_match_list args patterns closargs
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    78
            else
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    79
                NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    80
          | _ => NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    81
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    82
and pattern_match_list args [] [] = SOME args
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    83
  | pattern_match_list args (p::ps) (c::cs) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    84
    (case pattern_match args p c of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    85
        NONE => NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    86
      | SOME args => pattern_match_list args ps cs)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    87
  | pattern_match_list _ _ _ = NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    88
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    89
fun count_patternvars PVar = 1
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    90
  | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    91
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    92
fun pattern_key (PConst (c, ps)) = (c, length ps)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    93
  | pattern_key _ = raise (Compile "pattern reduces to variable")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    94
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    95
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    96
  check_freevars 0 t iff t is closed*)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    97
fun check_freevars free (Var x) = x < free
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    98
  | check_freevars free (Const c) = true
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
    99
  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   100
  | check_freevars free (Abs m) = check_freevars (free+1) m
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   101
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   102
fun compile eqs =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   103
    let
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   104
	val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   105
	val eqs = map (fn (a,b,c) => (b,c)) eqs
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   106
	fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule") 
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   107
        val eqs = map (fn (p, r) => (check (p,r); (pattern_key p, (p, clos_of_term r)))) eqs
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   108
	fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a] | SOME l => a::l) table
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   109
	val p = fold merge eqs prog_struct.empty 
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   110
    in
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   111
        Program p
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   112
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   113
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   114
fun match_rules n [] clos = NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   115
  | match_rules n ((p,eq)::rs) clos =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   116
    case pattern_match [] p clos of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   117
        NONE => match_rules (n+1) rs clos
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   118
      | SOME args => SOME (Closure (args, eq))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   119
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   120
fun match_closure (Program prog) clos =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   121
    case len_head_of_closure 0 clos of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   122
        (len, CConst c) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   123
        (case prog_struct.lookup prog (c, len) of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   124
            NONE => NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   125
          | SOME rules => match_rules 0 rules clos)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   126
      | _ => NONE
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   127
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   128
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   129
type state = bool * program * stack * closure
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   130
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   131
datatype loopstate = Continue of state | Stop of stack * closure
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   132
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   133
fun proj_C (Continue s) = s
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   134
  | proj_C _ = raise Match
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   135
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   136
exception InterruptedExecution of stack * closure
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   137
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   138
fun proj_S (Stop s) = s
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   139
  | proj_S (Continue (_,_,s,c)) = (s,c)
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   140
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   141
fun cont (Continue _) = true
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   142
  | cont _ = false
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   143
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   144
val max_reductions = ref (NONE : int option)
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   145
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   146
fun do_reduction reduce p =
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   147
    let
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   148
	val s = ref (Continue p)
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   149
	val counter = ref 0
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   150
	val _ = case !max_reductions of 
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   151
		    NONE => while cont (!s) do (s := reduce (proj_C (!s)))
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   152
		  | SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1)
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   153
    in
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   154
	case !max_reductions of
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   155
	    SOME m => if !counter >= m then raise InterruptedExecution (proj_S (!s)) else proj_S (!s)
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   156
	  | NONE => proj_S (!s)
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   157
    end
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   158
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   159
fun weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   160
  | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   161
  | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   162
  | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   163
  | weak_reduce (false, prog, stack, clos) =
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   164
    (case match_closure prog clos of
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   165
         NONE => Continue (true, prog, stack, clos)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   166
       | SOME r => Continue (false, prog, stack, r))
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   167
  | weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   168
  | weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   169
  | weak_reduce (true, prog, stack, c) = Stop (stack, c)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   170
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   171
fun strong_reduce (false, prog, stack, Closure (e, CAbs m)) =
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   172
    (let
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   173
         val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m))
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   174
     in
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   175
         case stack' of
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   176
             SEmpty => Continue (false, prog, SAbs stack, wnf)
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   177
           | _ => raise (Run "internal error in strong: weak failed")
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   178
     end handle InterruptedExecution state => raise InterruptedExecution (stack, resolve state))
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   179
  | strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   180
  | strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   181
  | strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   182
  | strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   183
  | strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b))
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   184
  | strong_reduce (true, prog, stack, clos) = Stop (stack, clos)
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   185
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   186
fun run prog t =
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   187
    (let
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   188
         val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t))
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   189
     in
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   190
         case stack of
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   191
             SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   192
                            (SEmpty, snf) => term_of_clos snf
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   193
                          | _ => raise (Run "internal error in run: strong failed"))
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   194
           | _ => raise (Run "internal error in run: weak failed")
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   195
     end handle InterruptedExecution state => term_of_clos (resolve state))
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   196
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   197
fun discard p = ()
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   198
23663
84b5c89b8b49 new version of computing oracle
obua
parents: 23174
diff changeset
   199
end