Skip to content

Let premise introduction pass #213

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

Draft
DCupello1 wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

Let premise introduction pass #213

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
589bccc
Let introduction pass
DCupello1 Jan 13, 2026
6bd6632
Fix on improve ids related to let premise
DCupello1 Jan 13, 2026
5a6957b
Fix tests
DCupello1 Jan 13, 2026
0528be4
Merge branch 'main' into letintro-pass
DCupello1 Feb 19, 2026
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
5 changes: 5 additions & 0 deletions spectec/src/exe-spectec/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ type pass =
| AliasDemut
| ImproveIds
| Ite
| LetIntro

(* This list declares the intended order of passes.

Expand All @@ -37,6 +38,7 @@ flags on the command line.
let _skip_passes = [ Unthe ] (* Not clear how to extend them to indexed types *)
let all_passes = [
Ite;
LetIntro;
TypeFamilyRemoval;
Undep;
Totalize;
Expand Down Expand Up @@ -112,6 +114,7 @@ let pass_flag = function
| Uncaseremoval -> "uncase-removal"
| ImproveIds -> "improve-ids"
| Ite -> "ite"
| LetIntro -> "let-intro"

let pass_desc = function
| Sub -> "Synthesize explicit subtype coercions"
Expand All @@ -126,6 +129,7 @@ let pass_desc = function
| AliasDemut -> "Lifts type aliases out of mutual groups"
| ImproveIds -> "Disambiguates ids used from each other"
| Ite -> "If-then-else introduction"
| LetIntro -> "Let Premise introduction"


let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
Expand All @@ -141,6 +145,7 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
| AliasDemut -> Middlend.AliasDemut.transform
| ImproveIds -> Middlend.Improveids.transform
| Ite -> Middlend.Ite.transform
| LetIntro -> Middlend.Letintro.transform


(* Argument parsing *)
Expand Down
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 @@ -15,5 +15,6 @@
aliasDemut
improveids
ite
letintro
)
)
9 changes: 8 additions & 1 deletion spectec/src/middlend/improveids.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,12 @@ let t_inst tf env id inst =
)
) $ inst.at

(* Necessary to reset ids due to change on iterE *)
let t_prem prem =
{ prem with it = match prem.it with
| LetPr (e1, e2, _) -> LetPr (e1, e2, Free.Set.elements (Free.free_exp e1).varid)
| p -> p }

let transform_rule tf env rel_id rule =
(match rule.it with
| RuleD (id, quants, m, exp, prems) ->
Expand All @@ -168,7 +174,8 @@ let rec t_def env def =
let tf = { base_transformer with
transform_exp = t_exp env;
transform_typ = t_typ env;
transform_path = t_path env;
transform_path = t_path env;
transform_prem = t_prem;
transform_var_id = t_var_id env;
transform_typ_id = t_user_def_id env;
transform_rel_id = t_user_def_id env;
Expand Down
72 changes: 72 additions & 0 deletions spectec/src/middlend/letintro.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
open Il.Ast
open Util.Source
open Il
open Il.Walk

let construct_let_prem exp1 exp2 at =
LetPr (exp1, exp2, Free.Set.elements (Free.free_exp exp1).varid) $ at

let diff = Free.Set.diff
let union = Free.Set.union
let empty = Free.Set.empty

let valid_exp exp =
let continue = true in
let validity =
match exp.it with
| StrE _
| TupE _
| CaseE _
| IterE _
| VarE _ -> true
| _ -> false
in
(validity, continue)

let inferrable_exp exp =
let continue = true in
let validity =
match exp.it with
(* OptE (for some reason) and StrE can never have their types inferred *)
| OptE _
| StrE _ -> false
| _ -> true
in
(validity, continue)

let t_prems free_vars_start prems =
let valid_lhs_checker = { forall_base_checker with collect_exp = valid_exp } in
let valid_rhs_checker = { forall_base_checker with collect_exp = inferrable_exp } in
List.fold_left ( fun (free, prev_prems) p ->
let free_vars = (Free.free_prem p).varid in
match p.it with
| IfPr {it = CmpE (`EqOp, _, exp1, exp2); _}
when diff (Free.free_exp exp1).varid free <> empty &&
diff (Free.free_exp exp2).varid free = empty &&
collect_exp valid_lhs_checker exp1 &&
collect_exp valid_rhs_checker exp2 ->
(union free free_vars, construct_let_prem exp1 exp2 p.at :: prev_prems)
| IfPr {it = CmpE (`EqOp, _, exp1, exp2); _}
when diff (Free.free_exp exp1).varid free = empty &&
diff (Free.free_exp exp2).varid free <> empty &&
collect_exp valid_lhs_checker exp2 &&
collect_exp valid_rhs_checker exp1 ->
(union free free_vars, construct_let_prem exp2 exp1 p.at :: prev_prems)
| _ -> (union free free_vars, p :: prev_prems)
) (free_vars_start, []) prems |>
snd |>
List.rev

let t_clause c =
let { it = DefD (binds, args, exp, prems); _} = c in
let free_vars = (Free.free_list Free.free_arg args).varid in
{ c with it = DefD (binds, args, exp, t_prems free_vars prems) }

let rec t_def d =
match d.it with
| DecD (id, params, typ, clauses) ->
{ d with it = DecD (id, params, typ, List.map t_clause clauses) }
| RecD defs -> RecD (List.map t_def defs) $ d.at
| _ -> d

let transform defs = List.map t_def defs
1 change: 1 addition & 0 deletions spectec/src/middlend/letintro.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
21 changes: 11 additions & 10 deletions spectec/test-middlend/dune.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
(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-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-uncase-removal.il specification.act/06-uncase-removal.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/07-sideconditions.il specification.act/07-sideconditions.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/08-sub-expansion.il specification.act/08-sub-expansion.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/09-sub.il specification.act/09-sub.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/10-alias-demut.il specification.act/10-alias-demut.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/11-improve-ids.il specification.act/11-improve-ids.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/02-let-intro.il specification.act/02-let-intro.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/03-typefamily-removal.il specification.act/03-typefamily-removal.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/04-remove-indexed-types.il specification.act/04-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/05-totalize.il specification.act/05-totalize.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/06-else.il specification.act/06-else.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/07-uncase-removal.il specification.act/07-uncase-removal.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/08-sideconditions.il specification.act/08-sideconditions.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/09-sub-expansion.il specification.act/09-sub-expansion.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/10-sub.il specification.act/10-sub.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/11-alias-demut.il specification.act/11-alias-demut.il))))
(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/12-improve-ids.il specification.act/12-improve-ids.il))))
Loading