def Blaster.Optimize.isNullString (e : Lean.Expr) : Bool

Return true when e corresponds to the null string literal.

Equations

• Blaster.Optimize.isNullString (Lean.Expr.lit (Lean.Literal.strVal "")) = true
• Blaster.Optimize.isNullString e = false

def Blaster.Optimize.normStringValue (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Normalize String.mk (List.cons c₁ (.. (List.cons cₙ List.nil))) to Expr.lit (Literal.strVal s) only when the list of chars are constant values. Otherwise return (mkApp f args[0]!). Assume that `f := Expr.const ``String.mk. An error is triggered when args.size ≠ 1.

Equations

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

def Blaster.Optimize.normStringValue.getListChars? (e : Lean.Expr) : Lean.MetaM (Option (Array Char))

Equations

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

def Blaster.Optimize.optimizeStrAppend (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on String.append :

• S1 ++ S2 ==> S1 "++" S2
• "" ++ e | e ++ "" ==> e Assume that f = Expr.const ``String.append. An error is triggered when args.size ≠ 2 (i.e., only fully applied String.append expected at this stage)

Equations

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

def Blaster.Optimize.optimizeStrAppend.cstStrAppend? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for String.append return some (S1 "++" S2) when op1 := S1 ∧ op2 := S2. Otherwise none.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeStrAppend.cstStrAppend? op1 op2 = pure none

def Blaster.Optimize.optimizeStrAppend.appendNull? (op1 op2 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for String.append,

• return some op2 when op1 := ""`.
• return some op1 when op2 := ""Otherwisenone`.

Equations

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

def Blaster.Optimize.optimizeStrLength (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on String.length :

• String.length S ==> "String.length" S Assume that f = Expr.const ``String.length. An error is triggered when args.size ≠ 1 (i.e., only fully applied String.length expected at this stage)

Equations

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

def Blaster.Optimize.optimizeStrLength.cstStrLength? (op : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op corresponding to the operand for String.length return some ("String.length" S) when op := S. Otherwise none.

Equations

• Blaster.Optimize.optimizeStrLength.cstStrLength? (Lean.Expr.lit (Lean.Literal.strVal s)) = do let a ← Blaster.Optimize.mkNatLitExpr s.length pure (some a)
• Blaster.Optimize.optimizeStrLength.cstStrLength? op = pure none

def Blaster.Optimize.optimizeStrReplace (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on String.replace :

• String.replace e1 e2 e3 ==> e1 (if e2 =ₚₜᵣ e3)
• String.replace S1 S2 S3 ==> "String.replace" S1 S2 S3
• String.replace "" e2 e3 ==> "" Assume that f = Expr.const ``String.replace. An error is triggered when args.size ≠ 3 (i.e., only fully applied String.replace expected at this stage)

Equations

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

def Blaster.Optimize.optimizeStrReplace.cstStrReplace? (op1 op2 op3 : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1, op2 and op3 corresponding to the operands for String.replace return some ("String.replace" S1 S2 S3) when op1 := S1 ∧ op2 := S2 ∧ op3 := S3. Otherwise none.

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeStrReplace.cstStrReplace? op1 op2 op3 = pure none

def Blaster.Optimize.optimizeString? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Apply simplification/normalization rules on String operators.

Equations

• Blaster.Optimize.optimizeString? (Lean.Expr.const `String.mk us) args = do let a ← Blaster.Optimize.normStringValue (Lean.Expr.const `String.mk us) args pure (some a)
• Blaster.Optimize.optimizeString? (Lean.Expr.const `String.append us) args = do let a ← Blaster.Optimize.optimizeStrAppend (Lean.Expr.const `String.append us) args pure (some a)
• Blaster.Optimize.optimizeString? (Lean.Expr.const `String.length us) args = do let a ← Blaster.Optimize.optimizeStrLength (Lean.Expr.const `String.length us) args pure (some a)
• Blaster.Optimize.optimizeString? (Lean.Expr.const `String.replace us) args = do let a ← Blaster.Optimize.optimizeStrReplace (Lean.Expr.const `String.replace us) args pure (some a)
• Blaster.Optimize.optimizeString? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizeString? f args = pure none