118 case try_unsuffixes ["!", "_bang"] s of |
118 case try_unsuffixes ["!", "_bang"] s of |
119 SOME s => (Finite_Types, s) |
119 SOME s => (Finite_Types, s) |
120 | NONE => (All_Types, s)) |
120 | NONE => (All_Types, s)) |
121 ||> apsnd (fn s => |
121 ||> apsnd (fn s => |
122 case try (unsuffix "_heavy") s of |
122 case try (unsuffix "_heavy") s of |
123 SOME s => (SOME Heavy, s) |
123 SOME s => (Heavy, s) |
124 | NONE => |
124 | NONE => (Light, s)) |
125 case try (unsuffix "_light") s of |
|
126 SOME s => (SOME Light, s) |
|
127 | NONE => (NONE, s)) |
|
128 |> (fn (poly, (level, (heaviness, core))) => |
125 |> (fn (poly, (level, (heaviness, core))) => |
129 case (core, (poly, level, heaviness)) of |
126 case (core, (poly, level, heaviness)) of |
130 ("simple_types", (NONE, _, NONE)) => Simple_Types level |
127 ("simple_types", (NONE, _, Light)) => Simple_Types level |
131 | ("preds", (SOME Polymorphic, _, _)) => |
128 | ("preds", (SOME Polymorphic, _, _)) => |
132 if level = All_Types then |
129 if level = All_Types then Preds (Polymorphic, level, heaviness) |
133 Preds (Polymorphic, level, heaviness |> the_default Light) |
130 else raise Same.SAME |
134 else |
131 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) |
135 raise Same.SAME |
|
136 | ("preds", (SOME poly, _, _)) => |
|
137 Preds (poly, level, heaviness |> the_default Light) |
|
138 | ("tags", (SOME Polymorphic, All_Types, _)) => |
132 | ("tags", (SOME Polymorphic, All_Types, _)) => |
139 Tags (Polymorphic, All_Types, heaviness |> the_default Light) |
133 Tags (Polymorphic, All_Types, heaviness) |
140 | ("tags", (SOME Polymorphic, Finite_Types, _)) => |
134 | ("tags", (SOME Polymorphic, Finite_Types, _)) => |
141 if heaviness = SOME Light then raise Same.SAME |
135 (* The light encoding yields too many unsound proofs. *) |
142 else Tags (Polymorphic, Finite_Types, Heavy) |
136 Tags (Polymorphic, Finite_Types, Heavy) |
143 | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME |
137 | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME |
144 | ("tags", (SOME poly, _, _)) => |
138 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) |
145 Tags (poly, level, heaviness |> the_default Light) |
139 | ("args", (SOME poly, All_Types (* naja *), Light)) => |
146 | ("args", (SOME poly, All_Types (* naja *), NONE)) => |
|
147 Preds (poly, Const_Arg_Types, Light) |
140 Preds (poly, Const_Arg_Types, Light) |
148 | ("erased", (NONE, All_Types (* naja *), NONE)) => |
141 | ("erased", (NONE, All_Types (* naja *), Light)) => |
149 Preds (Polymorphic, No_Types, Light) |
142 Preds (Polymorphic, No_Types, Light) |
150 | _ => raise Same.SAME) |
143 | _ => raise Same.SAME) |
151 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") |
144 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") |
152 |
145 |
153 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic |
146 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic |