src/Pure/Tools/am_interpreter.ML
changeset 16842 5979c46853d1
parent 16782 b214f21ae396
child 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/Tools/am_interpreter.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/Tools/am_interpreter.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -3,7 +3,9 @@
     1.4      Author:     Steven Obua
     1.5  *)
     1.6  
     1.7 -signature ABSTRACT_MACHINE = sig							     
     1.8 +signature ABSTRACT_MACHINE =
     1.9 +sig
    1.10 +
    1.11  datatype term = Var of int | Const of int | App of term * term | Abs of term
    1.12  
    1.13  datatype pattern = PVar | PConst of int * (pattern list)
    1.14 @@ -12,7 +14,7 @@
    1.15  
    1.16  exception Compile of string;
    1.17  val compile : (pattern * term) list -> program
    1.18 - 
    1.19 +
    1.20  exception Run of string;
    1.21  val run : program -> term -> term
    1.22  
    1.23 @@ -25,8 +27,8 @@
    1.24  datatype pattern = PVar | PConst of int * (pattern list)
    1.25  
    1.26  datatype closure = CVar of int | CConst of int
    1.27 -		 | CApp of closure * closure | CAbs of closure 
    1.28 -		 | Closure of (closure list) * closure 
    1.29 +                 | CApp of closure * closure | CAbs of closure
    1.30 +                 | Closure of (closure list) * closure
    1.31  
    1.32  structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
    1.33  
    1.34 @@ -57,22 +59,22 @@
    1.35  
    1.36  (* earlier occurrence of PVar corresponds to higher de Bruijn index *)
    1.37  fun pattern_match args PVar clos = SOME (clos::args)
    1.38 -  | pattern_match args (PConst (c, patterns)) clos = 
    1.39 +  | pattern_match args (PConst (c, patterns)) clos =
    1.40      let
    1.41 -	val (f, closargs) = strip_closure [] clos
    1.42 +        val (f, closargs) = strip_closure [] clos
    1.43      in
    1.44 -	case f of 
    1.45 -	    CConst d => 
    1.46 -	    if c = d then 
    1.47 -		pattern_match_list args patterns closargs
    1.48 -	    else 
    1.49 -		NONE
    1.50 -	  | _ => NONE
    1.51 +        case f of
    1.52 +            CConst d =>
    1.53 +            if c = d then
    1.54 +                pattern_match_list args patterns closargs
    1.55 +            else
    1.56 +                NONE
    1.57 +          | _ => NONE
    1.58      end
    1.59  and pattern_match_list args [] [] = SOME args
    1.60 -  | pattern_match_list args (p::ps) (c::cs) = 
    1.61 +  | pattern_match_list args (p::ps) (c::cs) =
    1.62      (case pattern_match args p c of
    1.63 -	NONE => NONE
    1.64 +        NONE => NONE
    1.65        | SOME args => pattern_match_list args ps cs)
    1.66    | pattern_match_list _ _ _ = NONE
    1.67  
    1.68 @@ -88,26 +90,26 @@
    1.69  fun pattern_key (PConst (c, ps)) = (c, length ps)
    1.70    | pattern_key _ = raise (Compile "pattern reduces to variable")
    1.71  
    1.72 -fun compile eqs = 
    1.73 +fun compile eqs =
    1.74      let
    1.75 -	val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r; 
    1.76 -				     (pattern_key p, (p, clos_of_term r)))) eqs
    1.77 +        val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
    1.78 +                                     (pattern_key p, (p, clos_of_term r)))) eqs
    1.79      in
    1.80 -	prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
    1.81 -    end	
    1.82 +        prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
    1.83 +    end
    1.84  
    1.85  fun match_rules n [] clos = NONE
    1.86    | match_rules n ((p,eq)::rs) clos =
    1.87      case pattern_match [] p clos of
    1.88 -	NONE => match_rules (n+1) rs clos
    1.89 +        NONE => match_rules (n+1) rs clos
    1.90        | SOME args => SOME (Closure (args, eq))
    1.91  
    1.92 -fun match_closure prog clos = 
    1.93 +fun match_closure prog clos =
    1.94      case len_head_of_closure 0 clos of
    1.95 -	(len, CConst c) =>
    1.96 -	(case prog_struct.lookup (prog, (c, len)) of
    1.97 -	    NONE => NONE
    1.98 -	  | SOME rules => match_rules 0 rules clos)
    1.99 +        (len, CConst c) =>
   1.100 +        (case prog_struct.lookup (prog, (c, len)) of
   1.101 +            NONE => NONE
   1.102 +          | SOME rules => match_rules 0 rules clos)
   1.103        | _ => NONE
   1.104  
   1.105  fun lift n (c as (CConst _)) = c
   1.106 @@ -121,21 +123,21 @@
   1.107    | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
   1.108    | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
   1.109    | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
   1.110 -  | weak prog stack clos =    
   1.111 +  | weak prog stack clos =
   1.112      case match_closure prog clos of
   1.113 -	NONE => weak_last prog stack clos
   1.114 +        NONE => weak_last prog stack clos
   1.115        | SOME r => weak prog stack r
   1.116  and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
   1.117    | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
   1.118 -  | weak_last prog stack c = (stack, c) 
   1.119 +  | weak_last prog stack c = (stack, c)
   1.120  
   1.121 -fun strong prog stack (Closure (e, CAbs m)) = 
   1.122 +fun strong prog stack (Closure (e, CAbs m)) =
   1.123      let
   1.124 -	val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
   1.125 +        val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
   1.126      in
   1.127 -	case stack' of
   1.128 -	    SEmpty => strong prog (SAbs stack) wnf
   1.129 -	  | _ => raise (Run "internal error in strong: weak failed")
   1.130 +        case stack' of
   1.131 +            SEmpty => strong prog (SAbs stack) wnf
   1.132 +          | _ => raise (Run "internal error in strong: weak failed")
   1.133      end
   1.134    | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
   1.135    | strong prog stack clos = strong_last prog stack clos
   1.136 @@ -144,17 +146,17 @@
   1.137    | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
   1.138    | strong_last prog stack clos = (stack, clos)
   1.139  
   1.140 -fun run prog t = 
   1.141 +fun run prog t =
   1.142      let
   1.143 -	val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
   1.144 +        val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
   1.145      in
   1.146 -	case stack of 
   1.147 -	    SEmpty => (case strong prog SEmpty wnf of
   1.148 -			   (SEmpty, snf) => term_of_clos snf
   1.149 -			 | _ => raise (Run "internal error in run: strong failed"))
   1.150 -	  | _ => raise (Run "internal error in run: weak failed")
   1.151 +        case stack of
   1.152 +            SEmpty => (case strong prog SEmpty wnf of
   1.153 +                           (SEmpty, snf) => term_of_clos snf
   1.154 +                         | _ => raise (Run "internal error in run: strong failed"))
   1.155 +          | _ => raise (Run "internal error in run: weak failed")
   1.156      end
   1.157 -	  
   1.158 +
   1.159  end
   1.160  
   1.161  structure AbstractMachine = AM_Interpreter