@@ -16,7 +16,8 @@ data Prim = Prim { p_name :: Name,
1616 p_type :: Type,
1717 p_arity :: Int,
1818 p_def :: [Value] -> Maybe Value,
19− p_epic :: ([E.Name], E.Term)
19+ p_epic :: ([E.Name], E.Term),
20+ p_total :: Totality
2021 }
2122
2223ty [] x = Constant x
@@ -71,138 +72,141 @@ strRev x = foreign_ tyString "strrev" [(x, tyString)]
7172strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
7273strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
7374
75+total = Total []
76+partial = Partial NotCovering
77+
7478primitives =
7579 -- operators
7680 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
77− (eOp E.plus_),
81+ (eOp E.plus_) total,
7882 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
79− (eOp E.minus_),
83+ (eOp E.minus_) total,
8084 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
81− (eOp E.times_),
85+ (eOp E.times_) total,
8286 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
83− (eOp E.divide_),
87+ (eOp E.divide_) partial,
8488 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
85− (eOp E.eq_),
89+ (eOp E.eq_) total,
8690 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
87− (eOp E.lt_),
91+ (eOp E.lt_) total,
8892 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
89− (eOp E.lte_),
93+ (eOp E.lte_) total,
9094 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
91− (eOp E.gt_),
95+ (eOp E.gt_) total,
9296 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
93− (eOp E.gte_),
97+ (eOp E.gte_) total,
9498 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
95− (eOp E.eq_),
99+ (eOp E.eq_) total,
96100 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
97− (eOp E.lt_),
101+ (eOp E.lt_) total,
98102 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
99− (eOp E.lte_),
103+ (eOp E.lte_) total,
100104 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
101− (eOp E.gt_),
105+ (eOp E.gt_) total,
102106 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
103− (eOp E.gte_),
107+ (eOp E.gte_) total,
104108 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
105− (eOpFn tyBigInt tyBigInt "addBig"),
109+ (eOpFn tyBigInt tyBigInt "addBig") total,
106110 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
107− (eOpFn tyBigInt tyBigInt "subBig"),
111+ (eOpFn tyBigInt tyBigInt "subBig") total,
108112 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
109− (eOpFn tyBigInt tyBigInt "mulBig"),
113+ (eOpFn tyBigInt tyBigInt "mulBig") total,
110114 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
111− (eOpFn tyBigInt tyBigInt "divBig"),
115+ (eOpFn tyBigInt tyBigInt "divBig") partial,
112116 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
113− (eOpFn tyBigInt tyInt "eqBig"),
117+ (eOpFn tyBigInt tyInt "eqBig") total,
114118 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
115− (eOpFn tyBigInt tyInt "ltBig"),
119+ (eOpFn tyBigInt tyInt "ltBig") total,
116120 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
117− (eOpFn tyBigInt tyInt "leBig"),
121+ (eOpFn tyBigInt tyInt "leBig") total,
118122 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
119− (eOpFn tyBigInt tyInt "gtBig"),
123+ (eOpFn tyBigInt tyInt "gtBig") total,
120124 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
121− (eOpFn tyBigInt tyInt "geBig"),
125+ (eOpFn tyBigInt tyInt "geBig") total,
122126 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
123− (eOp E.plusF_),
127+ (eOp E.plusF_) total,
124128 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
125− (eOp E.minusF_),
129+ (eOp E.minusF_) total,
126130 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
127− (eOp E.timesF_),
131+ (eOp E.timesF_) total,
128132 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
129− (eOp E.divideF_),
133+ (eOp E.divideF_) total,
130134 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
131− (eOp E.eqF_),
135+ (eOp E.eqF_) total,
132136 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
133− (eOp E.ltF_),
137+ (eOp E.ltF_) total,
134138 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
135− (eOp E.lteF_),
139+ (eOp E.lteF_) total,
136140 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
137− (eOp E.gtF_),
141+ (eOp E.gtF_) total,
138142 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
139− (eOp E.gteF_),
143+ (eOp E.gteF_) total,
140144 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,
142146 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,
144148 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,
146150 -- Conversions
147151 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,
149153 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,
151155 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,
153157 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,
155159 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,
157161 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,
159163 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,
161165 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,
163167 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,
165169 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,
167171 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,
169173
170174 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,
172176 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,
174178 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,
176180 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,
178182 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,
180184 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,
182186 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,
184188 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,
186190 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,
188192 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,
190194 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,
192196
193197 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,
195199 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,
197201 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,
199203 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,
201205 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,
203207
204208 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
206210 ]
207211
208212p_believeMe [_,_,x] = Just x
@@ -241,7 +245,9 @@ sBin _ _ = Nothing
241245
242246c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
243247c_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)
245251c_strToInt _ = Nothing
246252
247253c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
@@ -254,12 +260,16 @@ c_intToBigInt _ = Nothing
254260
255261c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
256262c_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)
258266c_strToBigInt _ = Nothing
259267
260268c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
261269c_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)
263273c_strToFloat _ = Nothing
264274
265275c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
@@ -296,8 +306,9 @@ p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
296306p_strRev _ = Nothing
297307
298308elabPrim :: Prim -> Idris ()
299−elabPrim (Prim n ty i def epic)
309+elabPrim (Prim n ty i def epic tot)
300310 = do updateContext (addOperator n ty i def)
311+ setTotality n tot
301312 i <- getIState
302313 putIState i { idris_prims = (n, epic) : idris_prims i }
303314