src/Pure/Tools/am_interpreter.ML
author wenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14)
changeset 16842 5979c46853d1
parent 16782 b214f21ae396
child 17412 e26cb20ef0cc
permissions -rw-r--r--
tuned;
obua@16781
     1
(*  Title:      Pure/Tools/am_interpreter.ML
obua@16781
     2
    ID:         $Id$
obua@16781
     3
    Author:     Steven Obua
obua@16781
     4
*)
obua@16781
     5
wenzelm@16842
     6
signature ABSTRACT_MACHINE =
wenzelm@16842
     7
sig
wenzelm@16842
     8
obua@16781
     9
datatype term = Var of int | Const of int | App of term * term | Abs of term
obua@16781
    10
obua@16781
    11
datatype pattern = PVar | PConst of int * (pattern list)
obua@16781
    12
obua@16781
    13
type program
obua@16781
    14
obua@16781
    15
exception Compile of string;
obua@16781
    16
val compile : (pattern * term) list -> program
wenzelm@16842
    17
obua@16781
    18
exception Run of string;
obua@16781
    19
val run : program -> term -> term
obua@16781
    20
obua@16781
    21
end
obua@16781
    22
obua@16781
    23
structure AM_Interpreter :> ABSTRACT_MACHINE = struct
obua@16781
    24
obua@16781
    25
datatype term = Var of int | Const of int | App of term * term | Abs of term
obua@16781
    26
obua@16781
    27
datatype pattern = PVar | PConst of int * (pattern list)
obua@16781
    28
obua@16781
    29
datatype closure = CVar of int | CConst of int
wenzelm@16842
    30
                 | CApp of closure * closure | CAbs of closure
wenzelm@16842
    31
                 | Closure of (closure list) * closure
obua@16781
    32
obua@16782
    33
structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
obua@16781
    34
obua@16782
    35
type program = ((pattern * closure) list) prog_struct.table
obua@16781
    36
obua@16781
    37
datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
obua@16781
    38
obua@16781
    39
exception Compile of string;
obua@16781
    40
exception Run of string;
obua@16781
    41
obua@16781
    42
fun clos_of_term (Var x) = CVar x
obua@16781
    43
  | clos_of_term (Const c) = CConst c
obua@16781
    44
  | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
obua@16781
    45
  | clos_of_term (Abs u) = CAbs (clos_of_term u)
obua@16781
    46
obua@16781
    47
fun term_of_clos (CVar x) = Var x
obua@16781
    48
  | term_of_clos (CConst c) = Const c
obua@16781
    49
  | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
obua@16781
    50
  | term_of_clos (CAbs u) = Abs (term_of_clos u)
obua@16781
    51
  | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
obua@16781
    52
obua@16781
    53
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
obua@16781
    54
  | strip_closure args x = (x, args)
obua@16781
    55
obua@16781
    56
fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
obua@16781
    57
  | len_head_of_closure n x = (n, x)
obua@16781
    58
obua@16781
    59
obua@16781
    60
(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
obua@16781
    61
fun pattern_match args PVar clos = SOME (clos::args)
wenzelm@16842
    62
  | pattern_match args (PConst (c, patterns)) clos =
obua@16781
    63
    let
wenzelm@16842
    64
        val (f, closargs) = strip_closure [] clos
obua@16781
    65
    in
wenzelm@16842
    66
        case f of
wenzelm@16842
    67
            CConst d =>
wenzelm@16842
    68
            if c = d then
wenzelm@16842
    69
                pattern_match_list args patterns closargs
wenzelm@16842
    70
            else
wenzelm@16842
    71
                NONE
wenzelm@16842
    72
          | _ => NONE
obua@16781
    73
    end
obua@16781
    74
and pattern_match_list args [] [] = SOME args
wenzelm@16842
    75
  | pattern_match_list args (p::ps) (c::cs) =
obua@16781
    76
    (case pattern_match args p c of
wenzelm@16842
    77
        NONE => NONE
obua@16781
    78
      | SOME args => pattern_match_list args ps cs)
obua@16781
    79
  | pattern_match_list _ _ _ = NONE
obua@16781
    80
obua@16781
    81
(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
obua@16781
    82
fun check_freevars free (Var x) = x < free
obua@16781
    83
  | check_freevars free (Const c) = true
obua@16781
    84
  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
obua@16781
    85
  | check_freevars free (Abs m) = check_freevars (free+1) m
obua@16781
    86
obua@16781
    87
fun count_patternvars PVar = 1
obua@16781
    88
  | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
obua@16781
    89
obua@16781
    90
fun pattern_key (PConst (c, ps)) = (c, length ps)
obua@16781
    91
  | pattern_key _ = raise (Compile "pattern reduces to variable")
obua@16781
    92
wenzelm@16842
    93
fun compile eqs =
obua@16781
    94
    let
wenzelm@16842
    95
        val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
wenzelm@16842
    96
                                     (pattern_key p, (p, clos_of_term r)))) eqs
