578 in |
578 in |
579 translation_error thy permissive some_thm "Wellsortedness error" |
579 translation_error thy permissive some_thm "Wellsortedness error" |
580 (err_typ ^ "\n" ^ err_class) |
580 (err_typ ^ "\n" ^ err_class) |
581 end; |
581 end; |
582 |
582 |
|
583 |
583 (* inference of type annotations for disambiguation with type classes *) |
584 (* inference of type annotations for disambiguation with type classes *) |
584 |
585 |
585 fun mk_tagged_type (true, T) = Type ("", [T]) |
586 fun mk_tagged_type (true, T) = Type ("", [T]) |
586 | mk_tagged_type (false, T) = T |
587 | mk_tagged_type (false, T) = T; |
587 |
588 |
588 fun dest_tagged_type (Type ("", [T])) = (true, T) |
589 fun dest_tagged_type (Type ("", [T])) = (true, T) |
589 | dest_tagged_type T = (false, T) |
590 | dest_tagged_type T = (false, T); |
590 |
591 |
591 val untag_term = map_types (snd o dest_tagged_type) |
592 val untag_term = map_types (snd o dest_tagged_type); |
592 |
593 |
593 fun tag_term (proj_sort, _) eqngr = |
594 fun tag_term (proj_sort, _) eqngr = |
594 let |
595 let |
595 val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr |
596 val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr; |
596 fun tag (Const (c', T')) (Const (c, T)) = |
597 fun tag (Const (c', T')) (Const (c, T)) = |
597 Const (c, |
598 Const (c, |
598 mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T)) |
599 mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T)) |
599 | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u |
600 | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u |
600 | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t) |
601 | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t) |
601 | tag (Free _) (t as Free _) = t |
602 | tag (Free _) (t as Free _) = t |
602 | tag (Var _) (t as Var _) = t |
603 | tag (Var _) (t as Var _) = t |
603 | tag (Bound _) (t as Bound _) = t |
604 | tag (Bound _) (t as Bound _) = t; |
604 in |
605 in |
605 tag |
606 tag |
606 end |
607 end |
607 |
608 |
608 fun annotate thy algbr eqngr (c, ty) args rhs = |
609 fun annotate thy algbr eqngr (c, ty) args rhs = |
617 end |
618 end |
618 |
619 |
619 fun annotate_eqns thy algbr eqngr (c, ty) eqns = |
620 fun annotate_eqns thy algbr eqngr (c, ty) eqns = |
620 map (apfst (fn (args, (rhs, some_abs)) => (args, |
621 map (apfst (fn (args, (rhs, some_abs)) => (args, |
621 (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns |
622 (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns |
|
623 |
622 |
624 |
623 (* translation *) |
625 (* translation *) |
624 |
626 |
625 fun ensure_tyco thy algbr eqngr permissive tyco = |
627 fun ensure_tyco thy algbr eqngr permissive tyco = |
626 let |
628 let |
780 let |
782 let |
781 fun arg_types num_args ty = fst (chop num_args (binder_types ty)); |
783 fun arg_types num_args ty = fst (chop num_args (binder_types ty)); |
782 val tys = arg_types num_args (snd c_ty); |
784 val tys = arg_types num_args (snd c_ty); |
783 val ty = nth tys t_pos; |
785 val ty = nth tys t_pos; |
784 fun mk_constr NONE t = NONE |
786 fun mk_constr NONE t = NONE |
785 | mk_constr (SOME c) t = let val n = Code.args_number thy c |
787 | mk_constr (SOME c) t = |
786 in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end; |
788 let |
787 |
789 val n = Code.args_number thy c; |
788 val constrs = if null case_pats then [] |
790 in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end; |
789 else map2 mk_constr case_pats (nth_drop t_pos ts); |
791 val constrs = |
790 val constrs' = map_filter I constrs |
792 if null case_pats then [] |
791 |
793 else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts)); |
792 fun casify naming constrs ty ts = |
794 fun casify naming constrs ty ts = |
793 let |
795 let |
794 val undefineds = map_filter (lookup_const naming) (Code.undefineds thy); |
796 val undefineds = map_filter (lookup_const naming) (Code.undefineds thy); |
795 fun collapse_clause vs_map ts body = |
797 fun collapse_clause vs_map ts body = |
796 let |
798 let |
819 val ts_clause = nth_drop t_pos ts; |
821 val ts_clause = nth_drop t_pos ts; |
820 val clauses = if null case_pats |
822 val clauses = if null case_pats |
821 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) |
823 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) |
822 else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) => |
824 else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) => |
823 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t) |
825 mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t) |
824 (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause))); |
826 (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) |
|
827 (case_pats ~~ ts_clause))); |
825 in ((t, ty), clauses) end; |
828 in ((t, ty), clauses) end; |
826 in |
829 in |
827 translate_const thy algbr eqngr permissive some_thm (c_ty, NONE) |
830 translate_const thy algbr eqngr permissive some_thm (c_ty, NONE) |
828 ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE) |
831 ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE) |
829 #>> rpair n) constrs' |
832 #>> rpair n) constrs |
830 ##>> translate_typ thy algbr eqngr permissive ty |
833 ##>> translate_typ thy algbr eqngr permissive ty |
831 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts |
834 ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts |
832 #-> (fn (((t, constrs), ty), ts) => |
835 #-> (fn (((t, constrs), ty), ts) => |
833 `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts))) |
836 `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts))) |
834 end |
837 end |