ref: 3a29356d120d0a22a1ae327cad2ee55766e82608
parent: 0c7e35d8ca86321511f84a2c88999b18dc50f74f
parent: 25a4ef8b3bbfd898fa1e029a1228b863cac8c434
author: Rewbert <krookr@chalmers.se>
date: Mon Sep 25 09:15:19 EDT 2023
merge
--- a/README.md
+++ b/README.md
@@ -130,10 +130,15 @@
Available commands:
* `:quit` Quit the interactive system
-* `:clear` Clear all definitions
+* `:clear` Get back to start state
* `:del STR` Delete all definitions that begin with `STR`
* `expr` Evaluate expression. ***NOTE*** Currently only expressions of type `Int` are allowed.
* `defn` Add definition (can also be an `import`)
+
+***NOTE*** When you `import` a module it is cached.
+If the file changes and you import it again it will not reload.
+You can use `:clear` no get back to an empty cache.
+This is a bug.
## Runtime
The runtime system is written in C and is in `eval.c`.
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v3.5
-916
-(($A :0 _802) (($A :1 (($B _848) _0)) (($A :2 ((($S' _848) _0) $I)) (($A :3 _772) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _801) (($C _68) _5))) (($A :7 ((($C' _6) (_819 _65)) ((_68 _817) _64))) (($A :8 (($B (($S _848) _817)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_68 _179)) _10)) (($A :12 (($B ($B (_67 _9))) ((($C' $B) (($B $C) _10)) ($B _10)))) (($A :13 (($B ($B (_67 _9))) ((($C' $B) (($B $C) _10)) ($BK _10)))) (($A :14 (($B (_67 _9)) $P)) (($A :15 (($B ($B (_67 _9))) (($B (($C' $C) _10)) ($B $P)))) (($A :16 _15) (($A :17 (($B (_67 _9)) ($B ($P _731)))) (($A :18 (($B (_67 _9)) ($BK ($P _731)))) (($A :19 ((_67 _9) (($S $P) $I))) (($A :20 (($B (_67 _9)) (($C ($S' $P)) $I))) (($A :21 (($B $Y) (($B ($B ($P (_14 _108)))) ((($C' $B) (($B ($C' $B)) ($B _12))) ((($C' ($C' $B)) ($B _12)) (($B ($B _14)) _109)))))) (($A :22 (($B $Y) (($B ($B ($P (_14 _731)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _731))) (($A :25 (($C $C) _32)) (($A :26 ($T _31)) (($A :27 (($P _32) _31)) (($A :28 _32) (($A :29 (($C (($C $S') _27)) $I)) (($A :30 (($C $S) _27)) (($A :31 $K) (($A :32 $A) (($A :33 _777) (($A :34 _778) (($A :35 ((($S' _26) (_769 97)) (($C _769) 122))) (($A :36 ((($S' _26) (_769 65)) (($C _769) 90))) (($A :37 ((($S' _25) _35) _36)) (($A :38 ((($S' _26) (_769 48)) (($C _769) 57))) (($A :39 ((($S' _26) (_769 32)) (($C _769) 126))) (($A :40 _766) (($A :41 _767) (($A :42 _769) (($A :43 _768) (($A :44 _738) (($A :45 _739) (($A :46 _740) (($A :47 (_45 f0.0)) (($A :48 _44) (($A :49 _45) (($A :50 _46) (($A :51 _741) (($A :52 _742) (($A :53 _51) (($A :54 _52) (($A :55 _743) (($A :56 _744) (($A :57 _745) (($A :58 _746) (($A :59 _55) (($A :60 _56) (($A :61 _57) (($A :62 _58) (($A :63 _747) (($A :64 (($B $BK) $T)) (($A :65 ($BK $T)) (($A :66 $P) (($A :67 $I) (($A :68 $B) (($A :69 $I) (($A :70 $K) (($A :71 $C) (($A :72 _773) (($A :73 (($C (($C $S') _179)) _180)) (($A :74 ((($C' ($S' ($C' $B))) $B) $I)) (($A :75 _732) (($A :76 _733) (($A :77 _734) (($A :78 _735) (($A :79 _736) (($A :80 _737) (($A :81 (_76 0)) (($A :82 _754) (($A :83 _755) (($A :84 _756) (($A :85 _757) (($A :86 _758) (($A :87 _759) (($A :88 _82) (($A :89 ($BK $K)) (($A :90 (($B $BK) (($B ($B $BK)) $P))) (($A :91 (($B ($B ($B $BK))) (($B ($B ($B $BK))) (($B ($B ($B $C))) (($B ($B $C)) $P))))) (($A :92 ((($S' $S) ((($S' ($S' $C)) ((($C' ($C' $S)) ((($C' $B) (($B ($S' $S')) ((($C' $B) (($B _25) (_85 0))) (_82 0)))) (($B ($B (($C' $P) (_80 1)))) _75))) ($C $P))) _78)) _79)) (($A :93 _89) (($A :94 ((($S' $C) (($B ($P _168)) ((($C' ($C' $B)) ((($C' $C) _82) _168)) _169))) (($B (($C' ($C' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) (($B (($C' ($C' ($C' $C))) (($B ($B ($B (($S' $S') (_82 0))))) (($B (($C' ($C' $C)) (($B ($B (($S' $S') (_82 1)))) (($B (($C' $C) (($B (($C' $S') (_82 2))) ($C _94)))) ($C _94))))) ($C _94))))) ($C _94)))) ($T $K))) ($T $A)))) (($C _92) 4)))) (($A :95 (_101 _70)) (($A :96 ((_116 (_73 _95)) _93)) (($A :97 (($C ((($C' $B) (($P _108) ((($C' ($C' $O)) $P) $K))) ((($S' ($C' ($C' ($C' $B)))) (($B ($B ($B ($B _98)))) ((($S' ($C' ($C' $B))) (($B ($B ($B _98))) ((($S' ($C' $B)) (($B ($B _98)) ((($C' $B) (($B _114) ($T 0))) _97))) ((($C' $B) (($B _114) ($T 1))) _97)))) ((($C' $B) (($B _114) ($T 2))) _97)))) ((($C' $B) (($B _114) ($T 3))) _97)))) (($B $T) (($B ($B $P)) (($C' _75) (_77 4)))))) (($A :98 (($S $S) (($B $BK) (($B $BK) ((($S' $S) $T) (($B $BK) (($B $BK) (($C ((($S' $C') $S) (($B ($B ($B ($S $B)))) (($B ($B ($B ($B ($B $BK))))) (($B (($S' ($C' $B)) (($B $B') $B'))) (($B ($B ($B ($B ($B ($S $B)))))) (($B ($B ($B ($B ($B ($B ($B $BK))))))) ((($C' $B) ($B' ($B' (($B ($C' ($C' ($C' $C)))) (($B (($C' $B) ($B' (($B $C) _84)))) (($B (($C' $B) _109)) _98)))))) (($B (($C' $B) _109)) ($C _98)))))))))) (((_730 "lib/Data/IntMap.hs") 3) 8))))))))) (($A :99 ((_68 (_114 _179)) _97)) (($A :100 ((($C' $C) ((($C' $C) ($C _94)) (_3 "Data.IntMap.!"))) $I)) (($A :101 (($B (($C' $B) $T)) (($B ($B $Y)) ((($C' ($C' ($S' ($S' $C)))) (($B (($S' $B) (($B ($S' $P)) ($C _90)))) (($B ($B (($C' ($S' $C)
\ No newline at end of file
+922
+(($A :0 _807) (($A :1 (($B _853) _0)) (($A :2 ((($S' _853) _0) $I)) (($A :3 _777) (($A :4 (_3 "undefined")) (($A :5 $I) (($A :6 ((($C' $B) _806) (($C _69) _5))) (($A :7 ((($C' _6) (_824 _66)) ((_69 _822) _65))) (($A :8 (($B (($S _853) _822)) _3)) (($A :9 $T) (($A :10 ($T $I)) (($A :11 (($B (_69 _181)) _10)) (($A :12 (($B ($B (_68 _9))) ((($C' $B) (($B $C) _10)) ($B _10)))) (($A :13 (($B ($B (_68 _9))) ((($C' $B) (($B $C) _10)) ($BK _10)))) (($A :14 (($B (_68 _9)) $P)) (($A :15 (($B ($B (_68 _9))) (($B (($C' $C) _10)) ($B $P)))) (($A :16 _15) (($A :17 (($B (_68 _9)) ($B ($P _736)))) (($A :18 (($B (_68 _9)) ($BK ($P _736)))) (($A :19 ((_68 _9) (($S $P) $I))) (($A :20 (($B (_68 _9)) (($C ($S' $P)) $I))) (($A :21 (($B $Y) (($B ($B ($P (_14 _109)))) ((($C' $B) (($B ($C' $B)) ($B _12))) ((($C' ($C' $B)) ($B _12)) (($B ($B _14)) _110)))))) (($A :22 (($B $Y) (($B ($B ($P (_14 _736)))) (($B ($C' $B)) ($B _13))))) (($A :23 _3) (($A :24 ($T (_14 _736))) (($A :25 (($C $C) _32)) (($A :26 ($T _31)) (($A :27 (($P _32) _31)) (($A :28 _32) (($A :29 (($C (($C $S') _27)) $I)) (($A :30 (($C $S) _27)) (($A :31 $K) (($A :32 $A) (($A :33 _782) (($A :34 _783) (($A :35 ((($S' _26) (_774 97)) (($C _774) 122))) (($A :36 ((($S' _26) (_774 65)) (($C _774) 90))) (($A :37 ((($S' _25) _35) _36)) (($A :38 ((($S' _26) (_774 48)) (($C _774) 57))) (($A :39 ((($S' _26) (_774 32)) (($C _774) 126))) (($A :40 _771) (($A :41 _772) (($A :42 _774) (($A :43 _773) (($A :44 ((($S' _25) (($C _40) 32)) ((($S' _25) (($C _40) 9)) (($C _40) 10)))) (($A :45 _743) (($A :46 _744) (($A :47 _745) (($A :48 (_46 f0.0)) (($A :49 _45) (($A :50 _46) (($A :51 _47) (($A :52 _746) (($A :53 _747) (($A :54 _52) (($A :55 _53) (($A :56 _748) (($A :57 _749) (($A :58 _750) (($A :59 _751) (($A :60 _56) (($A :61 _57) (($A :62 _58) (($A :63 _59) (($A :64 _752) (($A :65 (($B $BK) $T)) (($A :66 ($BK $T)) (($A :67 $P) (($A :68 $I) (($A :69 $B) (($A :70 $I) (($A :71 $K) (($A :72 $C) (($A :73 _778) (($A :74 (($C (($C $S') _181)) _182)) (($A :75 ((($C' ($S' ($C' $B))) $B) $I)) (($A :76 _737) (($A :77 _738) (($A :78 _739) (($A :79 _740) (($A :80 _741) (($A :81 _742) (($A :82 (_77 0)) (($A :83 _759) (($A :84 _760) (($A :85 _761) (($A :86 _762) (($A :87 _763) (($A :88 _764) (($A :89 _83) (($A :90 ($BK $K)) (($A :91 (($B $BK) (($B ($B $BK)) $P))) (($A :92 (($B ($B ($B $BK))) (($B ($B ($B $BK))) (($B ($B ($B $C))) (($B ($B $C)) $P))))) (($A :93 ((($S' $S) ((($S' ($S' $C)) ((($C' ($C' $S)) ((($C' $B) (($B ($S' $S')) ((($C' $B) (($B _25) (_86 0))) (_83 0)))) (($B ($B (($C' $P) (_81 1)))) _76))) ($C $P))) _79)) _80)) (($A :94 _90) (($A :95 ((($S' $C) (($B ($P _170)) ((($C' ($C' $B)) ((($C' $C) _83) _170)) _171))) (($B (($C' ($C' ($C' $C))) ((($C' ($C' ($C' $C))) ((($C' ($C' ($C' ($C' $S')))) (($B ($B ($B ($B $C)))) (($B (($C' ($C' ($C' $C))) (($B ($B ($B (($S' $S') (_83 0))))) (($B (($C' ($C' $C)) (($B ($B (($S' $S') (_83 1)))) (($B (($C' $C) (($B (($C' $S') (_83 2))) ($C _95)))) ($C _95))))) ($C _95))))) ($C _95)))) ($T $K))) ($T $A)))) (($C _93) 4)))) (($A :96 (_102 _71)) (($A :97 ((_117 (_74 _96)) _94)) (($A :98 (($C ((($C' $B) (($P _109) ((($C' ($C' $O)) $P) $K))) ((($S' ($C' ($C' ($C' $B)))) (($B ($B ($B ($B _99)))) ((($S' ($C' ($C' $B))) (($B ($B ($B _99))) ((($S' ($C' $B)) (($B ($B _99)) ((($C' $B) (($B _115) ($T 0))) _98))) ((($C' $B) (($B _115) ($T 1))) _98)))) ((($C' $B) (($B _115) ($T 2))) _98)))) ((($C' $B) (($B _115) ($T 3))) _98)))) (($B $T) (($B ($B $P)) (($C' _76) (_78 4)))))) (($A :99 (($S $S) (($B $BK) (($B $BK) ((($S' $S) $T) (($B $BK) (($B $BK) (($C ((($S' $C') $S) (($B ($B ($B ($S $B)))) (($B ($B ($B ($B ($B $BK))))) (($B (($S' ($C' $B)) (($B $B') $B'))) (($B ($B ($B ($B ($B ($S $B)))))) (($B ($B ($B ($B ($B ($B ($B $BK))))))) ((($C' $B) ($B' ($B' (($B ($C' ($C' ($C' $C)))) (($B (($C' $B) ($B' (($B $C) _85)))) (($B (($C' $B) _110)) _99)))))) (($B (($C' $B) _110)) ($C _99)))))))))) (((_735 "lib/Data/IntMap.hs") 3) 8))))))))) (($A :100 ((_69 (_115 _181)) _98)) (($A :101 ((($C' $C) ((($C' $C) ($C _95)) (_3 "Data.IntMap.!"))) $I)) (($A :102 (($B (($C' $B) $T)) (($B ($B $Y)) ((($C' ($C' ($
\ No newline at end of file
--- a/lib/Data/Char.hs
+++ b/lib/Data/Char.hs
@@ -39,3 +39,6 @@
ltChar :: Char -> Char -> Bool
ltChar = primCharLT
+
+isSpace :: Char -> Bool
+isSpace c = eqChar c ' ' || eqChar c '\t' || eqChar c '\n'
--- a/lib/Data/Integer.hs
+++ b/lib/Data/Integer.hs
@@ -1,69 +1,407 @@
-- Copyright 2023 Lennart Augustsson
-- See LICENSE file for full license.
-- *** WIP, do not use! ***
-module Data.Integer(Integer) where
---Yimport Primitives(Word)
-import Control.Error
-import Data.Bool
-import Data.Function
-import qualified Data.Int as I
-import Data.List
-import qualified Data.Word as W
+module Data.Integer(
+ Integer,
+ addI, subI, mulI, quotI, remI,
+ negateI, absI,
+ quotRemI,
+ eqI, neI, ltI, leI, gtI, geI,
+ intToInteger,
+ showInteger,
+ ) where
+import Prelude
+{-+import Prelude hiding(Integer)
+import qualified Prelude as P
+import Data.Char
+import Compat
+import Test.QuickCheck
+import GHC.Stack
+import Debug.Trace
+-}
+--
+-- The Integer is stored in sign-magniture format with digits in base maxD (2^31)
+-- It has the following invariants:
+-- * each digit is >= 0 and < maxD
+-- * least signification digits first, most significant last
+-- * no tariling 0s in the digits
+-- * 0 is positive
+data Integer = I Sign [Digit]
+ --deriving Show
+
+type Digit = Int
+
data Sign = Plus | Minus
+ --deriving Show
-data Integer = I Sign [Word] -- each word is <2^32, LSW first
+eqSign :: Sign -> Sign -> Bool
+eqSign Plus Plus = True
+eqSign Minus Minus = True
+eqSign _ _ = False
-zeroW :: Word
-zeroW = W.intToWord 0
+-- Trim off 0s and make an Integer
+sI :: Sign -> [Digit] -> Integer
+sI s ds =
+ case trim0 ds of
+ [] -> I Plus []
+ ds' -> I s ds'
-maxW :: Word
-maxW = W.intToWord 4294967296
+intToInteger :: Int -> Integer
+intToInteger i | i >= 0 = I Plus (f i)
+ | i == negate i = I Minus [0,0,2] -- we are at minBound::Int. XXX deal with this in a more portable way.
+ | otherwise = I Minus (f (negate i))
+ where
+ f 0 = []
+ f x = rem x maxD : f (quot x maxD)
-(+) :: Integer -> Integer -> Integer
-(+) (I Plus xs) (I Plus ys) = I Plus (add xs ys)
-(+) (I Plus xs) (I Minus ys) | ltW xs ys = I Minus (sub ys xs)
- | True = I Plus (sub xs ys)
-(+) (I Minus xs) (I Plus ys) | ltW ys xs = I Minus (sub xs ys)
- | True = I Plus (sub ys xs)
-(+) (I Minus xs) (I Minus ys) = I Minus (add xs ys)
+zeroD :: Digit
+zeroD = 0
-negate :: Integer -> Integer
-negate (I Plus x) = I Minus x
-negate (I Minus x) = I Plus x
+maxD :: Digit
+maxD = 2147483648 -- 2^31, this is used so multiplication of two digit doesn't overflow a 64 bit Int
-(-) :: Integer -> Integer -> Integer
-(-) x y = x + negate y
+addI :: Integer -> Integer -> Integer
+addI (I Plus xs) (I Plus ys) = I Plus (add xs ys)
+addI (I Plus xs) (I Minus ys) | ltW xs ys = sI Minus (sub ys xs)
+ | True = sI Plus (sub xs ys)
+addI (I Minus xs) (I Plus ys) | ltW ys xs = sI Minus (sub xs ys)
+ | True = sI Plus (sub ys xs)
+addI (I Minus xs) (I Minus ys) = I Minus (add xs ys)
-add :: [Word] -> [Word] -> [Word]
-add = add' zeroW
+negateI :: Integer -> Integer
+negateI i@(I _ []) = i
+negateI (I Plus x) = I Minus x
+negateI (I Minus x) = I Plus x
-add' :: Word -> [Word] -> [Word] -> [Word]
-add' ci (x : xs) (y : ys) = s : add' co xs ys where (s, co) = addW ci x y
-add' ci (x : xs) [] = s : add' co xs [] where (s, co) = addW ci x zeroW
-add' ci [] (y : ys) = s : add' co [] ys where (s, co) = addW ci zeroW y
-add' ci [] [] = if (W.==) ci zeroW then [] else [ci]
+absI :: Integer -> Integer
+absI (I _ x) = I Plus x
--- Add 3 words with carry
-addW :: Word -> Word -> Word -> (Word, Word)
-addW x y z = (W.quot s maxW, W.rem s maxW) where s = (W.+) ((W.+) x y) z
+subI :: Integer -> Integer -> Integer
+subI x y = addI x (negateI y)
--- We always have xs <= ys
-sub :: [Word] -> [Word] -> [Word]
-sub = sub' zeroW
+add :: [Digit] -> [Digit] -> [Digit]
+add = add' zeroD
-sub' :: Word -> [Word] -> [Word] -> [Word]
-sub' bi (x : xs) (y : ys) = d : sub' bo xs ys where (d, bo) = subW bi x y
+add' :: Digit -> [Digit] -> [Digit] -> [Digit]
+add' ci (x : xs) (y : ys) = s : add' co xs ys where (co, s) = addD ci x y
+add' ci (x : xs) [] = s : add' co xs [] where (co, s) = addD ci x zeroD
+add' ci [] (y : ys) = s : add' co [] ys where (co, s) = addD ci zeroD y
+add' ci [] [] = if ci == zeroD then [] else [ci]
-subW :: Word -> Word -> Word -> (Word, Word)
-subW _ _ _ = error "subW"
+-- Add 3 digits with carry
+addD :: Digit -> Digit -> Digit -> (Digit, Digit)
+addD x y z = (quot s maxD, rem s maxD) where s = x + y + z
-ltW :: [Word] -> [Word] -> Bool
-ltW axs ays = (I.<) lxs lys || (I.==) lxs lys && cmp (reverse axs) (reverse ays)
+-- Invariant: xs >= ys, so result is always >= 0
+sub :: [Digit] -> [Digit] -> [Digit]
+sub xs ys = sub' zeroD xs ys
+
+sub' :: Digit -> [Digit] -> [Digit] -> [Digit]
+sub' bi (x : xs) (y : ys) = d : sub' bo xs ys where (bo, d) = subW bi x y
+sub' bi (x : xs) [] = d : sub' bo xs [] where (bo, d) = subW bi x zeroD
+sub' 0 [] [] = []
+sub' _ [] _ = undefined
+
+-- Subtract with borrow
+subW :: Digit -> Digit -> Digit -> (Digit, Digit)
+subW b x y =
+ let d = x - y + b
+ in if d < 0 then
+ (quot d maxD - 1, rem d maxD + maxD)
+ else
+ (quot d maxD, rem d maxD)
+
+-- Remove trailing 0s
+trim0 :: [Digit] -> [Digit]
+trim0 = reverse . dropWhile (== 0) . reverse
+
+-- Is axs < ays?
+ltW :: [Digit] -> [Digit] -> Bool
+ltW axs ays = lxs < lys || lxs == lys && cmp (reverse axs) (reverse ays)
where
lxs = length axs
lys = length ays
- cmp (x:xs) (y:ys) = (W.<) x y || (W.==) x y && cmp xs ys
+ cmp (x:xs) (y:ys) = x < y || x == y && cmp xs ys
cmp [] [] = False
cmp _ _ = error "cmp"
+mulI :: Integer -> Integer -> Integer
+mulI (I _ []) _ = I Plus [] -- 0 * x = 0
+mulI _ (I _ []) = I Plus [] -- x * 0 = 0
+mulI (I sx [x]) (I sy ys) = I (mulSign sx sy) (mulD zeroD ys x)
+mulI (I sx xs) (I sy [y]) = I (mulSign sx sy) (mulD zeroD xs y)
+mulI (I sx xs) (I sy ys) = I (mulSign sx sy) (mulM xs ys)
+
+mulSign :: Sign -> Sign -> Sign
+mulSign s t = if eqSign s t then Plus else Minus
+
+-- Multiply with a single digit, and add carry.
+mulD :: Digit -> [Digit] -> Digit -> [Digit]
+mulD ci [] _ = if ci == 0 then [] else [ci]
+mulD ci (x:xs) y = r : mulD q xs y
+ where
+ xy = x * y + ci
+ q = quot xy maxD
+ r = rem xy maxD
+
+mulM :: [Digit] -> [Digit] -> [Digit]
+mulM xs ys =
+ let rs = map (mulD zeroD xs) ys
+ ss = zipWith (++) (map (`replicate` 0) [0..]) rs
+ in foldl1 add ss
+
+quotI :: Integer -> Integer -> Integer
+quotI x y = fst (quotRemI x y)
+
+remI :: Integer -> Integer -> Integer
+remI x y = snd (quotRemI x y)
+
+-- Signs:
+-- + + -> (+,+)
+-- + - -> (-,+)
+-- - + -> (-,-)
+-- - - -> (+,-)
+quotRemI :: Integer -> Integer -> (Integer, Integer)
+quotRemI _ (I _ []) = error "Integer: division by 0" -- n / 0
+quotRemI (I _ []) _ = (I Plus [], I Plus []) -- 0 / n
+quotRemI (I sx xs) (I sy ys) | all (== 0) ys' =
+ -- All but the MSD are 0. Scale numerator accordingly and divide.
+ -- Then add back (the ++) the remainder we scaled off.
+ case quotRemD xs' y of
+ (q, r) -> qrRes sx sy (q, rs ++ r)
+ where ys' = init ys
+ y = last ys
+ n = length ys'
+ (rs, xs') = splitAt n xs -- xs' is the scaled number
+quotRemI (I sx xs) (I sy ys) = qrRes sx sy (quotRemB xs ys)
+
+qrRes :: Sign -> Sign -> ([Digit], [Digit]) -> (Integer, Integer)
+qrRes sx sy (ds, rs) = (sI (mulSign sx sy) ds, sI sx rs)
+
+-- Divide by a single digit.
+-- Does not return normalized numbers.
+quotRemD :: [Digit] -> Digit -> ([Digit], [Digit])
+quotRemD axs y = qr zeroD (reverse axs) []
+ where
+ qr ci [] res = (res, [ci])
+ qr ci (x:xs) res = qr r xs (q:res)
+ where
+ cx = ci * maxD + x
+ q = quot cx y
+ r = rem cx y
+
+-- Simple iterative long division.
+quotRemB :: [Digit] -> [Digit] -> ([Digit], [Digit])
+quotRemB xs ys =
+ let n = I Plus xs
+ d = I Plus ys
+ a = I Plus $ replicate (length ys - 1) 0 ++ [last ys] -- only MSD of ys
+ aq = quotI n a
+ ar = addI d oneI
+ loop q r =
+ if absI r `geI` d then
+ let r' = n `subI` (q `mulI` d)
+ qn = q `addI` (r' `quotI` a)
+ q' = (q `addI` qn) `quotI` twoI
+ in loop q' r'
+ else
+ q
+ q' = loop aq ar
+ r = n `subI` (q' `mulI` d)
+ in if r `ltI` zeroI then
+ (digits (q' `subI` oneI), digits (r `addI` d))
+ else
+ (digits q', digits r)
+
+digits :: Integer -> [Digit]
+digits (I _ ds) = ds
+
+zeroI :: Integer
+zeroI = I Plus []
+
+oneI :: Integer
+oneI = I Plus [1]
+
+twoI :: Integer
+twoI = I Plus [2]
+
+--------------
+
+showInteger :: Integer -> String
+showInteger (I _ []) = "0"
+showInteger (I Minus xs) = '-' : showInteger' xs
+showInteger (I Plus xs) = showInteger' xs
+
+showInteger' :: [Digit] -> String
+showInteger' [] = ""
+showInteger' xs = showInteger' (trim0 xs') ++ [chr (ord '0' + d)]
+ where
+ (xs', [d]) = quotRemD xs 10
+
+eqI :: Integer -> Integer -> Bool
+eqI (I sx xs) (I sy ys) = eqSign sx sy && eqList (==) xs ys
+
+neI :: Integer -> Integer -> Bool
+neI x y = not (eqI x y)
+
+ltI :: Integer -> Integer -> Bool
+ltI (I Plus xs) (I Plus ys) = ltW xs ys
+ltI (I Minus _) (I Plus _) = True
+ltI (I Plus _) (I Minus _) = False
+ltI (I Minus xs) (I Minus ys) = ltW ys xs
+
+leI :: Integer -> Integer -> Bool
+leI x y = not (ltI y x)
+
+gtI :: Integer -> Integer -> Bool
+gtI x y = ltI y x
+
+geI :: Integer -> Integer -> Bool
+geI x y = not (ltI x y)
+
+---------------------------------
+{-+pIntegerToInteger :: P.Integer -> Integer
+pIntegerToInteger i | i >= 0 = I Plus (f i)
+ | otherwise = I Minus (f (negate i))
+ where
+ f 0 = []
+ f x = fromInteger (rem x (toInteger maxD)) : f (quot x (toInteger maxD))
+
+integerToPInteger :: Integer -> P.Integer
+integerToPInteger (I s xs) =
+ let r = foldr (\ d r -> r * toInteger maxD + toInteger d) 0 xs
+ in case s of
+ Plus -> r
+ Minus -> negate r
+
+instance Num Integer where
+ (+) = addI
+ (-) = subI
+ (*) = mulI
+ abs x = if x < 0 then -x else x
+ signum x = if x > 0 then 1 else if x < 0 then -1 else 0
+ fromInteger = pIntegerToInteger
+
+instance Enum Integer where
+ fromEnum = fromEnum . integerToPInteger
+ toEnum = intToInteger
+
+instance Real Integer where
+ toRational = toRational . toInteger
+
+instance Integral Integer where
+ quotRem = quotRemI
+ toInteger = integerToPInteger
+
+--instance Show Integer where
+-- show = showInteger
+
+instance Eq Integer where
+ (==) = eqI
+
+instance Ord Integer where
+ x < y = x `ltI` y
+ x <= y = x == y || x `ltI` y
+ x > y = y `ltI` x
+ x >= y = x == y || y `ltI` x
+
+instance Arbitrary Integer where
+ arbitrary = do
+ ndig <- frequency
+ [(5, pure 0)
+ ,(25, pure 1)
+ ,(20, pure 2)
+ ,(10, pure 3)
+ ,(10, pure 4)
+ ,(2, pure 5)
+ ,(2, pure 6)
+ ]
+ digits <- vectorOf ndig (chooseInt (0, maxD - 1))
+ sign <- elements [Plus, Minus]
+ pure $ if null digits then I Plus [] else I sign digits
+
+{-+newtype SmallInteger = SmallInteger Integer
+ deriving Show
+
+instance Arbitrary SmallInteger where
+ arbitrary = do
+ ndig <- frequency
+ [(25, pure 1)
+ ,(20, pure 2)
+ ,(10, pure 3)
+ ,(10, pure 4)
+ ]
+ digit <- chooseInt (1, maxD - 1)
+ sign <- elements [Plus, Minus]
+ pure $ SmallInteger $ I sign (replicate (ndig - 1) 0 ++ [digit])
+-}
+{-+sanity :: HasCallStack => Integer -> Integer
+sanity (I Minus []) = undefined
+sanity (I _ ds) | any (< 0) ds = undefined
+sanity (I _ ds) | length ds > 1 && last ds == 0 = undefined
+sanity i = i
+-}
+
+prop_roundtrip1 :: Integer -> Bool
+prop_roundtrip1 i = fromInteger (toInteger i) == i
+
+prop_negate :: Integer -> Bool
+prop_negate i = toInteger (negate i) == negate (toInteger i)
+
+prop_abs :: Integer -> Bool
+prop_abs i = toInteger (abs i) == abs (toInteger i)
+
+prop_add :: Integer -> Integer -> Bool
+prop_add x y = toInteger (addI x y) == toInteger x + toInteger y
+
+prop_sub :: Integer -> Integer -> Bool
+prop_sub x y = toInteger (subI x y) == toInteger x - toInteger y
+
+prop_mul :: Integer -> Integer -> Bool
+prop_mul x y = toInteger (mulI x y) == toInteger x * toInteger y
+
+prop_div :: Integer -> NonZero Integer -> Bool
+prop_div x (NonZero y) =
+ to (quotRemI x y) == toInteger x `quotRem` toInteger y
+ where to (a, b) = (toInteger a, toInteger b)
+
+prop_muldiv :: Integer -> NonZero Integer -> Bool
+prop_muldiv x (NonZero y) =
+ let (q, r) = quotRemI x y
+ in q*y + r == x
+
+prop_eq :: Integer -> Integer -> Bool
+prop_eq x y = (eqI x y) == (toInteger x == toInteger y)
+
+prop_ne :: Integer -> Integer -> Bool
+prop_ne x y = (neI x y) == (toInteger x /= toInteger y)
+
+prop_lt :: Integer -> Integer -> Bool
+prop_lt x y = (ltI x y) == (toInteger x < toInteger y)
+
+prop_gt :: Integer -> Integer -> Bool
+prop_gt x y = (gtI x y) == (toInteger x > toInteger y)
+
+prop_le :: Integer -> Integer -> Bool
+prop_le x y = (leI x y) == (toInteger x <= toInteger y)
+
+prop_ge :: Integer -> Integer -> Bool
+prop_ge x y = (geI x y) == (toInteger x >= toInteger y)
+
+prop_show :: Integer -> Bool
+prop_show x = showInteger x == show (toInteger x)
+
+checkAll :: IO ()
+checkAll = do
+ let qc p = quickCheck (withMaxSuccess 100000 p)
+ mapM_ qc [prop_roundtrip1, prop_negate, prop_abs, prop_show]
+ mapM_ qc [prop_add, prop_sub, prop_mul,
+ prop_eq, prop_ne, prop_lt, prop_gt, prop_le, prop_ge]
+ mapM_ qc [prop_div, prop_muldiv]
+
+-}
--- a/lib/Data/List.hs
+++ b/lib/Data/List.hs
@@ -305,3 +305,8 @@
last [] = error "last: []"
last [x] = x
last (_:xs) = last xs
+
+init :: forall a . [a] -> [a]
+init [] = error "init: []"
+init [_] = []
+init (x:xs) = x : init xs
--- a/lib/Text/String.hs
+++ b/lib/Text/String.hs
@@ -96,6 +96,14 @@
unlines :: [String] -> String
unlines = concatMap (++ "\n")
+
+words :: String -> [String]
+words s =
+ case dropWhile isSpace s of
+ "" -> []
+ s' -> w : words s''
+ where (w, s'') = span (not . isSpace) s'
+
unwords :: [String] -> String
unwords ss = intercalate " " ss
@@ -114,8 +122,9 @@
[] -> False
y:ys -> eqChar x y && eqString xs ys
-}
-
leString :: String -> String -> Bool
+leString s t = not (eqOrdering GT (compareString s t))
+{-leString axs ays =
case axs of
[] -> True
@@ -123,6 +132,7 @@
case ays of
[] -> False
y:ys -> ltChar x y || eqChar x y && leString xs ys
+-}
padLeft :: Int -> String -> String
padLeft n s = replicate (n - length s) ' ' ++ s
--- a/src/MicroHs/Interactive.hs
+++ b/src/MicroHs/Interactive.hs
@@ -33,16 +33,44 @@
ms <- S.liftIO $ getInputLineHist ".mhsi" "> "
case ms of
Nothing -> repl
- Just ":quit" -> S.liftIO $ putStrLn "Bye"
- Just ":clear" -> S.do
+ Just s ->
+ case s of
+ [] -> repl
+ ':':r -> S.do
+ c <- command r
+ if c then repl else S.liftIO $ putStrLn "Bye"
+ _ -> S.do
+ oneline s
+ repl
+
+command :: String -> I Bool
+command s =
+ case words s of
+ [] -> S.return True
+ c : ws ->
+ case filter (isPrefixOfBy eqChar c . fst) commands of
+ [] -> S.do
+ S.liftIO $ putStrLn "Unrecognized command"
+ S.return True
+ [(_, cmd)] ->
+ cmd (unwords ws)
+ xs -> S.do
+ S.liftIO $ putStrLn $ "Ambiguous command: " ++ unwords (map fst xs)
+ S.return True
+
+commands :: [(String, String -> I Bool)]
+commands =
+ [ ("quit", const $ S.return False)+ , ("clear", const $ S.doupdateLines (const preamble)
- repl
- Just s | Just del <- stripPrefixBy eqChar ":del " s -> S.do
+ S.modify $ \ (ls, flgs, _) -> (ls, flgs, emptyCache)
+ S.return True
+ )
+ , ("delete", \ del -> S.doupdateLines (unlines . filter (not . isPrefixOfBy eqChar del) . lines)
- repl
- Just s -> S.do
- oneline s
- repl
+ S.return True
+ )
+ ]
updateLines :: (String -> String) -> I ()
updateLines f = S.modify $ \ (ls, flgs, cache) -> (f ls, flgs, cache)
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -60,8 +60,18 @@
(fexps, sexps) = unzip $ getFSExps impMap
-}
fexps = [ fe | TModule _ fe _ _ _ _ <- M.elems impMap ]
- in TModule mn (nubBy (eqIdent `on` fst) (concat fexps)) (concat texps) (concat sexps) (concat vexps) tds
+ in tModule mn (nubBy (eqIdent `on` fst) (concat fexps)) (concat texps) (concat sexps) (concat vexps) tds
+-- A hack to force evaluation of errors.
+-- This should be redone to all happen in the T monad.
+tModule :: IdentModule -> [FixDef] -> [TypeExport] -> [SynDef] -> [ValueExport] -> [EDef] ->
+ TModule [EDef]
+tModule mn fs ts ss vs ds = seqL ts `seq` seqL vs `seq` TModule mn fs ts ss vs ds
+ where
+ seqL :: forall a . [a] -> ()
+ seqL [] = ()
+ seqL (x:xs) = x `seq` seqL xs
+
filterImports :: forall a . (ImportSpec, TModule a) -> (ImportSpec, TModule a)
filterImports it@(ImportSpec _ _ _ Nothing, _) = it
filterImports (imp@(ImportSpec _ _ _ (Just (hide, is))), TModule mn fx ts ss vs a) =
@@ -749,7 +759,9 @@
(e, t) <- tLookupInst "variable" i
case mt of
Just tu@(EForall _ tt) -> T.do
- unify loc tt t -- XXX is this really sufficient?
+ -- XXX This is wrong in many ways.
+ -- Both t and tt may contain unification variables bound elsewhere.
+ unify loc tt t
T.return (e, tu)
_ -> T.do
munify loc mt t
--- /dev/null
+++ b/src/MicroHs/TypeCheck2.hs
@@ -1,0 +1,93 @@
+module MicroHs.TypeCheck2(module MicroHs.TypeCheck2) where
+import Data.IORef
+import qualified Data.Map as M
+type Name = String
+
+type ErrMsg = String
+type TcEnv = M.Map Name Sigma
+
+newtype Tc a = Tc (TcEnv -> IO (Either ErrMsg a))
+
+-- Control flow
+check :: Bool -> String -> Tc () -- Type inference can fail
+check = undefined
+
+-- The type environment
+lookupVar :: Name -> Tc Sigma -- Look up in the envt (may fail)
+lookupVar = undefined
+extendVarEnv :: Name -> Sigma -- Extend the envt
+ -> Tc a -> Tc a
+extendVarEnv = undefined
+getEnvTypes :: Tc [Sigma] -- Get all types in the envt
+
+-- Instantiation, skolemisation, quantification
+instantiate :: Sigma -> Tc Rho
+instantiate = undefined
+skolemise :: Sigma -> Tc ([TyVar], Rho)
+skolemise = undefined
+quantify :: [MetaTv] -> Rho -> Tc Sigma
+quantify = undefined
+
+-- Unification and fresh type variables
+newMetaTyVar :: Tc Tau -- Make (MetaTv tv), where tv is fresh
+newMetaTyVar = undefined
+newSkolemTyVar :: Tc TyVar -- Make a fresh skolem TyVar
+newSkolemTyVar = undefined
+unify :: Tau -> Tau -> Tc () -- Unification (may fail)
+unify = undefined
+
+-- Free type variables
+getMetaTyVars :: [Type] -> Tc [MetaTv]
+getMetaTyVars = undefined
+getFreeTyVars :: [Type] -> Tc [TyVar]
+getFreeTyVars = undefined
+
+newTcRef :: a -> Tc (IORef a)
+newTcRef = undefined
+readTcRef :: IORef a -> Tc a
+readTcRef = undefined
+writeTcRef :: IORef a -> a -> Tc ()
+writeTcRef = undefined
+
+---------------- Terms -------------------
+data Term
+ = Var Name -- x
+ | Lit Int -- 3
+ | App Term Term -- f x
+ | Lam Name Term -- \x. x
+ | Let Name Term Term -- let x = f y in x+1
+ | Ann Term Sigma -- f x :: Int
+
+---------------- Types -------------------
+type Sigma = Type
+type Rho = Type -- No top-level ForAll
+type Tau = Type -- No ForAlls anywhere
+
+data Type
+ = ForAll [TyVar] Rho -- Forall type
+ | Fun Type Type -- Function type
+ | TyCon TyCon -- Type constants
+ | TyVar TyVar -- Always bound by a ForAll
+ | MetaTv MetaTv -- A meta type variable
+
+data TyVar
+ = BoundTv String -- A type variable bound by a ForAll
+ | SkolemTv String Uniq -- A skolem constant; the String is
+ -- just to improve error messages
+data TyCon = IntT | BoolT
+
+(-->) :: Type -> Type-> Type -- Build a function type
+arg --> res = Fun arg res
+
+intType :: Tau
+intType = TyCon IntT
+
+--------------------------------------------
+
+data MetaTv = Meta Uniq TyRef
+type TyRef = IORef (Maybe Tau)
+ -- 'Nothing' means the type variable is not substituted
+ -- 'Just ty' means it has been substituted by ty
+type Uniq = Int
+
+--------------------------------------------
--
⑨