bbaa193 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better representation of names

commitbbaa1931a76112f950a3ec190447e0ead678aa26 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 18 Nov 2011, 12:13 (15 years ago) parent34f92f3

11 files changed+96−93

compare with master

unifiedsplit

src/Core/CaseTree.hs+6−6 src/Core/CoreParser.hs+1−1 src/Core/Elaborate.hs+2−2 src/Core/ProofState.hs+2−2 src/Core/TT.hs+8−7 src/Idris/AbsSyntax.hs+7−7 src/Idris/Compiler.hs+8−8 src/Idris/Delaborate.hs+1−1 src/Idris/ElabDecls.hs+9−7 src/Idris/Parser.hs+13−13 src/Idris/Primitives.hs+39−39

src/Core/CaseTree.hs+6−6

@@ -59,12 +59,12 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

5959 toPat' (P (TCon t a) n _) args | tc

6060 = do args' <- mapM (\x -> toPat' x []) args

6161 return $ PCon n t args'

62− toPat' (Constant IType) [] | tc = return $ PCon (UN ["Int"]) 1 []

63− toPat' (Constant FlType) [] | tc = return $ PCon (UN ["Float"]) 2 []

64− toPat' (Constant ChType) [] | tc = return $ PCon (UN ["Char"]) 3 []

65− toPat' (Constant StrType) [] | tc = return $ PCon (UN ["String"]) 4 []

66− toPat' (Constant PtrType) [] | tc = return $ PCon (UN ["Ptr"]) 5 []

67− toPat' (Constant BIType) [] | tc = return $ PCon (UN ["Integer"]) 6 []

62+ toPat' (Constant IType) [] | tc = return $ PCon (UN "Int") 1 []

63+ toPat' (Constant FlType) [] | tc = return $ PCon (UN "Float") 2 []

64+ toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []

65+ toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

66+ toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

67+ toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

6868

6969 toPat' (P Bound n _) [] = do ns <- get

7070 if n `elem` ns

src/Core/CoreParser.hs+1−1

@@ -59,7 +59,7 @@ pTestFile = do p <- many1 pDef ; eof

5959iName :: [String] -> CParser a Name

6060iName bad = do x <- identifier

6161 when (x `elem` bad) $ fail "Reserved identifier"

62− return (UN [x])

62+ return (UN x)

6363

6464pDef :: CParser a (Name, RDef)

6565pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

src/Core/Elaborate.hs+2−2

@@ -252,7 +252,7 @@ prepare_apply fn imps =

252252 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn

253253

254254 mkMN n@(MN _ _) = n

255− mkMN n@(UN [x]) = MN 0 x

255+ mkMN n@(UN x) = MN 0 x

256256

257257apply :: Raw -> [Bool] -> Elab [Name]

258258apply fn imps =

@@ -309,7 +309,7 @@ apply_elab n args =

309309 focus n; elaboration; elabClaims failed r xs

310310

311311 mkMN n@(MN _ _) = n

312− mkMN n@(UN [x]) = MN 0 x

312+ mkMN n@(UN x) = MN 0 x

313313

314314simple_app :: Elab () -> Elab () -> Elab ()

315315simple_app fun arg =

src/Core/ProofState.hs+2−2

@@ -302,11 +302,11 @@ rewrite :: Raw -> RunTactic

302302rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

303303 do (tmv, tmt) <- lift $ check ctxt env tm

304304 case unApply tmt of

305− (P _ (UN ["="]) _, [lt,rt,l,r]) ->

305+ (P _ (UN "=") _, [lt,rt,l,r]) ->

306306 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

307307 let newt = mkP l r l t

308308 let sc = forget $ (Bind x (Hole newt)

309− (mkApp (P Ref (UN ["replace"]) (Set 0))

309+ (mkApp (P Ref (UN "replace") (Set 0))

310310 [lt, l, r, p, tmv, xp]))

311311 (scv, sct) <- lift $ check ctxt env sc

312312 return scv

src/Core/TT.hs+8−7

@@ -89,13 +89,14 @@ traceWhen False _ a = a

8989-- duplicate names, but need to be careful on lookup).

9090-- Also MN for machine chosen names

9191

92−data Name = UN [String]

92+data Name = UN String

93+ | NS String Name

9394 | MN Int String

9495 deriving (Eq, Ord)

9596

9697instance Show Name where

97− show (UN [n]) = n

98− show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)

98+ show (UN n) = n

