|
1 signature ML_EXPR = sig |
|
2 datatype ml_expr = |
|
3 Lit of string |
|
4 | App of ml_expr * ml_expr |
|
5 | Val of string * XML.tree |
|
6 |
|
7 val print_ml_expr: Proof.context -> ml_expr -> string |
|
8 val eval: Proof.context -> ml_expr -> string -> XML.tree |
|
9 val eval_opaque: Proof.context -> ml_expr -> {table: string, repr_typ: string, conv: ml_expr} -> serial * XML.tree |
|
10 val check: Proof.context -> ml_expr -> string -> string option |
|
11 |
|
12 val print_tree: XML.tree -> string |
|
13 val print_body: XML.body -> string |
|
14 |
|
15 (* internal *) |
|
16 val codec: ml_expr codec |
|
17 structure Eval : TYPED_EVAL |
|
18 end |
|
19 |
|
20 structure ML_Expr : ML_EXPR = struct |
|
21 |
|
22 structure Eval = Typed_Eval |
|
23 ( |
|
24 type T = XML.tree |
|
25 val typ = "XML.tree" |
|
26 val name = "ML_Expr.Eval" |
|
27 ) |
|
28 |
|
29 fun print_tree (XML.Elem elem) = |
|
30 let |
|
31 val str = |
|
32 ML_Syntax.print_pair |
|
33 (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_properties) |
|
34 print_body |
|
35 elem |
|
36 in "(XML.Elem " ^ str ^ ")" end |
|
37 | print_tree (XML.Text text) = |
|
38 "(XML.Text " ^ ML_Syntax.print_string text ^ ")" |
|
39 and print_body body = |
|
40 ML_Syntax.print_list print_tree body |
|
41 |
|
42 datatype ml_expr = |
|
43 Lit of string |
|
44 | App of ml_expr * ml_expr |
|
45 | Val of string * XML.tree |
|
46 |
|
47 fun print_ml_expr _ (Lit text) = |
|
48 text |
|
49 | print_ml_expr ctxt (App (f, x)) = |
|
50 "(" ^ print_ml_expr ctxt f ^ ") (" ^ print_ml_expr ctxt x ^ ")" |
|
51 | print_ml_expr ctxt (Val (typ, value)) = |
|
52 let |
|
53 val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt) |
|
54 in "(Codec.the_decode " ^ codec ^ " " ^ print_tree value ^ ")" end |
|
55 |
|
56 fun check ctxt prog raw_typ = |
|
57 case try ML_Types.read_ml_type raw_typ of |
|
58 NONE => SOME ("failed to parse result type " ^ raw_typ) |
|
59 | SOME typ => |
|
60 let |
|
61 val context = Context.Proof ctxt |
|
62 val codec = can (Classy.resolve @{ML.class codec} typ) context |
|
63 |
|
64 fun check_vals (Lit _) = NONE |
|
65 | check_vals (App (f, x)) = merge_options (check_vals f, check_vals x) |
|
66 | check_vals (Val (raw_typ, _)) = |
|
67 case try ML_Types.read_ml_type raw_typ of |
|
68 NONE => SOME ("failed to parse value type " ^ raw_typ) |
|
69 | SOME _ => |
|
70 if can (Classy.resolve @{ML.class codec} typ) context then |
|
71 NONE |
|
72 else |
|
73 SOME ("could not resolve codec for value type " ^ raw_typ) |
|
74 in |
|
75 if not codec then |
|
76 SOME ("could not resolve codec for result type " ^ raw_typ) |
|
77 else |
|
78 case check_vals prog of |
|
79 SOME err => SOME err |
|
80 | NONE => |
|
81 case Exn.capture (ML_Types.ml_type_of ctxt) (print_ml_expr ctxt prog) of |
|
82 Exn.Res typ' => |
|
83 if typ = typ' then |
|
84 NONE |
|
85 else |
|
86 SOME ("expected result type " ^ raw_typ ^ " but got something else") |
|
87 | Exn.Exn exn => |
|
88 SOME ("compilation error: " ^ @{make_string} exn) |
|
89 end |
|
90 |
|
91 fun eval ctxt prog typ = |
|
92 let |
|
93 val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt) |
|
94 val prog = "(Codec.encode " ^ codec ^ " (" ^ print_ml_expr ctxt prog ^ "))" |
|
95 in |
|
96 Eval.eval (Input.string prog) ctxt |
|
97 end |
|
98 |
|
99 fun eval_opaque ctxt prog {table, repr_typ, conv} = |
|
100 let |
|
101 val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type repr_typ) (Context.Proof ctxt) |
|
102 val id = serial () |
|
103 val var = "eval_opaque_result" |
|
104 val inner_prog = "(" ^ print_ml_expr ctxt prog ^ ")" |
|
105 val store_prog = table ^ ".write " ^ ML_Syntax.print_int id ^ " " ^ var |
|
106 val res_prog = "Codec.encode " ^ codec ^ " ((" ^ print_ml_expr ctxt conv ^ ") " ^ var ^ ")" |
|
107 val prog = |
|
108 "(let " ^ |
|
109 "val " ^ var ^ " = " ^ inner_prog ^ |
|
110 " in " ^ |
|
111 "(" ^ store_prog ^ " ; " ^ res_prog ^ ") " ^ |
|
112 "end)" |
|
113 in |
|
114 (id, Eval.eval (Input.string prog) ctxt) |
|
115 end |
|
116 |
|
117 fun codec () = |
|
118 let |
|
119 val ml_expr_lit = Codec.string |
|
120 fun ml_expr_app () = Codec.tuple (codec ()) (codec ()) |
|
121 val ml_expr_val = Codec.tuple Codec.string Codec.tree |
|
122 |
|
123 fun enc _ = error "impossible" |
|
124 fun dec 0 = SOME (Codec.decode ml_expr_lit #> Codec.map_result Lit) |
|
125 | dec 1 = SOME (Codec.decode (ml_expr_app ()) #> Codec.map_result App) |
|
126 | dec 2 = SOME (Codec.decode ml_expr_val #> Codec.map_result Val) |
|
127 | dec _ = NONE |
|
128 in Codec.variant enc dec "ML_Expr.ml_expr" end |
|
129 |
|
130 val codec = codec () |
|
131 |
|
132 end |