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))