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