-
Notifications
You must be signed in to change notification settings - Fork 374
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.
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
[RefC] Object Immortalization and Pre-Generation of Constants #3242
Open
seagull-kamome
wants to merge
16
commits into
idris-lang:main
Choose a base branch
from
seagull-kamome:refc-sticky-value
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
16 commits
Select commit
Hold shift + click to select a range
95af70f
[RefC] shrink value_header; object imortalized; stock well knwon values.
seagull-kamome 769f695
[RefC] Allocated constants statically; Predefined commonly seen values.
seagull-kamome f0bcaf3
linter
seagull-kamome 00957e4
Merge remote-tracking branch 'upstream/main' into refc-sticky-value
seagull-kamome e8a011d
[RefC] make constants const.
seagull-kamome 373aeac
cleanup
seagull-kamome 91b4a2d
cleanup
seagull-kamome e3805ce
update CHANGELOG_NEXT
seagull-kamome 02b8fa3
[refc][test] revert debugging code
seagull-kamome 7ec8bc5
Refactor constantName function in RefC.idr
seagull-kamome 8aaebdd
Merge remote-tracking branch 'upstream/main' into refc-sticky-value
seagull-kamome 3fd0464
Merge remote-tracking branch 'upstream/main' into refc-sticky-value
seagull-kamome 9cde4df
Merge remote-tracking branch 'upstream/main' into refc-sticky-value
seagull-kamome b49be30
lint
seagull-kamome f4b06c1
Merge remote-tracking branch 'upstream/main' into refc-sticky-value
seagull-kamome b945254
fix typo in support/refc/memoryManagement.c
seagull-kamome File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -142,23 +142,6 @@ cPrimType CharType = "Char" | |
cPrimType DoubleType = "Double" | ||
cPrimType WorldType = "void" | ||
|
||
cConstant : Constant -> String | ||
cConstant (I x) = "idris2_mkInt64("++ showIntMin x ++")" | ||
cConstant (I8 x) = "idris2_mkInt8(INT8_C("++ show x ++"))" | ||
cConstant (I16 x) = "idris2_mkInt16(INT16_C("++ show x ++"))" | ||
cConstant (I32 x) = "idris2_mkInt32(INT32_C("++ show x ++"))" | ||
cConstant (I64 x) = "idris2_mkInt64("++ showInt64Min x ++")" | ||
cConstant (BI x) = "(Value*)idris2_mkIntegerLiteral(\""++ show x ++"\")" | ||
cConstant (B8 x) = "idris2_mkBits8(UINT8_C("++ show x ++"))" | ||
cConstant (B16 x) = "idris2_mkBits16(UINT16_C("++ show x ++"))" | ||
cConstant (B32 x) = "idris2_mkBits32(UINT32_C("++ show x ++"))" | ||
cConstant (B64 x) = "idris2_mkBits64(UINT64_C("++ show x ++"))" | ||
cConstant (Db x) = "idris2_mkDouble("++ show x ++")" | ||
cConstant (Ch x) = "idris2_mkChar("++ escapeChar x ++")" | ||
cConstant (Str x) = "(Value*)idris2_mkString("++ cStringQuoted x ++")" | ||
cConstant (PrT t) = cPrimType t | ||
cConstant WorldVal = "(Value*)NULL" | ||
|
||
||| Generate scheme for a primitive function. | ||
cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String | ||
cOp (Neg ty) [x] = "idris2_negate_" ++ cPrimType ty ++ "(" ++ x ++ ")" | ||
|
@@ -211,6 +194,7 @@ data EnvTracker : Type where | |
data FunctionDefinitions : Type where | ||
data IndentLevel : Type where | ||
data HeaderFiles : Type where | ||
data ConstDef : Type where | ||
|
||
ReuseMap = SortedMap Name String | ||
Owned = SortedSet AVar | ||
|
@@ -457,6 +441,7 @@ mutual | |
-> {auto e : Ref EnvTracker Env} | ||
-> {auto oft : Ref OutfileText Output} | ||
-> {auto il : Ref IndentLevel Nat} | ||
-> {auto _ : Ref ConstDef (SortedMap Constant String)} | ||
-> Env | ||
-> String -> String -> List Int -> ANF -> TailPositionStatus | ||
-> Core () | ||
|
@@ -479,6 +464,7 @@ mutual | |
-> {auto oft : Ref OutfileText Output} | ||
-> {auto il : Ref IndentLevel Nat} | ||
-> {auto e : Ref EnvTracker Env} | ||
-> {auto _ : Ref ConstDef (SortedMap Constant String)} | ||
-> ANF | ||
-> TailPositionStatus | ||
-> Core String | ||
|
@@ -557,8 +543,8 @@ mutual | |
"prim__void", "prim__os", "prim__codegen", "prim__onCollect", "prim__onCollectAny" ] | ||
case p of | ||
NS _ (UN (Basic pn)) => | ||
unless (elem pn prims) $ throw $ InternalError $ "INTERNAL ERROR: Unknown primitive: " ++ cName p | ||
_ => throw $ InternalError $ "INTERNAL ERROR: Unknown primitive: " ++ cName p | ||
unless (elem pn prims) $ throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p | ||
_ => throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p | ||
emit fc $ "// call to external primitive " ++ cName p | ||
pure $ "idris2_\{cName p}("++ showSep ", " (map varName args) ++")" | ||
|
||
|
@@ -635,7 +621,53 @@ mutual | |
emit emptyFC "}" | ||
pure switchReturnVar | ||
|
||
cStatementsFromANF (APrimVal fc c) _ = pure $ cConstant c | ||
cStatementsFromANF (APrimVal fc (I x)) tailPosition = cStatementsFromANF (APrimVal fc (I64 $ cast x)) tailPosition | ||
cStatementsFromANF (APrimVal fc c) _ = do | ||
constdefs <- get ConstDef | ||
case lookup c constdefs of | ||
Just constid => constantName c constid -- the constant already booked. | ||
Nothing => dyngen | ||
where | ||
constantName : Constant -> String -> Core String | ||
constantName c n = case c of | ||
I x => pure "((Value*)&idris2_constant_Int64_\{cCleanString $ show x})" | ||
I64 x => pure "((Value*)&idris2_constant_Int64_\{cCleanString $ show x})" | ||
B64 x => pure "((Value*)&idris2_constant_Bits64_\{show x})" | ||
Db x => pure "((Value*)&idris2_constant_Double_\{cCleanString $ show x})" | ||
Str x => pure "((Value*)&idris2_constant_String_\{n})" | ||
_ => throw $ InternalError "[refc] Unsupported type of constant." | ||
orStagen : Core String | ||
orStagen = do | ||
constdefs <- get ConstDef | ||
constid <- case c of | ||
Str _ => getNextCounter | ||
_ => pure "" | ||
-- booking the constant to generate later | ||
put ConstDef $ insert c constid constdefs | ||
constantName c constid | ||
dyngen : Core String | ||
dyngen = case c of | ||
I8 x => pure "idris2_mkInt8(INT8_C(\{show x}))" | ||
I16 x => pure "idris2_mkInt16(INT16_C(\{show x}))" | ||
I32 x => pure "idris2_mkInt32(INT32_C(\{show x}))" | ||
I64 x => if x >= 0 && x < 100 | ||
then pure "(Value*)(&idris2_predefined_Int64[\{show x}])" | ||
else orStagen | ||
BI x => if x >= 0 && x < 100 | ||
then pure "idris2_getPredefinedInteger(\{show x})" | ||
else pure "idris2_mkIntegerLiteral(\"\{show x}\")" | ||
B8 x => pure "idris2_mkBits8(UINT8_C(\{show x}))" | ||
B16 x => pure "idris2_mkBits16(UINT16_C(\{show x}))" | ||
B32 x => pure "idris2_mkBits32(UINT32_C(\{show x}))" | ||
B64 x => if x >= 0 && x < 100 | ||
then pure "(Value*)(&idris2_predefined_Bits64[\{show x}])" | ||
else orStagen | ||
Db _ => orStagen | ||
Ch x => pure "idris2_mkChar(\{escapeChar x})" | ||
Str _ => orStagen | ||
PrT t => pure $ cPrimType t | ||
_ => pure "NULL" | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this catch-all feels a bit brittle to me at first look at least |
||
|
||
cStatementsFromANF (AErased fc) _ = pure "NULL" | ||
cStatementsFromANF (ACrash fc x) _ = pure "(NULL /* CRASH */)" | ||
|
||
|
@@ -760,6 +792,7 @@ additionalFFIStub name argTypes retType = | |
|
||
createCFunctions : {auto c : Ref Ctxt Defs} | ||
-> {auto a : Ref ArgCounter Nat} | ||
-> {auto _ : Ref ConstDef (SortedMap Constant String)} | ||
-> {auto f : Ref FunctionDefinitions (List String)} | ||
-> {auto oft : Ref OutfileText Output} | ||
-> {auto il : Ref IndentLevel Nat} | ||
|
@@ -856,17 +889,19 @@ createCFunctions n (MkAForeign ccs fargs ret) = do | |
|
||
decreaseIndentation | ||
emit EmptyFC "}" | ||
_ => assert_total $ idris_crash ("INTERNAL ERROR: FFI not found for " ++ cName n) | ||
_ => throw $ InternalError "[refc] FFI not found for \{cName n}" | ||
-- not really total but this way this internal error does not contaminate everything else | ||
|
||
createCFunctions n (MkAError exp) = assert_total $ idris_crash ("INTERNAL ERROR: Error with expression: " ++ show exp) | ||
createCFunctions n (MkAError exp) = throw $ InternalError "[refc] Error with expression: \{show exp}" | ||
-- not really total but this way this internal error does not contaminate everything else | ||
|
||
|
||
header : {auto c : Ref Ctxt Defs} | ||
-> {auto f : Ref FunctionDefinitions (List String)} | ||
-> {auto o : Ref OutfileText Output} | ||
-> {auto il : Ref IndentLevel Nat} | ||
-> {auto h : Ref HeaderFiles (SortedSet String)} | ||
-> {auto _ : Ref ConstDef (SortedMap Constant String)} | ||
-> Core () | ||
header = do | ||
let initLines = """ | ||
|
@@ -875,9 +910,31 @@ header = do | |
|
||
""" | ||
let headerFiles = SortedSet.toList !(get HeaderFiles) | ||
let headerLines = map (\h => "#include <" ++ h ++ ">\n") headerFiles | ||
fns <- get FunctionDefinitions | ||
update OutfileText (appendL ([initLines] ++ headerLines ++ ["\n// function definitions"] ++ fns)) | ||
update OutfileText $ appendL $ | ||
[initLines] ++ | ||
map (\h => "#include <\{h}>\n") headerFiles ++ | ||
["\n// function definitions"] ++ | ||
fns ++ | ||
["\n// constant value definitions"] ++ | ||
map (uncurry genConstant) (SortedMap.toList !(get ConstDef)) | ||
where | ||
go : String -> String -> String -> String -> String | ||
go suffix ty tag v = | ||
"static Value_\{ty} const idris2_constant_\{ty}_\{cCleanString suffix}" | ||
++ " = { IDRIS2_STOCKVAL(\{tag}_TAG), \{v} };" | ||
genConstant : Constant -> String -> String | ||
genConstant c n = case c of | ||
I x => let x' = show x in go x' "Int64" "INT64" (showIntMin x) | ||
I64 x => let x' = show x in go x' "Int64" "INT64" (showInt64Min x) | ||
B64 x => let x' = show x in go x' "Bits64" "BITS64" "UINT64_C(\{x'})" | ||
Db x => let x' = show x in go x' "Double" "DOUBLE" x' | ||
Str x => go n "String" "STRING" (cStringQuoted x) | ||
_ => "/* bad constant */" | ||
|
||
|
||
|
||
|
||
|
||
footer : {auto il : Ref IndentLevel Nat} | ||
-> {auto f : Ref OutfileText Output} | ||
|
@@ -908,6 +965,7 @@ generateCSourceFile : {auto c : Ref Ctxt Defs} | |
generateCSourceFile defs outn = | ||
do _ <- newRef ArgCounter 0 | ||
_ <- newRef FunctionDefinitions [] | ||
_ <- newRef ConstDef Data.SortedMap.empty | ||
_ <- newRef OutfileText DList.Nil | ||
_ <- newRef HeaderFiles empty | ||
_ <- newRef IndentLevel 0 | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this compile-time error feels like it could be fairly easily remediated by a new smaller data-type than
Constant
so that we aren't relying on the invariant that no new type of constant is stored inConstDef
without a new case being added here.