Translate

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

structure Regex.Syntax.Translator : Type

Translator state

• stack : Array HirFrame

  Our call stack, but on the heap.

• flags : Flags

  The current flag settings.

def Regex.Syntax.finish (translator : Translator) : Except String Hir

Equations

• Regex.Syntax.finish translator = match translator.stack.pop? with | some (frame, snd) => frame.unwrap_expr | none => Except.error "empty stack"

def Regex.Syntax.start (translator : Translator) : Translator

Equations

• Regex.Syntax.start translator = translator

def Regex.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 Regex.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 Regex.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.
• Regex.Syntax.visit_class_set_item_pre ast = pure ()

def Regex.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 Regex.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

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

def Regex.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

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

def Regex.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.

@[implicit_reducible]

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

Equations

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

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

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

Equations

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