bbaa193 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better representation of names

bbaa193Edwin Brady15 years ago

src/Core/CaseTree.hs+6−6

compare with master

unifiedsplit

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

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

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

61 return $ PCon n t args'

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

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

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

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

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

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

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

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

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

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

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

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

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

70 if n `elem` ns

src/Core/CoreParser.hs+1−1

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

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

60iName bad = do x <- identifier

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

62− return (UN [x])

62+ return (UN x)

64pDef :: CParser a (Name, RDef)

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

src/Core/Elaborate.hs+2−2

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

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

253

254 mkMN n@(MN _ _) = n

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

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

256

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

258apply fn imps =

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

309 focus n; elaboration; elabClaims failed r xs

310

311 mkMN n@(MN _ _) = n

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

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

313

314simple_app :: Elab () -> Elab () -> Elab ()

315simple_app fun arg =

src/Core/ProofState.hs+2−2

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

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

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

304 case unApply tmt of

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

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

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

307 let newt = mkP l r l t

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

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

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

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

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

312 return scv

src/Core/TT.hs+8−7

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

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

90-- Also MN for machine chosen names

92−data Name = UN [String]

92+data Name = UN String

93+ | NS String Name

93 | MN Int String

94 | MN Int String

94 deriving (Eq, Ord)

95 deriving (Eq, Ord)

96instance Show Name where

97instance Show Name where

97− show (UN [n]) = n

98+ show (UN n) = n

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

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

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

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

100

101

102

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

308 | otherwise = n

309 | otherwise = n

309

310

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

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

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

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

312− nm = reverse nm'

313+ nm = reverse nm'

313− num = readN (reverse num') in

314+ num = readN (reverse num') in

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

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

315 where

316 where

316 readN "" = 0

317 readN "" = 0

317 readN x = read x

318 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

115 i <- get

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

117 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

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

120 tidyNames used (Bind n b sc)

121 = let n' = uniqueName n used in

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

384 | Expr Name

385 deriving Show

386

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

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

388

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

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

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

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

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

483 | not impl = show f

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

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

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

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

487 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)

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

595 where n a = MN 0 a

596

597−eqTy = UN ["="]

597+eqTy = UN "="

598−eqCon = UN ["refl"]

598+eqCon = UN "refl"

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

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

601 PSet)

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

608 where n a = MN 0 a

609

610-- Defined in builtins.idr

611−sigmaTy = UN ["Sigma"]

611+sigmaTy = UN "Sigma"

612−existsCon = UN ["Exists"]

612+existsCon = UN "Exists"

613

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

615piBind [] t = t

src/Idris/Compiler.hs+8−8

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

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

14import qualified Epic.Epic as E

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

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

18compile :: FilePath -> Idris ()

19compile f = do ds <- mkDecls

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

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

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

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

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

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

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

38class ToEpic a where

39 epic :: a -> Idris E.Term

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

56instance ToEpic (TT Name) where

57 epic tm = epic' [] tm where

58 epic' env tm@(App f a)

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

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

60 = doForeign args

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

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

62 = do arg' <- epic' env arg

63 return $ lazy_ arg'

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

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

65 = epic' env arg

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

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

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

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

85doForeign (_ : fgn : args)

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

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

87 = let tys = getFTypes fgnArgTys

88 rty = mkEty ret in

89 do args' <- mapM epic args

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

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

95getFTypes tm = case unApply tm of

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

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

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

98 let rest = getFTypes xs in

99 mkEty ty : rest

100

src/Idris/Delaborate.hs+1−1

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

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

19 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 ++ ""))

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

22 | n == unitCon = PTrue un

23 | 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)

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

167 return (clhs, crhs)

168 where

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

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

170 pinfo ns ps i

171 = let ds = concatMap declared ps

172 newps = params info ++ ns

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

286 FC -> [PTerm] ->

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

288elabClass 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)

290 let tty = pibind ps PSet

291 let constraint = PApp fc (PRef fc tn)

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

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

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

367 Just c -> return c

368 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)

370 elabType info syn fc iname t

371 let ips = zip (class_params ci) ps

372 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

394

395 papp fc f [] = f

396 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)

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

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

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

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

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

401 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

626 = elabArgs failed r ns args

627 = elabArgs failed r ns args

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

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

628 | lazy && not pattern

629 | lazy && not pattern

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

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

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

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

631 pexp t]);

632 pexp t]);

632 | otherwise = elabArg n t

633 | otherwise = elabArg n t

633 where elabArg n t = if r

634 where elabArg n t = if r

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

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

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

656 (blunderbuss t ns)

657 (blunderbuss t ns)

657 | otherwise = blunderbuss t ns

658 | otherwise = blunderbuss t ns

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

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

660+ tcname (NS _ n) = tcname n

659 tcname _ = False

661 tcname _ = False

660

662

661 resolve n depth

663 resolve n depth

src/Idris/Parser.hs+13−13

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

397 iName (syntax_keywords i)

398 <|> do reserved "instance"

399 i <- getState

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

400+ UN n <- iName (syntax_keywords i)

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

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

402

403pfName = try pName

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

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

405

406pSimpleExpr syn =

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

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

431modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

432modifyConst syn fc (PConstant (I x))

433 | 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))]

435modifyConst syn fc x = x

436

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

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

570 <|> return Dynamic

571

572table fixes

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

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

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

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

575 ++ toTable (reverse fixes) ++

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

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

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

579toTable fs = map (map toBin)

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

581 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])

583 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)

585 assoc (Infixl _) = AssocLeft

586 assoc (Infixr _) = AssocRight

587 assoc (InfixN _) = AssocNone

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

648 ni = no_imp syn in

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

650 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)

652

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

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

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

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

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

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

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

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

660 where n' = case n of

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

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

662 x -> x

663

664pClause :: SyntaxInfo -> IParser PClause

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

696

697 <|> do l <- pArgExpr syn

698 op <- operator

699− let n = UN [op]

699+ let n = UN op

700 r <- pArgExpr syn

701 fc <- pfc

702 wargs <- many (pWExpr syn)

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

709

710 <|> do l <- pArgExpr syn

711 op <- operator

712− let n = UN [op]

712+ let n = UN op

713 r <- pArgExpr syn

714 fc <- pfc

715 wargs <- many (pWExpr syn)

src/Idris/Primitives.hs+39−39

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

50primitives =

51 -- operators

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

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

53 (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 (-))

55 (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 (*))

57 (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))

59 (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 (==))

61 (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 (<))

63 (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 (<=))

65 (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 (>))

67 (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 (>=))

69 (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 (+))

71 (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 (-))

73 (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 (*))

75 (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))

77 (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 (==))

79 (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 (<))

81 (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 (<=))

83 (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 (>))

85 (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 (>=))

87 (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 (+))

89 (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 (-))

91 (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 (*))

93 (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 (/))

95 (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 (==))

97 (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 (<))

99 (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 (<=))

101 (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 (>))

103 (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 (>=))

105 (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 (++))

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

108 -- Conversions

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

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

110 ([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)

112 ([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)

114 ([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)

116 ([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)

118 ([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)

120 ([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)

122 ([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)

124 ([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)

126 ([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)

128 ([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)

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

131 ]

132