Translate

Translate (Syntax.translate) an abstract syntax tree Syntax.Ast.Ast into a high level intermediate representation Syntax.Hir.

structure Syntax.Translator : Type

Translator state

• stack : Array Syntax.HirFrame

  Our call stack, but on the heap.

• flags : Syntax.Flags

  The current flag settings.

def Syntax.Flags.is_case_insensitive (f : Syntax.Flags) : Bool

Equations

• f.is_case_insensitive = f.case_insensitive.getD false

def Syntax.Flags.is_dot_matches_new_line (f : Syntax.Flags) : Bool

Equations

• f.is_dot_matches_new_line = f.dot_matches_new_line.getD false

def Syntax.Flags.is_multi_line (f : Syntax.Flags) : Bool

Equations

• f.is_multi_line = f.multi_line.getD false

def Syntax.Flags.is_crlf (f : Syntax.Flags) : Bool

Equations

• f.is_crlf = f.crlf.getD false

def Syntax.Flags.is_swap_greed (f : Syntax.Flags) : Bool

Equations

• f.is_swap_greed = f.swap_greed.getD false

def Syntax.pop_concat_expr (stack : Array Syntax.HirFrame) : Except String (Array Syntax.HirFrame × Option Syntax.Hir)

Equations

• One or more equations did not get rendered due to their size.

theorem Syntax.sizeOf_pop_concat_expr {stack' : Array Syntax.HirFrame} {hir : Syntax.Hir} {stack : Array Syntax.HirFrame} (h : Syntax.pop_concat_expr stack = Except.ok (stack', some hir)) : sizeOf stack' < sizeOf stack

@[irreducible]

def Syntax.pop_concat_exprs (stack : Array Syntax.HirFrame) (exprs : Array Syntax.Hir) : Except String (Array Syntax.HirFrame × Array Syntax.Hir)

Equations

• One or more equations did not get rendered due to their size.

def Syntax.pop_alt_expr (stack : Array Syntax.HirFrame) : Except String (Array Syntax.HirFrame × Option Syntax.Hir)

Equations

• One or more equations did not get rendered due to their size.

theorem Syntax.sizeOf_pop_alt_expr {stack' : Array Syntax.HirFrame} {hir : Syntax.Hir} {stack : Array Syntax.HirFrame} (h : Syntax.pop_alt_expr stack = Except.ok (stack', some hir)) : sizeOf stack' < sizeOf stack

@[irreducible]

def Syntax.pop_alt_exprs (stack : Array Syntax.HirFrame) (exprs : Array Syntax.Hir) : Except String (Array Syntax.HirFrame × Array Syntax.Hir)

Equations

• One or more equations did not get rendered due to their size.

def Syntax.visit_pre (ast : Syntax.AstItems.Ast) : StateT Syntax.Translator (Except String) PUnit

This method is called on an Ast before descending into child Ast nodes.

Equations

• One or more equations did not get rendered due to their size.

def Syntax.visit_post (ast : Syntax.AstItems.Ast) : StateT Syntax.Translator (Except String) PUnit

This method is called on an Ast after descending all of its child Ast nodes.

Equations

• One or more equations did not get rendered due to their size.

def Syntax.visit_class_set_item_pre (ast : Syntax.AstItems.ClassSetItem) : StateT Syntax.Translator (Except String) PUnit

This method is called on every [ClassSetItem] before descending into child nodes.

Equations

• One or more equations did not get rendered due to their size.

def Syntax.visit_class_set_item_post (ast : Syntax.AstItems.ClassSetItem) : StateT Syntax.Translator (Except String) PUnit

This method is called on every [ClassSetItem] after descending into child nodes.

Equations

• One or more equations did not get rendered due to their size.

def Syntax.visit_class_set_binary_op_pre : StateT Syntax.Translator (Except String) PUnit

This method is called on every [ClassSetBinaryOp] before descending into child nodes.

Equations

• Syntax.visit_class_set_binary_op_pre = do let t ← get set { stack := t.stack.push (Syntax.HirFrame.ClassUnicode Syntax.ClassUnicode.empty), flags := t.flags }

def Syntax.visit_class_set_binary_op_in : StateT Syntax.Translator (Except String) PUnit

This method is called between the left hand and right hand child nodes.

Equations

• Syntax.visit_class_set_binary_op_in = do let t ← get set { stack := t.stack.push (Syntax.HirFrame.ClassUnicode Syntax.ClassUnicode.empty), flags := t.flags }

def Syntax.visit_class_set_binary_op_post (op : Syntax.AstItems.ClassSetBinaryOp) : StateT Syntax.Translator (Except String) PUnit

This method is called on every [ClassSetBinaryOp] after descending into child nodes.

Equations

• One or more equations did not get rendered due to their size.

instance Syntax.instVisitorHirTranslator : Syntax.AstItems.Visitor Syntax.Hir Syntax.Translator

Equations

• One or more equations did not get rendered due to their size.

def Syntax.translate (flags : optParam Syntax.Flags default) (ast : Syntax.AstItems.Ast) : Except String Syntax.Hir

Translate the given abstract syntax tree into a high level intermediate representation.

Equations

• Syntax.translate flags ast = Syntax.AstItems.visit Syntax.instVisitorHirTranslator { stack := #[], flags := flags } ast