Module: Jade::Frontend::TypeChecking

Extended by:
TypeChecking, Inference::Helpers
Included in:
TypeChecking
Defined in:
lib/jade/frontend/type_checking.rb,
lib/jade/frontend/type_checking/env.rb,
lib/jade/frontend/type_checking/state.rb,
lib/jade/frontend/type_checking/loader.rb,
lib/jade/frontend/type_checking/result.rb,
lib/jade/frontend/type_checking/scheme.rb,
lib/jade/frontend/type_checking/var_gen.rb,
lib/jade/frontend/type_checking/expected.rb,
lib/jade/frontend/type_checking/definition.rb,
lib/jade/frontend/type_checking/constraints.rb,
lib/jade/frontend/type_checking/generalizer.rb,
lib/jade/frontend/type_checking/placeholder.rb,
lib/jade/frontend/type_checking/unification.rb,
lib/jade/frontend/type_checking/canonicalize.rb,
lib/jade/frontend/type_checking/substitution.rb,
lib/jade/frontend/type_checking/instantiation.rb,
lib/jade/frontend/type_checking/generalization.rb,
lib/jade/frontend/type_checking/inference/body.rb,
lib/jade/frontend/type_checking/inference/list.rb,
lib/jade/frontend/type_checking/port_resolution.rb,
lib/jade/frontend/type_checking/inference/assign.rb,
lib/jade/frontend/type_checking/inference/lambda.rb,
lib/jade/frontend/type_checking/inference/module.rb,
lib/jade/frontend/type_checking/inference/case_of.rb,
lib/jade/frontend/type_checking/inference/helpers.rb,
lib/jade/frontend/type_checking/inference/literal.rb,
lib/jade/frontend/type_checking/inference/pattern.rb,
lib/jade/frontend/type_checking/inference/grouping.rb,
lib/jade/frontend/type_checking/error/type_mismatch.rb,
lib/jade/frontend/type_checking/constraints/deriving.rb,
lib/jade/frontend/type_checking/error/missing_patterns.rb,
lib/jade/frontend/type_checking/inference/if_then_else.rb,
lib/jade/frontend/type_checking/inference/record_field.rb,
lib/jade/frontend/type_checking/constraints/deriving/eq.rb,
lib/jade/frontend/type_checking/error/derivation_failed.rb,
lib/jade/frontend/type_checking/inference/function_call.rb,
lib/jade/frontend/type_checking/inference/record_access.rb,
lib/jade/frontend/type_checking/inference/record_update.rb,
lib/jade/frontend/type_checking/error/port_not_decodable.rb,
lib/jade/frontend/type_checking/error/port_not_encodable.rb,
lib/jade/frontend/type_checking/inference/implementation.rb,
lib/jade/frontend/type_checking/inference/record_literal.rb,
lib/jade/frontend/type_checking/constraints/deriving/show.rb,
lib/jade/frontend/type_checking/inference/qualified_access.rb,
lib/jade/frontend/type_checking/inference/type_declaration.rb,
lib/jade/frontend/type_checking/error/pattern_type_mismatch.rb,
lib/jade/frontend/type_checking/error/unresolved_constraint.rb,
lib/jade/frontend/type_checking/constraints/deriving/helpers.rb,
lib/jade/frontend/type_checking/error/missing_implementation.rb,
lib/jade/frontend/type_checking/inference/import_declaration.rb,
lib/jade/frontend/type_checking/inference/struct_declaration.rb,
lib/jade/frontend/type_checking/inference/variable_reference.rb,
lib/jade/frontend/type_checking/error/if_branch_type_mismatch.rb,
lib/jade/frontend/type_checking/error/list_item_type_mismatch.rb,
lib/jade/frontend/type_checking/constraints/deriving/decodable.rb,
lib/jade/frontend/type_checking/constraints/deriving/encodable.rb,
lib/jade/frontend/type_checking/inference/function_declaration.rb,
lib/jade/frontend/type_checking/constraints/deriving/assignable.rb,
lib/jade/frontend/type_checking/error/if_branches_type_mismatch.rb,
lib/jade/frontend/type_checking/inference/constructor_reference.rb,
lib/jade/frontend/type_checking/inference/interface_declaration.rb,
lib/jade/frontend/type_checking/error/if_condition_type_mismatch.rb,
lib/jade/frontend/type_checking/error/function_body_type_mismatch.rb,
lib/jade/frontend/type_checking/error/function_call_type_mismatch.rb,
lib/jade/frontend/type_checking/error/record_access_type_mismatch.rb,
lib/jade/frontend/type_checking/error/implementation_type_mismatch.rb,
lib/jade/frontend/type_checking/error/case_of_branches_type_mismatch.rb,
lib/jade/frontend/type_checking/inference/interop_import_declaration.rb

