idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #442 from melted/fix_bootstrap2

Browse Source 
Fix bootstrap
This commit is contained in:
Niklas Larsson 2020-07-10 00:48:26 +02:00 committed by GitHub
commit 80f4ced386
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/ci-full-bootstrap.yml vendored
View File

@ -2,7 +2,7 @@ name: Idris bootstrap
on: on:
push: push:
branches: branches:
- master - '*'
tags: tags:
- '*' - '*'

9
src/Compiler/ES/Imperative.idr
View File

@ -54,14 +54,17 @@ genName =
pure $ MN "imp_gen" i pure $ MN "imp_gen" i
mutual mutual
ifThenElse : Bool -> a -> a -> a
ifThenElse True t e = t
ifThenElse False t e = e
pairToReturn : (toReturn : Bool) -> (ImperativeStatement, ImperativeExp) -> pairToReturn : (toReturn : Bool) -> (ImperativeStatement, ImperativeExp) ->
Core (if toReturn then ImperativeStatement else (ImperativeStatement, ImperativeExp)) Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp))
pairToReturn False (s, e) = pure (s, e) pairToReturn False (s, e) = pure (s, e)
pairToReturn True (s, e) = pure $ s <+> ReturnStatement e pairToReturn True (s, e) = pure $ s <+> ReturnStatement e
expToReturn : (toReturn : Bool) -> ImperativeExp -> expToReturn : (toReturn : Bool) -> ImperativeExp ->
Core (if toReturn then ImperativeStatement else (ImperativeStatement, ImperativeExp)) Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp))
expToReturn False e = pure $ (DoNothing, e) expToReturn False e = pure $ (DoNothing, e)
expToReturn True e = pure $ ReturnStatement e expToReturn True e = pure $ ReturnStatement e
@ -78,7 +81,7 @@ mutual
pure (concat (map fst a), map snd a) pure (concat (map fst a), map snd a)
impExp : {auto c : Ref Imps ImpSt} -> (toReturn : Bool) -> NamedCExp -> impExp : {auto c : Ref Imps ImpSt} -> (toReturn : Bool) -> NamedCExp ->
Core (if toReturn then ImperativeStatement else (ImperativeStatement, ImperativeExp)) Core (ifThenElse toReturn ImperativeStatement (ImperativeStatement, ImperativeExp))
impExp toReturn (NmLocal fc n) = expToReturn toReturn $ IEVar n impExp toReturn (NmLocal fc n) = expToReturn toReturn $ IEVar n
impExp toReturn (NmRef fc n) = expToReturn toReturn $ IEVar n impExp toReturn (NmRef fc n) = expToReturn toReturn $ IEVar n
impExp toReturn (NmLam fc n e) = expToReturn toReturn $ IELambda [n] !(impExp True e) impExp toReturn (NmLam fc n e) = expToReturn toReturn $ IELambda [n] !(impExp True e)