224 let |
224 let |
225 val j = length ts; |
225 val j = length ts; |
226 val l = k - j; |
226 val l = k - j; |
227 val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
227 val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
228 val vs_tys = (map o apfst) SOME |
228 val vs_tys = (map o apfst) SOME |
229 (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys)); |
229 (Name.names ctxt "a" ((curry (uncurry take) l o curry (uncurry drop) j) tys)); |
230 in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end; |
230 in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end; |
231 |
231 |
232 fun contains_dictvar t = |
232 fun contains_dictvar t = |
233 let |
233 let |
234 fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss |
234 fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss |
771 val t = nth ts t_pos; |
771 val t = nth ts t_pos; |
772 val ts_clause = nth_drop t_pos ts; |
772 val ts_clause = nth_drop t_pos ts; |
773 val clauses = if null case_pats |
773 val clauses = if null case_pats |
774 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) |
774 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) |
775 else maps (fn ((constr as IConst (_, (_, tys)), n), t) => |
775 else maps (fn ((constr as IConst (_, (_, tys)), n), t) => |
776 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t) |
776 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry (uncurry take) n tys) t) |
777 (constrs ~~ ts_clause); |
777 (constrs ~~ ts_clause); |
778 in ((t, ty), clauses) end; |
778 in ((t, ty), clauses) end; |
779 in |
779 in |
780 translate_const thy algbr eqngr thm c_ty |
780 translate_const thy algbr eqngr thm c_ty |
781 ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs |
781 ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs |
786 end |
786 end |
787 and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) = |
787 and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) = |
788 if length ts < num_args then |
788 if length ts < num_args then |
789 let |
789 let |
790 val k = length ts; |
790 val k = length ts; |
791 val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty; |
791 val tys = (curry (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty; |
792 val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context; |
792 val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context; |
793 val vs = Name.names ctxt "a" tys; |
793 val vs = Name.names ctxt "a" tys; |
794 in |
794 in |
795 fold_map (translate_typ thy algbr eqngr) tys |
795 fold_map (translate_typ thy algbr eqngr) tys |
796 ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs) |
796 ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs) |
797 #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) |
797 #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) |
798 end |
798 end |
799 else if length ts > num_args then |
799 else if length ts > num_args then |
800 translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts)) |
800 translate_case thy algbr eqngr thm case_scheme ((c, ty), (uncurry take) (num_args, ts)) |
801 ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts)) |
801 ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts)) |
802 #>> (fn (t, ts) => t `$$ ts) |
802 #>> (fn (t, ts) => t `$$ ts) |
803 else |
803 else |
804 translate_case thy algbr eqngr thm case_scheme ((c, ty), ts) |
804 translate_case thy algbr eqngr thm case_scheme ((c, ty), ts) |
805 and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) = |
805 and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) = |
806 case Code.get_case_scheme thy c |
806 case Code.get_case_scheme thy c |