Unified · Split
| @@ -223,7 +223,6 @@ mutual · 222 unmodified lines | |||
| 223 | pure $ natHack res | 223 | pure $ natHack res |
| 224 | 224 | ||
| 225 | mutual | 225 | mutual |
| 226 | -- In the below, treat %World, and newtypes, as default cases | ||
| 227 | conCases : {auto c : Ref Ctxt Defs} -> | 226 | conCases : {auto c : Ref Ctxt Defs} -> |
| 228 | NameTags -> Name -> List (CaseAlt vars) -> | 227 | NameTags -> Name -> List (CaseAlt vars) -> |
| 229 | Core (List (CConAlt vars)) | 228 | Core (List (CConAlt vars)) |
| @@ -244,8 +243,6 @@ mutual · 14 unmodified lines | |||
| 244 | NameTags -> Name -> List (CaseAlt vars) -> | 243 | NameTags -> Name -> List (CaseAlt vars) -> |
| 245 | Core (List (CConstAlt vars)) | 244 | Core (List (CConstAlt vars)) |
| 246 | constCases tags n [] = pure [] | 245 | constCases tags n [] = pure [] |
| 247 | constCases tags n (ConstCase WorldVal sc :: ns) | ||
| 248 | = constCases tags n ns | ||
| 249 | constCases tags n (ConstCase x sc :: ns) | 246 | constCases tags n (ConstCase x sc :: ns) |
| 250 | = pure $ MkConstAlt x !(toCExpTree tags n sc) :: | 247 | = pure $ MkConstAlt x !(toCExpTree tags n sc) :: |
| 251 | !(constCases tags n ns) | 248 | !(constCases tags n ns) |
| @@ -258,8 +255,6 @@ mutual · 6 unmodified lines | |||
| 258 | getDef fc scr tags n [] = pure Nothing | 255 | getDef fc scr tags n [] = pure Nothing |
| 259 | getDef fc scr tags n (DefaultCase sc :: ns) | 256 | getDef fc scr tags n (DefaultCase sc :: ns) |
| 260 | = pure $ Just !(toCExpTree tags n sc) | 257 | = pure $ Just !(toCExpTree tags n sc) |
| 261 | getDef fc scr tags n (ConstCase WorldVal sc :: ns) | ||
| 262 | = pure $ Just !(toCExpTree tags n sc) | ||
| 263 | getDef {vars} fc scr tags n (ConCase x tag args sc :: ns) | 258 | getDef {vars} fc scr tags n (ConCase x tag args sc :: ns) |
| 264 | = do defs <- get Ctxt | 259 | = do defs <- get Ctxt |
| 265 | case !(lookupDefExact x (gamma defs)) of | 260 | case !(lookupDefExact x (gamma defs)) of |
| @@ -190,7 +190,7 @@ mutual · 189 unmodified lines | |||
| 190 | | Nothing => pure (unload stk (CRef fc n)) | 190 | | Nothing => pure (unload stk (CRef fc n)) |
| 191 | let arity = getArity def | 191 | let arity = getArity def |
| 192 | if (Inline `elem` flags gdef) && (not (n `elem` rec)) | 192 | if (Inline `elem` flags gdef) && (not (n `elem` rec)) |
| 193 | then do ap <- tryApply (n :: rec) stk env def | 193 | then do ap <- tryApply (n :: rec) stk env def |
| 194 | pure $ maybe (unloadApp arity stk (CRef fc n)) id ap | 194 | pure $ maybe (unloadApp arity stk (CRef fc n)) id ap |
| 195 | else pure $ unloadApp arity stk (CRef fc n) | 195 | else pure $ unloadApp arity stk (CRef fc n) |
| 196 | eval {vars} {free} rec env [] (CLam fc x sc) | 196 | eval {vars} {free} rec env [] (CLam fc x sc) |
| @@ -202,11 +202,16 @@ cCall fc cfn clib args ret · 201 unmodified lines | |||
| 202 | applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as | 202 | applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as |
| 203 | applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as | 203 | applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as |
| 204 | 204 | ||
| 205 | getVal : String -> String | ||
| 206 | getVal str = "(vector-ref " ++ str ++ "2)" | ||
| 207 | |||
| 205 | mkFun : List CFType -> CFType -> String -> String | 208 | mkFun : List CFType -> CFType -> String -> String |
| 206 | mkFun args ret n | 209 | mkFun args ret n |
| 207 | = let argns = mkNs 0 args in | 210 | = let argns = mkNs 0 args in |
| 208 | "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++ | 211 | "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++ |
| 209 | (applyLams n argns ++ ")") | 212 | (case ret of |
| 213 | CFIORes _ => getVal (applyLams n argns) ++ ")" | ||
| 214 | _ => applyLams n argns ++ ")") | ||
| 210 | 215 | ||
| 211 | notWorld : CFType -> Bool | 216 | notWorld : CFType -> Bool |
| 212 | notWorld CFWorld = False | 217 | notWorld CFWorld = False |
| @@ -234,7 +234,7 @@ toPrim pn = Unknown pn · 233 unmodified lines | |||
| 234 | 234 | ||
| 235 | export | 235 | export |
| 236 | mkWorld : String -> String | 236 | mkWorld : String -> String |
| 237 | mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 ["#f", res, "#f"] -- MkIORes | 237 | mkWorld res = schConstructor 0 ["#f", res, "#f"] -- MkIORes |
| 238 | 238 | ||
| 239 | schConstant : (String -> String) -> Constant -> String | 239 | schConstant : (String -> String) -> Constant -> String |
| 240 | schConstant _ (I x) = show x | 240 | schConstant _ (I x) = show x |
| @@ -346,11 +346,11 @@ parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String, · 105 unmodified lines | |||
| 346 | = pure $ mkWorld ("(apply (eval (string->symbol " ++ !(schExp i fn) ++")) " | 346 | = pure $ mkWorld ("(apply (eval (string->symbol " ++ !(schExp i fn) ++")) " |
| 347 | ++ !(readArgs i args) ++ ")") | 347 | ++ !(readArgs i args) ++ ")") |
| 348 | schExtCommon i PutStr [arg, world] | 348 | schExtCommon i PutStr [arg, world] |
| 349 | = pure $ "(display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) -- code for MkUnit | 349 | = pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit |
| 350 | schExtCommon i GetStr [world] | 350 | schExtCommon i GetStr [world] |
| 351 | = pure $ mkWorld "(blodwen-get-line (current-input-port))" | 351 | = pure $ mkWorld "(blodwen-get-line (current-input-port))" |
| 352 | schExtCommon i PutChar [arg, world] | 352 | schExtCommon i PutChar [arg, world] |
| 353 | = pure $ "(display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) -- code for MkUnit | 353 | = pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit |
| 354 | schExtCommon i GetChar [world] | 354 | schExtCommon i GetChar [world] |
| 355 | = pure $ mkWorld "(blodwen-get-char (current-input-port))" | 355 | = pure $ mkWorld "(blodwen-get-char (current-input-port))" |
| 356 | schExtCommon i FileOpen [file, mode, bin, world] | 356 | schExtCommon i FileOpen [file, mode, bin, world] |
| @@ -180,11 +180,15 @@ cCall fc cfn libspec args ret · 179 unmodified lines | |||
| 180 | applyLams n (Just (a, ty) :: as) | 180 | applyLams n (Just (a, ty) :: as) |
| 181 | = applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as | 181 | = applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as |
| 182 | 182 | ||
| 183 | getVal : CFType -> String -> String | ||
| 184 | getVal ty str = rktToC ty ("(vector-ref " ++ str ++ "2)") | ||
| 185 | |||
| 183 | mkFun : List CFType -> CFType -> String -> String | 186 | mkFun : List CFType -> CFType -> String -> String |
| 184 | mkFun args ret n | 187 | mkFun args ret n |
| 185 | = let argns = mkNs 0 args in | 188 | = let argns = mkNs 0 args in |
| 186 | "(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++ | 189 | (case ret of |
| 187 | (applyLams n argns ++ ")") | 190 | CFIORes rt => getVal rt (applyLams n argns) ++ ")" |
| 191 | _ => applyLams n argns ++ ")") | ||
| 188 | 192 | ||
| 189 | notWorld : CFType -> Bool | 193 | notWorld : CFType -> Bool |
| 190 | notWorld CFWorld = False | 194 | notWorld CFWorld = False |
| @@ -973,4 +973,3 @@ Core.Context.decode gam idx update (Coded bin) · 972 unmodified lines | |||
| 973 | when update $ coreLift $ writeArray arr idx (Decoded def') | 973 | when update $ coreLift $ writeArray arr idx (Decoded def') |
| 974 | pure def' | 974 | pure def' |
| 975 | Core.Context.decode gam idx update (Decoded def) = pure def | 975 | Core.Context.decode gam idx update (Decoded def) = pure def |
| 976 | |||
| @@ -199,10 +199,6 @@ getRelevantArg : Defs -> Nat -> Maybe Nat -> NF [] -> Core (Maybe Nat) · 198 unmodified lines | |||
| 199 | getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc) | 199 | getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc) |
| 200 | = getRelevantArg defs (1 + i) rel | 200 | = getRelevantArg defs (1 + i) rel |
| 201 | !(sc defs (toClosure defaultOpts [] (Erased fc False))) | 201 | !(sc defs (toClosure defaultOpts [] (Erased fc False))) |
| 202 | -- %World is never inspected, so might as well be deleted from data types | ||
| 203 | getRelevantArg defs i rel (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc) | ||
| 204 | = getRelevantArg defs (1 + i) rel | ||
| 205 | !(sc defs (toClosure defaultOpts [] (Erased fc False))) | ||
| 206 | getRelevantArg defs i Nothing (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg | 202 | getRelevantArg defs i Nothing (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg |
| 207 | = getRelevantArg defs (1 + i) (Just i) | 203 | = getRelevantArg defs (1 + i) (Just i) |
| 208 | !(sc defs (toClosure defaultOpts [] (Erased fc False))) | 204 | !(sc defs (toClosure defaultOpts [] (Erased fc False))) |
| @@ -114,7 +114,7 @@ initBinaryS s · 113 unmodified lines | |||
| 114 | extendBinary : Int -> Binary -> Core Binary | 114 | extendBinary : Int -> Binary -> Core Binary |
| 115 | extendBinary need (MkBin buf l s u) | 115 | extendBinary need (MkBin buf l s u) |
| 116 | = do let newsize = s * 2 | 116 | = do let newsize = s * 2 |
| 117 | let s' = if newsize < need | 117 | let s' = if (newsize - l) < need |
| 118 | then newsize + need | 118 | then newsize + need |
| 119 | else newsize | 119 | else newsize |
| 120 | Just buf' <- coreLift $ resizeBuffer buf s' | 120 | Just buf' <- coreLift $ resizeBuffer buf s' |