msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Transfer: Added Double type.

Browse Source
This commit is contained in:
bringert
2005-12-01 16:55:57 +00:00
parent f66e6e301c
commit df1e92e837
20 changed files with 1134 additions and 1002 deletions
Download Patch File Download Diff File Expand all files Collapse all files

29
src/Transfer/Core/Abs.hs
View File

@@ -59,7 +59,8 @@ data Tree :: * -> * where
EVar :: CIdent -> Tree Exp_
EType :: Tree Exp_
EStr :: String -> Tree Exp_
EInt :: Integer -> Tree Exp_
EInteger :: Integer -> Tree Exp_
EDouble :: Double -> Tree Exp_
EMeta :: TMeta -> Tree Exp_
LetDef :: CIdent -> Exp -> Exp -> Tree LetDef_
FieldType :: CIdent -> Exp -> Tree FieldType_
@@ -163,7 +164,8 @@ instance Show (Tree c) where
EVar cident -> opar n . showString "EVar" . showChar ' ' . showsPrec 1 cident . cpar n
EType -> showString "EType"
EStr str -> opar n . showString "EStr" . showChar ' ' . showsPrec 1 str . cpar n
EInt n -> opar n . showString "EInt" . showChar ' ' . showsPrec 1 n . cpar n
EInteger n -> opar n . showString "EInteger" . showChar ' ' . showsPrec 1 n . cpar n
EDouble d -> opar n . showString "EDouble" . showChar ' ' . showsPrec 1 d . cpar n
EMeta tmeta -> opar n . showString "EMeta" . showChar ' ' . showsPrec 1 tmeta . cpar n
LetDef cident exp0 exp1 -> opar n . showString "LetDef" . showChar ' ' . showsPrec 1 cident . showChar ' ' . showsPrec 1 exp0 . showChar ' ' . showsPrec 1 exp1 . cpar n
FieldType cident exp -> opar n . showString "FieldType" . showChar ' ' . showsPrec 1 cident . showChar ' ' . showsPrec 1 exp . cpar n
@@ -202,7 +204,8 @@ johnMajorEq (ERec fieldvalues) (ERec fieldvalues_) = fieldvalues == fieldvalues_
johnMajorEq (EVar cident) (EVar cident_) = cident == cident_
johnMajorEq EType EType = True
johnMajorEq (EStr str) (EStr str_) = str == str_
johnMajorEq (EInt n) (EInt n_) = n == n_
johnMajorEq (EInteger n) (EInteger n_) = n == n_
johnMajorEq (EDouble d) (EDouble d_) = d == d_
johnMajorEq (EMeta tmeta) (EMeta tmeta_) = tmeta == tmeta_
johnMajorEq (LetDef cident exp0 exp1) (LetDef cident_ exp0_ exp1_) = cident == cident_ && exp0 == exp0_ && exp1 == exp1_
johnMajorEq (FieldType cident exp) (FieldType cident_ exp_) = cident == cident_ && exp == exp_
@@ -240,14 +243,15 @@ instance Ord (Tree c) where
index (EVar _) = 22
index (EType ) = 23
index (EStr _) = 24
index (EInt _) = 25
index (EMeta _) = 26
index (LetDef _ _ _) = 27
index (FieldType _ _) = 28
index (FieldValue _ _) = 29
index (Case _ _) = 30
index (TMeta _) = 31
index (CIdent _) = 32
index (EInteger _) = 25
index (EDouble _) = 26
index (EMeta _) = 27
index (LetDef _ _ _) = 28
index (FieldType _ _) = 29
index (FieldValue _ _) = 30
index (Case _ _) = 31
index (TMeta _) = 32
index (CIdent _) = 33
compareSame (Module decls) (Module decls_) = compare decls decls_
compareSame (DataDecl cident exp consdecls) (DataDecl cident_ exp_ consdecls_) = mappend (compare cident cident_) (mappend (compare exp exp_) (compare consdecls consdecls_))
compareSame (TypeDecl cident exp) (TypeDecl cident_ exp_) = mappend (compare cident cident_) (compare exp exp_)
@@ -273,7 +277,8 @@ instance Ord (Tree c) where
compareSame (EVar cident) (EVar cident_) = compare cident cident_
compareSame EType EType = EQ
compareSame (EStr str) (EStr str_) = compare str str_
compareSame (EInt n) (EInt n_) = compare n n_
compareSame (EInteger n) (EInteger n_) = compare n n_
compareSame (EDouble d) (EDouble d_) = compare d d_
compareSame (EMeta tmeta) (EMeta tmeta_) = compare tmeta tmeta_
compareSame (LetDef cident exp0 exp1) (LetDef cident_ exp0_ exp1_) = mappend (compare cident cident_) (mappend (compare exp0 exp0_) (compare exp1 exp1_))
compareSame (FieldType cident exp) (FieldType cident_ exp_) = mappend (compare cident cident_) (compare exp exp_)