99+ show (NS s n) = s ++ "." ++ show n

99100 show (MN i s) = "{" ++ s ++ show i ++ "}"

100101

101102

@@ -308,10 +309,10 @@ uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

308309 | otherwise = n

309310

310311nextName (MN i n) = MN (i+1) n

311−nextName (UN (x:xs)) = let (num', nm') = span isDigit (reverse x)

312− nm = reverse nm'

313− num = readN (reverse num') in

314− UN ((nm ++ show (num+1)) : xs)

312+nextName (UN x) = let (num', nm') = span isDigit (reverse x)

313+ nm = reverse nm'

314+ num = readN (reverse num') in

315+ UN (nm ++ show (num+1))

315316 where

316317 readN "" = 0

317318 readN x = read x

src/Idris/AbsSyntax.hs+7−7

@@ -115,7 +115,7 @@ addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t

115115 i <- get

116116 put (i { idris_metavars = map fst ns ++ idris_metavars i })

117117 where tidyNames used (Bind (MN i x) b sc)

118− = let n' = uniqueName (UN [x]) used in

118+ = let n' = uniqueName (UN x) used in

119119 Bind n' b $ tidyNames (n':used) sc

120120 tidyNames used (Bind n b sc)

121121 = let n' = uniqueName n used in

@@ -384,7 +384,7 @@ data SSymbol = Keyword Name

384384 | Expr Name

385385 deriving Show

386386

387−initDSL = DSL (UN [">>="]) (UN ["return"])

387+initDSL = DSL (UN ">>=") (UN "return")

388388

389389data SyntaxInfo = Syn { using :: [(Name, PTerm)],

390390 syn_params :: [(Name, PTerm)],

@@ -481,7 +481,7 @@ showImp impl tm = se 10 tm where

481481 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

482482 se p (PApp _ (PRef _ f) [])

483483 | not impl = show f

484− se p (PApp _ (PRef _ op@(UN [f:_])) args)

484+ se p (PApp _ (PRef _ op@(UN (f:_))) args)

485485 | length (getExps args) == 2 && not impl && not (isAlpha f)

486486 = let [l, r] = getExps args in

487487 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

@@ -594,8 +594,8 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

594594 pexp (PRef bi (n "B"))])))), bi)]

595595 where n a = MN 0 a

596596

597−eqTy = UN ["="]

598−eqCon = UN ["refl"]

597+eqTy = UN "="

598+eqCon = UN "refl"

599599eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

600600 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]

601601 PSet)

@@ -608,8 +608,8 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

608608 where n a = MN 0 a

609609

610610-- Defined in builtins.idr

611−sigmaTy = UN ["Sigma"]

612−existsCon = UN ["Exists"]

611+sigmaTy = UN "Sigma"

612+existsCon = UN "Exists"

613613

614614piBind :: [(Name, PTerm)] -> PTerm -> PTerm

615615piBind [] t = t

src/Idris/Compiler.hs+8−8

@@ -13,7 +13,7 @@ import Control.Monad.State

1313import Epic.Epic hiding (Term, Type, Name, fn, compile)

1414import qualified Epic.Epic as E

1515

16−primDefs = [UN ["mkForeign"], UN ["FalseElim"], UN ["believe_me"]]

16+primDefs = [UN "mkForeign", UN "FalseElim", UN "believe_me"]

1717

1818compile :: FilePath -> Idris ()

1919compile f = do ds <- mkDecls

@@ -32,8 +32,8 @@ mkDecls = do i <- getIState

3232ename x = name ("idris_" ++ show x)

3333aname x = name ("a_" ++ show x)

3434

35−epicMain = effect_ $ ref (ename (UN ["run__IO"])) @@

36− ref (ename (UN ["main"]))

35+epicMain = effect_ $ ref (ename (UN "run__IO")) @@

36+ ref (ename (UN "main"))

3737

3838class ToEpic a where

3939 epic :: a -> Idris E.Term

@@ -56,12 +56,12 @@ instance ToEpic Def where

5656instance ToEpic (TT Name) where

5757 epic tm = epic' [] tm where

5858 epic' env tm@(App f a)

59− | (P _ (UN ["mkForeign"]) _, args) <- unApply tm

59+ | (P _ (UN "mkForeign") _, args) <- unApply tm

6060 = doForeign args

61− | (P _ (UN ["lazy"]) _, [_, arg]) <- unApply tm

61+ | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

6262 = do arg' <- epic' env arg

