1 (* Title: HOL/Nunchaku/Tools/nunchaku_translate.ML |
|
2 Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII |
|
3 Copyright 2015, 2016 |
|
4 |
|
5 Translation of Isabelle/HOL problems to Nunchaku. |
|
6 *) |
|
7 |
|
8 signature NUNCHAKU_TRANSLATE = |
|
9 sig |
|
10 type isa_problem = Nunchaku_Collect.isa_problem |
|
11 type ty = Nunchaku_Problem.ty |
|
12 type nun_problem = Nunchaku_Problem.nun_problem |
|
13 |
|
14 val flip_quote: string -> string |
|
15 val lowlevel_str_of_ty: ty -> string |
|
16 |
|
17 val nun_problem_of_isa: Proof.context -> isa_problem -> nun_problem |
|
18 end; |
|
19 |
|
20 structure Nunchaku_Translate : NUNCHAKU_TRANSLATE = |
|
21 struct |
|
22 |
|
23 open Nunchaku_Util; |
|
24 open Nunchaku_Collect; |
|
25 open Nunchaku_Problem; |
|
26 |
|
27 fun flip_quote s = |
|
28 (case try (unprefix "'") s of |
|
29 SOME s' => s' |
|
30 | NONE => prefix "'" s); |
|
31 |
|
32 fun lowlevel_str_of_ty (NType (id, tys)) = |
|
33 (if null tys then "" else encode_args (map lowlevel_str_of_ty tys)) ^ id; |
|
34 |
|
35 fun strip_nun_abs 0 tm = ([], tm) |
|
36 | strip_nun_abs n (NAbs (var, body)) = |
|
37 strip_nun_abs (n - 1) body |
|
38 |>> cons var; |
|
39 |
|
40 val strip_nun_comb = |
|
41 let |
|
42 fun strip args (NApp (func, arg)) = strip (arg :: args) func |
|
43 | strip args tm = (tm, args); |
|
44 in |
|
45 strip [] |
|
46 end; |
|
47 |
|
48 fun ty_of_isa (Type (s, Ts)) = |
|
49 let val tys = map ty_of_isa Ts in |
|
50 (case s of |
|
51 @{type_name bool} => prop_ty |
|
52 | @{type_name fun} => NType (nun_arrow, tys) |
|
53 | _ => |
|
54 let |
|
55 val args = map lowlevel_str_of_ty tys; |
|
56 val id = nun_tconst_of_str args s; |
|
57 in |
|
58 NType (id, []) |
|
59 end) |
|
60 end |
|
61 | ty_of_isa (TFree (s, _)) = NType (nun_tfree_of_str (flip_quote s), []) |
|
62 | ty_of_isa (TVar _) = raise Fail "unexpected TVar"; |
|
63 |
|
64 fun gen_tm_of_isa in_prop ctxt t = |
|
65 let |
|
66 val thy = Proof_Context.theory_of ctxt; |
|
67 |
|
68 fun id_of_const (x as (s, _)) = |
|
69 let val args = map (lowlevel_str_of_ty o ty_of_isa) (Sign.const_typargs thy x) in |
|
70 nun_const_of_str args s |
|
71 end; |
|
72 |
|
73 fun tm_of_branch ctr_id var_count f_arg_tm = |
|
74 let val (vars, body) = strip_nun_abs var_count f_arg_tm in |
|
75 (ctr_id, vars, body) |
|
76 end; |
|
77 |
|
78 fun tm_of bounds (Const (x as (s, T))) = |
|
79 (case try (dest_co_datatype_case ctxt) x of |
|
80 SOME ctrs => |
|
81 let |
|
82 val num_f_args = length ctrs; |
|
83 val min_args = num_f_args + 1; |
|
84 val var_counts = map (num_binder_types o snd) ctrs; |
|
85 |
|
86 val dummy_free = Free (Name.uu, T); |
|
87 val tm = tm_of bounds dummy_free; |
|
88 val tm' = eta_expandN_tm min_args tm; |
|
89 val (vars, body) = strip_nun_abs min_args tm'; |
|
90 val (_, (f_args, obj :: other_args)) = strip_nun_comb body ||> chop num_f_args; |
|
91 val f_args' = map2 eta_expandN_tm var_counts f_args; |
|
92 |
|
93 val ctr_ids = map id_of_const ctrs; |
|
94 in |
|
95 NMatch (obj, @{map 3} tm_of_branch ctr_ids var_counts f_args') |
|
96 |> rcomb_tms other_args |
|
97 |> abs_tms vars |
|
98 end |
|
99 | NONE => |
|
100 if s = @{const_name unreachable} andalso in_prop then |
|
101 let val ty = ty_of_isa T in |
|
102 napps (NConst (nun_asserting, [ty], mk_arrows_ty ([ty, prop_ty], ty)), |
|
103 [NConst (id_of_const x, [], ty), NConst (nun_false, [], prop_ty)]) |
|
104 end |
|
105 else |
|
106 let |
|
107 val id = |
|
108 (case s of |
|
109 @{const_name All} => nun_forall |
|
110 | @{const_name conj} => nun_conj |
|
111 | @{const_name disj} => nun_disj |
|
112 | @{const_name HOL.eq} => nun_equals |
|
113 | @{const_name Eps} => nun_choice |
|
114 | @{const_name Ex} => nun_exists |
|
115 | @{const_name False} => nun_false |
|
116 | @{const_name If} => nun_if |
|
117 | @{const_name implies} => nun_implies |
|
118 | @{const_name Not} => nun_not |
|
119 | @{const_name The} => nun_unique |
|
120 | @{const_name The_unsafe} => nun_unique_unsafe |
|
121 | @{const_name True} => nun_true |
|
122 | _ => id_of_const x); |
|
123 in |
|
124 NConst (id, [], ty_of_isa T) |
|
125 end) |
|
126 | tm_of _ (Free (s, T)) = NConst (nun_free_of_str s, [], ty_of_isa T) |
|
127 | tm_of _ (Var ((s, _), T)) = NConst (nun_var_of_str s, [], ty_of_isa T) |
|
128 | tm_of bounds (Abs (s, T, t)) = |
|
129 let |
|
130 val (s', bounds') = Name.variant s bounds; |
|
131 val x = Var ((s', 0), T); |
|
132 in |
|
133 NAbs (tm_of bounds' x, tm_of bounds' (subst_bound (x, t))) |
|
134 end |
|
135 | tm_of bounds (t $ u) = NApp (tm_of bounds t, tm_of bounds u) |
|
136 | tm_of _ (Bound _) = raise Fail "unexpected Bound"; |
|
137 in |
|
138 t |
|
139 |> tm_of Name.context |
|
140 |> beta_reduce_tm |
|
141 |> eta_expand_builtin_tm |
|
142 end; |
|
143 |
|
144 val tm_of_isa = gen_tm_of_isa false; |
|
145 val prop_of_isa = gen_tm_of_isa true; |
|
146 |
|
147 fun nun_copy_spec_of_isa_typedef ctxt {abs_typ, rep_typ, wrt, abs, rep} = |
|
148 {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, subset = SOME (tm_of_isa ctxt wrt), |
|
149 quotient = NONE, abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep}; |
|
150 |
|
151 fun nun_copy_spec_of_isa_quotient ctxt {abs_typ, rep_typ, wrt, abs, rep} = |
|
152 {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, subset = NONE, |
|
153 quotient = SOME (tm_of_isa ctxt wrt), abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep}; |
|
154 |
|
155 fun nun_ctr_of_isa ctxt ctr = |
|
156 {ctr = tm_of_isa ctxt ctr, arg_tys = map ty_of_isa (binder_types (fastype_of ctr))}; |
|
157 |
|
158 fun nun_co_data_spec_of_isa ctxt {typ, ctrs} = |
|
159 {ty = ty_of_isa typ, ctrs = map (nun_ctr_of_isa ctxt) ctrs}; |
|
160 |
|
161 fun nun_const_spec_of_isa ctxt {const, props} = |
|
162 {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props}; |
|
163 |
|
164 fun nun_rec_spec_of_isa ctxt {const, props, ...} = |
|
165 {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props}; |
|
166 |
|
167 fun nun_consts_spec_of_isa ctxt {consts, props} = |
|
168 {consts = map (tm_of_isa ctxt) consts, props = map (prop_of_isa ctxt) props}; |
|
169 |
|
170 fun nun_problem_of_isa ctxt {commandss, sound, complete} = |
|
171 let |
|
172 fun cmd_of cmd = |
|
173 (case cmd of |
|
174 ITVal (T, cards) => NTVal (ty_of_isa T, cards) |
|
175 | ITypedef spec => NCopy (nun_copy_spec_of_isa_typedef ctxt spec) |
|
176 | IQuotient spec => NCopy (nun_copy_spec_of_isa_quotient ctxt spec) |
|
177 | ICoData (fp, specs) => |
|
178 BNF_Util.case_fp fp NData NCodata (map (nun_co_data_spec_of_isa ctxt) specs) |
|
179 | IVal t => NVal (tm_of_isa ctxt t, ty_of_isa (fastype_of t)) |
|
180 | ICoPred (fp, wf, specs) => |
|
181 (if wf then curry NPred true |
|
182 else if fp = BNF_Util.Least_FP then curry NPred false |
|
183 else NCopred) (map (nun_const_spec_of_isa ctxt) specs) |
|
184 | IRec specs => NRec (map (nun_rec_spec_of_isa ctxt) specs) |
|
185 | ISpec spec => NSpec (nun_consts_spec_of_isa ctxt spec) |
|
186 | IAxiom prop => NAxiom (prop_of_isa ctxt prop) |
|
187 | IGoal prop => NGoal (prop_of_isa ctxt prop) |
|
188 | IEval t => NEval (tm_of_isa ctxt t)); |
|
189 in |
|
190 {commandss = map (map cmd_of) commandss, sound = sound, complete = complete} |
|
191 end; |
|
192 |
|
193 end; |
|