src/Pure/Tools/am_interpreter.ML
changeset 23174 3913451b0418
parent 23173 51179ca0c429
child 23175 267ba70e7a9d
     1.1 --- a/src/Pure/Tools/am_interpreter.ML	Thu May 31 20:55:32 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,162 +0,0 @@
     1.4 -(*  Title:      Pure/Tools/am_interpreter.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Steven Obua
     1.7 -*)
     1.8 -
     1.9 -signature ABSTRACT_MACHINE =
    1.10 -sig
    1.11 -
    1.12 -datatype term = Var of int | Const of int | App of term * term | Abs of term
    1.13 -
    1.14 -datatype pattern = PVar | PConst of int * (pattern list)
    1.15 -
    1.16 -type program
    1.17 -
    1.18 -exception Compile of string;
    1.19 -val compile : (pattern * term) list -> program
    1.20 -
    1.21 -exception Run of string;
    1.22 -val run : program -> term -> term
    1.23 -
    1.24 -end
    1.25 -
    1.26 -structure AM_Interpreter : ABSTRACT_MACHINE = struct
    1.27 -
    1.28 -datatype term = Var of int | Const of int | App of term * term | Abs of term
    1.29 -
    1.30 -datatype pattern = PVar | PConst of int * (pattern list)
    1.31 -
    1.32 -datatype closure = CVar of int | CConst of int
    1.33 -                 | CApp of closure * closure | CAbs of closure
    1.34 -                 | Closure of (closure list) * closure
    1.35 -
    1.36 -structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
    1.37 -
    1.38 -datatype program = Program of ((pattern * closure) list) prog_struct.table
    1.39 -
    1.40 -datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
    1.41 -
    1.42 -exception Compile of string;
    1.43 -exception Run of string;
    1.44 -
    1.45 -fun clos_of_term (Var x) = CVar x
    1.46 -  | clos_of_term (Const c) = CConst c
    1.47 -  | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
    1.48 -  | clos_of_term (Abs u) = CAbs (clos_of_term u)
    1.49 -
    1.50 -fun term_of_clos (CVar x) = Var x
    1.51 -  | term_of_clos (CConst c) = Const c
    1.52 -  | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
    1.53 -  | term_of_clos (CAbs u) = Abs (term_of_clos u)
    1.54 -  | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
    1.55 -
    1.56 -fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
    1.57 -  | strip_closure args x = (x, args)
    1.58 -
    1.59 -fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
    1.60 -  | len_head_of_closure n x = (n, x)
    1.61 -
    1.62 -
    1.63 -(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
    1.64 -fun pattern_match args PVar clos = SOME (clos::args)
    1.65 -  | pattern_match args (PConst (c, patterns)) clos =
    1.66 -    let
    1.67 -        val (f, closargs) = strip_closure [] clos
    1.68 -    in
    1.69 -        case f of
    1.70 -            CConst d =>
    1.71 -            if c = d then
    1.72 -                pattern_match_list args patterns closargs
    1.73 -            else
    1.74 -                NONE
    1.75 -          | _ => NONE
    1.76 -    end
    1.77 -and pattern_match_list args [] [] = SOME args
    1.78 -  | pattern_match_list args (p::ps) (c::cs) =
    1.79 -    (case pattern_match args p c of
    1.80 -        NONE => NONE
    1.81 -      | SOME args => pattern_match_list args ps cs)
    1.82 -  | pattern_match_list _ _ _ = NONE
    1.83 -
    1.84 -(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
    1.85 -fun check_freevars free (Var x) = x < free
    1.86 -  | check_freevars free (Const c) = true
    1.87 -  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    1.88 -  | check_freevars free (Abs m) = check_freevars (free+1) m
    1.89 -
    1.90 -fun count_patternvars PVar = 1
    1.91 -  | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    1.92 -
    1.93 -fun pattern_key (PConst (c, ps)) = (c, length ps)
    1.94 -  | pattern_key _ = raise (Compile "pattern reduces to variable")
    1.95 -
    1.96 -fun compile eqs =
    1.97 -    let
    1.98 -        val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
    1.99 -                                     (pattern_key p, (p, clos_of_term r)))) eqs
   1.100 -    in
   1.101 -        Program (prog_struct.make (map (fn (k, a) => (k, [a])) eqs))
   1.102 -    end
   1.103 -
   1.104 -fun match_rules n [] clos = NONE
   1.105 -  | match_rules n ((p,eq)::rs) clos =
   1.106 -    case pattern_match [] p clos of
   1.107 -        NONE => match_rules (n+1) rs clos
   1.108 -      | SOME args => SOME (Closure (args, eq))
   1.109 -
   1.110 -fun match_closure (Program prog) clos =
   1.111 -    case len_head_of_closure 0 clos of
   1.112 -        (len, CConst c) =>
   1.113 -        (case prog_struct.lookup prog (c, len) of
   1.114 -            NONE => NONE
   1.115 -          | SOME rules => match_rules 0 rules clos)
   1.116 -      | _ => NONE
   1.117 -
   1.118 -fun lift n (c as (CConst _)) = c
   1.119 -  | lift n (v as CVar m) = if m < n then v else CVar (m+1)
   1.120 -  | lift n (CAbs t) = CAbs (lift (n+1) t)
   1.121 -  | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
   1.122 -  | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
   1.123 -and lift_env n e = map (lift n) e
   1.124 -
   1.125 -fun weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
   1.126 -  | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
   1.127 -  | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
   1.128 -  | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
   1.129 -  | weak prog stack clos =
   1.130 -    case match_closure prog clos of
   1.131 -        NONE => weak_last prog stack clos
   1.132 -      | SOME r => weak prog stack r
   1.133 -and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
   1.134 -  | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
   1.135 -  | weak_last prog stack c = (stack, c)
   1.136 -
   1.137 -fun strong prog stack (Closure (e, CAbs m)) =
   1.138 -    let
   1.139 -        val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
   1.140 -    in
   1.141 -        case stack' of
   1.142 -            SEmpty => strong prog (SAbs stack) wnf
   1.143 -          | _ => raise (Run "internal error in strong: weak failed")
   1.144 -    end
   1.145 -  | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
   1.146 -  | strong prog stack clos = strong_last prog stack clos
   1.147 -and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
   1.148 -  | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
   1.149 -  | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
   1.150 -  | strong_last prog stack clos = (stack, clos)
   1.151 -
   1.152 -fun run prog t =
   1.153 -    let
   1.154 -        val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
   1.155 -    in
   1.156 -        case stack of
   1.157 -            SEmpty => (case strong prog SEmpty wnf of
   1.158 -                           (SEmpty, snf) => term_of_clos snf
   1.159 -                         | _ => raise (Run "internal error in run: strong failed"))
   1.160 -          | _ => raise (Run "internal error in run: weak failed")
   1.161 -    end
   1.162 -
   1.163 -end
   1.164 -
   1.165 -structure AbstractMachine = AM_Interpreter