Defined Under Namespace

Modules: Canonicalize, Constraints, Definition, Error, Generalization, Generalizer, Inference, Instantiation, Loader, PortResolution, Unification Classes: ConstructorDef, Env, Expected, InterfaceDef, Placeholder, Result, ResultAcc, Scheme, State, StructDef, Substitution, TypeDef, VarGen

Instance Method Summary collapse

Methods included from Inference::Helpers

generalize, instantiate, type_from_symbol, unify

Instance Method Details

#check(entry, registry) ⇒ Object 



23
24
25
26
27
28
29
30
31
32
33
 
# File 'lib/jade/frontend/type_checking.rb', line 23

def check(entry, registry)
  Loader
    .load(entry, registry)
    .then { collect_constraints(entry, registry, it) }
    .then { check_node(entry.ast, registry, State.init(it), Expected.infer(it.fresh)) }
    .then { finalize(*it, registry) }
    .map { Canonicalize.run(entry.ast, it, registry) }
    .map { it.canonicalize_node_types }
    .map { entry.with(env: it) }
    .and_then { PortResolution.resolve(it, registry) }
end

#check_node(node, registry, state, expected_type) ⇒ Object 



127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
 
# File 'lib/jade/frontend/type_checking.rb', line 127

def check_node(node, registry, state, expected_type)
  case node
  in AST::Body then Inference::Body
  in AST::CaseOf then Inference::CaseOf
  in AST::ConstructorReference then Inference::ConstructorReference
  in AST::FunctionCall then Inference::FunctionCall
  in AST::FunctionDeclaration then Inference::FunctionDeclaration
  in AST::Grouping then Inference::Grouping
  in AST::IfThenElse then Inference::IfThenElse
  in AST::Implementation then Inference::Implementation
  in AST::ImportDeclaration then Inference::ImportDeclaration
  in AST::InteropImportDeclaration then Inference::InteropImportDeclaration
  in AST::Lambda then Inference::Lambda
  in AST::List then Inference::List
  in AST::Literal | AST::CharLiteral then Inference::Literal
  in AST::Module then Inference::Module
  in AST::QualifiedAccess then Inference::QualifiedAccess
  in AST::RecordAccess then Inference::RecordAccess
  in AST::StructDeclaration then Inference::StructDeclaration
  in AST::InterfaceDeclaration then Inference::InterfaceDeclaration
  in AST::RecordField then Inference::RecordField
  in AST::RecordLiteral then Inference::RecordLiteral
  in AST::RecordUpdate then Inference::RecordUpdate
  in AST::TypeDeclaration then Inference::TypeDeclaration
  in AST::Assign then Inference::Assign
  in AST::VariableReference then Inference::VariableReference
  end
    .infer(node, registry, state, expected_type)
    .then { |s, r| [pin_node_type(s, node, r), r] }
end

#check_repl(node, registry, env = Env.new) ⇒ Object 



122
123
124
125
 
# File 'lib/jade/frontend/type_checking.rb', line 122

def check_repl(node, registry, env = Env.new)
  check_node(node, registry, env, Expected.infer(env.fresh))
    .to_result
end

#collect_constraints(entry, registry, env, rounds = declaration_count(entry)) ⇒ Object

