author  wenzelm 
Tue, 24 Mar 2009 16:11:09 +0100  
changeset 30705  e8ab35c6ade6 
parent 30704  d6d4828e74a2 
child 30709  d9ca766bf24c 
permissions  rwrr 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/ML/ml_test.ML 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

3 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

4 
Test of advanced ML compiler invocation in Poly/ML 5.3. 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

5 
*) 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

6 

30646  7 
signature ML_TEST = 
8 
sig 

30680  9 
val eval: bool > Position.T > ML_Lex.token list > unit 
30646  10 
end 
11 

12 
structure ML_Test: ML_TEST = 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

13 
struct 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

14 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

15 
(* extra ML environment *) 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

16 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

17 
structure Extra_Env = GenericDataFun 
30646  18 
( 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

19 
type T = Position.T Inttab.table; (*position of registered tokens*) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

20 
val empty = Inttab.empty; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

21 
val extend = I; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

22 
fun merge _ = Inttab.merge (K true); 
30646  23 
); 
24 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

25 
fun inherit_env context = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

26 
ML_Context.inherit_env context #> 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

27 
Extra_Env.put (Extra_Env.get context); 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

28 

d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

29 
fun register_tokens toks context = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

30 
let 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

31 
val regs = map (fn tok => (serial (), tok)) toks; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

32 
val context' = context 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

33 
> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs); 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

34 
in (regs, context') end; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

35 

d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

36 
fun pos_of_location context 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

37 
({file, startLine = line, startPosition = i, endPosition = j, ...}: location) = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

38 
(case pairself (Inttab.lookup (Extra_Env.get context)) (i, j) of 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

39 
(SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

40 
 (SOME pos, NONE) => pos 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

41 
 _ => Position.line_file line file); 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

42 

30646  43 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

44 
(* parse trees *) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

45 

d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

46 
fun report_parse_tree context = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

47 
let 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

48 
val pos_of = pos_of_location context; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

49 
fun report loc (PTtype types) = (* FIXME body text *) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

50 
Position.report Markup.ML_typing (pos_of loc) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

51 
 report loc (PTdeclaredAt decl) = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

52 
Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) "" 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

53 
> Position.report_text Markup.ML_ref (pos_of loc) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

54 
 report _ (PTnextSibling tree) = report_tree (tree ()) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

55 
 report _ (PTfirstChild tree) = report_tree (tree ()) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

56 
 report _ _ = () 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

57 
and report_tree (loc, props) = List.app (report loc) props; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

58 
in report_tree end; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

59 

d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

60 

d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

61 
(* eval ML source tokens *) 
30680  62 

63 
fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks = 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

64 
let 
30680  65 
(* input *) 
66 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

67 
val input = Context.>>> (register_tokens toks); 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

68 
val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input); 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

69 

d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

70 
val current_line = ref (the_default 1 (Position.line_of pos)); 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

71 

30705
e8ab35c6ade6
get_index: produce index of next pending token, not the last one;
wenzelm
parents:
30704
diff
changeset

72 
fun get_index () = 
e8ab35c6ade6
get_index: produce index of next pending token, not the last one;
wenzelm
parents:
30704
diff
changeset

73 
the_default 0 (get_first (fn (_, []) => NONE  (i, _) => SOME i) (! input_buffer)); 
e8ab35c6ade6
get_index: produce index of next pending token, not the last one;
wenzelm
parents:
30704
diff
changeset

74 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

75 
fun get () = 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

76 
(case ! input_buffer of 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

77 
[] => NONE 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

78 
 (_, []) :: rest => (input_buffer := rest; get ()) 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

79 
 (i, c :: cs) :: rest => 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

80 
(input_buffer := (i, cs) :: rest; 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

81 
if c = #"\n" then current_line := ! current_line + 1 else (); 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

82 
SOME c)); 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

83 

30680  84 

85 
(* output *) 

86 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

87 
val output_buffer = ref Buffer.empty; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

88 
fun output () = Buffer.content (! output_buffer); 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

89 
fun put s = change output_buffer (Buffer.add s); 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

90 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

91 
fun put_message {message, hard, location, context = _} = 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

92 
(put (if hard then "Error: " else "Warning: "); 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

93 
put (Pretty.string_of (Pretty.from_ML (pretty_ml message))); 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

94 
put (Position.str_of (pos_of_location (the (Context.thread_data ())) location) ^ "\n")); 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

95 

30680  96 

