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 HirFrame

  Our call stack, but on the heap.

• flags : Flags

  The current flag settings.

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

Equations

• f.is_case_insensitive = f.case_insensitive.getD false

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

Equations

• f.is_dot_matches_new_line = f.dot_matches_new_line.getD false

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

Equations

• f.is_multi_line = f.multi_line.getD false

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

Equations

• f.is_crlf = f.crlf.getD false

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

Equations

• f.is_swap_greed = f.swap_greed.getD false

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

Equations

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

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

@[irreducible]

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

Equations

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

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

Equations

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

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

@[irreducible]

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

Equations

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

def Syntax.visit_pre (ast : AstItems.Ast) : StateT 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 : AstItems.Ast) : StateT 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 : AstItems.ClassSetItem) : StateT 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.
• Syntax.visit_class_set_item_pre ast = pure ()

def Syntax.visit_class_set_item_post (ast : AstItems.ClassSetItem) : StateT 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 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 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 : AstItems.ClassSetBinaryOp) : StateT 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 : AstItems.Visitor Hir Translator

Equations

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

def Syntax.translate (flags : Flags := default) (ast : AstItems.Ast) : Except String 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