93 fun meets (c, ty) = case typ_of c |
93 fun meets (c, ty) = case typ_of c |
94 of SOME (vs, _) => |
94 of SOME (vs, _) => |
95 meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs) |
95 meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs) |
96 | NONE => I; |
96 | NONE => I; |
97 val tab = fold meets cs Vartab.empty; |
97 val tab = fold meets cs Vartab.empty; |
98 in map (Code_Unit.inst_thm tab) thms end; |
98 in map (Code_Unit.inst_thm thy tab) thms end; |
99 |
99 |
100 fun resort_eqnss thy algebra funcgr = |
100 fun resort_eqnss thy algebra funcgr = |
101 let |
101 let |
102 val typ_funcgr = try (fst o Graph.get_node funcgr); |
102 val typ_funcgr = try (fst o Graph.get_node funcgr); |
103 val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr); |
103 val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr); |
104 fun resort_rec typ_of (c, []) = (true, (c, [])) |
104 fun resort_rec typ_of (c, []) = (true, (c, [])) |
105 | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c) |
105 | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c) |
106 then (true, (c, thms)) |
106 then (true, (c, thms)) |
107 else let |
107 else let |
108 val (_, (vs, ty)) = Code_Unit.head_eqn thm; |
108 val (_, (vs, ty)) = Code_Unit.head_eqn thy thm; |
109 val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms |
109 val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms |
110 val (_, (vs', ty')) = Code_Unit.head_eqn thm'; (*FIXME simplify check*) |
110 val (_, (vs', ty')) = Code_Unit.head_eqn thy thm'; (*FIXME simplify check*) |
111 in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end; |
111 in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end; |
112 fun resort_recs eqnss = |
112 fun resort_recs eqnss = |
113 let |
113 let |
114 fun typ_of c = case these (AList.lookup (op =) eqnss c) |
114 fun typ_of c = case these (AList.lookup (op =) eqnss c) |
115 of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn) thm |
115 of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn thy) thm |
116 | [] => NONE; |
116 | [] => NONE; |
117 val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss); |
117 val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss); |
118 val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; |
118 val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; |
119 in (unchanged, eqnss') end; |
119 in (unchanged, eqnss') end; |
120 fun resort_rec_until eqnss = |
120 fun resort_rec_until eqnss = |
156 auxgr |
156 auxgr |
157 |> Graph.new_node (const, []) |
157 |> Graph.new_node (const, []) |
158 |> pair (SOME const) |
158 |> pair (SOME const) |
159 else let |
159 else let |
160 val thms = Code.these_eqns thy const |
160 val thms = Code.these_eqns thy const |
161 |> burrow_fst Code_Unit.norm_args |
161 |> burrow_fst (Code_Unit.norm_args thy) |
162 |> burrow_fst (Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var); |
162 |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var); |
163 val rhs = consts_of (const, thms); |
163 val rhs = consts_of (const, thms); |
164 in |
164 in |
165 auxgr |
165 auxgr |
166 |> Graph.new_node (const, thms) |
166 |> Graph.new_node (const, thms) |
167 |> fold_map (ensure_const thy algebra funcgr) rhs |
167 |> fold_map (ensure_const thy algebra funcgr) rhs |
179 fun merge_eqnss thy algebra raw_eqnss funcgr = |
179 fun merge_eqnss thy algebra raw_eqnss funcgr = |
180 let |
180 let |
181 val eqnss = raw_eqnss |
181 val eqnss = raw_eqnss |
182 |> resort_eqnss thy algebra funcgr |
182 |> resort_eqnss thy algebra funcgr |
183 |> filter_out (can (Graph.get_node funcgr) o fst); |
183 |> filter_out (can (Graph.get_node funcgr) o fst); |
184 fun typ_eqn c [] = Code.default_typ thy c |
184 fun typ_eqn c [] = Code.default_typscheme thy c |
185 | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn) thm; |
185 | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn thy) thm; |
186 fun add_eqns (const, thms) = |
186 fun add_eqns (const, thms) = |
187 Graph.new_node (const, (typ_eqn const thms, thms)); |
187 Graph.new_node (const, (typ_eqn const thms, thms)); |
188 fun add_deps (eqns as (const, thms)) funcgr = |
188 fun add_deps (eqns as (const, thms)) funcgr = |
189 let |
189 let |
190 val deps = consts_of eqns; |
190 val deps = consts_of eqns; |
224 val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct); |
224 val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct); |
225 val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); |
225 val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); |
226 fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I) |
226 fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I) |
227 t []; |
227 t []; |
228 val algebra = Code.coregular_algebra thy; |
228 val algebra = Code.coregular_algebra thy; |
229 val thm = Code.preprocess_conv ct; |
229 val thm = Code.preprocess_conv thy ct; |
230 val ct' = Thm.rhs_of thm; |
230 val ct' = Thm.rhs_of thm; |
231 val t' = Thm.term_of ct'; |
231 val t' = Thm.term_of ct'; |
232 val consts = map fst (consts_of t'); |
232 val consts = map fst (consts_of t'); |
233 val funcgr' = ensure_consts thy algebra consts funcgr; |
233 val funcgr' = ensure_consts thy algebra consts funcgr; |
234 val (t'', evaluator') = apsnd evaluator_fr (evaluator t'); |
234 val (t'', evaluator') = apsnd evaluator_fr (evaluator t'); |
240 fun proto_eval_conv thy = |
240 fun proto_eval_conv thy = |
241 let |
241 let |
242 fun evaluator evaluator' thm1 funcgr t = |
242 fun evaluator evaluator' thm1 funcgr t = |
243 let |
243 let |
244 val thm2 = evaluator' funcgr t; |
244 val thm2 = evaluator' funcgr t; |
245 val thm3 = Code.postprocess_conv (Thm.rhs_of thm2); |
245 val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2); |
246 in |
246 in |
247 Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => |
247 Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => |
248 error ("could not construct evaluation proof:\n" |
248 error ("could not construct evaluation proof:\n" |
249 ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) |
249 ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) |
250 end; |
250 end; |