Skip to content

Add if-then-else introduction IL pass #211

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nomeata merged 5 commits into from
Dec 3, 2025
Merged

Add if-then-else introduction IL pass #211

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c056eed
Add Ite-introduction pass
nomeata Nov 23, 2025
bf27487
Run CI on all PRs
nomeata Nov 23, 2025
98d965f
Fix pass comment
nomeata Nov 23, 2025
b6df6cf
Wrap list of all passes for easier merging
nomeata Dec 1, 2025
9aeb906
Handle NegPr
nomeata Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .github/workflows/ci-spectec.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ on:
paths: [ spectec/**, document/** ]

pull_request:
branches: [ main ]
paths: [ spectec/**, document/** ]

# Allows you to run this workflow manually from the Actions tab
Expand Down
15 changes: 14 additions & 1 deletion spectec/src/exe-spectec/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ type pass =
| Else
| Undep
| AliasDemut
| Ite

(* This list declares the intended order of passes.

Expand All @@ -31,7 +32,16 @@ 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 = [
Ite;
TypeFamilyRemoval;
Undep;
Totalize;
Else;
Sideconditions;
Sub;
AliasDemut;
]

type file_kind =
| Spec
Expand Down Expand Up @@ -92,6 +102,7 @@ let pass_flag = function
| AliasDemut -> "alias-demut"
| Else -> "else"
| Undep -> "remove-indexed-types"
| Ite -> "ite"

let pass_desc = function
| Sub -> "Synthesize explicit subtype coercions"
Expand All @@ -102,6 +113,7 @@ let pass_desc = function
| Else -> "Eliminate the otherwise premise in relations"
| Undep -> "Transform indexed types into types with well-formedness predicates"
| AliasDemut -> "Lifts type aliases out of mutual groups"
| Ite -> "If-then-else introduction"


let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
Expand All @@ -113,6 +125,7 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
| Else -> Middlend.Else.transform
| Undep -> Middlend.Undep.transform
| AliasDemut -> Middlend.AliasDemut.transform
| Ite -> Middlend.Ite.transform


(* Argument parsing *)
Expand Down
7 changes: 7 additions & 0 deletions spectec/src/il/eq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,3 +155,10 @@ and eq_arg a1 a2 =
| DefA id1, DefA id2 -> eq_id id1 id2
| GramA g1, GramA g2 -> eq_sym g1 g2
| _, _ -> false

and eq_bind b1 b2 =
match b1.it, b2.it with
| ExpB (id1, t1), ExpB (id2, t2) ->
eq_id id1 id2 && eq_typ t1 t2
| TypB id1, TypB id2 -> eq_id id1 id2
| _ -> false (* unsupported *)
1 change: 1 addition & 0 deletions spectec/src/il/eq.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ val eq_path : path -> path -> bool
val eq_sym : sym -> sym -> bool
val eq_prem : prem -> prem -> bool
val eq_arg : arg -> arg -> bool
val eq_bind : bind -> bind -> bool

val eq_opt : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
val eq_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
1 change: 1 addition & 0 deletions spectec/src/middlend/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,5 +11,6 @@
undep
utils
aliasDemut
ite
)
)
113 changes: 113 additions & 0 deletions spectec/src/middlend/ite.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
(*
This pass recongizes when multiple subsequent clauses of a definition share the pattern and have
only boolean premises, and rewrites that to a single clause using if-then-else on the right-hand side.
*)

open Util
open Source
open Il.Ast

(* Errors *)

(* let error at msg = Error.error at "if-then-else introduction" msg *)

let clauses_have_same_args (c1 : clause) (c2 : clause) =
Copy link

@DCupello1 DCupello1 Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would we maybe want a little weaker of a condition? (i.e. if the preceding clause pattern matches to the next clause)

i.e for a function as such:

def $foo(nat) : nat
def $foo(5) = 10
  -- if cond
def $foo(n) = 20

Could technically group up as well. (But would need to add n = 5 to the condition)

Though this might be too tricky for such a pass.

Copy link
Author

@nomeata nomeata Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right, I thought about this, but didn't necessarily want it in the first version. I would actually say that should be a separate pass that runs first, an overlap-removal pass, after which all patterns are either the same or clearly apart. This would compose well, I think.

match (c1.it, c2.it) with
| (DefD (binds1, args1, _, _), DefD (binds2, args2, _, _)) ->
Il.Eq.eq_list Il.Eq.eq_bind binds1 binds2 &&
Il.Eq.eq_list Il.Eq.eq_arg args1 args2

let group_clauses_by_same_args clauses =
let group_helper acc clause =
match acc with
| [] -> [[clause]]
| group :: rest ->
let representative = List.hd group in
if clauses_have_same_args representative clause then
(group @ [clause]) :: rest
else
[clause] :: group :: rest
in
List.fold_left group_helper [] clauses |> List.rev

let is_else_premise prem =
match prem.it with
| ElsePr -> true
| _ -> false

let has_only_else_premise clause =
match clause.it with
| DefD (_, _, _, ([_] as prems)) ->
List.for_all is_else_premise prems
| _ -> false

let mk_and : exp -> exp -> exp = fun e1 e2 ->
BinE (`AndOp, `BoolT, e1, e2) $$ (no_region, BoolT $ no_region)

let rec prem_to_bool_exp (prem : prem) : exp option =
match prem.it with
| IfPr exp -> Some exp
| NegPr prem' ->
Option.bind (prem_to_bool_exp prem') (fun exp ->
Some (UnE (`NotOp, `BoolT, exp) $$ (prem.at, BoolT $ no_region)))
| _ -> None

and prems_to_bool_exp = function
| [] -> Some (BoolE true $$ (no_region, BoolT $ no_region))
| [prem] -> prem_to_bool_exp prem
| prem :: rest ->
Option.bind (prem_to_bool_exp prem) (fun exp1 ->
Option.bind (prems_to_bool_exp rest) (fun exp2 ->
Some (mk_and exp1 exp2)
)
)

let clause_prems_to_bool_exp (clause : clause) : exp option =
match clause.it with
| DefD (_, _, _, prems) ->
prems_to_bool_exp prems

let mk_if (cond : exp) (then_exp : exp) (else_exp : exp) : exp =
IfE (cond, then_exp, else_exp) $$ (no_region, then_exp.note)

let rec t_clause_group_to_expr (clauses : clause list) : exp option =
match clauses with
| [] -> None
| [clause] ->
if has_only_else_premise clause then
match clause.it with
| DefD (_, _, rhs, _) -> Some rhs
else
None
| clause :: rest_clauses ->
match clause_prems_to_bool_exp clause with
| None -> None
| Some cond ->
match clause.it with
| DefD (_, _, rhs, _) ->
match t_clause_group_to_expr rest_clauses with
| None -> None
| Some else_exp -> Some (mk_if cond rhs else_exp)

let t_clause_group (clauses : clause list) : clause list =
match t_clause_group_to_expr clauses with
| None -> clauses
| Some exp ->
let rep = List.hd clauses in
let DefD (binds, args, _rhs, _prems) = rep.it in
[{ rep with it = DefD (binds, args, exp, []) }]


let t_clauses clauses =
List.concat_map t_clause_group (group_clauses_by_same_args clauses)

let rec t_def (def : def) : def = { def with it = t_def' def.it }
and t_def' = function
| RecD defs ->
RecD (List.map t_def defs)
| DecD (id, params, typ, clauses) ->
DecD (id, params, typ, t_clauses clauses)
| def -> def

let transform (defs : script) : script =
List.map t_def defs
1 change: 1 addition & 0 deletions spectec/src/middlend/ite.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
val transform : Il.Ast.script -> Il.Ast.script
15 changes: 8 additions & 7 deletions spectec/test-middlend/dune.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/00-elab.il specification.act/00-elab.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/01-typefamily-removal.il specification.act/01-typefamily-removal.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/02-remove-indexed-types.il specification.act/02-remove-indexed-types.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/03-totalize.il specification.act/03-totalize.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/04-else.il specification.act/04-else.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/05-sideconditions.il specification.act/05-sideconditions.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/06-sub.il specification.act/06-sub.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/07-alias-demut.il specification.act/07-alias-demut.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/01-ite.il specification.act/01-ite.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/02-typefamily-removal.il specification.act/02-typefamily-removal.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/03-remove-indexed-types.il specification.act/03-remove-indexed-types.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/04-totalize.il specification.act/04-totalize.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/05-else.il specification.act/05-else.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/06-sideconditions.il specification.act/06-sideconditions.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/07-sub.il specification.act/07-sub.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/08-alias-demut.il specification.act/08-alias-demut.il))))
Loading
Loading