on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit92dcd2244ae28808388513341535976c7e453c8e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 30 Apr 2014, 15:58 (12 years ago) parent4c452e7fd1219b
13 files changed+33−188
CHANGELOG+1 CONTRIBUTORS+1 idris.cabal−5 libs/Makefile−3 libs/base/Data/Complex.idr+2−2 libs/effects/Effect/Random.idr+15−1 libs/javascript/JavaScript.idr−104 libs/javascript/JavaScript/JSON.idr−44 libs/javascript/Makefile−14 libs/javascript/javascript.ipkg−5 src/Idris/CaseSplit.hs+7−4 src/Idris/ElabTerm.hs+2−2 src/Idris/REPL.hs+5−4
CHANGELOG+1
@@ -6,6 +6,7 @@ New in 0.9.13:
66* Command line option -e (or --eval) to evaluate expressions without loading the
77 REPL. This is useful for writing more portable tests.
88* Many more of the basic functions and datatypes are documented.
9+* Removed javascript lib in favor of idris-hackers/iQuery
910
1011Internal changes
1112
CONTRIBUTORS+1
@@ -8,6 +8,7 @@ Edwin Brady
88David Raymond Christiansen
99Jason Dagit
1010Simon Fowler
11+Google
1112Cezar Ionescu
1213Irene Knapp
1314Shea Levy
idris.cabal−5
@@ -103,11 +103,6 @@ Extra-source-files:
103103 libs/oldeffects/Effect/*.idr
104104 libs/oldeffects/*.idr
105105
106− libs/javascript/*.idr
107− libs/javascript/JavaScript/*.idr
108− libs/javascript/Makefile
109− libs/javascript/javascript.ipkg
110−
111106 llvm/*.c
112107 llvm/Makefile
113108
libs/Makefile−3
@@ -2,19 +2,16 @@ build:
22 $(MAKE) -C prelude build
33 $(MAKE) -C base build
44 $(MAKE) -C effects build
5− $(MAKE) -C javascript build
65
76
87install:
98 $(MAKE) -C prelude install
109 $(MAKE) -C base install
1110 $(MAKE) -C effects install
12− $(MAKE) -C javascript install
1311
1412clean:
1513 $(MAKE) -C prelude clean
1614 $(MAKE) -C base clean
1715 $(MAKE) -C effects clean
18− $(MAKE) -C javascript clean
1916
2017.PHONY: build install clean
libs/base/Data/Complex.idr+2−2
@@ -62,8 +62,8 @@ conjugate (r:+i) = (r :+ (0-i))
6262-- We can't do "instance Num a => Num (Complex a)" because
6363-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
6464instance Num (Complex Float) where
65− (+) (a:+b) (c:+d) = ((a+b):+(c+d))
66− (-) (a:+b) (c:+d) = ((a-b):+(c-d))
65+ (+) (a:+b) (c:+d) = ((a+c):+(b+d))
66+ (-) (a:+b) (c:+d) = ((a-c):+(b-d))
6767 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
6868 fromInteger x = (fromInteger x:+0)
6969 abs (a:+b) = (magnitude (a:+b):+0)
libs/effects/Effect/Random.idr+15−1
@@ -16,18 +16,32 @@ using (m : Type -> Type)
1616RND : EFFECT
1717RND = MkEff Integer Random
1818
19+||| Generates a random Integer in a given range
1920rndInt : Integer -> Integer -> { [RND] } Eff m Integer
2021rndInt lower upper = do v <- getRandom
2122 return (v `prim__sremBigInt` (upper - lower) + lower)
2223
24+||| Generate a random number in Fin (S `k`)
25+|||
26+||| Note that rndFin k takes values 0, 1, ..., k.
2327rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
24−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)
28+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
2529 return (toFin v)
2630 where toFin : Integer -> Fin (S k)
2731 toFin x = case integerToFin x (S k) of
2832 Just v => v
2933 Nothing => toFin (assert_smaller x (x - cast (S k)))
3034
35+||| Select a random element from a vector
36+rndSelect' : Vect (S k) a -> { [RND] } Eff IO a
37+rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
38+
39+||| Select a random element from a list, or Nothing if the list is empty
40+rndSelect : List a -> { [RND] } Eff IO (Maybe a)
41+rndSelect [] = return Nothing
42+rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
43+
44+||| Sets the random seed
3145srand : Integer -> { [RND] } Eff m ()
3246srand n = setSeed n
3347
libs/javascript/JavaScript.idrdeleted−104
@@ -1,104 +0,0 @@
1−module JavaScript
2−
3−%access public
4−
5−private
6−isUndefined : Ptr -> IO Bool
7−isUndefined p = do
8− res <- mkForeign (
9− FFun "%0 === undefined" [FPtr] FString) p
10− if res == "false"
11− then (return False)
12− else (return True)
13−
14−--------------------------------------------------------------------------------
15−-- Events
16−--------------------------------------------------------------------------------
17−abstract
18−data Event : Type where
19− MkEvent : Ptr -> Event
20−
21−--------------------------------------------------------------------------------
22−-- Elements
23−--------------------------------------------------------------------------------
24−abstract
25−data Element : Type where
26− MkElem : Ptr -> Element
27−
28−setText : Element -> String -> IO ()
29−setText (MkElem p) s =
30− mkForeign (FFun "%0.textContent=%1" [FPtr, FString] FUnit) p s
31−
32−
33−setOnClick : Element -> (Event -> IO Bool) -> IO ()
34−setOnClick (MkElem e) f =
35− mkForeign (
36− FFun "%0['onclick']=%1" [ FPtr
37− , FFunction (FAny Event) (FAny (IO Bool))
38− ] FUnit) e f
39−--------------------------------------------------------------------------------
40−-- Nodelists
41−--------------------------------------------------------------------------------
42−abstract
43−data NodeList : Type where
44− MkNodeList : Ptr -> NodeList
45−
46−elemAt : NodeList -> Nat -> IO (Maybe Element)
47−elemAt (MkNodeList p) i = do
48− e <- mkForeign (FFun "%0.item(%1)" [FPtr, FInt] FPtr) p (
49− prim__truncBigInt_Int (cast i)
50− )
51− d <- isUndefined e
52− if d
53− then return $ Just (MkElem e)
54− else return Nothing
55−
56−--------------------------------------------------------------------------------
57−-- Intervals
58−--------------------------------------------------------------------------------
59−abstract
60−data Interval : Type where
61− MkInterval : Ptr -> Interval
62−
63−setInterval : (() -> IO ()) -> Float -> IO Interval
64−setInterval f t = do
65− e <- mkForeign (
66− FFun "setInterval(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr
67− ) f t
68− return (MkInterval e)
69−
70−clearInterval : Interval -> IO ()
71−clearInterval (MkInterval p) =
72− mkForeign (FFun "clearInterval(%0)" [FPtr] FUnit) p
73−
74−--------------------------------------------------------------------------------
75−-- Timeouts
76−--------------------------------------------------------------------------------
77−data Timeout : Type where
78− MkTimeout : Ptr -> Timeout
79−
80−setTimeout : (() -> IO ()) -> Float -> IO Timeout
81−setTimeout f t = do
82− e <- mkForeign (
83− FFun "setTimeout(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr
84− ) f t
85− return (MkTimeout e)
86−
87−clearTimeout : Timeout -> IO ()
88−clearTimeout (MkTimeout p) =
89− mkForeign (FFun "clearTimeout(%0)" [FPtr] FUnit) p
90−
91−--------------------------------------------------------------------------------
92−-- Basic IO
93−--------------------------------------------------------------------------------
94−alert : String -> IO ()
95−alert msg =
96− mkForeign (FFun "alert(%0)" [FString] FUnit) msg
97−
98−--------------------------------------------------------------------------------
99−-- DOM
100−--------------------------------------------------------------------------------
101−query : String -> IO NodeList
102−query q = do
103− e <- mkForeign (FFun "document.querySelectorAll(%0)" [FString] FPtr) q
104− return (MkNodeList e)
libs/javascript/JavaScript/JSON.idrdeleted−44
@@ -1,44 +0,0 @@
1−module JSON
2−
3−import Data.SortedMap
4−
5−data JSONType : Type where
6− JSONArray : (n : Nat) -> Vect n JSONType -> JSONType
7− JSONString : JSONType
8− JSONNumber : JSONType
9− JSONBool : JSONType
10− JSONObject : SortedMap String JSONType -> JSONType
11− JSONNull : JSONType
12−
13−mutual
14− using (ts : Vect n JSONType, fs : SortedMap String JSONType)
15− namespace JArray
16− data JArray : (n : Nat) -> Vect n JSONType -> Type where
17− Nil : JArray 0 []
18− (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)
19−
20− namespace JObject
21− data JObject : SortedMap String JSONType -> Type where
22− Nil : JObject empty
23− (::) : (f : (String, JSON t)) ->
24− JObject fs ->
25− JObject (insert (fst f) t fs)
26−
27− data JSON : JSONType -> Type where
28− JSString : String -> JSON JSONString
29− JSNumber : Float -> JSON JSONNumber
30− JSBool : Bool -> JSON JSONBool
31− JSNull : JSON JSONNull
32− JSArray : JArray n ts -> JSON (JSONArray n ts)
33− JSObject : JObject fs -> JSON (JSONObject fs)
34−
35−index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)
36−index fZ (JSArray (x :: xs)) = x
37−index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
38−
39−(++) : JSON (JSONArray m ts1) ->
40− JSON (JSONArray n ts2) ->
41− JSON (JSONArray (m + n) (ts1 ++ ts2))
42−(++) (JSArray []) ys = ys
43−(++) (JSArray (x :: xs)) ys with ((JSArray xs) ++ ys)
44− | (JSArray as) = JSArray (x :: as)
libs/javascript/Makefiledeleted−14
@@ -1,14 +0,0 @@
1−IDRIS := idris
2−
3−build:
4− $(IDRIS) --build javascript.ipkg
5−
6−install:
7− $(IDRIS) --install javascript.ipkg
8−
9−clean:
10− $(IDRIS) --clean javascript.ipkg
11−
12−rebuild: clean build
13−
14−.PHONY: build install clean rebuild
libs/javascript/javascript.ipkgdeleted−5
@@ -1,5 +0,0 @@
1−package javascript
2−
3−opts = "--nobasepkgs -i ../prelude -i ../base"
4−modules = JavaScript, JavaScript.JSON
5−
src/Idris/CaseSplit.hs+7−4
@@ -361,16 +361,19 @@ getProofClause l fn fp
361361
362362mkWith :: String -> Name -> String
363363mkWith str n = let str' = replaceRHS str "with (_)"
364− newpat = " " ++
365− replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
366− str' ++ "\n" ++ newpat
364+ in str' ++ "\n" ++ newpat str
367365
368366 where replaceRHS [] str = str
369367 replaceRHS ('?':'=': rest) str = str
370− replaceRHS ('=': rest) str
368+ replaceRHS ('=': rest) str
371369 | not ('=' `elem` rest) = str
372370 replaceRHS (x : rest) str = x : replaceRHS rest str
373371
372+ newpat ('>':patstr) = '>':newpat patstr
373+ newpat patstr =
374+ " " ++
375+ replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
376+
374377-- Replace _ with names in missing clauses
375378
376379nameMissing :: [PTerm] -> Idris [PTerm]
src/Idris/ElabTerm.hs+2−2
@@ -1187,8 +1187,8 @@ reifyApp _ t [x]
11871187reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
11881188reifyApp ist t [Constant (Str n), x]
11891189 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1190−reifyApp _ t [Constant (Str n)]
1191− | t == reflm "Intro" = return $ Intro [sUN n]
1190+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1191+reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)
11921192reifyApp ist t [t']
11931193 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
11941194reifyApp ist t [t']
src/Idris/REPL.hs+5−4
@@ -900,14 +900,15 @@ process h fn (RmProof n')
900900
901901process h fn' (AddProof prf)
902902 = do fn <- do
903− ex <- runIO $ doesFileExist fn'
904− let fnExt = fn' <.> "idr"
903+ let fn'' = takeWhile (/= ' ') fn'
904+ ex <- runIO $ doesFileExist fn''
905+ let fnExt = fn'' <.> "idr"
905906 exExt <- runIO $ doesFileExist fnExt
906907 if ex
907− then return fn'
908+ then return fn''
908909 else if exExt
909910 then return fnExt
910− else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
911+ else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"
911912 let fb = fn ++ "~"
912913 runIO $ copyFile fn fb -- make a backup in case something goes wrong!
913914 prog <- runIO $ readFile fb