author | wenzelm |
Sun, 13 Mar 2011 19:27:39 +0100 | |
changeset 41953 | 994d088fbfbc |
parent 41952 | c7297638599b |
child 41959 | b460124855b8 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Tools/Compute_Oracle/am_ghc.ML |
23663 | 2 |
Author: Steven Obua |
3 |
*) |
|
4 |
||
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
5 |
structure AM_GHC : ABSTRACT_MACHINE = |
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
6 |
struct |
23663 | 7 |
|
8 |
open AbstractMachine; |
|
9 |
||
10 |
type program = string * string * (int Inttab.table) |
|
11 |
||
12 |
fun count_patternvars PVar = 1 |
|
13 |
| count_patternvars (PConst (_, ps)) = |
|
14 |
List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps |
|
15 |
||
16 |
fun update_arity arity code a = |
|
17 |
(case Inttab.lookup arity code of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
18 |
NONE => Inttab.update_new (code, a) arity |
24134
6e69e0031f34
added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents:
23663
diff
changeset
|
19 |
| SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity) |
23663 | 20 |
|
21 |
(* We have to find out the maximal arity of each constant *) |
|
22 |
fun collect_pattern_arity PVar arity = arity |
|
23 |
| collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args)) |
|
24 |
||
25 |
local |
|
26 |
fun collect applevel (Var _) arity = arity |
|
27 |
| collect applevel (Const c) arity = update_arity arity c applevel |
|
28 |
| collect applevel (Abs m) arity = collect 0 m arity |
|
29 |
| collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity) |
|
30 |
in |
|
31 |
fun collect_term_arity t arity = collect 0 t arity |
|
32 |
end |
|
33 |
||
34 |
fun nlift level n (Var m) = if m < level then Var m else Var (m+n) |
|
35 |
| nlift level n (Const c) = Const c |
|
36 |
| nlift level n (App (a,b)) = App (nlift level n a, nlift level n b) |
|
37 |
| nlift level n (Abs b) = Abs (nlift (level+1) n b) |
|
38 |
||
39 |
fun rep n x = if n = 0 then [] else x::(rep (n-1) x) |
|
40 |
||
41 |
fun adjust_rules rules = |
|
42 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
43 |
val arity = fold (fn (p, t) => fn arity => collect_term_arity t (collect_pattern_arity p arity)) rules Inttab.empty |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
44 |
fun arity_of c = the (Inttab.lookup arity c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
45 |
fun adjust_pattern PVar = PVar |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
46 |
| adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
47 |
fun adjust_rule (PVar, t) = raise Compile ("pattern may not be a variable") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
48 |
| adjust_rule (rule as (p as PConst (c, args),t)) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
49 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
50 |
val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
51 |
val args = map adjust_pattern args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
52 |
val len = length args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
53 |
val arity = arity_of c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
54 |
fun lift level n (Var m) = if m < level then Var m else Var (m+n) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
55 |
| lift level n (Const c) = Const c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
56 |
| lift level n (App (a,b)) = App (lift level n a, lift level n b) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
57 |
| lift level n (Abs b) = Abs (lift (level+1) n b) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
58 |
val lift = lift 0 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
59 |
fun adjust_term n t = if n=0 then t else adjust_term (n-1) (App (t, Var (n-1))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
60 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
61 |
if len = arity then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
62 |
rule |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
63 |
else if arity >= len then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
64 |
(PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) (lift (arity-len) t)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
65 |
else (raise Compile "internal error in adjust_rule") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
66 |
end |
23663 | 67 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
68 |
(arity, map adjust_rule rules) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
69 |
end |
23663 | 70 |
|
71 |
fun print_term arity_of n = |
|
72 |
let |
|
73 |
fun str x = string_of_int x |
|
74 |
fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
75 |
|
23663 | 76 |
fun print_apps d f [] = f |
77 |
| print_apps d f (a::args) = print_apps d ("app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args |
|
78 |
and print_call d (App (a, b)) args = print_call d a (b::args) |
|
79 |
| print_call d (Const c) args = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
80 |
(case arity_of c of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
81 |
NONE => print_apps d ("Const "^(str c)) args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
82 |
| SOME a => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
83 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
84 |
val len = length args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
85 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
86 |
if a <= len then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
87 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
88 |
val s = "c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a)))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
89 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
90 |
print_apps d s (List.drop (args, a)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
91 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
92 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
93 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
94 |
fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n-1))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
95 |
fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
96 |
fun append_args [] t = t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
97 |
| append_args (c::cs) t = append_args cs (App (t, c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
98 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
99 |
print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c))))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
100 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
101 |
end) |
23663 | 102 |
| print_call d t args = print_apps d (print_term d t) args |
103 |
and print_term d (Var x) = if x < d then "b"^(str (d-x-1)) else "x"^(str (n-(x-d)-1)) |
|
104 |
| print_term d (Abs c) = "Abs (\\b"^(str d)^" -> "^(print_term (d + 1) c)^")" |
|
105 |
| print_term d t = print_call d t [] |
|
106 |
in |
|
107 |
print_term 0 |
|
108 |
end |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
109 |
|
23663 | 110 |
fun print_rule arity_of (p, t) = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
111 |
let |
41491 | 112 |
fun str x = string_of_int x |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
113 |
fun print_pattern top n PVar = (n+1, "x"^(str n)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
114 |
| print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
115 |
| print_pattern top n (PConst (c, args)) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
116 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
117 |
val (n,s) = print_pattern_list (n, (if top then "c" else "C")^(str c)) args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
118 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
119 |
(n, if top then s else "("^s^")") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
120 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
121 |
and print_pattern_list r [] = r |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
122 |
| print_pattern_list (n, p) (t::ts) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
123 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
124 |
val (n, t) = print_pattern false n t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
125 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
126 |
print_pattern_list (n, p^" "^t) ts |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
127 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
128 |
val (n, pattern) = print_pattern true 0 p |
23663 | 129 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
130 |
pattern^" = "^(print_term arity_of n t) |
23663 | 131 |
end |
132 |
||
133 |
fun group_rules rules = |
|
134 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
135 |
fun add_rule (r as (PConst (c,_), _)) groups = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
136 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
137 |
val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
138 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
139 |
Inttab.update (c, r::rs) groups |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
140 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
141 |
| add_rule _ _ = raise Compile "internal error group_rules" |
23663 | 142 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
143 |
fold_rev add_rule rules Inttab.empty |
23663 | 144 |
end |
145 |
||
146 |
fun haskell_prog name rules = |
|
147 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
148 |
val buffer = Unsynchronized.ref "" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
149 |
fun write s = (buffer := (!buffer)^s) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
150 |
fun writeln s = (write s; write "\n") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
151 |
fun writelist [] = () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
152 |
| writelist (s::ss) = (writeln s; writelist ss) |
41491 | 153 |
fun str i = string_of_int i |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
154 |
val (arity, rules) = adjust_rules rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
155 |
val rules = group_rules rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
156 |
val constants = Inttab.keys arity |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
157 |
fun arity_of c = Inttab.lookup arity c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
158 |
fun rep_str s n = implode (rep n s) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
159 |
fun indexed s n = s^(str n) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
160 |
fun section n = if n = 0 then [] else (section (n-1))@[n-1] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
161 |
fun make_show c = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
162 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
163 |
val args = section (the (arity_of c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
164 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
165 |
" show ("^(indexed "C" c)^(implode (map (indexed " a") args))^") = " |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
166 |
^"\""^(indexed "C" c)^"\""^(implode (map (fn a => "++(show "^(indexed "a" a)^")") args)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
167 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
168 |
fun default_case c = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
169 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
170 |
val args = implode (map (indexed " x") (section (the (arity_of c)))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
171 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
172 |
(indexed "c" c)^args^" = "^(indexed "C" c)^args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
173 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
174 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
175 |
"module "^name^" where", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
176 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
177 |
"data Term = Const Integer | App Term Term | Abs (Term -> Term)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
178 |
" "^(implode (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
179 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
180 |
"instance Show Term where"] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
181 |
val _ = writelist (map make_show constants) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
182 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
183 |
" show (Const c) = \"c\"++(show c)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
184 |
" show (App a b) = \"A\"++(show a)++(show b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
185 |
" show (Abs _) = \"L\"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
186 |
""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
187 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
188 |
"app (Abs a) b = a b", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
189 |
"app a b = App a b", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
190 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
191 |
"calc s c = writeFile s (show c)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
192 |
""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
193 |
fun list_group c = (writelist (case Inttab.lookup rules c of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
194 |
NONE => [default_case c, ""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
195 |
| SOME (rs as ((PConst (_, []), _)::rs')) => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
196 |
if not (null rs') then raise Compile "multiple declaration of constant" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
197 |
else (map (print_rule arity_of) rs) @ [""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
198 |
| SOME rs => (map (print_rule arity_of) rs) @ [default_case c, ""])) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
199 |
val _ = map list_group constants |
23663 | 200 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
201 |
(arity, !buffer) |
23663 | 202 |
end |
203 |
||
32740 | 204 |
val guid_counter = Unsynchronized.ref 0 |
23663 | 205 |
fun get_guid () = |
206 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
207 |
val c = !guid_counter |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
208 |
val _ = guid_counter := !guid_counter + 1 |
23663 | 209 |
in |
41491 | 210 |
string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c |
23663 | 211 |
end |
212 |
||
213 |
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s]))); |
|
214 |
fun wrap s = "\""^s^"\"" |
|
215 |
||
216 |
fun writeTextFile name s = File.write (Path.explode name) s |
|
217 |
||
218 |
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false) |
|
219 |
||
25520 | 220 |
fun compile cache_patterns const_arity eqs = |
23663 | 221 |
let |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
222 |
val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
223 |
val eqs = map (fn (a,b,c) => (b,c)) eqs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
224 |
val guid = get_guid () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
225 |
val module = "AMGHC_Prog_"^guid |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
226 |
val (arity, source) = haskell_prog module eqs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
227 |
val module_file = tmp_file (module^".hs") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
228 |
val object_file = tmp_file (module^".o") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
229 |
val _ = writeTextFile module_file source |
41953
994d088fbfbc
slightly more robust bash exec, which fails on empty executable;
wenzelm
parents:
41952
diff
changeset
|
230 |
val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file) |
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
231 |
val _ = |
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
232 |
if not (fileExists object_file) then |
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
233 |
raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')") |
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
234 |
else () |
23663 | 235 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
236 |
(guid, module_file, arity) |
23663 | 237 |
end |
238 |
||
239 |
fun readResultFile name = File.read (Path.explode name) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
240 |
|
23663 | 241 |
fun parse_result arity_of result = |
242 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
243 |
val result = String.explode result |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
244 |
fun shift NONE x = SOME x |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
245 |
| shift (SOME y) x = SOME (y*10 + x) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
246 |
fun parse_int' x (#"0"::rest) = parse_int' (shift x 0) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
247 |
| parse_int' x (#"1"::rest) = parse_int' (shift x 1) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
248 |
| parse_int' x (#"2"::rest) = parse_int' (shift x 2) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
249 |
| parse_int' x (#"3"::rest) = parse_int' (shift x 3) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
250 |
| parse_int' x (#"4"::rest) = parse_int' (shift x 4) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
251 |
| parse_int' x (#"5"::rest) = parse_int' (shift x 5) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
252 |
| parse_int' x (#"6"::rest) = parse_int' (shift x 6) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
253 |
| parse_int' x (#"7"::rest) = parse_int' (shift x 7) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
254 |
| parse_int' x (#"8"::rest) = parse_int' (shift x 8) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
255 |
| parse_int' x (#"9"::rest) = parse_int' (shift x 9) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
256 |
| parse_int' x rest = (x, rest) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
257 |
fun parse_int rest = parse_int' NONE rest |
23663 | 258 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
259 |
fun parse (#"C"::rest) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
260 |
(case parse_int rest of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
261 |
(SOME c, rest) => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
262 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
263 |
val (args, rest) = parse_list (the (arity_of c)) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
264 |
fun app_args [] t = t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
265 |
| app_args (x::xs) t = app_args xs (App (t, x)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
266 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
267 |
(app_args args (Const c), rest) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
268 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
269 |
| (NONE, rest) => raise Run "parse C") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
270 |
| parse (#"c"::rest) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
271 |
(case parse_int rest of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
272 |
(SOME c, rest) => (Const c, rest) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
273 |
| _ => raise Run "parse c") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
274 |
| parse (#"A"::rest) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
275 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
276 |
val (a, rest) = parse rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
277 |
val (b, rest) = parse rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
278 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
279 |
(App (a,b), rest) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
280 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
281 |
| parse (#"L"::rest) = raise Run "there may be no abstraction in the result" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
282 |
| parse _ = raise Run "invalid result" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
283 |
and parse_list n rest = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
284 |
if n = 0 then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
285 |
([], rest) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
286 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
287 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
288 |
val (x, rest) = parse rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
289 |
val (xs, rest) = parse_list (n-1) rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
290 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
291 |
(x::xs, rest) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
292 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
293 |
val (parsed, rest) = parse result |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
294 |
fun is_blank (#" "::rest) = is_blank rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
295 |
| is_blank (#"\n"::rest) = is_blank rest |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
296 |
| is_blank [] = true |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
297 |
| is_blank _ = false |
23663 | 298 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
299 |
if is_blank rest then parsed else raise Run "non-blank suffix in result file" |
23663 | 300 |
end |
301 |
||
302 |
fun run (guid, module_file, arity) t = |
|
303 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
304 |
val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
305 |
fun arity_of c = Inttab.lookup arity c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
306 |
val callguid = get_guid() |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
307 |
val module = "AMGHC_Prog_"^guid |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
308 |
val call = module^"_Call_"^callguid |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
309 |
val result_file = tmp_file (module^"_Result_"^callguid^".txt") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
310 |
val call_file = tmp_file (call^".hs") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
311 |
val term = print_term arity_of 0 t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
312 |
val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
313 |
val _ = writeTextFile call_file call_source |
41953
994d088fbfbc
slightly more robust bash exec, which fails on empty executable;
wenzelm
parents:
41952
diff
changeset
|
314 |
val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file) |
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
315 |
val result = readResultFile result_file handle IO.Io _ => |
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
wenzelm
parents:
41491
diff
changeset
|
316 |
raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')") |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
317 |
val t' = parse_result arity_of result |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
318 |
val _ = OS.FileSys.remove call_file |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
319 |
val _ = OS.FileSys.remove result_file |
23663 | 320 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
321 |
t' |
23663 | 322 |
end |
323 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
324 |
|
23663 | 325 |
fun discard _ = () |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
326 |
|
23663 | 327 |
end |
328 |