Class: IgniterLang::TypeChecker

Inherits:
Object
  • Object
show all
Defined in:
lib/igniter_lang/typechecker.rb

Constant Summary collapse

DEFAULT_VERSION = 
"typed-pass-executable-proof-v0"

Instance Method Summary collapse

Constructor Details

#initialize(typechecker_version: DEFAULT_VERSION) ⇒ TypeChecker

Returns a new instance of TypeChecker.



9
10
11
 
# File 'lib/igniter_lang/typechecker.rb', line 9

def initialize(typechecker_version: DEFAULT_VERSION)
  @typechecker_version = typechecker_version
end

Instance Method Details

#typecheck(classified_program) ⇒ Object 



13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
 
# File 'lib/igniter_lang/typechecker.rb', line 13

def typecheck(classified_program)
  @type_shapes = type_shapes(classified_program)
  @assumption_registry = classified_program.fetch("assumption_registry", [])
  @type_shapes["Assumption"] = assumption_shape if assumptions_present?(classified_program)
  @assumption_errors = assumption_errors_by_name(@assumption_registry)
  @olap_env = olap_env(classified_program.fetch("olap_points", []))
  @olap_errors = olap_declaration_errors(@olap_env)
  typed_contracts = classified_program.fetch("contracts").map do |contract|
    typecheck_contract(contract)
  end

  result = {
    "kind" => "typed_program",
    "typechecker_version" => @typechecker_version,
    "program_id" => program_id(classified_program),
    "classified_program_id" => classified_program.fetch("program_id"),
    "source_path" => classified_program.fetch("source_path"),
    "source_hash" => classified_program.fetch("source_hash"),
    "grammar_version" => classified_program.fetch("grammar_version"),
    "module" => classified_program.fetch("module"),
    "type_env" => @type_shapes,
    "contracts" => typed_contracts,
    "type_errors" => typed_contracts.flat_map { |contract| contract.fetch("type_errors") },
    "semantic_ir_ref" => nil
  }
  result["assumption_registry"] = @assumption_registry unless @assumption_registry.empty?
  result["olap_points"] = @olap_env.values.map { |decl| decl.fetch("semantic_node") } unless @olap_env.empty?
  type_warnings = typed_contracts.flat_map { |contract| contract.fetch("type_warnings", []) }
  result["type_warnings"] = type_warnings unless type_warnings.empty?
  result
end