@@ -16,7 +16,8 @@ data Prim = Prim { p_name :: Name,
16 p_type :: Type,
16 p_type :: Type,
17 p_arity :: Int,
17 p_arity :: Int,
18 p_def :: [Value] -> Maybe Value,
18 p_def :: [Value] -> Maybe Value,
19− p_epic :: ([E.Name], E.Term)
19+ p_epic :: ([E.Name], E.Term),
22ty [] x = Constant x
23ty [] x = Constant x
@@ -71,138 +72,141 @@ strRev x = foreign_ tyString "strrev" [(x, tyString)]
71strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
72strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
72strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
73strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
76+partial = Partial NotCovering
74primitives =
78primitives =
75 -- operators
79 -- operators
76 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
80 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
77− (eOp E.plus_),
81+ (eOp E.plus_) total,
78 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
82 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
79− (eOp E.minus_),
83+ (eOp E.minus_) total,
80 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
84 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
81− (eOp E.times_),
85+ (eOp E.times_) total,
82 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
86 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
83− (eOp E.divide_),
87+ (eOp E.divide_) partial,
84 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
88 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
85− (eOp E.eq_),
89+ (eOp E.eq_) total,
86 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
90 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
87− (eOp E.lt_),
91+ (eOp E.lt_) total,
88 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
92 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
89− (eOp E.lte_),
93+ (eOp E.lte_) total,
90 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
94 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
91− (eOp E.gt_),
95+ (eOp E.gt_) total,
92 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
96 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
93− (eOp E.gte_),
97+ (eOp E.gte_) total,
94 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
98 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
95− (eOp E.eq_),
99+ (eOp E.eq_) total,
96 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
100 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
97− (eOp E.lt_),
101+ (eOp E.lt_) total,
98 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
102 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
99− (eOp E.lte_),
103+ (eOp E.lte_) total,
100 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
104 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
101− (eOp E.gt_),
105+ (eOp E.gt_) total,
102 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
106 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
103− (eOp E.gte_),
107+ (eOp E.gte_) total,
104 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
108 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
105− (eOpFn tyBigInt tyBigInt "addBig"),
109+ (eOpFn tyBigInt tyBigInt "addBig") total,
106 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
110 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
107− (eOpFn tyBigInt tyBigInt "subBig"),
111+ (eOpFn tyBigInt tyBigInt "subBig") total,
108 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
112 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
109− (eOpFn tyBigInt tyBigInt "mulBig"),
113+ (eOpFn tyBigInt tyBigInt "mulBig") total,
110 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
114 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
111− (eOpFn tyBigInt tyBigInt "divBig"),
115+ (eOpFn tyBigInt tyBigInt "divBig") partial,
112 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
116 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
113− (eOpFn tyBigInt tyInt "eqBig"),
117+ (eOpFn tyBigInt tyInt "eqBig") total,
114 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
118 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
115− (eOpFn tyBigInt tyInt "ltBig"),
119+ (eOpFn tyBigInt tyInt "ltBig") total,
116 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
120 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
117− (eOpFn tyBigInt tyInt "leBig"),
121+ (eOpFn tyBigInt tyInt "leBig") total,
118 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
122 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
119− (eOpFn tyBigInt tyInt "gtBig"),
123+ (eOpFn tyBigInt tyInt "gtBig") total,
120 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
124 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
121− (eOpFn tyBigInt tyInt "geBig"),
125+ (eOpFn tyBigInt tyInt "geBig") total,
122 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
126 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
123− (eOp E.plusF_),
127+ (eOp E.plusF_) total,
124 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
128 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
125− (eOp E.minusF_),
129+ (eOp E.minusF_) total,
126 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
130 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
127− (eOp E.timesF_),
131+ (eOp E.timesF_) total,
128 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
132 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
129− (eOp E.divideF_),
133+ (eOp E.divideF_) total,
130 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
134 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
131− (eOp E.eqF_),
135+ (eOp E.eqF_) total,
132 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
136 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
133− (eOp E.ltF_),
137+ (eOp E.ltF_) total,
134 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
138 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
135− (eOp E.lteF_),
139+ (eOp E.lteF_) total,
136 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
140 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
137− (eOp E.gtF_),
141+ (eOp E.gtF_) total,
138 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
142 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
139− (eOp E.gteF_),
143+ (eOp E.gteF_) total,
140 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
144 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
141− ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
145+ ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y") total,
142 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
146 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
143− ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")),
147+ ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")) total,
144 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
148 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
145− ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")),
149+ ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")) total,
146 -- Conversions
150 -- Conversions
147 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
151 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
148− ([E.name "x"], strToInt (fun "x")),
152+ ([E.name "x"], strToInt (fun "x")) total,
149 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
153 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
150− ([E.name "x"], intToStr (fun "x")),
154+ ([E.name "x"], intToStr (fun "x")) total,
151 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
155 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
152− ([E.name "x"], charToInt (fun "x")),
156+ ([E.name "x"], charToInt (fun "x")) total,
153 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
157 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
154− ([E.name "x"], intToChar (fun "x")),
158+ ([E.name "x"], intToChar (fun "x")) total,
155 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
159 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
156− ([E.name "x"], intToBigInt (fun "x")),
160+ ([E.name "x"], intToBigInt (fun "x")) total,
157 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
161 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
158− ([E.name "x"], strToBigInt (fun "x")),
162+ ([E.name "x"], strToBigInt (fun "x")) total,
159 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
163 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
160− ([E.name "x"], bigIntToStr (fun "x")),
164+ ([E.name "x"], bigIntToStr (fun "x")) total,
161 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
165 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
162− ([E.name "x"], strToFloat (fun "x")),
166+ ([E.name "x"], strToFloat (fun "x")) total,
163 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
167 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
164− ([E.name "x"], floatToStr (fun "x")),
168+ ([E.name "x"], floatToStr (fun "x")) total,
165 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
169 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
166− ([E.name "x"], intToFloat (fun "x")),
170+ ([E.name "x"], intToFloat (fun "x")) total,
167 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
171 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
168− ([E.name "x"], floatToInt (fun "x")),
172+ ([E.name "x"], floatToInt (fun "x")) total,
170 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
174 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
171− ([E.name "x"], floatExp (fun "x")),
175+ ([E.name "x"], floatExp (fun "x")) total,
172 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
176 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
173− ([E.name "x"], floatLog (fun "x")),
177+ ([E.name "x"], floatLog (fun "x")) total,
174 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
178 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
175− ([E.name "x"], floatSin (fun "x")),
179+ ([E.name "x"], floatSin (fun "x")) total,
176 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
180 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
177− ([E.name "x"], floatCos (fun "x")),
181+ ([E.name "x"], floatCos (fun "x")) total,
178 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
182 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
179− ([E.name "x"], floatTan (fun "x")),
183+ ([E.name "x"], floatTan (fun "x")) total,
180 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
184 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
181− ([E.name "x"], floatASin (fun "x")),
185+ ([E.name "x"], floatASin (fun "x")) total,
182 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
186 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
183− ([E.name "x"], floatACos (fun "x")),
187+ ([E.name "x"], floatACos (fun "x")) total,
184 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
188 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
185− ([E.name "x"], floatATan (fun "x")),
189+ ([E.name "x"], floatATan (fun "x")) total,
186 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
190 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
187− ([E.name "x"], floatSqrt (fun "x")),
191+ ([E.name "x"], floatSqrt (fun "x")) total,
188 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
192 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
189− ([E.name "x"], floatFloor (fun "x")),
193+ ([E.name "x"], floatFloor (fun "x")) total,
190 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
194 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
191− ([E.name "x"], floatCeil (fun "x")),
195+ ([E.name "x"], floatCeil (fun "x")) total,
193 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
197 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
194− ([E.name "x"], strHead (fun "x")),
198+ ([E.name "x"], strHead (fun "x")) partial,
195 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
199 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
196− ([E.name "x"], strTail (fun "x")),
200+ ([E.name "x"], strTail (fun "x")) partial,
197 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
201 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
198− ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")),
202+ ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")) total,
199 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
203 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
200− ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")),
204+ ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")) partial,
201 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
205 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
202− ([E.name "x"], strRev (fun "x")),
206+ ([E.name "x"], strRev (fun "x")) total,
204 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
208 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
205− ([E.name "a", E.name "b", E.name "x"], fun "x")
209+ ([E.name "a", E.name "b", E.name "x"], fun "x") total -- ahem
208p_believeMe [_,_,x] = Just x
212p_believeMe [_,_,x] = Just x
@@ -241,7 +245,9 @@ sBin _ _ = Nothing
242c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
246c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
243c_intToStr _ = Nothing
247c_intToStr _ = Nothing
244−c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))
248+c_strToInt [VConstant (Str x)] = case reads x of
249+ [(n,"")] -> Just $ VConstant (I n)
250+ _ -> Just $ VConstant (I 0)
245c_strToInt _ = Nothing
251c_strToInt _ = Nothing
247c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
253c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
@@ -254,12 +260,16 @@ c_intToBigInt _ = Nothing
255c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
261c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
256c_bigIntToStr _ = Nothing
262c_bigIntToStr _ = Nothing
257−c_strToBigInt [VConstant (Str x)] = Just $ VConstant (BI (read x))
263+c_strToBigInt [VConstant (Str x)] = case reads x of
264+ [(n,"")] -> Just $ VConstant (BI n)
265+ _ -> Just $ VConstant (BI 0)
258c_strToBigInt _ = Nothing
266c_strToBigInt _ = Nothing
260c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
268c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
261c_floatToStr _ = Nothing
269c_floatToStr _ = Nothing
262−c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))
270+c_strToFloat [VConstant (Str x)] = case reads x of
271+ [(n,"")] -> Just $ VConstant (Fl n)
272+ _ -> Just $ VConstant (Fl 0)
263c_strToFloat _ = Nothing
273c_strToFloat _ = Nothing
265c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
275c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
@@ -296,8 +306,9 @@ p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
296p_strRev _ = Nothing
306p_strRev _ = Nothing
298elabPrim :: Prim -> Idris ()
308elabPrim :: Prim -> Idris ()
299−elabPrim (Prim n ty i def epic)
309+elabPrim (Prim n ty i def epic tot)
300 = do updateContext (addOperator n ty i def)
310 = do updateContext (addOperator n ty i def)
301 i <- getIState
312 i <- getIState
302 putIState i { idris_prims = (n, epic) : idris_prims i }
313 putIState i { idris_prims = (n, epic) : idris_prims i }