Uncase removal pass

spectec/src/exe-spectec/main.ml

@@ -22,6 +22,7 @@ type pass =
   | TypeFamilyRemoval
   | Else
   | Undep
+  | Uncaseremoval
   | AliasDemut
 
 (* This list declares the intended order of passes.
@@ -31,7 +32,7 @@ passers (--all-passes, some targets), we do _not_ want to use the order of
 flags on the command line.
 *)
 let _skip_passes = [ Unthe ]  (* Not clear how to extend them to indexed types *)
-let all_passes = [ TypeFamilyRemoval; Undep; Totalize; Else; Sideconditions; Sub; AliasDemut ]
+let all_passes = [ TypeFamilyRemoval; Undep; Totalize; Else; Uncaseremoval; Sideconditions; Sub; AliasDemut ]
 
 type file_kind =
   | Spec
@@ -92,6 +93,7 @@ let pass_flag = function
   | AliasDemut -> "alias-demut"
   | Else -> "else"
   | Undep -> "remove-indexed-types"
+  | Uncaseremoval -> "uncase-removal"
 
 let pass_desc = function
   | Sub -> "Synthesize explicit subtype coercions"
@@ -101,6 +103,7 @@ let pass_desc = function
   | TypeFamilyRemoval -> "Transform Type families into sum types"
   | Else -> "Eliminate the otherwise premise in relations"
   | Undep -> "Transform indexed types into types with well-formedness predicates"
+  | Uncaseremoval -> "Eliminate the uncase expression"
   | AliasDemut -> "Lifts type aliases out of mutual groups"
 
 
@@ -112,6 +115,7 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | TypeFamilyRemoval -> Middlend.Typefamilyremoval.transform
   | Else -> Middlend.Else.transform
   | Undep -> Middlend.Undep.transform
+  | Uncaseremoval -> Middlend.Uncaseremoval.transform
   | AliasDemut -> Middlend.AliasDemut.transform
 
 

spectec/src/middlend/dune

@@ -10,6 +10,7 @@
     else
     undep
     utils
+    uncaseremoval
     aliasDemut
   )
 )