Links

• https://cs3110.github.io/textbook/chapters/interp/intro.html

• finished simple interpreter here: https://cs3110.github.io/textbook/code/simpl.zip

• progress:

  • https://www.youtube.com/watch?v=duTIBuK_fdw&list=PLre5AT9JnKShBOPeuiD9b-I4XROIJhkIU&index=174

Overview

Definitions

• Lexer: produces tokens
• Parser: declares tokens, produces AST nodes
• Evaluator: computes on AST nodes

Steps

• single-step relation: e -> e'

  • exactly one step of evaluation.
  • values do not step.

• multi-step relation: e ->* e'

  • star is reflexive transitive closure.

• big-step relation: e => v

  • it reduces e all way down to a value v
  • it is the eval function.

• Hints: when running interp in utop you can enable tracing of the step function.

─( 14:01:57 )─< command 0 >──────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # interp "let x = 12 in let y = 13 in x + y";;
- : string = "25"
─( 14:01:57 )─< command 1 >──────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # parse "let x = 12 in let y = 13 in x + y";;
- : expr = Let ("x", Int 12, Let ("y", Int 13, Binop (Add, Var "x", Var "y")))
─( 14:02:08 )─< command 2 >──────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # #trace step;;
step is now traced.
─( 14:02:18 )─< command 3 >──────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # interp "let x = 12 in let y = 13 in x + y";;
step <-- Let ("x", Int 12, Let ("y", Int 13, Binop (Add, Var "x", Var "y")))
step --> Let ("y", Int 13, Binop (Add, Int 12, Var "y"))
step <-- Let ("y", Int 13, Binop (Add, Int 12, Var "y"))
step --> Binop (Add, Int 12, Int 13)
step <-- Binop (Add, Int 12, Int 13)
step --> Int 25
- : string = "25"

Single step semantics

Value

• A value is ... a value, it cannot take a step.

Binary op semantics

• e1 bop e2 -> e1' bop e2 if e1 -> e1'
  • if we can single step e1 we do. And we start from left
• v1 bop e2 -> v1 bop e2' if e2 -> e2'
• v1 bop v2 -> v where v is the result of the operation

If semantics

• if e1 then e2 else e3 -> if e1' then e2 else e3 if e1 -> e1'
  • if we can single step e1 we do
• if true then e2 else e3 -> e2
• if false then e2 else e3 -> e3

Let semantics

• let x = e1 in e2 -> let x = e1' in e2 if e1 -> e1'
• let x = v1 in e2 -> e2 with v1 substituted for x

Function semantics

• e1 e2 -> e1' e2 if e1 -> e1'
• v1 e2 -> v1 e2' if e2 -> e2'
• (fun x -> e) v2 -> e {v2/x}
  • it means the first expression must be a function

Pairs semantics

• (e1, e2) -> (e1', e2) if e1 -> e1'
• (v1, e2) -> (v1, e2') if e2 -> e2'
• fst (v1, v2) -> v1
• snd (v1, v2) -> v2

Constructors semantics

• Left e -> Left e' if e -> e'
• Right e -> Right e' if e -> e'

Pattern matching semantics

• (match e with Left x1 -> e1 | Right x2 -> e2) -> (match e' with Left x1 -> e1 | Right x2 -> e2 if e -> e'
• (match Left v with Left x1 -> e1 | Right x2 -> e2) -> e1{v/x1}
• (match Right v with Left x1 -> e1 | Right x2 -> e2) -> e2{v/x2}

Big step semantics

Value

• v => v

Binary op semantics

e1 + e2 => v
 if e1 => v1
 and e2 => v2
 and v is the result of primitive operation v1 + v2

If semantics

if e1 then e2 else e3 => v2
 if e1 => true
 and e2 => v2
if e1 then e2 else e3 => v3
 if e1 => false
 and e3 => v3

Let semantics

let x = e1 in e2 => v2
 if e1 => v1
 and e2{v1/x} => v2

Substitutions

Definition

• Substitution: e{v/x}
  • means e with v substituted for x
  • a substitution is not a step

Integer

• For integer, nothing to do: i{v/x} = i

Binary operators

• For binary op: (e1 + e2){v/x} = (e1{v/x}) + (e2{v/x})
  • same for all binary operators

Variables

• For variables:
  • x{v/x} = v
  • y{v/x} = y

Let semantic

• Two cases:
  • (let x = e1 in e2){v/x} = let y = (e1{v/x}) in e2
  • (let y = e1 in e2){v/x} = let y = (e1{v/x}) in (e2{v/x})

If semantic

• (if e1 then e2 else e3){e/x} = if e1{e/x} then e2{e/x} else e3{e/x}