18 (Attrib.binding * string) list -> local_theory -> Proof.state |
18 (Attrib.binding * string) list -> local_theory -> Proof.state |
19 end; |
19 end; |
20 |
20 |
21 structure NominalPrimrec : NOMINAL_PRIMREC = |
21 structure NominalPrimrec : NOMINAL_PRIMREC = |
22 struct |
22 struct |
23 |
|
24 open Datatype_Aux; |
|
25 |
23 |
26 exception RecError of string; |
24 exception RecError of string; |
27 |
25 |
28 fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s); |
26 fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s); |
29 fun primrec_eq_err lthy s eq = |
27 fun primrec_eq_err lthy s eq = |
154 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
152 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
155 "\nin definition of function " ^ quote fname); |
153 "\nin definition of function " ^ quote fname); |
156 (fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns)) |
154 (fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns)) |
157 | SOME (ls, cargs', rs, rhs, eq) => |
155 | SOME (ls, cargs', rs, rhs, eq) => |
158 let |
156 let |
159 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
157 val recs = filter (Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); |
160 val rargs = map fst recs; |
158 val rargs = map fst recs; |
161 val subs = map (rpair dummyT o fst) |
159 val subs = map (rpair dummyT o fst) |
162 (rev (Term.rename_wrt_term rhs rargs)); |
160 (rev (Term.rename_wrt_term rhs rargs)); |
163 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
161 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
164 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
162 (Free x, (Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') |
165 handle RecError s => primrec_eq_err lthy s eq |
163 handle RecError s => primrec_eq_err lthy s eq |
166 in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns) |
164 in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns) |
167 end) |
165 end) |
168 |
166 |
169 in (case AList.lookup (op =) fnames i of |
167 in (case AList.lookup (op =) fnames i of |
190 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
188 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
191 case AList.lookup (op =) fns i of |
189 case AList.lookup (op =) fns i of |
192 NONE => |
190 NONE => |
193 let |
191 let |
194 val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, |
192 val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, |
195 replicate (length cargs + length (filter is_rec_type cargs)) |
193 replicate (length cargs + length (filter Datatype_Aux.is_rec_type cargs)) |
196 dummyT ---> HOLogic.unitT)) constrs; |
194 dummyT ---> HOLogic.unitT)) constrs; |
197 val _ = warning ("No function definition for datatype " ^ quote tname) |
195 val _ = warning ("No function definition for datatype " ^ quote tname) |
198 in |
196 in |
199 (dummy_fns @ fs, defs) |
197 (dummy_fns @ fs, defs) |
200 end |
198 end |