src/Pure/Tools/am_compiler.ML
changeset 16842 5979c46853d1
parent 16782 b214f21ae396
child 17795 5b18c3343028
     1.1 --- a/src/Pure/Tools/am_compiler.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/Tools/am_compiler.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -5,14 +5,14 @@
     1.4  
     1.5  signature COMPILING_AM = 
     1.6  sig
     1.7 -    include ABSTRACT_MACHINE
     1.8 +  include ABSTRACT_MACHINE
     1.9  
    1.10 -    datatype closure = CVar of int | CConst of int
    1.11 -		     | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
    1.12 +  datatype closure = CVar of int | CConst of int
    1.13 +    | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
    1.14  
    1.15 -    val set_compiled_rewriter : (term -> closure) -> unit
    1.16 -    val list_nth : 'a list * int -> 'a
    1.17 -    val list_map : ('a -> 'b) -> 'a list -> 'b list
    1.18 +  val set_compiled_rewriter : (term -> closure) -> unit
    1.19 +  val list_nth : 'a list * int -> 'a
    1.20 +  val list_map : ('a -> 'b) -> 'a list -> 'b list
    1.21  end
    1.22  
    1.23  structure AM_Compiler :> COMPILING_AM = struct
    1.24 @@ -25,7 +25,8 @@
    1.25  datatype pattern = PVar | PConst of int * (pattern list)
    1.26  
    1.27  datatype closure = CVar of int | CConst of int
    1.28 -		 | CApp of closure * closure | CAbs of closure | 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  val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
    1.33  
    1.34 @@ -47,19 +48,22 @@
    1.35    | term_of_clos (CConst c) = Const c
    1.36    | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
    1.37    | term_of_clos (CAbs u) = Abs (term_of_clos u)
    1.38 -  | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
    1.39 +  | term_of_clos (Closure (e, u)) =
    1.40 +      raise (Run "internal error: closure in normalized term found")
    1.41  
    1.42  fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
    1.43    | strip_closure args x = (x, args)
    1.44  
    1.45 -(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
    1.46 +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
    1.47 +  check_freevars 0 t iff t is closed*)
    1.48  fun check_freevars free (Var x) = x < free
    1.49    | check_freevars free (Const c) = true
    1.50    | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    1.51    | check_freevars free (Abs m) = check_freevars (free+1) m
    1.52  
    1.53  fun count_patternvars PVar = 1
    1.54 -  | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    1.55 +  | count_patternvars (PConst (_, ps)) =
    1.56 +      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    1.57  
    1.58  fun print_rule (p, t) = 
    1.59      let	
    1.60 @@ -81,17 +85,22 @@
    1.61  	    end
    1.62  
    1.63  	val (n, pattern) = print_pattern 0 p
    1.64 -	val pattern = if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")" else pattern
    1.65 +	val pattern =
    1.66 +            if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")"
    1.67 +            else pattern
    1.68  	
    1.69 -	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) "Var "^(str x)
    1.70 -	  | print_term d (Const c) = "c"^(str c)
    1.71 -	  | print_term d (App (a,b)) = "App ("^(print_term d a)^", "^(print_term d b)^")"
    1.72 -	  | print_term d (Abs c) = "Abs ("^(print_term (d+1) c)^")"
    1.73 +	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
    1.74 +              "Var " ^ str x
    1.75 +	  | print_term d (Const c) = "c" ^ str c
    1.76 +	  | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
    1.77 +	  | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
    1.78  
    1.79  	fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))
    1.80  
    1.81  	val term = print_term 0 t
    1.82 -	val term = if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")" else "Closure ([], "^term^")"
    1.83 +	val term =
    1.84 +            if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
    1.85 +            else "Closure ([], "^term^")"
    1.86  			   
    1.87      in
    1.88  	"lookup stack "^pattern^" = weak stack ("^term^")"
    1.89 @@ -104,7 +113,7 @@
    1.90    | remove_dups [] = []
    1.91  
    1.92  fun constants_of PVar = []
    1.93 -  | constants_of (PConst (c, ps)) = c::(List.concat (map constants_of ps))
    1.94 +  | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
    1.95  
    1.96  fun constants_of_term (Var _) = []
    1.97    | constants_of_term (Abs m) = constants_of_term m
    1.98 @@ -113,6 +122,7 @@
    1.99      
   1.100  fun load_rules sname name prog = 
   1.101      let
   1.102 +        (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
   1.103  	val buffer = ref ""
   1.104  	fun write s = (buffer := (!buffer)^s)
   1.105  	fun writeln s = (write s; write "\n")
   1.106 @@ -210,11 +220,9 @@
   1.107  	    in
   1.108  		()
   1.109  	    end
   1.110 -	    
   1.111 -	val dummy = (fn s => ())		    
   1.112      in
   1.113  	compiled_rewriter := NONE;	
   1.114 -	use_text (dummy, dummy) false (!buffer);
   1.115 +	use_text (K (), K ()) false (!buffer);
   1.116  	case !compiled_rewriter of 
   1.117  	    NONE => raise (Compile "cannot communicate with compiled function")
   1.118  	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))