6363 return $ lazy_ arg'

64− | (P _ (UN ["believe_me"]) _, [_, _, arg]) <- unApply tm

64+ | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm

6565 = epic' env arg

6666 epic' env (P (DCon t a) n _) = return $ con_ t

6767 epic' env (P (TCon t a) n _) = return $ con_ t

@@ -83,7 +83,7 @@ instance ToEpic (TT Name) where

8383

8484doForeign :: [TT Name] -> Idris E.Term

8585doForeign (_ : fgn : args)

86− | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN [ret]) _ : [])) <- unApply fgn

86+ | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn

8787 = let tys = getFTypes fgnArgTys

8888 rty = mkEty ret in

8989 do args' <- mapM epic args

@@ -94,7 +94,7 @@ doForeign (_ : fgn : args)

9494getFTypes :: TT Name -> [E.Type]

9595getFTypes tm = case unApply tm of

9696 (nil, [arg]) -> []

97− (cons, [a, (P _ (UN [ty]) _), xs]) ->

97+ (cons, [a, (P _ (UN ty) _), xs]) ->

9898 let rest = getFTypes xs in

9999 mkEty ty : rest

100100

src/Idris/Delaborate.hs+1−1

@@ -17,7 +17,7 @@ delab ist tm = de [] tm

1717

1818 de env (App f a) = deFn env f [a]

1919 de env (V i) | i < length env = PRef un (env!!i)

20− | otherwise = PRef un (UN ["v" ++ show i ++ ""])

20+ | otherwise = PRef un (UN ("v" ++ show i ++ ""))

2121 de env (P _ n _) | n == unitTy = PTrue un

2222 | n == unitCon = PTrue un

2323 | n == falseTy = PFalse un

src/Idris/ElabDecls.hs+9−7

@@ -166,7 +166,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

166166 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

167167 return (clhs, crhs)

168168 where

169− decorate x = UN [show fname ++ "#" ++ show x]

169+ decorate x = UN (show fname ++ "#" ++ show x)

170170 pinfo ns ps i

171171 = let ds = concatMap declared ps

172172 newps = params info ++ ns

@@ -286,7 +286,7 @@ elabClass :: ElabInfo -> SyntaxInfo ->

286286 FC -> [PTerm] ->

287287 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

288288elabClass info syn fc constraints tn ps ds

289− = do let cn = UN ["instance" ++ show tn] -- MN 0 ("instance" ++ show tn)

289+ = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

290290 let tty = pibind ps PSet

291291 let constraint = PApp fc (PRef fc tn)

292292 (map (pexp . PRef fc) (map fst ps))

@@ -366,7 +366,7 @@ elabInstance info syn fc cs n ps t ds

366366 ci <- case lookupCtxt n (idris_classes i) of

367367 Just c -> return c

368368 Nothing -> fail $ show n ++ " is not a type class"

369− let iname = UN ['@':show n ++ "$" ++ show ps]

369+ let iname = UN ('@':show n ++ "$" ++ show ps)

370370 elabType info syn fc iname t

371371 let ips = zip (class_params ci) ps

372372 let mtys = map (\ (n, t) -> (decorate n, coninsert cs $ substMatches ips t))

@@ -394,7 +394,8 @@ elabInstance info syn fc cs n ps t ds

394394

395395 papp fc f [] = f

396396 papp fc f as = PApp fc f as

397− decorate (UN (n:ns)) = UN (('!':n) : ns)

397+ decorate (UN n) = UN ('!':n)

398+ decorate (NS s n) = NS s (decorate n)

398399 decorateid (PTy s f n t) = PTy s f (decorate n) t

399400 decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)

400401 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

@@ -626,8 +627,8 @@ elab ist info pattern tm

626627 = elabArgs failed r ns args

627628 elabArgs failed r (n:ns) ((lazy, t) : args)

628629 | lazy && not pattern

