Skip to content

Commit

Permalink
Removed deprecated uses
Browse files Browse the repository at this point in the history
- changed `public` to `public export`
- changed `class` to `interface`
- changed `instance` to `implementation`
- changed `Float` to `Double`
  • Loading branch information
yacinehmito committed May 25, 2016
1 parent 363df3b commit 98cff16
Show file tree
Hide file tree
Showing 15 changed files with 40 additions and 39 deletions.
26 changes: 13 additions & 13 deletions IdrisScript.idr
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module IdrisScript

%access public
%access public export

JSRef : Type
JSRef = Ptr
Expand All @@ -18,7 +18,7 @@ data JSType = JSNumber
| JSObject String
| JSUndefined

instance Eq JSType where
implementation Eq JSType where
JSNumber == JSNumber = True
JSString == JSString = True
JSBoolean == JSBoolean = True
Expand Down Expand Up @@ -75,35 +75,35 @@ where
return 6;
})(%0)"""

class ToJS from (to : JSType) where
interface ToJS from (to : JSType) where
toJS : from -> JSValue to

instance ToJS String JSString where
implementation ToJS String JSString where
toJS str = MkJSString (believe_me str)

instance ToJS Int JSNumber where
implementation ToJS Int JSNumber where
toJS num = MkJSNumber (believe_me num)

instance ToJS Float JSNumber where
implementation ToJS Double JSNumber where
toJS num = MkJSNumber (believe_me num)

instance ToJS Bool JSBoolean where
implementation ToJS Bool JSBoolean where
toJS False = MkJSBoolean (believe_me 0)
toJS True = MkJSBoolean (believe_me 1)

class FromJS (from : JSType) to where
interface FromJS (from : JSType) to where
fromJS : JSValue from -> to

instance FromJS JSString String where
implementation FromJS JSString String where
fromJS (MkJSString str) = believe_me str

instance FromJS JSNumber Int where
fromJS (MkJSNumber num) = cast {from=Float} {to=Int} (believe_me num)
implementation FromJS JSNumber Int where
fromJS (MkJSNumber num) = cast {from=Double} {to=Int} (believe_me num)

instance FromJS JSNumber Float where
implementation FromJS JSNumber Double where
fromJS (MkJSNumber num) = believe_me num

instance FromJS JSBoolean Bool where
implementation FromJS JSBoolean Bool where
fromJS (MkJSBoolean b) = check (believe_me b)
where
check : Int -> Bool
Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Arrays.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Arrays

import IdrisScript

%access public
%access public export

infixr 7 ++

Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Arrays/Unpacked.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Arrays.Unpacked

import IdrisScript

%access public
%access public export

singleton : ToJS from to => from -> JS_IO (JSValue JSArray)
singleton {from} {to} val = do
Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Date.idr
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import public IdrisScript.Date.Months
import public IdrisScript.Date.Days
import public IdrisScript.Date.Types

%access public
%access public export

Date : JS_IO (JSValue JSFunction)
Date = do
Expand Down
10 changes: 5 additions & 5 deletions IdrisScript/Date/Days.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Date.Days

import IdrisScript

%access public
%access public export

data Day = Monday
| Tuesday
Expand All @@ -12,7 +12,7 @@ data Day = Monday
| Saturday
| Sunday

instance Eq Day where
implementation Eq Day where
Monday == Monday = True
Tuesday == Tuesday = True
Wednesday == Wednesday = True
Expand All @@ -22,7 +22,7 @@ instance Eq Day where
Sunday == Sunday = True
_ == _ = False

instance Cast Day Int where
implementation Cast Day Int where
cast Monday = 1
cast Tuesday = 2
cast Wednesday = 3
Expand All @@ -31,7 +31,7 @@ instance Cast Day Int where
cast Saturday = 6
cast Sunday = 7

instance Cast Day Integer where
implementation Cast Day Integer where
cast Monday = 1
cast Tuesday = 2
cast Wednesday = 3
Expand All @@ -40,7 +40,7 @@ instance Cast Day Integer where
cast Saturday = 6
cast Sunday = 7

instance Cast Day Nat where
implementation Cast Day Nat where
cast Monday = 1
cast Tuesday = 2
cast Wednesday = 3
Expand Down
4 changes: 2 additions & 2 deletions IdrisScript/Date/Months.idr
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module IdrisScript.Date.Months

%access public
%access public export

data Month = January
| February
Expand All @@ -15,7 +15,7 @@ data Month = January
| November
| December

instance Eq Month where
implementation Eq Month where
January == January = True
February == February = True
March == March = True
Expand Down
14 changes: 7 additions & 7 deletions IdrisScript/Date/Types.idr
Original file line number Diff line number Diff line change
Expand Up @@ -3,46 +3,46 @@ module IdrisScript.Date.Types
import IdrisScript.Date.Months
import IdrisScript.Date.Days

%access public
%access public export

record Year where
constructor MkYear
unYear : Int

instance Eq Year where
implementation Eq Year where
year == year' = unYear year == unYear year'

record Date where
constructor MkDate
unDate : Int

instance Eq Date where
implementation Eq Date where
date == date' = unDate date == unDate date'

record Hours where
constructor MkHours
unHours : Int

instance Eq Hours where
implementation Eq Hours where
hours == hours' = unHours hours == unHours hours'

record Minutes where
constructor MkMinutes
unMinutes : Int

instance Eq Minutes where
implementation Eq Minutes where
mins == mins' = unMinutes mins == unMinutes mins'

record Seconds where
constructor MkSeconds
unSeconds : Int

instance Eq Seconds where
implementation Eq Seconds where
secs == secs' = unSeconds secs == unSeconds secs'

record Milliseconds where
constructor MkMilliseconds
unMilliseconds : Int

instance Eq Milliseconds where
implementation Eq Milliseconds where
millis == millis' = unMilliseconds millis == unMilliseconds millis'
2 changes: 1 addition & 1 deletion IdrisScript/Functions.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Functions

import IdrisScript

%access public
%access public export

infixl 6 !!

Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Functions/Unpacked.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Functions.Unpacked

import IdrisScript

%access public
%access public export

setProperty : ToJS from to
=> String
Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/JSON.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.JSON

import IdrisScript

%access public
%access public export

||| Converts an object into a JSON string
stringfy : JSValue (JSObject c) -> JS_IO String
Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Objects.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Objects

import IdrisScript

%access public
%access public export

infixl 6 !!

Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Objects/Unpacked.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Objects.Unpacked

import IdrisScript

%access public
%access public export

setProperty : ToJS from to
=> String
Expand Down
4 changes: 2 additions & 2 deletions IdrisScript/RegExps.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.RegExps

import IdrisScript

%access public
%access public export

RegExp : JS_IO (JSValue JSFunction)
RegExp = do
Expand All @@ -13,7 +13,7 @@ data RegExpFlags = Global
| IgnoreCase
| Multiline

instance Eq RegExpFlags where
implementation Eq RegExpFlags where
Global == Global = True
IgnoreCase == IgnoreCase = True
Multiline == Multiline = True
Expand Down
2 changes: 1 addition & 1 deletion IdrisScript/Strings.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Strings

import IdrisScript

%access public
%access public export

||| Upper case a string.
toUpperCase : String -> JS_IO String
Expand Down
3 changes: 2 additions & 1 deletion IdrisScript/Timer.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module IdrisScript.Timer

import IdrisScript

%access public
%access public export

export
record Timeout where
Expand All @@ -23,6 +23,7 @@ setTimeout f millis = do
return $ MkTimeout timeout

||| Clears a timeout.
export
clearTimeout : Timeout -> JS_IO ()
clearTimeout timeout =
jscall "clearTimeout(%0)" (Ptr -> JS_IO ()) (unTimeout timeout)
Expand Down

0 comments on commit 98cff16

Please sign in to comment.