Skip to content

Commit

Permalink
Support more naturalL4 and honour name shadowing
Browse files Browse the repository at this point in the history 
After adding a test case, I realised the name shadowing did not work as
anticipated. We fix this now, move some code around and extend the
transpiler to work correctly for many more naturalL4 constructs and
fragments.
  • Loading branch information
@fendor
fendor committed Aug 23, 2024
1 parent f1efe65 commit 4e6208e
Show file tree
Hide file tree
Showing 10 changed files with 722 additions and 177 deletions.
8 changes: 5 additions & 3 deletions lib/haskell/natural4/src/LS/Renamer.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -410,9 +410,11 @@ scanTypeDeclName tracer mtexprs = do
-- |
-- Lexical Scoping rules for hornlike rules:
--
-- GIVETH's are global
-- GIVEN's are local
-- DECIDE head term in "IS" clauses is global
-- * GIVENs are local to the rule
-- * A GIVETH can be referred to in other rules up the scope hierarchy
-- * The head in DECIDE clauses can also be referred to by other rules in scope hierarchy
-- * WHERE clauses are local to the rule
--
renameRules :: (Traversable f) => Tracer Log -> f Rule -> Renamer (f RnRule)
renameRules tracer rules = do
rulesWithLocalDefs <-
Expand Down
4 changes: 2 additions & 2 deletions lib/haskell/natural4/src/LS/Renamer/Scope.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@ data ScopeTable = ScopeTable
unionScopeTable :: ScopeTable -> ScopeTable -> ScopeTable
unionScopeTable tbl1 tbl2 =
ScopeTable
{ _stVariables = Map.union tbl1._stVariables tbl2._stVariables
, _stFunction = Map.union tbl1._stFunction tbl2._stFunction
{ _stVariables = Map.union tbl2._stVariables tbl1._stVariables
, _stFunction = Map.union tbl2._stFunction tbl1._stFunction
}

differenceScopeTable :: ScopeTable -> ScopeTable -> ScopeTable
Expand Down
355 changes: 183 additions & 172 deletions lib/haskell/natural4/src/LS/XPile/Simala/Transpile.hs
View file

Large diffs are not rendered by default.

19 changes: 19 additions & 0 deletions lib/haskell/natural4/test/LS/RenamerSpec.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,25 @@ spec = do
GIVEN x
DECIDE x g IS x
|]
test' "function-with-name-shadowing"
[i|
GIVEN x
DECIDE f x IS g x
WHERE (
GIVEN x DECIDE g x IS x
)
|]
test'
"function-with-name-shadowing-with-where-rules"
[i|
GIVEN x
DECIDE f x IS y
WHERE (
GIVETH y DECIDE y IS g x
§
GIVEN d DECIDE g d IS y WHERE y IS SUM(d, d)
)
|]
where
test' :: String -> String -> SpecWith (Arg (IO (Golden TL.Text)))
test' fname ruleSource =
Expand Down
30 changes: 30 additions & 0 deletions lib/haskell/natural4/test/LS/XPile/SimalaSpec.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,36 @@ basicTests = do
y IS A Number
DECIDE x `discounted by` y IS SUM(x, MINUS(1, y))
|]
transpilerTest "function-with-name-shadowing"
[i|
GIVEN x
DECIDE f x IS g x
WHERE (
GIVEN x DECIDE g x IS x
)
|]
transpilerTest
"function-with-name-shadowing-with-where-rules-1"
[i|
GIVEN x
DECIDE f x IS y
WHERE (
GIVETH y DECIDE y IS g x
§
GIVEN d DECIDE g d IS y WHERE y IS SUM(d, d)
)
|]
transpilerTest
"function-with-name-shadowing-with-where-rules-2"
[i|
GIVEN x
DECIDE f x IS y
WHERE (
GIVEN d DECIDE g d IS y WHERE y IS SUM(d, d)
§
GIVETH y DECIDE y IS g x
)
|]

