32 |
32 |
33 (* preprocessing of equations *) |
33 (* preprocessing of equations *) |
34 |
34 |
35 fun process_eqn is_fixed spec rec_fns = |
35 fun process_eqn is_fixed spec rec_fns = |
36 let |
36 let |
37 val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} spec); |
37 val (vs, Ts) = split_list (strip_qnt_vars \<^const_name>\<open>Pure.all\<close> spec); |
38 val body = strip_qnt_body @{const_name Pure.all} spec; |
38 val body = strip_qnt_body \<^const_name>\<open>Pure.all\<close> spec; |
39 val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms |
39 val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms |
40 (fn Free (v, _) => insert (op =) v | _ => I) body [])); |
40 (fn Free (v, _) => insert (op =) v | _ => I) body [])); |
41 val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; |
41 val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; |
42 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn) |
42 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn) |
43 handle TERM _ => primrec_error "not a proper equation"; |
43 handle TERM _ => primrec_error "not a proper equation"; |
140 |
140 |
141 fun trans eqns (cname, cargs) (fnames', fnss', fns) = |
141 fun trans eqns (cname, cargs) (fnames', fnss', fns) = |
142 (case AList.lookup (op =) eqns cname of |
142 (case AList.lookup (op =) eqns cname of |
143 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
143 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
144 "\nin definition of function " ^ quote fname); |
144 "\nin definition of function " ^ quote fname); |
145 (fnames', fnss', (Const (@{const_name undefined}, dummyT)) :: fns)) |
145 (fnames', fnss', (Const (\<^const_name>\<open>undefined\<close>, dummyT)) :: fns)) |
146 | SOME (ls, cargs', rs, rhs, eq) => |
146 | SOME (ls, cargs', rs, rhs, eq) => |
147 let |
147 let |
148 val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); |
148 val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); |
149 val rargs = map fst recs; |
149 val rargs = map fst recs; |
150 val subs = map (rpair dummyT o fst) |
150 val subs = map (rpair dummyT o fst) |
179 |
179 |
180 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
180 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
181 (case AList.lookup (op =) fns i of |
181 (case AList.lookup (op =) fns i of |
182 NONE => |
182 NONE => |
183 let |
183 let |
184 val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, |
184 val dummy_fns = map (fn (_, cargs) => Const (\<^const_name>\<open>undefined\<close>, |
185 replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs)) |
185 replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs)) |
186 dummyT ---> HOLogic.unitT)) constrs; |
186 dummyT ---> HOLogic.unitT)) constrs; |
187 val _ = warning ("No function definition for datatype " ^ quote tname) |
187 val _ = warning ("No function definition for datatype " ^ quote tname) |
188 in |
188 in |
189 (dummy_fns @ fs, defs) |
189 (dummy_fns @ fs, defs) |