4
src/Transfer/Core/Core.cf
View File

@@ -77,7 +77,9 @@ EType. Exp5 ::= "Type" ;
-- String literal expressions.
EStr. Exp5 ::= String ;
-- Integer literal expressions.
EInt. Exp5 ::= Integer ;
EInteger. Exp5 ::= Integer ;
-- Double literal expressions.
EDouble. Exp5 ::= Double ;
-- Meta variables
EMeta. Exp5 ::= TMeta ;

7
src/Transfer/Core/Doc.tex
View File

@@ -32,6 +32,12 @@ except \terminal{"}\ unless preceded by \verb6\6.
Integer literals \nonterminal{Int}\ are nonempty sequences of digits.
Double-precision float literals \nonterminal{Double}\ have the structure
indicated by the regular expression $\nonterminal{digit}+ \mbox{{\it `.'}} \nonterminal{digit}+ (\mbox{{\it `e'}} \mbox{{\it `-'}}? \nonterminal{digit}+)?$ i.e.\
two sequences of digits separated by a decimal point, optionally
followed by an unsigned or negative exponent.
@@ -165,6 +171,7 @@ All other symbols are terminals.\\
& {\delimit} &{\terminal{Type}} \\
& {\delimit} &{\nonterminal{String}} \\
& {\delimit} &{\nonterminal{Integer}} \\
& {\delimit} &{\nonterminal{Double}} \\
& {\delimit} &{\nonterminal{TMeta}} \\
& {\delimit} &{\terminal{(}} {\nonterminal{Exp}} {\terminal{)}} \\
\end{tabular}\\

11
src/Transfer/Core/Lex.hs
View File

File diff suppressed because one or more lines are too long

2
src/Transfer/Core/Lex.x
View File