629− = do elabArg n (PApp bi (PRef bi (UN ["lazy"]))

630− [pimp (UN ["a"]) Placeholder,

630+ = do elabArg n (PApp bi (PRef bi (UN "lazy"))

631+ [pimp (UN "a") Placeholder,

631632 pexp t]);

632633 | otherwise = elabArg n t

633634 where elabArg n t = if r

@@ -655,7 +656,8 @@ resolveTC depth ist

655656 blunderbuss t (n:ns) | tcname n = try (resolve n depth)

656657 (blunderbuss t ns)

657658 | otherwise = blunderbuss t ns

658− tcname (UN (('@':_) : _)) = True

659+ tcname (UN ('@':_)) = True

660+ tcname (NS _ n) = tcname n

659661 tcname _ = False

660662

661663 resolve n depth

src/Idris/Parser.hs+13−13

@@ -397,11 +397,11 @@ pName = do i <- getState

397397 iName (syntax_keywords i)

398398 <|> do reserved "instance"

399399 i <- getState

400− UN (n:ns) <- iName (syntax_keywords i)

401− return (UN (('@':n) : ns))

400+ UN n <- iName (syntax_keywords i)

401+ return (UN ('@':n))

402402

403403pfName = try pName

404− <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

404+ <|> do lchar '('; o <- operator; lchar ')'; return (UN o)

405405

406406pSimpleExpr syn =

407407 try (do symbol "!["; t <- pTerm; lchar ']'

@@ -431,7 +431,7 @@ pSimpleExpr syn =

431431modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

432432modifyConst syn fc (PConstant (I x))

433433 | not (inPattern syn)

434− = PApp fc (PRef fc (UN ["fromInteger"])) [pexp (PConstant (I x))]

434+ = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]

435435modifyConst syn fc x = x

436436

437437pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp

@@ -570,8 +570,8 @@ pStatic = do lchar '['; reserved "static"; lchar ']';

570570 <|> return Dynamic

571571

572572table fixes

573− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"]))

574− [pexp (PApp fc (PRef fc (UN ["fromInteger"])) [pexp (PConstant (I 0))]), pexp x])]]

573+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

574+ [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]

575575 ++ toTable (reverse fixes) ++

576576 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],

577577 [binary "->" (\fc x y -> PPi expl (MN 0 "X") x y) AssocRight]]

@@ -579,9 +579,9 @@ table fixes

579579toTable fs = map (map toBin)

580580 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

581581 where toBin (Fix (PrefixN _) op) = prefix op

582− (\fc x -> PApp fc (PRef fc (UN [op])) [pexp x])

582+ (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])

583583 toBin (Fix f op)

584− = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [pexp x,pexp y]) (assoc f)

584+ = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)

585585 assoc (Infixl _) = AssocLeft

586586 assoc (Infixr _) = AssocRight

587587 assoc (InfixN _) = AssocNone

@@ -648,7 +648,7 @@ whereSyn n syn args = let ns = concatMap allNamesIn args

648648 ni = no_imp syn in

649649 syn { decoration = \x -> decorate n (decoration syn x),

650650 no_imp = nub (ni ++ ns) }

651− where decorate n x = UN [(show n ++ "_" ++ show x)]

651+ where decorate n x = UN (show n ++ "_" ++ show x)

652652

653653pArgExpr syn = let syn' = syn { inPattern = True } in

654654 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'

@@ -656,9 +656,9 @@ pArgExpr syn = let syn' = syn { inPattern = True } in

656656pRHS :: SyntaxInfo -> Name -> IParser PTerm

657657pRHS syn n = do lchar '='; pExpr syn

658658 <|> do symbol "?="; rhs <- pExpr syn;

659− return (PLet (UN ["value"]) Placeholder rhs (PMetavar n'))

659+ return (PLet (UN "value") Placeholder rhs (PMetavar n'))

660660 where n' = case n of

661− UN [x] -> UN [x++"_lemma_1"]

661+ UN x -> UN (x++"_lemma_1")

662662 x -> x

663663

664664pClause :: SyntaxInfo -> IParser PClause

@@ -696,7 +696,7 @@ pClause syn

696696

697697 <|> do l <- pArgExpr syn

698698 op <- operator

699− let n = UN [op]

699+ let n = UN op

700700 r <- pArgExpr syn

701701 fc <- pfc

702702 wargs <- many (pWExpr syn)

@@ -709,7 +709,7 @@ pClause syn

709709

710710 <|> do l <- pArgExpr syn

711711 op <- operator

712− let n = UN [op]

712+ let n = UN op

713713 r <- pArgExpr syn

714714 fc <- pfc

715715 wargs <- many (pWExpr syn)

src/Idris/Primitives.hs+39−39

@@ -49,84 +49,84 @@ floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]

4949

5050primitives =

5151 -- operators

52− [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))

52+ [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

5353 (eOp E.plus_),

54− Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-))

54+ Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))

5555 (eOp E.minus_),

56− Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*))

56+ Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))

5757 (eOp E.times_),

58− Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div))

58+ Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))

5959 (eOp E.divide_),

60− Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==))

60+ Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))

6161 (eOp E.eq_),

62− Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<))

62+ Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))

6363 (eOp E.lt_),

64− Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=))

64+ Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))

6565 (eOp E.lte_),

66− Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>))

66+ Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))

6767 (eOp E.gt_),

68− Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=))

68+ Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))

6969 (eOp E.gte_),

70− Prim (UN ["prim__addBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (+))

70+ Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

7171 (eOpFn tyBigInt tyBigInt "addBig"),

72− Prim (UN ["prim__subBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (-))

72+ Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

7373 (eOpFn tyBigInt tyBigInt "subBig"),

74− Prim (UN ["prim__mulBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (*))

74+ Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))

7575 (eOpFn tyBigInt tyBigInt "mulBig"),

76− Prim (UN ["prim__divBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (div))

76+ Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))

7777 (eOpFn tyBigInt tyBigInt "divBig"),

78− Prim (UN ["prim__eqBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (==))

78+ Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))

7979 (eOpFn tyBigInt tyInt "eqBig"),

80− Prim (UN ["prim__ltBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (<))

80+ Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))

8181 (eOpFn tyBigInt tyInt "ltBig"),

82− Prim (UN ["prim__lteBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (<=))

82+ Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))

8383 (eOpFn tyBigInt tyInt "leBig"),

84− Prim (UN ["prim__gtBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (>))

84+ Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))

8585 (eOpFn tyBigInt tyInt "gtBig"),

86− Prim (UN ["prim__gtBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (>=))

86+ Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))

8787 (eOpFn tyBigInt tyInt "geBig"),

88− Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+))

88+ Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

8989 (eOp E.plusF_),

90− Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-))

90+ Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

9191 (eOp E.minusF_),

92− Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*))

92+ Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))

9393 (eOp E.timesF_),

94− Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/))

94+ Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))

9595 (eOp E.divideF_),

96− Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==))

96+ Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))

9797 (eOp E.eqF_),

98− Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<))

98+ Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))

9999 (eOp E.ltF_),

100− Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=))

100+ Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))

101101 (eOp E.lteF_),

102− Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>))

102+ Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))

103103 (eOp E.gtF_),

104− Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))

104+ Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))

105105 (eOp E.gteF_),

106− Prim (UN ["prim__concat"]) (ty [StrType, StrType] StrType) 2 (sBin (++))

106+ Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

107107 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),

108108 -- Conversions

109− Prim (UN ["prim__strToInt"]) (ty [StrType] IType) 1 (c_strToInt)

109+ Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

110110 ([E.name "x"], strToInt (fun "x")),

111− Prim (UN ["prim__intToStr"]) (ty [IType] StrType) 1 (c_intToStr)

111+ Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

112112 ([E.name "x"], intToStr (fun "x")),

113− Prim (UN ["prim__intToBigInt"]) (ty [IType] BIType) 1 (c_intToBigInt)

113+ Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

114114 ([E.name "x"], intToBigInt (fun "x")),

115− Prim (UN ["prim__strToBigInt"]) (ty [StrType] BIType) 1 (c_strToBigInt)

115+ Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

116116 ([E.name "x"], strToBigInt (fun "x")),

117− Prim (UN ["prim__bigIntToStr"]) (ty [BIType] StrType) 1 (c_bigIntToStr)

117+ Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

118118 ([E.name "x"], bigIntToStr (fun "x")),

119− Prim (UN ["prim__strToFloat"]) (ty [StrType] FlType) 1 (c_strToFloat)

119+ Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

120120 ([E.name "x"], strToFloat (fun "x")),

121− Prim (UN ["prim__floatToStr"]) (ty [FlType] StrType) 1 (c_floatToStr)

121+ Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

122122 ([E.name "x"], floatToStr (fun "x")),

123− Prim (UN ["prim__intToFloat"]) (ty [IType] FlType) 1 (c_intToFloat)

123+ Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)

124124 ([E.name "x"], intToFloat (fun "x")),

125− Prim (UN ["prim__floatToInt"]) (ty [FlType] IType) 1 (c_floatToInt)

125+ Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

126126 ([E.name "x"], floatToInt (fun "x")),

127− Prim (UN ["prim__floatExp"]) (ty [FlType] FlType) 1 (p_floatExp)

127+ Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

128128 ([E.name "x"], floatExp (fun "x")),

129− Prim (UN ["prim__floatLog"]) (ty [FlType] FlType) 1 (p_floatLog)

129+ Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

130130 ([E.name "x"], floatLog (fun "x"))

131131 ]

132132