43 (fn Free (v, _) => insert (op =) v | _ => I) body [])); |
44 (fn Free (v, _) => insert (op =) v | _ => I) body [])); |
44 val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; |
45 val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; |
45 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn) |
46 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn) |
46 handle TERM _ => primrec_error "not a proper equation"; |
47 handle TERM _ => primrec_error "not a proper equation"; |
47 val (recfun, args) = strip_comb lhs; |
48 val (recfun, args) = strip_comb lhs; |
48 val fname = case recfun of Free (v, _) => if is_fixed v then v |
49 val fname = |
|
50 (case recfun of |
|
51 Free (v, _) => |
|
52 if is_fixed v then v |
49 else primrec_error "illegal head of function equation" |
53 else primrec_error "illegal head of function equation" |
50 | _ => primrec_error "illegal head of function equation"; |
54 | _ => primrec_error "illegal head of function equation"); |
51 |
55 |
52 val (ls', rest) = take_prefix is_Free args; |
56 val (ls', rest) = take_prefix is_Free args; |
53 val (middle, rs') = take_suffix is_Free rest; |
57 val (middle, rs') = take_suffix is_Free rest; |
54 val rpos = length ls'; |
58 val rpos = length ls'; |
55 |
59 |
56 val (constr, cargs') = if null middle then primrec_error "constructor missing" |
60 val (constr, cargs') = |
|
61 if null middle then primrec_error "constructor missing" |
57 else strip_comb (hd middle); |
62 else strip_comb (hd middle); |
58 val (cname, T) = dest_Const constr |
63 val (cname, T) = dest_Const constr |
59 handle TERM _ => primrec_error "ill-formed constructor"; |
64 handle TERM _ => primrec_error "ill-formed constructor"; |
60 val (tname, _) = dest_Type (body_type T) handle TYPE _ => |
65 val (tname, _) = dest_Type (body_type T) handle TYPE _ => |
61 primrec_error "cannot determine datatype associated with function" |
66 primrec_error "cannot determine datatype associated with function" |
73 else |
78 else |
74 (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees); |
79 (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees); |
75 check_vars "extra variables on rhs: " |
80 check_vars "extra variables on rhs: " |
76 (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees |
81 (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees |
77 |> filter_out (is_fixed o fst)); |
82 |> filter_out (is_fixed o fst)); |
78 case AList.lookup (op =) rec_fns fname of |
83 (case AList.lookup (op =) rec_fns fname of |
79 NONE => |
84 NONE => |
80 (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eqn))]))::rec_fns |
85 (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eqn))])) :: rec_fns |
81 | SOME (_, rpos', eqns) => |
86 | SOME (_, rpos', eqns) => |
82 if AList.defined (op =) eqns cname then |
87 if AList.defined (op =) eqns cname then |
83 primrec_error "constructor already occurred as pattern" |
88 primrec_error "constructor already occurred as pattern" |
84 else if rpos <> rpos' then |
89 else if rpos <> rpos' then |
85 primrec_error "position of recursive argument inconsistent" |
90 primrec_error "position of recursive argument inconsistent" |
86 else |
91 else |
87 AList.update (op =) |
92 AList.update (op =) |
88 (fname, (tname, rpos, (cname, (ls, cargs, rs, rhs, eqn))::eqns)) |
93 (fname, (tname, rpos, (cname, (ls, cargs, rs, rhs, eqn)) :: eqns)) |
89 rec_fns) |
94 rec_fns)) |
90 end handle PrimrecError (msg, NONE) => primrec_error_eqn msg spec; |
95 end handle PrimrecError (msg, NONE) => primrec_error_eqn msg spec; |
91 |
96 |
92 fun process_fun descr eqns (i, fname) (fnames, fnss) = |
97 fun process_fun descr eqns (i, fname) (fnames, fnss) = |
93 let |
98 let |
94 val (_, (tname, _, constrs)) = nth descr i; |
99 val (_, (tname, _, constrs)) = nth descr i; |
108 andalso member (fn ((v, _), (w, _)) => v = w) eqns (dest_Free f) then |
113 andalso member (fn ((v, _), (w, _)) => v = w) eqns (dest_Free f) then |
109 let |
114 let |
110 val (fname', _) = dest_Free f; |
115 val (fname', _) = dest_Free f; |
111 val (_, rpos, _) = the (AList.lookup (op =) eqns fname'); |
116 val (_, rpos, _) = the (AList.lookup (op =) eqns fname'); |
112 val (ls, rs) = chop rpos ts |
117 val (ls, rs) = chop rpos ts |
113 val (x', rs') = case rs |
118 val (x', rs') = |
114 of x' :: rs => (x', rs) |
119 (case rs of |
115 | [] => primrec_error ("not enough arguments in recursive application\n" |
120 x' :: rs => (x', rs) |
116 ^ "of function " ^ quote fname' ^ " on rhs"); |
121 | [] => primrec_error ("not enough arguments in recursive application\n" ^ |
|
122 "of function " ^ quote fname' ^ " on rhs")); |
117 val (x, xs) = strip_comb x'; |
123 val (x, xs) = strip_comb x'; |
118 in case AList.lookup (op =) subs x |
124 in |
119 of NONE => |
125 (case AList.lookup (op =) subs x of |
|
126 NONE => |
120 fs |
127 fs |
121 |> fold_map (subst subs) ts |
128 |> fold_map (subst subs) ts |
122 |-> (fn ts' => pair (list_comb (f, ts'))) |
129 |-> (fn ts' => pair (list_comb (f, ts'))) |
123 | SOME (i', y) => |
130 | SOME (i', y) => |
124 fs |
131 fs |
125 |> fold_map (subst subs) (xs @ ls @ rs') |
132 |> fold_map (subst subs) (xs @ ls @ rs') |
126 ||> process_fun descr eqns (i', fname') |
133 ||> process_fun descr eqns (i', fname') |
127 |-> (fn ts' => pair (list_comb (y, ts'))) |
134 |-> (fn ts' => pair (list_comb (y, ts')))) |
128 end |
135 end |
129 else |
136 else |
130 fs |
137 fs |
131 |> fold_map (subst subs) (f :: ts) |
138 |> fold_map (subst subs) (f :: ts) |
132 |-> (fn (f'::ts') => pair (list_comb (f', ts'))) |
139 |-> (fn f' :: ts' => pair (list_comb (f', ts'))) |
133 end |
140 end |
134 | subst _ t fs = (t, fs); |
141 | subst _ t fs = (t, fs); |
135 |
142 |
136 (* translate rec equations into function arguments suitable for rec comb *) |
143 (* translate rec equations into function arguments suitable for rec comb *) |
137 |
144 |
138 fun trans eqns (cname, cargs) (fnames', fnss', fns) = |
145 fun trans eqns (cname, cargs) (fnames', fnss', fns) = |
139 (case AList.lookup (op =) eqns cname of |
146 (case AList.lookup (op =) eqns cname of |
140 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
147 NONE => (warning ("No equation for constructor " ^ quote cname ^ |
141 "\nin definition of function " ^ quote fname); |
148 "\nin definition of function " ^ quote fname); |
142 (fnames', fnss', (Const ("HOL.undefined", dummyT))::fns)) |
149 (fnames', fnss', (Const ("HOL.undefined", dummyT)) :: fns)) |
143 | SOME (ls, cargs', rs, rhs, eq) => |
150 | SOME (ls, cargs', rs, rhs, eq) => |
144 let |
151 let |
145 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
152 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
146 val rargs = map fst recs; |
153 val rargs = map fst recs; |
147 val subs = map (rpair dummyT o fst) |
154 val subs = map (rpair dummyT o fst) |
148 (rev (Term.rename_wrt_term rhs rargs)); |
155 (rev (Term.rename_wrt_term rhs rargs)); |
149 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
156 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
150 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
157 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
151 handle PrimrecError (s, NONE) => primrec_error_eqn s eq |
158 handle PrimrecError (s, NONE) => primrec_error_eqn s eq |
152 in (fnames'', fnss'', |
159 in (fnames'', fnss'', |
153 (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns) |
160 (list_abs_free (cargs' @ subs @ ls @ rs, rhs')) :: fns) |
154 end) |
161 end) |
155 |
162 |
156 in (case AList.lookup (op =) fnames i of |
163 in |
|
164 (case AList.lookup (op =) fnames i of |
157 NONE => |
165 NONE => |
158 if exists (fn (_, v) => fname = v) fnames then |
166 if exists (fn (_, v) => fname = v) fnames then |
159 primrec_error ("inconsistent functions for datatype " ^ quote tname) |
167 primrec_error ("inconsistent functions for datatype " ^ quote tname) |
160 else |
168 else |
161 let |
169 let |
162 val (_, _, eqns) = the (AList.lookup (op =) eqns fname); |
170 val (_, _, eqns) = the (AList.lookup (op =) eqns fname); |
163 val (fnames', fnss', fns) = fold_rev (trans eqns) constrs |
171 val (fnames', fnss', fns) = fold_rev (trans eqns) constrs |
164 ((i, fname)::fnames, fnss, []) |
172 ((i, fname) :: fnames, fnss, []) |
165 in |
173 in |
166 (fnames', (i, (fname, #1 (snd (hd eqns)), fns))::fnss') |
174 (fnames', (i, (fname, #1 (snd (hd eqns)), fns)) :: fnss') |
167 end |
175 end |
168 | SOME fname' => |
176 | SOME fname' => |
169 if fname = fname' then (fnames, fnss) |
177 if fname = fname' then (fnames, fnss) |
170 else primrec_error ("inconsistent functions for datatype " ^ quote tname)) |
178 else primrec_error ("inconsistent functions for datatype " ^ quote tname)) |
171 end; |
179 end; |
172 |
180 |
173 |
181 |
174 (* prepare functions needed for definitions *) |
182 (* prepare functions needed for definitions *) |
175 |
183 |
176 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
184 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
177 case AList.lookup (op =) fns i of |
185 (case AList.lookup (op =) fns i of |
178 NONE => |
186 NONE => |
179 let |
187 let |
180 val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined", |
188 val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined", |
181 replicate (length cargs + length (filter is_rec_type cargs)) |
189 replicate (length cargs + length (filter is_rec_type cargs)) |
182 dummyT ---> HOLogic.unitT)) constrs; |
190 dummyT ---> HOLogic.unitT)) constrs; |
183 val _ = warning ("No function definition for datatype " ^ quote tname) |
191 val _ = warning ("No function definition for datatype " ^ quote tname) |
184 in |
192 in |
185 (dummy_fns @ fs, defs) |
193 (dummy_fns @ fs, defs) |
186 end |
194 end |
187 | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname) :: defs); |
195 | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname) :: defs)); |
188 |
196 |
189 |
197 |
190 (* make definition *) |
198 (* make definition *) |
191 |
199 |
192 fun make_def ctxt fixes fs (fname, ls, rec_name, tname) = |
200 fun make_def ctxt fixes fs (fname, ls, rec_name, tname) = |