@@ -31,7 +31,7 @@ $l $i* { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t)))* \"{ tok (\p s -> PT p (TL $ share $ unescapeInitTail s)) }
$d+ { tok (\p s -> PT p (TI $ share s)) }
$d+ \. $d+ (e (\-)? $d+)? { tok (\p s -> PT p (TD $ share s)) }
{

731
src/Transfer/Core/Par.hs
View File

File diff suppressed because it is too large Load Diff

5
src/Transfer/Core/Par.y
View File

@@ -37,6 +37,7 @@ import Transfer.ErrM
L_quoted { PT _ (TL $$) }
L_integ { PT _ (TI $$) }
L_doubl { PT _ (TD $$) }
L_TMeta { PT _ (T_TMeta $$) }
L_CIdent { PT _ (T_CIdent $$) }
L_err { _ }
@@ -46,6 +47,7 @@ L_err { _ }
String :: { String } : L_quoted { $1 }
Integer :: { Integer } : L_integ { (read $1) :: Integer }
Double :: { Double } : L_doubl { (read $1) :: Double }
TMeta :: { TMeta} : L_TMeta { TMeta ($1)}
CIdent :: { CIdent} : L_CIdent { CIdent ($1)}
@@ -142,7 +144,8 @@ Exp5 : 'sig' '{' ListFieldType '}' { ERecType $3 }
| CIdent { EVar $1 }
| 'Type' { EType }
| String { EStr $1 }
| Integer { EInt $1 }
| Integer { EInteger $1 }
| Double { EDouble $1 }
| TMeta { EMeta $1 }
| '(' Exp ')' { $2 }

3
src/Transfer/Core/Print.hs
View File

@@ -105,7 +105,8 @@ instance Print (Tree c) where
EVar cident -> prPrec _i 5 (concatD [prt 0 cident])
EType -> prPrec _i 5 (concatD [doc (showString "Type")])
EStr str -> prPrec _i 5 (concatD [prt 0 str])
EInt n -> prPrec _i 5 (concatD [prt 0 n])
EInteger n -> prPrec _i 5 (concatD [prt 0 n])
EDouble d -> prPrec _i 5 (concatD [prt 0 d])
EMeta tmeta -> prPrec _i 5 (concatD [prt 0 tmeta])
LetDef cident exp0 exp1 -> prPrec _i 0 (concatD [prt 0 cident , doc (showString ":") , prt 0 exp0 , doc (showString "=") , prt 0 exp1])
FieldType cident exp -> prPrec _i 0 (concatD [prt 0 cident , doc (showString ":") , prt 0 exp])

6
src/Transfer/Core/Skel.hs
View File

@@ -36,7 +36,8 @@ transTree t = case t of
EVar cident -> failure t
EType -> failure t
EStr str -> failure t
EInt n -> failure t
EInteger n -> failure t
EDouble d -> failure t
EMeta tmeta -> failure t
LetDef cident exp0 exp1 -> failure t
FieldType cident exp -> failure t
@@ -90,7 +91,8 @@ transExp t = case t of
EVar cident -> failure t
EType -> failure t
EStr str -> failure t
EInt n -> failure t
EInteger n -> failure t
EDouble d -> failure t
EMeta tmeta -> failure t
transLetDef :: LetDef -> Result

55
src/Transfer/Interpreter.hs
View File

@@ -11,6 +11,7 @@ import Debug.Trace
data Value = VStr String
| VInt Integer
| VDbl Double
| VType
| VRec [(CIdent,Value)]
| VClos Env Exp
@@ -51,7 +52,8 @@ seqEnv (Env e) = Env $! deepSeqList [ fst p `seq` p | p <- e ]
-- | The built-in types and functions.
builtin :: Env
builtin =
mkEnv [(CIdent "Int",VType),
mkEnv [(CIdent "Integer",VType),
(CIdent "Double",VType),
(CIdent "String",VType),
mkIntUn "neg" negate toInt,
mkIntBin "add" (+) toInt,
@@ -62,6 +64,15 @@ builtin =
mkIntBin "eq" (==) toBool,
mkIntBin "cmp" compare toOrd,
mkIntUn "show" show toStr,
mkDblUn "neg" negate toDbl,
mkDblBin "add" (+) toDbl,
mkDblBin "sub" (-) toDbl,
mkDblBin "mul" (*) toDbl,
mkDblBin "div" (/) toDbl,
mkDblBin "mod" (\_ _ -> 0.0) toDbl,
mkDblBin "eq" (==) toBool,
mkDblBin "cmp" compare toOrd,
mkDblUn "show" show toStr,
mkStrBin "add" (++) toStr,
mkStrBin "eq" (==) toBool,
mkStrBin "cmp" compare toOrd,
@@ -69,28 +80,38 @@ builtin =
]
where
toInt i = VInt i
toDbl i = VDbl i
toBool b = VCons (CIdent (show b)) []
toOrd o = VCons (CIdent (show o)) []
toStr s = VStr s
mkIntUn x f g = let c = CIdent ("prim_"++x++"_Int")
in (c, VPrim (\n -> appInt1 f g n))
mkIntBin x f g = let c = CIdent ("prim_"++x++"_Int")
in (c, VPrim (\n -> VPrim (\m -> appInt2 f g n m )))
appInt1 f g x = case x of
mkUn t a x f g = let c = CIdent ("prim_" ++ x ++ "_" ++ t)
in (c, VPrim (\n -> a f g n))
mkBin t a x f g = let c = CIdent ("prim_" ++ x ++ "_" ++ t)
in (c, VPrim (\n -> VPrim (\m -> a f g n m )))
mkIntUn = mkUn "Integer" $ \ f g x ->
case x of
VInt n -> g (f n)
_ -> error $ printValue x ++ " is not an integer"
appInt2 f g x y = case (x,y) of
mkIntBin = mkBin "Integer" $ \ f g x y ->
case (x,y) of
(VInt n,VInt m) -> g (f n m)
_ -> error $ printValue x ++ " and " ++ printValue y
++ " are not both integers"
mkStrUn x f g = let c = CIdent ("prim_"++x++"_Str")
in (c, VPrim (\n -> appStr1 f g n))
mkStrBin x f g = let c = CIdent ("prim_"++x++"_Str")
in (c, VPrim (\n -> VPrim (\m -> appStr2 f g n m )))
appStr1 f g x = case x of
mkDblUn = mkUn "Double" $ \ f g x ->
case x of
VDbl n -> g (f n)
_ -> error $ printValue x ++ " is not a double"
mkDblBin = mkBin "Double" $ \ f g x y ->
case (x,y) of
(VDbl n,VDbl m) -> g (f n m)
_ -> error $ printValue x ++ " and " ++ printValue y
++ " are not both doubles"
mkStrUn = mkUn "String" $ \ f g x ->
case x of
VStr n -> g (f n)
_ -> error $ printValue x ++ " is not an integer"
appStr2 f g x y = case (x,y) of
_ -> error $ printValue x ++ " is not a string"
mkStrBin = mkBin "String" $ \ f g x y ->
case (x,y) of
(VStr n,VStr m) -> g (f n m)
_ -> error $ printValue x ++ " and " ++ printValue y
++ " are not both strings"
@@ -144,7 +165,8 @@ eval env x = case x of
EVar id -> lookupEnv env id
EType -> VType
EStr str -> VStr str
EInt n -> VInt n
EInteger n -> VInt n
EDouble n -> VDbl n
EMeta (TMeta t) -> VMeta (read $ drop 1 t)
firstMatch :: Value -> [Case] -> Maybe (Exp,[(CIdent,Value)])
@@ -196,7 +218,8 @@ valueToExp :: Value -> Exp
valueToExp v =
case v of
VStr s -> EStr s
VInt i -> EInt i
VInt i -> EInteger i
VDbl i -> EDouble i
VType -> EType
VRec fs -> ERec [ FieldValue f (valueToExp v) | (f,v) <- fs]
VClos env e -> e

35
src/Transfer/Syntax/Abs.hs
View File

@@ -85,7 +85,8 @@ data Tree :: * -> * where
EVar :: Ident -> Tree Exp_
EType :: Tree Exp_
EStr :: String -> Tree Exp_
EInt :: Integer -> Tree Exp_
EInteger :: Integer -> Tree Exp_
EDouble :: Double -> Tree Exp_
EMeta :: Tree Exp_
LetDef :: Ident -> Exp -> Exp -> Tree LetDef_
Case :: Pattern -> Exp -> Tree Case_
@@ -268,7 +269,8 @@ instance Show (Tree c) where
EVar i -> opar n . showString "EVar" . showChar ' ' . showsPrec 1 i . cpar n
EType -> showString "EType"
EStr str -> opar n . showString "EStr" . showChar ' ' . showsPrec 1 str . cpar n
EInt n -> opar n . showString "EInt" . showChar ' ' . showsPrec 1 n . cpar n
EInteger n -> opar n . showString "EInteger" . showChar ' ' . showsPrec 1 n . cpar n
EDouble d -> opar n . showString "EDouble" . showChar ' ' . showsPrec 1 d . cpar n
EMeta -> showString "EMeta"
LetDef i exp0 exp1 -> opar n . showString "LetDef" . showChar ' ' . showsPrec 1 i . showChar ' ' . showsPrec 1 exp0 . showChar ' ' . showsPrec 1 exp1 . cpar n
Case pattern exp -> opar n . showString "Case" . showChar ' ' . showsPrec 1 pattern . showChar ' ' . showsPrec 1 exp . cpar n
@@ -334,7 +336,8 @@ johnMajorEq (EList exps) (EList exps_) = exps == exps_
johnMajorEq (EVar i) (EVar i_) = i == i_
johnMajorEq EType EType = True
johnMajorEq (EStr str) (EStr str_) = str == str_
johnMajorEq (EInt n) (EInt n_) = n == n_
johnMajorEq (EInteger n) (EInteger n_) = n == n_
johnMajorEq (EDouble d) (EDouble d_) = d == d_
johnMajorEq EMeta EMeta = True
johnMajorEq (LetDef i exp0 exp1) (LetDef i_ exp0_ exp1_) = i == i_ && exp0 == exp0_ && exp1 == exp1_
johnMajorEq (Case pattern exp) (Case pattern_ exp_) = pattern == pattern_ && exp == exp_
@@ -399,17 +402,18 @@ instance Ord (Tree c) where
index (EVar _) = 46
index (EType ) = 47
index (EStr _) = 48
index (EInt _) = 49
index (EMeta ) = 50
index (LetDef _ _ _) = 51
index (Case _ _) = 52
index (BindVar _ _) = 53
index (BindNoVar _) = 54
index (VVar _) = 55
index (VWild ) = 56
index (FieldType _ _) = 57
index (FieldValue _ _) = 58
index (Ident _) = 59
index (EInteger _) = 49
index (EDouble _) = 50
index (EMeta ) = 51
index (LetDef _ _ _) = 52
index (Case _ _) = 53
index (BindVar _ _) = 54
index (BindNoVar _) = 55
index (VVar _) = 56
index (VWild ) = 57
index (FieldType _ _) = 58
index (FieldValue _ _) = 59
index (Ident _) = 60
compareSame (Module imports decls) (Module imports_ decls_) = mappend (compare imports imports_) (compare decls decls_)
compareSame (Import i) (Import i_) = compare i i_
compareSame (DataDecl i exp consdecls) (DataDecl i_ exp_ consdecls_) = mappend (compare i i_) (mappend (compare exp exp_) (compare consdecls consdecls_))
@@ -459,7 +463,8 @@ instance Ord (Tree c) where
compareSame (EVar i) (EVar i_) = compare i i_
compareSame EType EType = EQ
compareSame (EStr str) (EStr str_) = compare str str_
compareSame (EInt n) (EInt n_) = compare n n_
compareSame (EInteger n) (EInteger n_) = compare n n_
compareSame (EDouble d) (EDouble d_) = compare d d_
compareSame EMeta EMeta = EQ
compareSame (LetDef i exp0 exp1) (LetDef i_ exp0_ exp1_) = mappend (compare i i_) (mappend (compare exp0 exp0_) (compare exp1 exp1_))
compareSame (Case pattern exp) (Case pattern_ exp_) = mappend (compare pattern pattern_) (compare exp exp_)

7
src/Transfer/Syntax/Doc.tex
View File

@@ -37,6 +37,12 @@ except \terminal{"}\ unless preceded by \verb6\6.
Integer literals \nonterminal{Int}\ are nonempty sequences of digits.
Double-precision float literals \nonterminal{Double}\ have the structure
indicated by the regular expression $\nonterminal{digit}+ \mbox{{\it `.'}} \nonterminal{digit}+ (\mbox{{\it `e'}} \mbox{{\it `-'}}? \nonterminal{digit}+)?$ i.e.\
two sequences of digits separated by a decimal point, optionally
followed by an unsigned or negative exponent.
\subsection*{Reserved words and symbols}
@@ -266,6 +272,7 @@ All other symbols are terminals.\\
& {\delimit} &{\terminal{Type}} \\
& {\delimit} &{\nonterminal{String}} \\
& {\delimit} &{\nonterminal{Integer}} \\
& {\delimit} &{\nonterminal{Double}} \\
& {\delimit} &{\terminal{?}} \\
& {\delimit} &{\terminal{(}} {\nonterminal{Exp}} {\terminal{)}} \\
\end{tabular}\\

11
src/Transfer/Syntax/Lex.hs
View File

File diff suppressed because one or more lines are too long

2
src/Transfer/Syntax/Lex.x
View File

@@ -29,7 +29,7 @@ $l $i* { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t)))* \"{ tok (\p s -> PT p (TL $ share $ unescapeInitTail s)) }
$d+ { tok (\p s -> PT p (TI $ share s)) }
$d+ \. $d+ (e (\-)? $d+)? { tok (\p s -> PT p (TD $ share s)) }
{

1163
src/Transfer/Syntax/Par.hs
View File

File diff suppressed because one or more lines are too long

5
src/Transfer/Syntax/Par.y
View File

@@ -65,6 +65,7 @@ import Transfer.ErrM
L_ident { PT _ (TV $$) }
L_quoted { PT _ (TL $$) }
L_integ { PT _ (TI $$) }
L_doubl { PT _ (TD $$) }
L_err { _ }
@@ -73,6 +74,7 @@ L_err { _ }
Ident :: { Ident } : L_ident { Ident $1 }
String :: { String } : L_quoted { $1 }
Integer :: { Integer } : L_integ { (read $1) :: Integer }
Double :: { Double } : L_doubl { (read $1) :: Double }
Module :: { Module }
Module : ListImport ListDecl { Module $1 $2 }
@@ -262,7 +264,8 @@ Exp13 : 'sig' '{' ListFieldType '}' { ERecType $3 }
| Ident { EVar $1 }
| 'Type' { EType }
| String { EStr $1 }
| Integer { EInt $1 }
| Integer { EInteger $1 }
| Double { EDouble $1 }
| '?' { EMeta }
| '(' Exp ')' { $2 }

3
src/Transfer/Syntax/Print.hs
View File

@@ -129,7 +129,8 @@ instance Print (Tree c) where
EVar i -> prPrec _i 13 (concatD [prt 0 i])
EType -> prPrec _i 13 (concatD [doc (showString "Type")])
EStr str -> prPrec _i 13 (concatD [prt 0 str])
EInt n -> prPrec _i 13 (concatD [prt 0 n])
EInteger n -> prPrec _i 13 (concatD [prt 0 n])
EDouble d -> prPrec _i 13 (concatD [prt 0 d])
EMeta -> prPrec _i 13 (concatD [doc (showString "?")])
LetDef i exp0 exp1 -> prPrec _i 0 (concatD [prt 0 i , doc (showString ":") , prt 0 exp0 , doc (showString "=") , prt 0 exp1])
Case pattern exp -> prPrec _i 0 (concatD [prt 0 pattern , doc (showString "->") , prt 0 exp])

6
src/Transfer/Syntax/Skel.hs
View File

@@ -60,7 +60,8 @@ transTree t = case t of
EVar i -> failure t
EType -> failure t
EStr str -> failure t
EInt n -> failure t
EInteger n -> failure t
EDouble d -> failure t
EMeta -> failure t
LetDef i exp0 exp1 -> failure t
Case pattern exp -> failure t
@@ -141,7 +142,8 @@ transExp t = case t of
EVar i -> failure t
EType -> failure t
EStr str -> failure t
EInt n -> failure t
EInteger n -> failure t
EDouble d -> failure t
EMeta -> failure t
transLetDef :: LetDef -> Result

3
src/Transfer/Syntax/Syntax.cf
View File

@@ -115,7 +115,8 @@ EList. Exp13 ::= "[" [Exp] "]" ;
EVar. Exp13 ::= Ident ;
EType. Exp13 ::= "Type" ;
EStr. Exp13 ::= String ;
EInt. Exp13 ::= Integer ;
EInteger. Exp13 ::= Integer ;
EDouble. Exp13 ::= Double ;
EMeta. Exp13 ::= "?" ;
coercions Exp 13 ;

48
transfer/lib/prelude.tr
View File

@@ -22,18 +22,40 @@ id _ x = x
num_Integer : Num Integer
num_Integer = rec zero = 0
plus = prim_add_Int
minus = prim_sub_Int
plus = prim_add_Integer
minus = prim_sub_Integer
one = 1
times = prim_mul_Int
div = prim_div_Int
mod = prim_mod_Int
negate = prim_neg_Int
eq = prim_eq_Int
compare = prim_cmp_Int
times = prim_mul_Integer
div = prim_div_Integer
mod = prim_mod_Integer
negate = prim_neg_Integer
eq = prim_eq_Integer
compare = prim_cmp_Integer
show_Integer : Show Integer
show_Integer = rec show = prim_show_Int
show_Integer = rec show = prim_show_Integer
--
-- The Double type
--
-- Instances:
num_Double : Num Double
num_Double = rec zero = 0.0
plus = prim_add_Double
minus = prim_sub_Double
one = 1.0
times = prim_mul_Double
div = prim_div_Double
mod = prim_mod_Double
negate = prim_neg_Double
eq = prim_eq_Double
compare = prim_cmp_Double
show_Double : Show Double
show_Double = rec show = prim_show_Double
@@ -45,15 +67,15 @@ show_Integer = rec show = prim_show_Int
add_String : Add String
add_String = rec zero = ""
plus = prim_add_Str
plus = prim_add_String
ord_String : Ord String
ord_String = rec eq = prim_eq_Str
compare = prim_cmp_Str
compare = prim_cmp_String
show_String : Show String
show_String = rec show = prim_show_Str
show_String = rec show = prim_show_String
--
@@ -283,7 +305,7 @@ Neg : Type -> Type
Neg = sig negate : A -> A
negate : (A : Type) -> Neg A -> A -> A
negate _ d = d.neg
negate _ d = d.negate
-- Operators: