569 |
569 |
570 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true |
570 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true |
571 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true |
571 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true |
572 | is_type_level_monotonicity_based _ = false |
572 | is_type_level_monotonicity_based _ = false |
573 |
573 |
|
574 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and |
|
575 Mirabelle. *) |
|
576 val queries = ["?", "_query"] |
|
577 val bangs = ["!", "_bang"] |
|
578 val ats = ["@", "_at"] |
|
579 |
574 fun try_unsuffixes ss s = |
580 fun try_unsuffixes ss s = |
575 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE |
581 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE |
576 |
582 |
577 val queries = ["?", "_query"] |
583 fun try_nonmono constr suffixes fallback s = |
578 val bangs = ["!", "_bang"] |
584 case try_unsuffixes suffixes s of |
|
585 SOME s => |
|
586 (case try_unsuffixes suffixes s of |
|
587 SOME s => (constr Ann_Light, s) |
|
588 | NONE => |
|
589 case try_unsuffixes ats s of |
|
590 SOME s => (constr Arg_Light, s) |
|
591 | NONE => (constr Heavy, s)) |
|
592 | NONE => fallback s |
579 |
593 |
580 fun type_enc_from_string soundness s = |
594 fun type_enc_from_string soundness s = |
581 (case try (unprefix "poly_") s of |
595 (case try (unprefix "poly_") s of |
582 SOME s => (SOME Polymorphic, s) |
596 SOME s => (SOME Polymorphic, s) |
583 | NONE => |
597 | NONE => |
585 SOME s => (SOME Raw_Monomorphic, s) |
599 SOME s => (SOME Raw_Monomorphic, s) |
586 | NONE => |
600 | NONE => |
587 case try (unprefix "mono_") s of |
601 case try (unprefix "mono_") s of |
588 SOME s => (SOME Mangled_Monomorphic, s) |
602 SOME s => (SOME Mangled_Monomorphic, s) |
589 | NONE => (NONE, s)) |
603 | NONE => (NONE, s)) |
590 ||> (fn s => |
604 ||> (pair All_Types |
591 (* "_query" and "_bang" are for the ASCII-challenged Metis and |
605 |> try_nonmono Fin_Nonmono_Types bangs |
592 Mirabelle. *) |
606 |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries) |
593 case try_unsuffixes queries s of |
|
594 SOME s => |
|
595 (case try_unsuffixes queries s of |
|
596 SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s) |
|
597 | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s)) |
|
598 | NONE => |
|
599 case try_unsuffixes bangs s of |
|
600 SOME s => |
|
601 (case try_unsuffixes bangs s of |
|
602 SOME s => (Fin_Nonmono_Types Ann_Light, s) |
|
603 | NONE => (Fin_Nonmono_Types Heavy, s)) |
|
604 | NONE => (All_Types, s)) |
|
605 |> (fn (poly, (level, core)) => |
607 |> (fn (poly, (level, core)) => |
606 case (core, (poly, level)) of |
608 case (core, (poly, level)) of |
607 ("simple", (SOME poly, _)) => |
609 ("simple", (SOME poly, _)) => |
608 (case (poly, level) of |
610 (case (poly, level) of |
609 (Polymorphic, All_Types) => |
611 (Polymorphic, All_Types) => |
631 | ("args", (SOME poly, All_Types (* naja *))) => |
633 | ("args", (SOME poly, All_Types (* naja *))) => |
632 Guards (poly, Const_Arg_Types) |
634 Guards (poly, Const_Arg_Types) |
633 | ("erased", (NONE, All_Types (* naja *))) => |
635 | ("erased", (NONE, All_Types (* naja *))) => |
634 Guards (Polymorphic, No_Types) |
636 Guards (Polymorphic, No_Types) |
635 | _ => raise Same.SAME) |
637 | _ => raise Same.SAME) |
636 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") |
638 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") |
637 |
639 |
638 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _)) |
640 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _)) |
639 (Simple_Types (order, _, level)) = |
641 (Simple_Types (order, _, level)) = |
640 Simple_Types (order, Mangled_Monomorphic, level) |
642 Simple_Types (order, Mangled_Monomorphic, level) |
641 | adjust_type_enc (THF _) type_enc = type_enc |
643 | adjust_type_enc (THF _) type_enc = type_enc |