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 committed Aug 22, 2024
1 parent f1efe65 commit ea50df1
Show file tree
Hide file tree
Showing 10 changed files with 723 additions and 177 deletions.
8 changes: 5 additions & 3 deletions lib/haskell/natural4/src/LS/Renamer.hs
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
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
356 changes: 184 additions & 172 deletions lib/haskell/natural4/src/LS/XPile/Simala/Transpile.hs

Large diffs are not rendered by default.

19 changes: 19 additions & 0 deletions lib/haskell/natural4/test/LS/RenamerSpec.hs
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
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
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 ea50df1

Please sign in to comment.