author  wenzelm 
Sun, 13 Mar 2011 19:27:39 +0100  
changeset 41953  994d088fbfbc 
parent 41952  c7297638599b 
child 41959  b460124855b8 
permissions  rwrr 
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 tabwidth;
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 (n1) x) 

40 

41 
fun adjust_rules rules = 

42 
let 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

45 
fun adjust_pattern PVar = PVar 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

49 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

51 
val args = map adjust_pattern args 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

52 
val len = length args 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

53 
val arity = arity_of c 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

55 
 lift level n (Const c) = Const c 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

58 
val lift = lift 0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

59 
fun adjust_term n t = if n=0 then t else adjust_term (n1) (App (t, Var (n1))) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

60 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

61 
if len = arity then 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

62 
rule 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

63 
else if arity >= len then 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

64 
(PConst (c, args @ (rep (aritylen) PVar)), adjust_term (aritylen) (lift (aritylen) t)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

65 
else (raise Compile "internal error in adjust_rule") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

66 
end 
23663  67 
in 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

68 
(arity, map adjust_rule rules) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

80 
(case arity_of c of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

81 
NONE => print_apps d ("Const "^(str c)) args 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

82 
 SOME a => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

83 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

84 
val len = length args 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

85 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

86 
if a <= len then 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

87 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

89 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

90 
print_apps d s (List.drop (args, a)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

91 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

92 
else 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

93 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

94 
fun mk_apps n t = if n = 0 then t else mk_apps (n1) (App (t, Var (n1))) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

95 
fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n1) (Abs t) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

96 
fun append_args [] t = t 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

98 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

99 
print_term d (mk_lambdas (alen) (mk_apps (alen) (nlift 0 (alen) (append_args args (Const c))))) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

100 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 (dx1)) else "x"^(str (n(xd)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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

115 
 print_pattern top n (PConst (c, args)) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

116 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

118 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

119 
(n, if top then s else "("^s^")") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

120 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

121 
and print_pattern_list r [] = r 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

122 
 print_pattern_list (n, p) (t::ts) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

123 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

124 
val (n, t) = print_pattern false n t 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

125 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

126 
print_pattern_list (n, p^" "^t) ts 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

127 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

135 
fun add_rule (r as (PConst (c,_), _)) groups = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

136 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

138 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

139 
Inttab.update (c, r::rs) groups 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

140 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

148 
val buffer = Unsynchronized.ref "" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

149 
fun write s = (buffer := (!buffer)^s) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

150 
fun writeln s = (write s; write "\n") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

151 
fun writelist [] = () 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

154 
val (arity, rules) = adjust_rules rules 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

155 
val rules = group_rules rules 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

156 
val constants = Inttab.keys arity 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

157 
fun arity_of c = Inttab.lookup arity c 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

159 
fun indexed s n = s^(str n) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

160 
fun section n = if n = 0 then [] else (section (n1))@[n1] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

161 
fun make_show c = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

162 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

163 
val args = section (the (arity_of c)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

164 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

167 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

168 
fun default_case c = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

169 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

171 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

172 
(indexed "c" c)^args^" = "^(indexed "C" c)^args 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

173 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

174 
val _ = writelist [ 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

175 
"module "^name^" where", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

176 
"", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

179 
"", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

180 
"instance Show Term where"] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

181 
val _ = writelist (map make_show constants) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

182 
val _ = writelist [ 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

183 
" show (Const c) = \"c\"++(show c)", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

185 
" show (Abs _) = \"L\"", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

186 
""] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

187 
val _ = writelist [ 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

188 
"app (Abs a) b = a b", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

189 
"app a b = App a b", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

190 
"", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

191 
"calc s c = writeFile s (show c)", 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

192 
""] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

194 
NONE => [default_case c, ""] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

195 
 SOME (rs as ((PConst (_, []), _)::rs')) => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

197 
else (map (print_rule arity_of) rs) @ [""] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

207 
val c = !guid_counter 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

224 
val guid = get_guid () 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

225 
val module = "AMGHC_Prog_"^guid 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

226 
val (arity, source) = haskell_prog module eqs 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

227 
val module_file = tmp_file (module^".hs") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

228 
val object_file = tmp_file (module^".o") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

243 
val result = String.explode result 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

244 
fun shift NONE x = SOME x 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

245 
 shift (SOME y) x = SOME (y*10 + x) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

256 
 parse_int' x rest = (x, rest) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

259 
fun parse (#"C"::rest) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

260 
(case parse_int rest of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

261 
(SOME c, rest) => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

262 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

264 
fun app_args [] t = t 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

266 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

267 
(app_args args (Const c), rest) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

268 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

269 
 (NONE, rest) => raise Run "parse C") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

270 
 parse (#"c"::rest) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

271 
(case parse_int rest of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

272 
(SOME c, rest) => (Const c, rest) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

273 
 _ => raise Run "parse c") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

274 
 parse (#"A"::rest) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

275 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

276 
val (a, rest) = parse rest 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

277 
val (b, rest) = parse rest 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

278 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

279 
(App (a,b), rest) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

280 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

282 
 parse _ = raise Run "invalid result" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

283 
and parse_list n rest = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

284 
if n = 0 then 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

285 
([], rest) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

286 
else 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

287 
let 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

288 
val (x, rest) = parse rest 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

289 
val (xs, rest) = parse_list (n1) rest 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

290 
in 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

291 
(x::xs, rest) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

292 
end 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

293 
val (parsed, rest) = parse result 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

294 
fun is_blank (#" "::rest) = is_blank rest 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

295 
 is_blank (#"\n"::rest) = is_blank rest 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

296 
 is_blank [] = true 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

297 
 is_blank _ = false 
23663  298 
in 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

299 
if is_blank rest then parsed else raise Run "nonblank 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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

305 
fun arity_of c = Inttab.lookup arity c 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

306 
val callguid = get_guid() 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

307 
val module = "AMGHC_Prog_"^guid 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

308 
val call = module^"_Call_"^callguid 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

310 
val call_file = tmp_file (call^".hs") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

311 
val term = print_term arity_of 0 t 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

317 
val t' = parse_result arity_of result 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

318 
val _ = OS.FileSys.remove call_file 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
32952
diff
changeset

321 
t' 
23663  322 
end 
323 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

324 

23663  325 
fun discard _ = () 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32952
diff
changeset

326 

23663  327 
end 
328 