650 if granularity_of_type_level level = All_Vars then |
650 if granularity_of_type_level level = All_Vars then |
651 Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, |
651 Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, |
652 level) |
652 level) |
653 else |
653 else |
654 raise Same.SAME |
654 raise Same.SAME |
655 | (Raw_Monomorphic, _) => raise Same.SAME |
655 | (poly as Raw_Polymorphic _, All_Types) => |
656 | (poly, All_Types) => |
656 Native (Higher_Order THF_With_Choice, poly, All_Types) |
657 Native (Higher_Order THF_With_Choice, poly, All_Types)) |
657 | _ => raise Same.SAME) |
658 | ("guards", (SOME poly, _)) => |
658 | ("guards", (SOME poly, _)) => |
659 if poly = Mangled_Monomorphic andalso |
659 if (poly = Mangled_Monomorphic andalso |
660 granularity_of_type_level level = Undercover_Vars then |
660 granularity_of_type_level level = Undercover_Vars) orelse |
|
661 poly = Type_Class_Polymorphic then |
661 raise Same.SAME |
662 raise Same.SAME |
662 else |
663 else |
663 Guards (poly, level) |
664 Guards (poly, level) |
664 | ("tags", (SOME poly, _)) => |
665 | ("tags", (SOME poly, _)) => |
665 if granularity_of_type_level level = Undercover_Vars then |
666 if granularity_of_type_level level = Undercover_Vars orelse |
|
667 poly = Type_Class_Polymorphic then |
666 raise Same.SAME |
668 raise Same.SAME |
667 else |
669 else |
668 Tags (poly, level) |
670 Tags (poly, level) |
669 | ("args", (SOME poly, All_Types (* naja *))) => |
671 | ("args", (SOME poly, All_Types (* naja *))) => |
670 Guards (poly, Const_Types false) |
672 if poly = Type_Class_Polymorphic then raise Same.SAME |
|
673 else Guards (poly, Const_Types false) |
671 | ("args", (SOME poly, Nonmono_Types (_, All_Vars) (* naja *))) => |
674 | ("args", (SOME poly, Nonmono_Types (_, All_Vars) (* naja *))) => |
672 if poly = Mangled_Monomorphic then raise Same.SAME |
675 if poly = Mangled_Monomorphic orelse |
673 else Guards (poly, Const_Types true) |
676 poly = Type_Class_Polymorphic then |
|
677 raise Same.SAME |
|
678 else |
|
679 Guards (poly, Const_Types true) |
674 | ("erased", (NONE, All_Types (* naja *))) => |
680 | ("erased", (NONE, All_Types (* naja *))) => |
675 Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) |
681 Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) |
676 | _ => raise Same.SAME) |
682 | _ => raise Same.SAME) |
677 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") |
683 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") |
678 |
684 |
679 fun adjust_order THF_Without_Choice (Higher_Order _) = |
685 fun adjust_order THF_Without_Choice (Higher_Order _) = |
680 Higher_Order THF_Without_Choice |
686 Higher_Order THF_Without_Choice |
681 | adjust_order _ type_enc = type_enc |
687 | adjust_order _ type_enc = type_enc |
682 |
688 |
|
689 fun no_type_classes Type_Class_Polymorphic = |
|
690 Raw_Polymorphic With_Phantom_Type_Vars |
|
691 | no_type_classes poly = poly |
|
692 |
683 fun adjust_type_enc (THF (Polymorphic, _, choice, _)) |
693 fun adjust_type_enc (THF (Polymorphic, _, choice, _)) |
684 (Native (order, poly, level)) = |
694 (Native (order, poly, level)) = |
685 Native (adjust_order choice order, poly, level) |
695 Native (adjust_order choice order, no_type_classes poly, level) |
686 | adjust_type_enc (THF (Monomorphic, _, choice, _)) |
696 | adjust_type_enc (THF (Monomorphic, _, choice, _)) |
687 (Native (order, _, level)) = |
697 (Native (order, _, level)) = |
688 Native (adjust_order choice order, Mangled_Monomorphic, level) |
698 Native (adjust_order choice order, Mangled_Monomorphic, level) |
689 | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) = |
699 | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) = |
690 Native (First_Order, Mangled_Monomorphic, level) |
700 Native (First_Order, Mangled_Monomorphic, level) |
691 | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) = |
701 | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) = |
692 Native (First_Order, poly, level) |
702 Native (First_Order, poly, level) |
693 | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) = |
703 | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) = |
694 Native (First_Order, Mangled_Monomorphic, level) |
704 Native (First_Order, Mangled_Monomorphic, level) |
695 | adjust_type_enc (TFF _) (Native (_, poly, level)) = |
705 | adjust_type_enc (TFF _) (Native (_, poly, level)) = |
696 Native (First_Order, poly, level) |
706 Native (First_Order, no_type_classes poly, level) |
697 | adjust_type_enc format (Native (_, poly, level)) = |
707 | adjust_type_enc format (Native (_, poly, level)) = |
698 adjust_type_enc format (Guards (poly, level)) |
708 adjust_type_enc format (Guards (no_type_classes poly, level)) |
699 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = |
709 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = |
700 (if is_type_enc_sound type_enc then Tags else Guards) stuff |
710 (if is_type_enc_sound type_enc then Tags else Guards) stuff |
701 | adjust_type_enc _ type_enc = type_enc |
711 | adjust_type_enc _ type_enc = type_enc |
702 |
712 |
703 fun is_fol_term t = |
713 fun is_fol_term t = |