Skip to content

Commit

Permalink
I hate rebasing
Browse files Browse the repository at this point in the history
  • Loading branch information
mbellotti committed Apr 14, 2023
1 parent 23a0e40 commit 92ca280
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 54 deletions.
44 changes: 0 additions & 44 deletions smt/generator_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -612,52 +612,8 @@ func prepTest(filepath string, test string, specType bool, testRun bool) string
compiler := llvm.Execute(ty.Checked, ty.SpecStructs, l.Uncertains, l.Unknowns, true)

//fmt.Println(compiler.GetIR())
<<<<<<< HEAD
generator := Execute(compiler)
return generator.SMT()
=======
generator := NewGenerator()
generator.LoadMeta(compiler.RunRound, compiler.Uncertains, compiler.Unknowns, compiler.Asserts, compiler.Assumes)
generator.Run(compiler.GetIR())
//fmt.Println(generator.SMT())
return generator.SMT(), nil
}

func prepTestSys(filepath string, test string, imports bool) (string, error) {
filepath = util.Filepath(filepath)
path := gopath.Dir(filepath)

is := antlr.NewInputStream(test)
lexer := parser.NewFaultLexer(is)
stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)

p := parser.NewFaultParser(stream)
l := listener.NewListener(path, !imports, false) //imports being true means testing is false :)
antlr.ParseTreeWalkerDefault.Walk(l, p.SysSpec())

pre := preprocess.NewProcesser()
pre.StructsPropertyOrder = l.StructsPropertyOrder
tree := pre.Run(l.AST)

ty := types.NewTypeChecker(pre)
tree, err := ty.Check(tree)

if err != nil {
return "", err
}
compiler := llvm.NewCompiler()
compiler.LoadMeta(ty.SpecStructs, l.Uncertains, l.Unknowns, true)
err = compiler.Compile(tree)
if err != nil {
return "", err
}
//fmt.Println(compiler.GetIR())
generator := NewGenerator()
generator.LoadMeta(compiler.RunRound, compiler.Uncertains, compiler.Unknowns, compiler.Asserts, compiler.Assumes)
generator.Run(compiler.GetIR())
//fmt.Println(generator.SMT())
return generator.SMT(), nil
>>>>>>> 163641c (here's a crazy idea: let the typechecker just have the preprocessor and let it do partial runs to rename nodes post-swap)
}

func notStrictlyOrdered(want string, got string) bool {
Expand Down
39 changes: 29 additions & 10 deletions types/types.go
Original file line number Diff line number Diff line change
Expand Up @@ -879,23 +879,42 @@ func (c *Checker) inferSwapNode(node ast.Expression) (ast.Node, error) {
}

func (c *Checker) swapValues(base *ast.StructInstance) (*ast.StructInstance, error) {
var swaps []ast.Node
for _, s := range base.Swaps {
n, err := c.typecheck(s)
if err != nil {
return base, err
}

infix := n.(*ast.InfixExpression)
rawid := infix.Left.(ast.Nameable).RawId()
key := rawid[len(rawid)-1]
val, err := c.lookupReference(infix.Right)
if err != nil {
return base, err
}
base.Properties[key].Value = val
base = c.swapDeepNames(base)
swaps = append(swaps, n)
// infix := n.(*ast.InfixExpression)
// rawid := infix.Left.(ast.Nameable).RawId()
// key := rawid[len(rawid)-1]
// val, err := c.lookupReference(infix.Right)
// if err != nil {
// return base, err
// }

// // Because part of what we're doing here is renaming
// // these nodes. We need to do a deep copy to separate
// // the swapped nodes from their original reference values
// copyVal, err := deepcopy.Anything(val)
// if err != nil {
// return base, err
// }

// val = copyVal.(ast.Node)

// switch v := val.(type) {
// case *ast.StructInstance:
// v.Name = key
// val = v
// }

// base.Properties[key].Value = val
// base = c.swapDeepNames(base)

}
base.Swaps = swaps
return base, nil
}

Expand Down

0 comments on commit 92ca280

Please sign in to comment.