A collecting pass walks declarations in source order, so a call to a function declared later sees it before its constraints are known and collects nothing. Each repeat carries them one caller further back, so a chain of forward references needs as many rounds as it is long.



39
40
41
42
43
44
45
46
47
48
 
# File 'lib/jade/frontend/type_checking.rb', line 39

def collect_constraints(entry, registry, env, rounds = declaration_count(entry))
  return env if rounds.zero?

  collect_round(entry, registry, env)
    .then do |collected|
      next env if same_constraints?(collected, env)

      collect_constraints(entry, registry, collected, rounds - 1)
    end
end

#collect_round(entry, registry, env) ⇒ Object 



50
51
52
53
54
55
 
# File 'lib/jade/frontend/type_checking.rb', line 50

def collect_round(entry, registry, env)
  State
    .init(env, skip_constraints: true)
    .then { check_node(entry.ast, registry, it, Expected.infer(env.fresh)) }
    .then { Generalizer.generalize(it.first.env) }
end

#constraint_fingerprint(env) ⇒ Object 



61
62
63
64
65
66
 
# File 'lib/jade/frontend/type_checking.rb', line 61

def constraint_fingerprint(env)
  env
    .bindings
    .map { |name, binding| [name, binding.constraints.map { [it.interface, it.type.to_s] }.sort] }
    .sort
end

#declaration_count(entry) ⇒ Object 



68
69
70
71
72
73
74
75
76
 
# File 'lib/jade/frontend/type_checking.rb', line 68

def declaration_count(entry)
  case entry.ast
  in AST::Module(body: AST::Body(expressions:)) then expressions
  in AST::Body(expressions:) then expressions
  else []
  end
    .count { it.is_a?(AST::FunctionDeclaration) }
    .then { it + 1 }
end

#finalize(state, result, registry) ⇒ Object 



78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
 
# File 'lib/jade/frontend/type_checking.rb', line 78

def finalize(state, result, registry)
  state.env => { bindings:, entry_name: }

  errors = bindings
    .select do |k,v|
      # filter locals
      b_entry_name = k.split('.')[0..-2].join(',')
      b_entry_name == entry_name
    end
    .reject { |k, _| interface_function?(k, registry) }
    .reject { |k, _| interop_function?(k, registry) }
    .values
    .flat_map(&:constraints)
    .flat_map { Constraints.solve_at_finalize(it, registry, entry_name) }

  # TODO: impl declarations need their own finalization pass here.
  # Unresolved constraints from impl function bodies (e.g. Eq(a) from
  # `one.id == other.id` inside `impl Eq for Pepe(a)`) should be promoted
  # to impl-level requirements — making the impl an ImplementationTemplate
  # with those constraints — rather than being dropped silently.

  state
    .with(errors: state.errors + errors)
    .to_result
end

#interface_function?(qname, registry) ⇒ Boolean

Returns:

  • (Boolean) 


104
105
106
107
108
109
110
 
# File 'lib/jade/frontend/type_checking.rb', line 104

def interface_function?(qname, registry)
  *module_parts, name = qname.split('.')
  Symbol
    .value_ref(module_parts.join('.'), name)
    .then { registry.lookup(it) }
    .is_a?(Symbol::InterfaceFunction)
end

#interop_function?(qname, registry) ⇒ Boolean

Polymorphic-port constraints represent caller requirements (resolved at each call site), not body obligations to verify here.

Returns:

  • (Boolean) 


114
115
116
117
118
119
120
 
# File 'lib/jade/frontend/type_checking.rb', line 114

def interop_function?(qname, registry)
  *module_parts, name = qname.split('.')
  Symbol
    .value_ref(module_parts.join('.'), name)
    .then { registry.lookup(it) }
    .is_a?(Symbol::InteropFunction)
end

#same_constraints?(one, other) ⇒ Boolean

Returns:

  • (Boolean) 


57
58
59
 
# File 'lib/jade/frontend/type_checking.rb', line 57

def same_constraints?(one, other)
  constraint_fingerprint(one) == constraint_fingerprint(other)
end