97 
(* results *) 

98 

99 
fun apply_result {fixes, types, signatures, structures, functors, values} = 

100 
let 

101 
fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) = 

102 
let 

103 
fun make_prefix context = 

104 
(case get_first (fn ContextParentStructure p => SOME p  _ => NONE) context of 

105 
SOME (name, sub_context) => make_prefix sub_context ^ name ^ "." 

106 
 NONE => prefix); 

107 
val this_prefix = make_prefix context; 

108 
in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end 

109 
 add_prefix prefix (prt as PrettyString s) = 

110 
if prefix = "" then prt else PrettyString (prefix ^ s) 

111 
 add_prefix _ (prt as PrettyBreak _) = prt; 

112 

113 
val depth = get_print_depth (); 

114 
val with_struct = ! PolyML.Compiler.printTypesWithStructureName; 

115 

116 
fun display disp x = 

117 
if depth > 0 then 

118 
(disp x 

119 
> with_struct ? add_prefix "" 

120 
> pretty_ml > Pretty.from_ML > Pretty.string_of > put; put "\n") 

121 
else (); 

122 

123 
fun apply_fix (a, b) = 

124 
(display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); 

125 
fun apply_type (a, b) = 

126 
(display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b)); 

127 
fun apply_sig (a, b) = 

128 
(display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); 

129 
fun apply_struct (a, b) = 

130 
(display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); 

131 
fun apply_funct (a, b) = 

132 
(display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); 

133 
fun apply_val (a, b) = 

134 
(display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); 

135 
in 

136 
List.app apply_fix fixes; 

137 
List.app apply_type types; 

138 
List.app apply_sig signatures; 

139 
List.app apply_struct structures; 

140 
List.app apply_funct functors; 

141 
List.app apply_val values 

142 
end; 

143 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

144 
fun result_fun (phase1, phase2) () = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

145 
(case phase1 of NONE => () 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

146 
 SOME parse_tree => report_parse_tree (the (Context.thread_data ())) parse_tree; 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

147 
case phase2 of NONE => error "Static Errors" 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

148 
 SOME code => apply_result (Toplevel.program code)); 
30680  149 

150 

151 
(* compiler invocation *) 

30646  152 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

153 
val parameters = 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

154 
[PolyML.Compiler.CPOutStream put, 
30680  155 
PolyML.Compiler.CPNameSpace space, 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

156 
PolyML.Compiler.CPErrorMessageProc put_message, 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

157 
PolyML.Compiler.CPLineNo (fn () => ! current_line), 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

158 
PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

159 
PolyML.Compiler.CPLineOffset get_index, 
30680  160 
PolyML.Compiler.CPCompilerResultFun result_fun]; 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

161 
val _ = 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

162 
(while not (List.null (! input_buffer)) do 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

163 
PolyML.compiler (get, parameters) ()) 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

164 
handle exn => 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

165 
(put ("Exception " ^ General.exnMessage exn ^ " raised"); 
30677  166 
error (output ()); raise exn); 
30680  167 
in if verbose then print (output ()) else () end; 
168 

169 
val eval = use_text ML_Context.local_context; 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

170 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

171 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

172 
(* ML test command *) 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

173 

30680  174 
fun ML_test (txt, pos) = 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

175 
let 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

176 
val _ = Position.report Markup.ML_source pos; 
30644  177 
val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos); 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

178 
val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ()); 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

179 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

180 
val _ = Context.setmp_thread_data env_ctxt 
30680  181 
(fn () => (eval false Position.none env; Context.thread_data ())) () 
30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

182 
> (fn NONE => ()  SOME context' => Context.>> (inherit_env context')); 
30680  183 
val _ = eval true pos body; 
184 
val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end"); 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

185 
in () end; 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

186 

30644  187 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

188 
local structure P = OuterParse and K = OuterKeyword in 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

189 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

190 
fun propagate_env (context as Context.Proof lthy) = 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

191 
Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy) 
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

192 
 propagate_env context = context; 
30644  193 

30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

194 
val _ = 
30644  195 
OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl) 
196 
(P.ML_source >> (fn src => 

30704
d6d4828e74a2
register token positions persistently with context;
wenzelm
parents:
30681
diff
changeset

197 
Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env))); 
30640
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

198 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

199 
end; 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

200 

3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

201 
end; 
3f3d1e218b64
Test of advanced ML compiler invocation in Poly/ML 5.3.
wenzelm
parents:
diff
changeset

202 