obua@16781
    97
    in
wenzelm@16842
    98
        prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
wenzelm@16842
    99
    end
obua@16781
   100
obua@16781
   101
fun match_rules n [] clos = NONE
obua@16781
   102
  | match_rules n ((p,eq)::rs) clos =
obua@16781
   103
    case pattern_match [] p clos of
wenzelm@16842
   104
        NONE => match_rules (n+1) rs clos
obua@16781
   105
      | SOME args => SOME (Closure (args, eq))
obua@16781
   106
wenzelm@16842
   107
fun match_closure prog clos =
obua@16781
   108
    case len_head_of_closure 0 clos of
wenzelm@16842
   109
        (len, CConst c) =>
wenzelm@16842
   110
        (case prog_struct.lookup (prog, (c, len)) of
wenzelm@16842
   111
            NONE => NONE
wenzelm@16842
   112
          | SOME rules => match_rules 0 rules clos)
obua@16781
   113
      | _ => NONE
obua@16781
   114
obua@16781
   115
fun lift n (c as (CConst _)) = c
obua@16781
   116
  | lift n (v as CVar m) = if m < n then v else CVar (m+1)
obua@16781
   117
  | lift n (CAbs t) = CAbs (lift (n+1) t)
obua@16781
   118
  | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
obua@16781
   119
  | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
obua@16781
   120
and lift_env n e = map (lift n) e
obua@16781
   121
obua@16781
   122
fun weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
obua@16781
   123
  | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
obua@16781
   124
  | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
obua@16781
   125
  | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
wenzelm@16842
   126
  | weak prog stack clos =
obua@16781
   127
    case match_closure prog clos of
wenzelm@16842
   128
        NONE => weak_last prog stack clos
obua@16781
   129
      | SOME r => weak prog stack r
obua@16781
   130
and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
obua@16781
   131
  | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
wenzelm@16842
   132
  | weak_last prog stack c = (stack, c)
obua@16781
   133
wenzelm@16842
   134
fun strong prog stack (Closure (e, CAbs m)) =
obua@16781
   135
    let
wenzelm@16842
   136
        val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
obua@16781
   137
    in
wenzelm@16842
   138
        case stack' of
wenzelm@16842
   139
            SEmpty => strong prog (SAbs stack) wnf
wenzelm@16842
   140
          | _ => raise (Run "internal error in strong: weak failed")
obua@16781
   141
    end
obua@16781
   142
  | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
obua@16781
   143
  | strong prog stack clos = strong_last prog stack clos
obua@16781
   144
and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
obua@16781
   145
  | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
obua@16781
   146
  | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
obua@16781
   147
  | strong_last prog stack clos = (stack, clos)
obua@16781
   148
wenzelm@16842
   149
fun run prog t =
obua@16781
   150
    let
wenzelm@16842
   151
        val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
obua@16781
   152
    in
wenzelm@16842
   153
        case stack of
wenzelm@16842
   154
            SEmpty => (case strong prog SEmpty wnf of
wenzelm@16842
   155
                           (SEmpty, snf) => term_of_clos snf
wenzelm@16842
   156
                         | _ => raise (Run "internal error in run: strong failed"))
wenzelm@16842
   157
          | _ => raise (Run "internal error in run: weak failed")
obua@16781
   158
    end
wenzelm@16842
   159
obua@16781
   160
end
obua@16781
   161
obua@16781
   162
structure AbstractMachine = AM_Interpreter