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