SHARE
TWEET

Untitled

a guest Sep 12th, 2019 73 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. # Types
  2.  
  3. abstract type Type
  4. end
  5.  
  6. struct VarType <: Type
  7.     name  :: String
  8.     rigid :: Bool
  9. end
  10.  
  11. struct FunType <: Type
  12.     domain   :: Array{Type}
  13.     codomain :: Type
  14. end
  15.  
  16. struct TupleType <: Type
  17.     types :: Array{Type}
  18. end
  19.  
  20. struct RefType <: Type
  21.     type_ :: Type
  22. end
  23.  
  24. abstract type AtomType <: Type
  25. end
  26.  
  27. struct IntType <: AtomType
  28. end
  29.  
  30. struct BoolType <: AtomType
  31. end
  32.  
  33. struct StringType <: AtomType
  34. end
  35.  
  36. struct VoidType <: AtomType
  37. end
  38.  
  39. # Polymorphic types (rank 1)
  40.  
  41. struct Scheme
  42.     vars  :: Array{String}
  43.     type_ :: Type
  44. end
  45.  
  46. function monotype(type_ :: Type)
  47.     return Scheme([], type_)
  48. end
  49.  
  50. # AST
  51.  
  52. abstract type Expr
  53. end
  54.  
  55. struct VarExpr <: Expr
  56.     name :: String
  57. end
  58.  
  59. struct Param
  60.     name  :: String
  61.     type_ :: Any
  62. end
  63.  
  64. struct FunExpr <: Expr
  65.     params :: Array{Param}
  66.     body   :: Expr
  67. end
  68.  
  69. struct CallExpr <: Expr
  70.     called :: Expr
  71.     arguments :: Array{Expr}
  72. end
  73.  
  74. abstract type Instruction
  75. end
  76.  
  77. struct VarInstr <: Instruction
  78.     name  :: String
  79.     value :: Expr
  80. end
  81.  
  82. struct AssignInstr <: Instruction
  83.     name  :: String
  84.     value :: Expr
  85. end
  86.  
  87. struct LetInstr <: Instruction
  88.     name  :: String
  89.     value :: Expr
  90. end
  91.  
  92. struct ExprInstr <: Instruction
  93.     expr :: Expr
  94. end
  95.  
  96. struct BlockExpr <: Expr
  97.     instructions :: Array{Instruction}
  98.     last         :: Expr
  99. end
  100.  
  101. struct IfExpr <: Expr
  102.     condition  :: Expr
  103.     true_case  :: Expr
  104.     false_case :: Expr
  105. end
  106.  
  107. struct TupleExpr <: Expr
  108.     elements :: Array{Expr}
  109. end
  110.  
  111. abstract type BinaryOperation <: Expr
  112. end
  113.  
  114. struct AddExpr <: BinaryOperation
  115.     lhs :: Expr
  116.     rhs :: Expr
  117. end
  118.  
  119. abstract type ComparisonExpr <: BinaryOperation
  120. end
  121.  
  122. struct EQExpr <: ComparisonExpr
  123.     lhs :: Expr
  124.     rhs :: Expr
  125. end
  126.  
  127. struct GTExpr <: ComparisonExpr
  128.     lhs :: Expr
  129.     rhs :: Expr
  130. end
  131.  
  132. struct LTExpr <: ComparisonExpr
  133.     lhs :: Expr
  134.     rhs :: Expr
  135. end
  136.  
  137. abstract type LitExpr <: Expr
  138. end
  139.  
  140. struct IntLit <: LitExpr
  141.     value :: Int
  142. end
  143.  
  144. struct BoolLit <: LitExpr
  145.     value :: Bool
  146. end
  147.  
  148. struct StringLit <: LitExpr
  149.     value :: String
  150. end
  151.  
  152. # Free variables
  153.  
  154. freeVariables(expr :: VarExpr) = Set{String}([expr.name])
  155. freeVariables(expr :: FunExpr) = setdiff(freeVariables(expr.body), Set{String}([param.name for param in expr.params]))
  156. freeVariables(expr :: CallExpr) = union(freeVariables(expr.called), map(freeVariables, expr.arguments)...)
  157. freeVariables(expr :: VarInstr) = freeVariables(expr.value)
  158. freeVariables(expr :: LetInstr) = freeVariables(expr.value)
  159. freeVariables(expr :: AssignInstr) = freeVariables(expr.value)
  160. freeVariables(expr :: ExprInstr) = freeVariables(expr.expr)
  161. freeVariables(expr :: BlockExpr) = union(freeVariables(expr.last), map(freeVariables, expr.instructions)...)
  162. freeVariables(expr :: IfExpr) = union(map(freeVariables, [expr.condition, expr.true_case, expr.false_case])...)
  163. freeVariables(expr :: TupleExpr) = union(map(freeVariables, expr.elements)...)
  164. freeVariables(expr :: E) where E <: BinaryOperation = union(freeVariables(expr.lhs), freeVariables(expr.rhs))
  165. freeVariables(expr :: E) where E <: Expr = Set{String}()
  166.  
  167. # Free type variables
  168.  
  169. freeTypeVars(type_ :: VarType) = Set{String}([type_.name])
  170.  
  171. function freeTypeVars(type_ :: FunType)
  172.     domainFTVs = Set{String}()
  173.     for paramType in type_.domain
  174.         domainFTVs = union(domainFTVs, freeTypeVars(paramType))
  175.     end
  176.     return union(domainFTVs, freeTypeVars(type_.codomain))
  177. end
  178.  
  179. function freeTypeVars(type_ :: TupleType)
  180.     ftvs = Set{String}()
  181.     for elemType in type_.types
  182.         ftvs = union(ftvs, freeTypeVars(elemType))
  183.     end
  184.     return ftvs
  185. end
  186.  
  187. freeTypeVars(type_ :: RefType) = freeTypeVars(type_.type_)
  188. freeTypeVars(type_ :: T) where T <: AtomType = Set{String}()
  189. freeTypeVars(scheme :: Scheme) = setdiff(freeTypeVars(scheme.type_), Set{String}(scheme.vars))
  190.  
  191. # Substitution
  192.  
  193. function substitute(varName :: String, varType :: Type, ctxType :: VarType)
  194.     if ctxType.name == varName && !ctxType.rigid
  195.         return varType
  196.     else
  197.         return ctxType
  198.     end
  199. end
  200.  
  201. function substitute(varName :: String, varType :: Type, ctxType :: FunType)
  202.     return FunType([substitute(varName, varType, paramType) for paramType in ctxType.domain],
  203.                    substitute(varName, varType, ctxType.codomain))
  204. end
  205.  
  206. function substitute(varName :: String, varType :: Type, ctxType :: TupleType)
  207.     newTypes = []
  208.     for type_ in ctxType.types
  209.         push!(newTypes, substitute(varName, varType, type_))
  210.     end
  211.     return TupleType(newTypes)
  212. end
  213.  
  214. substitute(varName :: String, varType :: Type, ctxType :: RefType) = RefType(substitute(varName, varType, ctxType.type_))
  215. substitute(varName :: String, varType :: Type, ctxType :: T) where T <: AtomType = ctxType
  216.  
  217. function substitute(varName :: String, varType :: Type, ctxType :: Scheme)
  218.     if varName in ctxType.vars
  219.         return ctxType
  220.     else
  221.         return Scheme(ctxType.vars, substitute(varName, varType, ctxType.type_))
  222.     end
  223. end
  224.  
  225. # Typechecking utilities
  226.  
  227. abstract type TypecheckErrorType
  228. end
  229.  
  230. struct ScopeError <: TypecheckErrorType
  231.     name :: String
  232. end
  233.  
  234. struct TypeMismatch <: TypecheckErrorType
  235.     a :: Type
  236.     b :: Type
  237. end
  238.  
  239. struct RigidityError <: TypecheckErrorType
  240.     var   :: String
  241.     type_ :: Type
  242. end
  243.  
  244. struct OccursCheckFailure <: TypecheckErrorType
  245.     var   :: String
  246.     type_ :: Type
  247. end
  248.  
  249. struct TypecheckError
  250.     type_    :: TypecheckErrorType
  251.     decl     :: String
  252.     nesting  :: Array{Expr}
  253.     bindings :: Dict{String, Type}
  254. end
  255.  
  256. mutable struct Context
  257.     environment    :: Dict{String, Scheme}
  258.     bindings       :: Dict{String, Type}
  259.     freshVarSupply :: Int
  260.     decl           :: String
  261.     nesting        :: Array{Expr}
  262. end
  263.  
  264. macro focus(func)
  265.     instrs = func.args[2]
  266.     if length(func.args[1].args) == 2
  267.         node = Symbol(func.args[1].args[1].args[3].args[1])
  268.     else
  269.         node = Symbol(func.args[1].args[3].args[1])
  270.     end
  271.  
  272.     func.args[2] = quote
  273.         if isa($(node), Expr)
  274.             push!(ctx.nesting, $(node))
  275.         end
  276.  
  277.         try
  278.             ret = eval($instrs)
  279.             return ret
  280.         catch err
  281.             if isa(err, TypecheckError)
  282.                 rethrow(TypecheckError(err.type_, err.decl, err.nesting[1:end], err.bindings))
  283.             else
  284.                 rethrow(err)
  285.             end
  286.         finally if isa($(node), Expr)
  287.             pop!(ctx.nesting)
  288.         end end
  289.     end
  290.     return func
  291. end
  292.  
  293. function throwTypecheckError(ctx :: Context, err :: TypecheckErrorType)
  294.     freeVars = collect(setdiff(freeVariables(ctx.nesting[1]), keys(ctx.environment)))[1:min(10,end)]
  295.     relevantBindings = Dict{String,Type}([(var, ctx.bindings[var]) for var in freeVars])
  296.     throw(TypecheckError(err, ctx.decl, ctx.nesting, relevantBindings))
  297. end
  298.  
  299. function freshVar(ctx :: Context)
  300.     name = "#$(ctx.freshVarSupply)"
  301.     ctx.freshVarSupply += 1
  302.     return name
  303. end
  304.  
  305. freshType(ctx :: Context) = VarType(freshVar(ctx), false)
  306.  
  307. function substitute(varName :: String, varType :: Type, ctx :: Context)
  308.     for (var, typ) in ctx.bindings
  309.         ctx.bindings[var] = substitute(varName, varType, typ)
  310.     end
  311. end
  312.  
  313. rigidify(type_ :: T) where T <: Type = rigidify(type_, freeTypeVars(type_))
  314.  
  315. function rigidify(type_ :: VarType, ftvs :: Set{String})
  316.     if type_.name in ftvs
  317.         return VarType(type_.name, true)
  318.     else
  319.         return type_
  320.     end
  321. end
  322.  
  323. rigidify(type_ :: FunType, ftvs :: Set{String}) = FunType(map(t -> rigidify(t, ftvs), type_.domain), relax(type_.codomain))
  324. rigidify(type_ :: TupleType, ftvs :: Set{String}) = TupleType(map(t -> rigidity(t, ftvs), type_.types))
  325. rigidify(type_ :: T, ftvs :: Set{String}) where T <: AtomType = type_
  326.  
  327. function generalize(type_ :: Type)
  328.     ftvs = collect(freeTypeVars(type_))
  329.     tmpVarIndex = 0
  330.  
  331.     for (i, ftv) in enumerate(ftvs)
  332.         if startswith(ftv, "#")
  333.             newName = String([Char(Int('A') + tmpVarIndex)])
  334.             ftvs[i] = newName
  335.             type_ = substitute(ftv, VarType(newName, false), type_)
  336.             tmpVarIndex += 1
  337.         end
  338.     end
  339.  
  340.     return Scheme(ftvs, rigidify(type_))
  341. end
  342.  
  343. relax(type_ :: VarType) = VarType(type_.name, false)
  344. relax(type_ :: FunType) = FunType(map(relax, type_.domain), relax(type_.codomain))
  345. relax(type_ :: TupleType) = TupleType(map(relax, type_.types))
  346. relax(type_ :: T) where T <: AtomType = type_
  347.  
  348. function instantiate(ctx :: Context, scheme :: Scheme)
  349.     instantiated = relax(scheme.type_)
  350.     for var in scheme.vars
  351.         newVar = freshType(ctx)
  352.         instantiated = substitute(var, newVar, instantiated)
  353.     end
  354.     return instantiated
  355. end
  356.  
  357. # Unification
  358.  
  359. function unify(ctx :: Context, a :: VarType, b :: VarType)
  360.     if a.rigid && b.rigid && a.name != b.name
  361.         throwTypecheckError(ctx, TypeMismatch(a, b))
  362.     elseif a.rigid
  363.         substitute(b.name, a, ctx)
  364.         return a
  365.     else
  366.         substitute(a.name, b, ctx)
  367.         return b
  368.     end
  369. end
  370.  
  371. function unify(ctx :: Context, a :: VarType, b :: RefType)
  372.     if a.rigid
  373.         throwTypecheckError(ctx, RigidityError(a.name, b))
  374.     elseif a.name in freeTypeVars(b)
  375.         throwTypecheckError(ctx, OccursCheckFailure(a.name, b))
  376.     else
  377.         substitute(a.name, b, ctx)
  378.     end
  379.     return b
  380. end
  381.  
  382. function unify(ctx :: Context, a :: RefType, b :: VarType)
  383.     if b.rigid
  384.         throwTypecheckError(ctx, RigidityError(b.name, a))
  385.     elseif b.name in freeTypeVars(a)
  386.         throwTypecheckError(ctx, OccursCheckFailure(b.name, a))
  387.     else
  388.         substitute(b.name, a, ctx)
  389.     end
  390.     return a
  391. end
  392.  
  393. function unify(ctx :: Context, a :: VarType, b :: T) where T <: Type
  394.     if a.rigid
  395.         throwTypecheckError(ctx, RigidityError(a.name, b))
  396.     elseif a.name in freeTypeVars(b)
  397.         throwTypecheckError(ctx, OccursCheckFailure(a.name, b))
  398.     else
  399.         substitute(a.name, b, ctx)
  400.     end
  401.     return b
  402. end
  403.  
  404. function unify(ctx :: Context, a :: T, b :: VarType) where T <: Type
  405.     if b.rigid
  406.         throwTypecheckError(ctx, RigidityError(b.name, a))
  407.     elseif b.name in freeTypeVars(a)
  408.         throwTypecheckError(ctx, OccursCheckFailure(b.name, a))
  409.     else
  410.         substitute(b.name, a, ctx)
  411.     end
  412.     return a
  413. end
  414.  
  415. function unify(ctx :: Context, a :: FunType, b :: FunType)
  416.     if length(a.domain) != length(b.domain)
  417.         throwTypecheckError(ctx, TypeMismatch(a, b))
  418.     end
  419.  
  420.     domain = []
  421.     for (paramA, paramB) in zip(a.domain, b.domain)
  422.         push!(domain, unify(ctx, paramA, paramB))
  423.     end
  424.     return FunType(domain, unify(ctx, a.codomain, b.codomain))
  425. end
  426.  
  427. function unify(ctx :: Context, a :: TupleType, b :: TupleType)
  428.     if length(a.types) != length(b.types)
  429.         throwTypecheckError(ctx, TypeMismatch(a, b))
  430.     end
  431.  
  432.     newTypes = []
  433.     for (x, y) in zip(a.types, b.types)
  434.         push!(newTypes, unify(ctx, x, y))
  435.     end
  436.     return TupleType(newTypes)
  437. end
  438.  
  439. unify(ctx :: Context, a :: RefType, b :: RefType) = RefType(unify(ctx, a.type_, b.type_))
  440. unify(ctx :: Context, a :: RefType, b :: T) where T <: Type = RefType(unify(ctx, a.type_, b))
  441. unify(ctx :: Context, a :: T, b :: RefType) where T <: Type = RefType(unify(ctx, a, b.type_))
  442. unify(ctx :: Context, a :: T, b :: T) where T <: AtomType = a
  443. unify(ctx :: Context, a :: T, b :: U) where T <: Type where U <: Type = throwTypecheckError(ctx, TypeMismatch(a, b))
  444.  
  445. function unify(ctx :: Context, a :: Scheme, b :: Scheme)
  446.     t = a.type_
  447.     for (ta, tb) in zip(a.vars, b.vars)
  448.         t = substitute(ta, VarType(tb, true), t)
  449.     end
  450.     return unify(ctx, t, b.type_)
  451. end
  452.  
  453. # Inference algorithm
  454.  
  455. @focus function typecheck(ctx :: Context, expr :: VarExpr)
  456.     try
  457.         return instantiate(ctx, ctx.environment[expr.name])
  458.     catch err
  459.         if isa(err, KeyError)
  460.             try
  461.                 return ctx.bindings[expr.name]
  462.             catch err
  463.                 if isa(err, KeyError)
  464.                     throwTypecheckError(ctx, ScopeError(expr.name))
  465.                 else
  466.                     rethrow(err)
  467.                 end
  468.             end
  469.         else
  470.             rethrow(err)
  471.         end
  472.     end
  473. end
  474.  
  475. @focus function typecheck(ctx :: Context, expr :: FunExpr)
  476.     for param in expr.params
  477.         if isa(param.type_, Type)
  478.             ctx.bindings[param.name] = param.type_
  479.         else
  480.             ctx.bindings[param.name] = freshType(ctx)
  481.         end
  482.     end
  483.  
  484.     codomain = typecheck(ctx, expr.body)
  485.     domain = []
  486.     for param in expr.params
  487.         push!(domain, ctx.bindings[param.name])
  488.         delete!(ctx.bindings, param.name)
  489.     end
  490.     return FunType(domain, codomain)
  491. end
  492.  
  493. @focus typecheck(ctx :: Context, expr :: CallExpr) =
  494.     unify(ctx, typecheck(ctx, expr.called), FunType([typecheck(ctx, arg) for arg in expr.arguments], freshType(ctx))).codomain
  495.  
  496. typecheck(ctx :: Context, instr :: LetInstr) = ctx.environment[instr.name] = generalize(typecheck(ctx, instr.value))
  497. typecheck(ctx :: Context, instr :: VarInstr) = ctx.bindings[instr.name] = RefType(typecheck(ctx, instr.value))
  498. typecheck(ctx :: Context, instr :: ExprInstr) = typecheck(ctx, instr.expr)
  499.  
  500. @focus function typecheck(ctx :: Context, instr :: AssignInstr)
  501.     try
  502.         varType = ctx.bindings[instr.name]
  503.         valType = typecheck(ctx, instr.value)
  504.         unify(ctx, varType, RefType(valType))
  505.     catch err
  506.         if isa(err, KeyError)
  507.             throwTypecheckError(ctx, ScopeError(instr.name))
  508.         else
  509.             rethrow(err)
  510.         end
  511.     end
  512. end
  513.  
  514. @focus function typecheck(ctx :: Context, expr :: BlockExpr)
  515.     old_environment = copy(ctx.environment)
  516.     old_bindings = copy(ctx.bindings)
  517.     for instr in expr.instructions
  518.         typecheck(ctx, instr)
  519.     end
  520.     last = typecheck(ctx, expr.last)
  521.     ctx.environment = old_environment
  522.     ctx.bindings = old_bindings
  523.     return last
  524. end
  525.  
  526. @focus function typecheck(ctx :: Context, expr :: IfExpr)
  527.     unify(ctx, typecheck(ctx, expr.condition), BoolType())
  528.     tr = typecheck(ctx, expr.true_case)
  529.     fl = typecheck(ctx, expr.false_case)
  530.     return unify(ctx, tr, fl)
  531. end
  532.  
  533. @focus typecheck(ctx :: Context, expr :: IntLit) = IntType()
  534. @focus typecheck(ctx :: Context, expr :: BoolLit) = BoolType()
  535. @focus typecheck(ctx :: Context, expr :: StringLit) = StringType()
  536. @focus typecheck(ctx :: Context, expr :: TupleExpr) = TupleType(map(elt -> typecheck(ctx, elt), expr.elements))
  537.  
  538. @focus function typecheck(ctx :: Context, expr :: AddExpr)
  539.     unify(ctx, typecheck(ctx, expr.lhs), IntType())
  540.     unify(ctx, typecheck(ctx, expr.rhs), IntType())
  541.     return IntType()
  542. end
  543.  
  544. @focus function typecheck(ctx :: Context, expr :: E) where E <: ComparisonExpr
  545.     a = typecheck(ctx, expr.lhs)
  546.     b = typecheck(ctx, expr.rhs)
  547.     unify(ctx, a, b)
  548.     return BoolType()
  549. end
  550.  
  551. # Module
  552.  
  553. abstract type Declaration
  554. end
  555.  
  556. struct FunDecl <: Declaration
  557.     name       :: String
  558.     typeParams :: Any
  559.     params     :: Array{Param}
  560.     returnType :: Any
  561.     body       :: Expr
  562. end
  563.  
  564. struct Module
  565.     declarations :: Array{Declaration}
  566. end
  567.  
  568. mutable struct ModuleContext
  569.     environment :: Dict{String, Scheme}
  570. end
  571.  
  572. function typecheck(modctx :: ModuleContext, decl :: FunDecl)
  573.     ctx = Context(modctx.environment, Dict{String, Type}(), 0, decl.name, [])
  574.     ctx.bindings[decl.name] = freshType(ctx)
  575.     funType = typecheck(ctx, FunExpr(decl.params, decl.body))
  576.  
  577.     if isa(decl.returnType, Type)
  578.         unify(ctx, funType.codomain, decl.returnType)
  579.     end
  580.  
  581.     declType = ctx.bindings[decl.name]
  582.     modctx.environment[decl.name] = generalize(unify(ctx, declType, funType))
  583. end
  584.  
  585. function typecheck(ctx :: ModuleContext, mod :: Module)
  586.     for decl in mod.declarations
  587.         typecheck(ctx, decl)
  588.     end
  589. end
  590.  
  591. # Pretty printing
  592.  
  593. pretty(expr :: VarExpr) = expr.name
  594. pretty(expr :: FunExpr) = "fun($(join(map(pretty, expr.params), ", "))) -> $(pretty(expr.body))"
  595. pretty(expr :: CallExpr) = "$(pretty(expr.called))($(join(map(pretty, expr.arguments), ", ")))"
  596. pretty(expr :: VarInstr) = "var $(expr.name) = $(pretty(expr.value))"
  597. pretty(expr :: LetInstr) = "let $(expr.name) = $(pretty(expr.value))"
  598. pretty(expr :: AssignInstr) = "$(expr.name) = $(pretty(expr.value))"
  599. pretty(expr :: ExprInstr) = pretty(expr.expr)
  600. pretty(expr :: BlockExpr) = "{ $(join(map(pretty, push!(copy(expr.instructions), ExprInstr(expr.last))), "; ")) }"
  601. pretty(expr :: IfExpr) = "if $(pretty(expr.condition)) $(pretty(expr.true_case)) else $(pretty(expr.false_case))"
  602. pretty(expr :: TupleExpr) = "($(join(map(pretty, expr.elements), ", ")))"
  603. pretty(expr :: AddExpr) = "$(pretty(expr.lhs)) + $(pretty(expr.rhs))"
  604. pretty(expr :: EQExpr) = "$(pretty(expr.lhs)) == $(pretty(expr.rhs))"
  605. pretty(expr :: GTExpr) = "$(pretty(expr.lhs)) > $(pretty(expr.rhs))"
  606. pretty(expr :: LTExpr) = "$(pretty(expr.lhs)) < $(pretty(expr.rhs))"
  607. pretty(expr :: E) where E <: LitExpr = repr(expr.value)
  608.  
  609. pretty(param :: Param) = if isa(param.type_, Type) "$(param.name): $(pretty(param.type_))" else param.name end
  610.  
  611. pretty(typ :: VarType)    = typ.name
  612. pretty(typ :: FunType)    = "fun($(join(map(pretty, typ.domain), ", "))) -> $(pretty(typ.codomain))"
  613. pretty(typ :: TupleType)  = "($(join(map(pretty, typ.types), ", ")))"
  614. pretty(typ :: RefType)    = "ref $(pretty(typ.type_))"
  615. pretty(typ :: IntType)    = "Int"
  616. pretty(typ :: BoolType)   = "Bool"
  617. pretty(typ :: StringType) = "String"
  618. pretty(typ :: VoidType)   = "Void"
  619.  
  620. function pretty(scheme :: Scheme)
  621.     if isempty(scheme.vars)
  622.         return pretty(scheme.type_)
  623.     end
  624.  
  625.     if isa(scheme.type_, FunType)
  626.         return "fun<$(join(scheme.vars, ", "))>($(join(map(pretty, scheme.type_.domain), ", "))) -> $(pretty(scheme.type_.codomain))"
  627.     else
  628.         return "<$(join(scheme.vars, ", "))>$(pretty(scheme.type_))"
  629.     end
  630. end
  631.  
  632. pretty(err :: ScopeError)         = "Name not in scope: `$(err.name)`"
  633. pretty(err :: TypeMismatch)       = "Type mismatch: Expected value of type `$(pretty(err.a))`, got `$(pretty(err.b))`"
  634. pretty(err :: RigidityError)      = "Cannot unify rigid type variable `$(err.var)` to `$(pretty(err.type_))`"
  635. pretty(err :: OccursCheckFailure) = "Occurs check fails: Cannot construct infinite type `$(err.var) ~ $(pretty(err.type_))`"
  636.  
  637. exprCategory(expr :: VarExpr) = "expression `$(pretty(expr))`"
  638. exprCategory(expr :: FunExpr) = "anonymous function `$(pretty(expr))`"
  639. exprCategory(expr :: CallExpr) = "function call `$(pretty(expr))`"
  640. exprCategory(expr :: BlockExpr) = "block `$(pretty(expr))`"
  641. exprCategory(expr :: IfExpr) = "if-expression `$(pretty(expr))`"
  642. exprCategory(expr :: TupleExpr) = "tuple `$(pretty(expr))`"
  643. exprCategory(expr :: AddExpr) = "arithmetic formula `$(pretty(expr))`"
  644. exprCategory(expr :: E) where E <: ComparisonExpr = "comparison `$(pretty(expr))`"
  645. exprCategory(expr :: E) where E <: LitExpr = "literal `$(pretty(expr))`"
  646.  
  647. function pretty(err :: TypecheckError)
  648.     s = "A type error was raised while trying to typecheck `$(err.decl)`:\n$(pretty(err.type_))\n"
  649.  
  650.     for expr in err.nesting[max(1,end-5):end]
  651.         s *= "\t• In $(exprCategory(expr))\n"
  652.     end
  653.  
  654.     s *= "Relevant bindings include:\n"
  655.  
  656.     for (name, type_) in err.bindings
  657.         s *= "\t• $(name) : $(pretty(type_))\n"
  658.     end
  659.  
  660.     return s
  661. end
  662.  
  663. # Example
  664.  
  665. function main()
  666.     prelude = Dict(
  667.         "input"  => Scheme([], FunType([], StringType())),
  668.         "print"  => Scheme(["T"], FunType([VarType("T", true)], VoidType())),
  669.         "to_int" => Scheme([], FunType([StringType()], IntType()))
  670.     )
  671.  
  672.     mod = Module(
  673.         [
  674.             FunDecl("app", Nothing, [Param("f", Nothing), Param("x", Nothing)], Nothing, CallExpr(VarExpr("f"), [VarExpr("x")])),
  675.             # fun app(f, x) = f(x)
  676.  
  677.             FunDecl("positive", Nothing, [Param("x", Nothing)], Nothing, GTExpr(VarExpr("x"), IntLit(0))),
  678.             # fun positive(x) = x > 0
  679.  
  680.             FunDecl("increment", Nothing, [Param("x", Nothing)], Nothing, AddExpr(VarExpr("x"), IntLit(1))),
  681.             # fun increment(x) = x + 1
  682.  
  683.             FunDecl("fix", Nothing, [Param("f", Nothing)], Nothing, CallExpr(VarExpr("f"), [CallExpr(VarExpr("fix"), [VarExpr("f")])])),
  684.             # fun fix(f) = f(fix(f))
  685.  
  686.             FunDecl("id", ["A"], [Param("x", VarType("A", true))], VarType("A", true), VarExpr("x")),
  687.             # fun id<A>(x: A) -> A = x
  688.  
  689.             FunDecl("letGeneralization", [], [], Nothing, BlockExpr([LetInstr("f", FunExpr([Param("x", Nothing)], VarExpr("x")))], TupleExpr([CallExpr(VarExpr("f"), [IntLit(0)]), CallExpr(VarExpr("f"), [StringLit("test")])]))),
  690.             # fun letGeneralization() = {
  691.             #   let f(x) = x
  692.             #   (f 1, f "test")
  693.             # }
  694.  
  695.             FunDecl(
  696.                 "play",
  697.                 Nothing,
  698.                 [Param("num", Nothing)],
  699.                 Nothing,
  700.                 BlockExpr(
  701.                     [
  702.                         ExprInstr(CallExpr(VarExpr("print"), [StringLit("> ")])),
  703.                         LetInstr("guess", CallExpr(VarExpr("to_int"), [CallExpr(VarExpr("input"), [])]))
  704.                     ],
  705.                     IfExpr(
  706.                         AddExpr(VarExpr("guess"), VarExpr("num")),
  707.                         CallExpr(VarExpr("print"), [StringLit("gagné")]),
  708.                         IfExpr(
  709.                             LTExpr(VarExpr("guess"), VarExpr("num")),
  710.                             BlockExpr(
  711.                                 [ExprInstr(CallExpr(VarExpr("print"), [StringLit("+")]))],
  712.                                 CallExpr(VarExpr("play"), [VarExpr("num")])
  713.                             ),
  714.                             BlockExpr(
  715.                                 [ExprInstr(CallExpr(VarExpr("print"), [StringLit("-")]))],
  716.                                 CallExpr(VarExpr("play"), [VarExpr("num")])
  717.                             )
  718.                         )
  719.                     )
  720.                 )
  721.             ),
  722.             # fun play(num) = {
  723.             #     print("Affiche un nombre: ")
  724.             #     let guess = to_int(input())
  725.             #     if guess == num then
  726.             #         print("gagné")
  727.             #     else if guess < num {
  728.             #         print("+")
  729.             #         play(num)
  730.             #     } else {
  731.             #         print("-")
  732.             #         play(num)
  733.             #     }
  734.             # }
  735.  
  736.             FunDecl(
  737.                 "mutation",
  738.                 Nothing,
  739.                 [Param("x", Nothing)],
  740.                 Nothing,
  741.                 BlockExpr(
  742.                     [
  743.                         AssignInstr("x", AddExpr(VarExpr("x"), IntLit(1)))
  744.                     ],
  745.                     CallExpr(VarExpr("print"), [VarExpr("x")])
  746.                 )
  747.             ),
  748.             # fun mutation(x) = {
  749.             #   x = x + 1
  750.             #   print(x)
  751.             # }
  752.         ]        
  753.     )
  754.  
  755.     ctx = ModuleContext(prelude)
  756.  
  757.     try
  758.         typecheck(ctx, mod)
  759.     catch err
  760.         if isa(err, TypecheckError)
  761.             println(pretty(err))
  762.         else
  763.             rethrow(err)
  764.         end
  765.     end
  766.  
  767.     for (name, typ) in ctx.environment
  768.         println(name, " : ", pretty(typ))
  769.     end
  770. end
  771.  
  772. main()
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top