multiRuleTests :: Spec
multiRuleTests = describe "multi-rules" do
Expand Down
308 changes: 308 additions & 0 deletions ...ural4/test/testdata/golden/renamer/function-with-name-shadowing-with-where-rules.expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,308 @@
Right
[ Hornlike
( RnHornlike
{ name =
[ RnExprName
( RnName
{ rnOccName = MTT "f" :| []
, rnUniqueId = 1
, rnNameType = RnFunction
}
)
, RnExprName
( RnName
{ rnOccName = MTT "x" :| []
, rnUniqueId = 0
, rnNameType = RnVariable
}
)
]
, super = Nothing
, keyword = Decide
, given = Just
( RnParamText
{ mkParamText = RnTypedMulti
{ rnTypedMultiExpr = RnExprName
( RnName
{ rnOccName = MTT "x" :| []
, rnUniqueId = 0
, rnNameType = RnVariable
}
) :| []
, rnTypedMultiTypeSig = Nothing
} :| []
}
)
, giveth = Nothing
, upon = Nothing
, clauses =
[ RnHornClause
{ rnHcHead = RnConstraint
[ RnExprName
( RnName
{ rnOccName = MTT "f" :| []
, rnUniqueId = 1
, rnNameType = RnFunction
}
)
, RnExprName
( RnName
{ rnOccName = MTT "x" :| []
, rnUniqueId = 0
, rnNameType = RnVariable
}
)
] RPis
[ RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
)
]
, rnHcBody = Nothing
}
]
, rlabel = Nothing
, lsource = Nothing
, wwhere =
[ Hornlike
( RnHornlike
{ name =
[ RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
)
]
, super = Nothing
, keyword = Where
, given = Nothing
, giveth = Just
( RnParamText
{ mkParamText = RnTypedMulti
{ rnTypedMultiExpr = RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
) :| []
, rnTypedMultiTypeSig = Nothing
} :| []
}
)
, upon = Nothing
, clauses =
[ RnHornClause
{ rnHcHead = RnConstraint
[ RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
)
] RPis
[ RnExprName
( RnName
{ rnOccName = MTT "g" :| []
, rnUniqueId = 4
, rnNameType = RnFunction
}
)
, RnExprName
( RnName
{ rnOccName = MTT "x" :| []
, rnUniqueId = 0
, rnNameType = RnVariable
}
)
]
, rnHcBody = Nothing
}
]
, rlabel = Nothing
, lsource = Nothing
, wwhere = []
, srcref = Just
( SrcRef
{ url = "test/Spec"
, short = "test/Spec"
, srcrow = 1
, srccol = 1
, version = Nothing
}
)
, defaults = []
, symtab = []
}
)
, Hornlike
( RnHornlike
{ name =
[ RnExprName
( RnName
{ rnOccName = MTT "g" :| []
, rnUniqueId = 4
, rnNameType = RnFunction
}
)
, RnExprName
( RnName
{ rnOccName = MTT "d" :| []
, rnUniqueId = 3
, rnNameType = RnVariable
}
)
]
, super = Nothing
, keyword = Where
, given = Just
( RnParamText
{ mkParamText = RnTypedMulti
{ rnTypedMultiExpr = RnExprName
( RnName
{ rnOccName = MTT "d" :| []
, rnUniqueId = 3
, rnNameType = RnVariable
}
) :| []
, rnTypedMultiTypeSig = Nothing
} :| []
}
)
, giveth = Nothing
, upon = Nothing
, clauses =
[ RnHornClause
{ rnHcHead = RnConstraint
[ RnExprName
( RnName
{ rnOccName = MTT "g" :| []
, rnUniqueId = 4
, rnNameType = RnFunction
}
)
, RnExprName
( RnName
{ rnOccName = MTT "d" :| []
, rnUniqueId = 3
, rnNameType = RnVariable
}
)
] RPis
[ RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
)
]
, rnHcBody = Nothing
}
]
, rlabel = Nothing
, lsource = Nothing
, wwhere =
[ Hornlike
( RnHornlike
{ name =
[ RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
)
]
, super = Nothing
, keyword = Where
, given = Nothing
, giveth = Nothing
, upon = Nothing
, clauses =
[ RnHornClause
{ rnHcHead = RnNary RPis
[ RnRelationalTerm
[ RnExprName
( RnName
{ rnOccName = MTT "y" :| []
, rnUniqueId = 2
, rnNameType = RnVariable
}
)
]
, RnNary RPsum
[ RnRelationalTerm
[ RnExprName
( RnName
{ rnOccName = MTT "d" :| []
, rnUniqueId = 3
, rnNameType = RnVariable
}
)
]
, RnRelationalTerm
[ RnExprName
( RnName
{ rnOccName = MTT "d" :| []
, rnUniqueId = 3
, rnNameType = RnVariable
}
)
]
]
]
, rnHcBody = Nothing
}
]
, rlabel = Nothing
, lsource = Nothing
, wwhere = []
, srcref = Just
( SrcRef
{ url = "test/Spec"
, short = "test/Spec"
, srcrow = 1
, srccol = 1
, version = Nothing
}
)
, defaults = []
, symtab = []
}
)
]
, srcref = Just
( SrcRef
{ url = "test/Spec"
, short = "test/Spec"
, srcrow = 1
, srccol = 1
, version = Nothing
}
)
, defaults = []
, symtab = []
}
)
]
, srcref = Just
( SrcRef
{ url = "test/Spec"
, short = "test/Spec"
, srcrow = 1
, srccol = 1
, version = Nothing
}
)
, defaults = []
, symtab = []
}
)
]
Loading

0 comments on commit 4e6208e

Please sign in to comment.