Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
cbef072
export variable type
kavigupta Aug 19, 2025
d0ffdce
add variable types to invention
kavigupta Aug 19, 2025
635129d
update
kavigupta Aug 19, 2025
d6d4c10
add from_compression_output
kavigupta Aug 19, 2025
f474a3f
use types here too
kavigupta Aug 19, 2025
5b49838
add field
kavigupta Aug 19, 2025
25d0354
add type constraints to variabletype
kavigupta Aug 19, 2025
eaa317c
imports
kavigupta Aug 19, 2025
f9b528b
add type of ivar to tracking
kavigupta Aug 19, 2025
f6da2fa
don't include in tracking
kavigupta Aug 19, 2025
0a1c1de
extract function to load an invention from json
kavigupta Aug 19, 2025
41c0122
Merge branch 'extract-loading-invention' into export-variable-type
kavigupta Aug 19, 2025
2afdb4b
clean
kavigupta Aug 19, 2025
8bfa0cd
add variable type outputs
kavigupta Aug 19, 2025
2d55f62
Merge remote-tracking branch 'origin/main' into export-variable-type
kavigupta Aug 19, 2025
31b7057
render variable types
kavigupta Aug 19, 2025
8651a8a
Merge remote-tracking branch 'origin/main' into export-variable-type
kavigupta Aug 19, 2025
5abf8d9
actually use follow types
kavigupta Aug 19, 2025
693d0fc
add test for symbol following
kavigupta Aug 19, 2025
7b00d60
Merge remote-tracking branch 'origin/main' into export-variable-type
kavigupta Aug 19, 2025
cc44770
Merge branch 'export-variable-type' into actually-use-follow-types
kavigupta Aug 19, 2025
6a5425f
add expected outputs
kavigupta Aug 19, 2025
c949f3c
actually use follow types (#261)
kavigupta Aug 19, 2025
8f99a58
Revert "actually use follow types (#261)"
kavigupta Aug 19, 2025
4ec2016
Merge branch 'export-variable-type' into actually-use-follow-types
kavigupta Aug 19, 2025
85c080c
bump
kavigupta Aug 19, 2025
e158157
bump
kavigupta Aug 19, 2025
20c835c
check the variable type outputs in addition to other stuff
kavigupta Aug 19, 2025
5ecb8f1
Merge branch 'export-variable-type' into actually-use-follow-types
kavigupta Aug 19, 2025
d72f534
add rewrite check to some experimentns
kavigupta Aug 29, 2025
a7ec637
Merge branch 'add-rewrite-check-to-some-experiments' into actually-us…
kavigupta Aug 29, 2025
a5742ab
update
kavigupta Aug 29, 2025
d2465d7
add relevant rewrite checks
kavigupta Aug 29, 2025
77c701c
Merge remote-tracking branch 'origin/main' into actually-use-follow-t…
kavigupta Sep 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
122 changes: 122 additions & 0 deletions data/expected_outputs/symbol-reuse-ssm.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
{
"cmd": "/home/kavi/mit/stitch/target/debug/deps/integration_tests-6cddd9da19e4976e symbols_following",
"args": {
"iterations": 1,
"abstraction_prefix": "fn_",
"previous_abstractions": 0,
"shuffle": false,
"truncate": null,
"no_opt": false,
"silent": false,
"verbose_rewrite": false,
"step": {
"max_arity": 6,
"threads": 1,
"no_stats": false,
"batch": 1,
"dynamic_batch": false,
"eta_long": false,
"no_curried_metavars": false,
"no_curried_bodies": false,
"inv_candidates": 1,
"hole_choice": "DepthFirst",
"cost": {
"cost_lam": 1,
"cost_app": 1,
"cost_var": 100,
"cost_ivar": 100,
"cost_prim_default": 100,
"cost_prim": "{}"
},
"no_mismatch_check": false,
"follow": "(+ 1 #2 #2 #1 #0 2 3 4)",
"follow_types": [
"Symvar",
"Symvar",
"Metavar"
],
"follow_prune": false,
"verbose_worklist": false,
"verbose_best": false,
"print_stats": 0,
"show_rewritten": false,
"rewritten_dreamcoder": false,
"rewritten_intermediates": false,
"inv_arg_cap": false,
"allow_single_task": false,
"no_opt_single_use": false,
"no_opt_upper_bound": false,
"no_opt_force_multiuse": false,
"no_opt_useless_abstract": false,
"no_opt_arity_zero": false,
"no_other_util": false,
"structure_penalty": 1.0,
"rewrite_check": false,
"utility_by_rewrite": false,
"dreamcoder_comparison": false,
"quiet": false,
"fused_lambda_tags": {
"tags": null
},
"tdfa": {
"tdfa_json_path": null,
"tdfa_root": null,
"valid_metavars": null,
"valid_roots": null,
"tdfa_non_eta_long_states": null,
"tdfa_split": null
},
"symvar": {
"symvar_prefix": "&"
}
}
},
"original_cost": 2724,
"final_cost": 1209,
"compression_ratio": 2.2531017369727047,
"num_abstractions": 1,
"original": [
"(+ 1 &x &x &y &z 2 3 4)",
"(+ 1 &y &y &x &z 2 3 4)",
"(+ 1 &x &x &x &z 2 3 4)"
],
"rewritten": [
"(fn_0 &z &y &x)",
"(fn_0 &z &x &y)",
"(fn_0 &z &x &x)"
],
"rewritten_dreamcoder": null,
"abstractions": [
{
"body": "(+ 1 #2 #2 #1 #0 2 3 4)",
"dreamcoder": "#(lambda (lambda (lambda (+ 1 $0 $0 $1 $2 2 3 4))))",
"arity": 3,
"name": "fn_0",
"utility": 1007,
"final_cost": 1209,
"compression_ratio": 2.2531017369727047,
"cumulative_compression_ratio": 2.2531017369727047,
"num_uses": 3,
"rewritten": null,
"rewritten_dreamcoder": null,
"uses": [
{
"fn_0 &z &x &x": "(+ 1 &x &x &x &z 2 3 4)"
},
{
"fn_0 &z &y &x": "(+ 1 &x &x &y &z 2 3 4)"
},
{
"fn_0 &z &x &y": "(+ 1 &y &y &x &z 2 3 4)"
}
],
"dc_comparison_millis": null,
"tdfa_annotation": null,
"variable_types": [
"S",
"M",
"M"
]
}
]
}
122 changes: 122 additions & 0 deletions data/expected_outputs/symbol-reuse-sss.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
{
"cmd": "/home/kavi/mit/stitch/target/debug/deps/integration_tests-6cddd9da19e4976e symbols_following",
"args": {
"iterations": 1,
"abstraction_prefix": "fn_",
"previous_abstractions": 0,
"shuffle": false,
"truncate": null,
"no_opt": false,
"silent": false,
"verbose_rewrite": false,
"step": {
"max_arity": 6,
"threads": 1,
"no_stats": false,
"batch": 1,
"dynamic_batch": false,
"eta_long": false,
"no_curried_metavars": false,
"no_curried_bodies": false,
"inv_candidates": 1,
"hole_choice": "DepthFirst",
"cost": {
"cost_lam": 1,
"cost_app": 1,
"cost_var": 100,
"cost_ivar": 100,
"cost_prim_default": 100,
"cost_prim": "{}"
},
"no_mismatch_check": false,
"follow": "(+ 1 #2 #2 #1 #0 2 3 4)",
"follow_types": [
"Symvar",
"Symvar",
"Symvar"
],
"follow_prune": false,
"verbose_worklist": false,
"verbose_best": false,
"print_stats": 0,
"show_rewritten": false,
"rewritten_dreamcoder": false,
"rewritten_intermediates": false,
"inv_arg_cap": false,
"allow_single_task": false,
"no_opt_single_use": false,
"no_opt_upper_bound": false,
"no_opt_force_multiuse": false,
"no_opt_useless_abstract": false,
"no_opt_arity_zero": false,
"no_other_util": false,
"structure_penalty": 1.0,
"rewrite_check": false,
"utility_by_rewrite": false,
"dreamcoder_comparison": false,
"quiet": false,
"fused_lambda_tags": {
"tags": null
},
"tdfa": {
"tdfa_json_path": null,
"tdfa_root": null,
"valid_metavars": null,
"valid_roots": null,
"tdfa_non_eta_long_states": null,
"tdfa_split": null
},
"symvar": {
"symvar_prefix": "&"
}
}
},
"original_cost": 2724,
"final_cost": 1209,
"compression_ratio": 2.2531017369727047,
"num_abstractions": 1,
"original": [
"(+ 1 &x &x &y &z 2 3 4)",
"(+ 1 &y &y &x &z 2 3 4)",
"(+ 1 &x &x &x &z 2 3 4)"
],
"rewritten": [
"(fn_0 &z &y &x)",
"(fn_0 &z &x &y)",
"(fn_0 &z &x &x)"
],
"rewritten_dreamcoder": null,
"abstractions": [
{
"body": "(+ 1 #2 #2 #1 #0 2 3 4)",
"dreamcoder": "#(lambda (lambda (lambda (+ 1 $0 $0 $1 $2 2 3 4))))",
"arity": 3,
"name": "fn_0",
"utility": 1007,
"final_cost": 1209,
"compression_ratio": 2.2531017369727047,
"cumulative_compression_ratio": 2.2531017369727047,
"num_uses": 3,
"rewritten": null,
"rewritten_dreamcoder": null,
"uses": [
{
"fn_0 &z &x &x": "(+ 1 &x &x &x &z 2 3 4)"
},
{
"fn_0 &z &y &x": "(+ 1 &x &x &y &z 2 3 4)"
},
{
"fn_0 &z &x &y": "(+ 1 &y &y &x &z 2 3 4)"
}
],
"dc_comparison_millis": null,
"tdfa_annotation": null,
"variable_types": [
"S",
"M",
"M"
]
}
]
}
2 changes: 2 additions & 0 deletions src/compression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -656,6 +656,7 @@ pub struct SharedData {
pub multistep_cfg: MultistepCompressionConfig,
pub tracking: Option<Tracking>,
pub fused_lambda_tags: Option<FxHashSet<Tag>>,
pub follow: Option<Invention>,
}

pub fn invalid_metavar_location(shared : &SharedData, node: Idx) -> bool {
Expand Down Expand Up @@ -2137,6 +2138,7 @@ pub fn construct_shared(
multistep_cfg: multistep_cfg.clone(),
tracking,
fused_lambda_tags: fused_copy,
follow: follow.clone(),
});

if !shared.cfg.quiet { println!("built SharedData: {:?}ms", tstart.elapsed().as_millis()) }
Expand Down
10 changes: 6 additions & 4 deletions src/expansion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -134,10 +134,12 @@ impl std::fmt::Display for ExpandsTo {
pub fn tracked_expands_to(pattern: &Pattern, hole_zid: ZId, shared: &SharedData) -> ExpandsTo {
// apply the hole zipper to the original expr being tracked to get the subtree
// this will expand into, then get the ExpandsTo of that
let idx = shared.tracking.as_ref().unwrap().expr.immut().zip(&shared.zip_of_zid[hole_zid]).idx;
let zip = &shared.zip_of_zid[hole_zid];
let idx = shared.tracking.as_ref().unwrap().expr.immut().zip(zip).idx;
match expands_to_of_node(&shared.tracking.as_ref().unwrap().expr.set[idx]) {
ExpandsTo(ExpandsToInner::IVar(i, VariableType::Metavar)) => {
ExpandsTo(ExpandsToInner::IVar(pattern.pattern_args.find_variable(shared, i as usize) as i32, VariableType::Metavar))
ExpandsTo(ExpandsToInner::IVar(i, _)) => {
let vt = shared.follow.as_ref().unwrap().variable_types[i as usize];
ExpandsTo(ExpandsToInner::IVar(pattern.pattern_args.find_variable(shared, i as usize) as i32, vt))
}
e => e
}
Expand All @@ -151,7 +153,7 @@ pub fn expands_to_of_node(node: &Node) -> ExpandsTo {
Node::Prim(p) => ExpandsToInner::Prim(p.clone()),
Node::Lam(_, tag) => ExpandsToInner::Lam(*tag),
Node::App(_,_) => ExpandsToInner::App,
Node::IVar(i) => ExpandsToInner::IVar(*i, VariableType::Metavar),
Node::IVar(i) => ExpandsToInner::IVar(*i, /*placeholder, will be determined by caller*/ VariableType::Metavar),
}
)
}
Expand Down
19 changes: 13 additions & 6 deletions tests/integration_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -142,12 +142,19 @@ fn python_symbols_regression() {

#[test]
fn symbols_basic() {
compare_out_jsons_testing("data/python/symbols-alignment.json", "data/expected_outputs/symbols-alignment.json", "-i2 -a3 --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbols-cannot-be-literal.json", "data/expected_outputs/symbols-cannot-be-literal.json", "-i2 -a3 --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbols-cannot-be-literal-0-arity.json", "data/expected_outputs/symbols-cannot-be-literal-0-arity.json", "-i2 -a3 --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbol-reuse.json", "data/expected_outputs/symbol-reuse.json", "-i1 -a0 --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbol-reuse-dfa.json", "data/expected_outputs/symbol-reuse-dfa.json", &("-i1 -a0 ".to_owned() + &python_args()), InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/pick-up-on-abstractions-0-arity.json", "data/expected_outputs/pick-up-on-abstractions-0-arity.json", &("-i1 -a0 ".to_owned() + &python_args()), InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbols-alignment.json", "data/expected_outputs/symbols-alignment.json", "-i2 -a3 --rewrite-check --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbols-cannot-be-literal.json", "data/expected_outputs/symbols-cannot-be-literal.json", "-i2 -a3 --rewrite-check --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbols-cannot-be-literal-0-arity.json", "data/expected_outputs/symbols-cannot-be-literal-0-arity.json", "-i2 -a3 --rewrite-check --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbol-reuse.json", "data/expected_outputs/symbol-reuse.json", "-i1 -a0 --rewrite-check --symvar-prefix & ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbol-reuse-dfa.json", "data/expected_outputs/symbol-reuse-dfa.json", &("-i1 -a0 --rewrite-check ".to_owned() + &python_args()), InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/pick-up-on-abstractions-0-arity.json", "data/expected_outputs/pick-up-on-abstractions-0-arity.json", &("-i1 -a0 --rewrite-check ".to_owned() + &python_args()), InputFormat::ProgramsList);
}

#[test]
fn symbols_following() {
compare_out_jsons_testing("data/python/symbol-reuse.json", "data/expected_outputs/symbol-reuse.json", "-i1 -a0 --symvar-prefix & --rewrite-check ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbol-reuse.json", "data/expected_outputs/symbol-reuse-sss.json", "-i1 -a6 --symvar-prefix & --follow '(+ 1 #2 #2 #1 #0 2 3 4)' --follow-types 'S S S' --rewrite-check ", InputFormat::ProgramsList);
compare_out_jsons_testing("data/python/symbol-reuse.json", "data/expected_outputs/symbol-reuse-ssm.json", "-i1 -a6 --symvar-prefix & --follow '(+ 1 #2 #2 #1 #0 2 3 4)' --follow-types 'S S M' --rewrite-check ", InputFormat::ProgramsList);
}

#[test]
Expand Down
Loading