21 local_theory -> (string * (term list * thm list)) * local_theory |
21 local_theory -> (string * (term list * thm list)) * local_theory |
22 end; |
22 end; |
23 |
23 |
24 structure Primrec : PRIMREC = |
24 structure Primrec : PRIMREC = |
25 struct |
25 struct |
26 |
|
27 open Datatype_Aux; |
|
28 |
26 |
29 exception PrimrecError of string * term option; |
27 exception PrimrecError of string * term option; |
30 |
28 |
31 fun primrec_error msg = raise PrimrecError (msg, NONE); |
29 fun primrec_error msg = raise PrimrecError (msg, NONE); |
32 fun primrec_error_eqn msg eqn = raise PrimrecError (msg, SOME eqn); |
30 fun primrec_error_eqn msg eqn = raise PrimrecError (msg, SOME eqn); |
145 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
143 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
146 "\nin definition of function " ^ quote fname); |
144 "\nin definition of function " ^ quote fname); |
147 (fnames', fnss', (Const (@{const_name undefined}, dummyT)) :: fns)) |
145 (fnames', fnss', (Const (@{const_name undefined}, dummyT)) :: fns)) |
148 | SOME (ls, cargs', rs, rhs, eq) => |
146 | SOME (ls, cargs', rs, rhs, eq) => |
149 let |
147 let |
150 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
148 val recs = filter (Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); |
151 val rargs = map fst recs; |
149 val rargs = map fst recs; |
152 val subs = map (rpair dummyT o fst) |
150 val subs = map (rpair dummyT o fst) |
153 (rev (Term.rename_wrt_term rhs rargs)); |
151 (rev (Term.rename_wrt_term rhs rargs)); |
154 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
152 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
155 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
153 (Free x, (Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') |
156 handle PrimrecError (s, NONE) => primrec_error_eqn s eq |
154 handle PrimrecError (s, NONE) => primrec_error_eqn s eq |
157 in |
155 in |
158 (fnames'', fnss'', fold_rev absfree (cargs' @ subs @ ls @ rs) rhs' :: fns) |
156 (fnames'', fnss'', fold_rev absfree (cargs' @ subs @ ls @ rs) rhs' :: fns) |
159 end) |
157 end) |
160 |
158 |
182 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) = |
183 (case AList.lookup (op =) fns i of |
181 (case AList.lookup (op =) fns i of |
184 NONE => |
182 NONE => |
185 let |
183 let |
186 val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, |
184 val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, |
187 replicate (length cargs + length (filter is_rec_type cargs)) |
185 replicate (length cargs + length (filter Datatype_Aux.is_rec_type cargs)) |
188 dummyT ---> HOLogic.unitT)) constrs; |
186 dummyT ---> HOLogic.unitT)) constrs; |
189 val _ = warning ("No function definition for datatype " ^ quote tname) |
187 val _ = warning ("No function definition for datatype " ^ quote tname) |
190 in |
188 in |
191 (dummy_fns @ fs, defs) |
189 (dummy_fns @ fs, defs) |
192 end |
190 end |
206 in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end; |
204 in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end; |
207 |
205 |
208 |
206 |
209 (* find datatypes which contain all datatypes in tnames' *) |
207 (* find datatypes which contain all datatypes in tnames' *) |
210 |
208 |
211 fun find_dts (dt_info : info Symtab.table) _ [] = [] |
209 fun find_dts (dt_info : Datatype_Aux.info Symtab.table) _ [] = [] |
212 | find_dts dt_info tnames' (tname :: tnames) = |
210 | find_dts dt_info tnames' (tname :: tnames) = |
213 (case Symtab.lookup dt_info tname of |
211 (case Symtab.lookup dt_info tname of |
214 NONE => primrec_error (quote tname ^ " is not a datatype") |
212 NONE => primrec_error (quote tname ^ " is not a datatype") |
215 | SOME dt => |
213 | SOME dt => |
216 if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then |
214 if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then |