***********************************************************
JOCALF SEMANTICS
***********************************************************

***********************************************************
EVALUATION RELATIONS
***********************************************************

Expressions:
<e, env, st> ==> <r, st'>

Definitions:
<d, env, st> ==> <r, env', st'>

Phrases:
<p, env, st> ==> <r, env', st'>

***********************************************************
PHRASES
***********************************************************
  
<p, env, st> ==> <r, env, st'>
  if p is an expression e
  and <e, env, st> ==> <r, st'>
  
<p, env, st> ==> <r, env', st'>
  if p is a definition d
  and <d, env, st> ==> <r, env', st'>
  
***********************************************************
DEFINITIONS
***********************************************************

<let x = e, env, st> ==> <v, env[x -> v], st'>
  if <e, env, st> ==> <v, st'>

<let x = e, env, st> ==> <exn v, env, st'>
  if <e, env, st> ==> <exn v, st'>

let rec f (x1 ... xn) = e, env, st> ==> <v, env[f -> v], st>
  if v = (| fun (x1 ... xn) -> e, env[f -> v] |)

***********************************************************
CONSTANTS
***********************************************************

<i, env, st> ==> <i, st>

<b, env, st> ==> <b, st>

<s, env, st> ==> <s, st>

<undefined, env, st> ==> <undefined, st>

***********************************************************
VARIABLES and LET
***********************************************************

<x, env, st> ==> <v, st>
  if env(x) = v
  
<x, env, st> ==> <exn "Unbound variable", st>
  if x is not bound in env
  
<let x = e1 in e2, env, st> ==> <v2, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env[x -> v1], st1> ==> <v2, st2>

<let x = e1 in e2, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env[x -> v1], st1> ==> <exn v, st'>

<let x = e1 in e2, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>

<let rec f (x1 ... xn) = e1 in e2, env, st> ==> <v2, st2>
  if v1 = (| fun (x1 ... xn) -> e1, env[f -> v1] |)
  and <e2, env[f -> v1], st> ==> <v2, st2>

***********************************************************
FUNCTIONS and APPLICATION
***********************************************************

<fun (x1 ... xn) -> e, env, st> ==> <(|fun (x1 ... xn) -> e, env|), st>

<e0 e1 ... en, env, st> ==> <r, st'>
  if <e0, env, st> ==> <(|fun (x1 ... xn) -> e, env_cl|), st0>
  and <e1, env, st0> ==> <v1, st1>
  and ...
  and <en, env, st(n-1)> ==> <vn, stn>
  and <e, env_cl[x1->v1, ..., xn->vn], stn> ==> <r, st'>
  
<e0 e1 ... en, env, st> ==> <v, stn>
  if <e0, env, st> ==> <extern, st0>
  and <e1, env, st0> ==> <v1, st1>
  and ...
  and <en, env, st(n-1)> ==> <vn, stn>
  and evaluating OCaml function extern in state stn
    on inputs v1 ... vn results in output value v

<e0 e1 ... en, env, st> ==> <exn "Application: not a function", st'>
  if <e0, env, st> ==> <v, st'>
  and v is neither a closure nor an external function

<e0 e1 ... en, env, st> ==> <exn "Application: wrong number of arguments", st'>
  if <e0, env, st> ==> <(|fun (x1 ... xm) -> e, env_cl|), st'> 
  and m <> n
  
<e0 e1 ... en, env, st> ==> <exn "Application: wrong number of arguments", st'>
  if <e0, env, st> ==> <extern, st'> 
  and extern is an external function that does not take exactly n arguments
  
<e0 e1 ... en, env, st> ==> <exn v, st'>
  if <e0, env, st> ==> <exn v, st'>

<e0 e1 ... en, env, st> ==> <exn v', st'>
  if <e0, env, st> ==> <v, st0>
  and v is either a closure or an external function
  and there exists a j in 1..n such that
    for all i in 1..j-1, <ei, env, st(i-1)> ==> <vi, sti>
    and <ej, env, st(j-1)> ==> <exn v', st'>

***********************************************************
CONTROL FLOW:  IF, SEQUENCE, WHILE
***********************************************************   

<if e1 then e2 else e3, env, st> ==> <r, st'>
  if <e1, env, st> ==> <v1, st1>
  and v1 is truthy
  and <e2, env, st1> ==> <r, st'>
  
<if e1 then e2 else e3, env, st> ==> <r, st'>
  if <e1, env, st> ==> <v1, st1>
  and v1 is falsy
  and <e3, env, st1> ==> <r, st'>
  
<if e1 then e2 else e3, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>
  
<if e1 then e2, env, st> ==> <r, st'>
  if <if e1 then e2 else undefined, env, st> ==> <r, st'>
  
<e1; ...; en, env, st> ==> <r, st'>
  if <e1, env, st> ==> <v1, st1>
  and <...; en, env, st1> ==> <r, st'>
  where ...; en is just en if there are no expressions in the ...

<e1; ...; en, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>
  
<while e1 do e2 done, env, st> ==> <r, st'>
  if <if e1 then (e2; while e1 do e2 done), env, st> ==> <r, st'>

***********************************************************
OPERATORS
*********************************************************** 

<uop e, env, st> ==> <r, st'>
  if <e, env, st> ==> <v, st'>
  and primop(uop, v) = r

<uop e, env, st> ==> <exn v, st'>
  if <e, env, st> ==> <exn v, st'>

<e1 bop e2, env, st> ==> <r, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and primop(bop, v1, v2) = r
  
<e1 bop e2, env, st> ==> <exn v, st1>
  if <e1, env, st> ==> <exn v, st1>

<e1 bop e2, env, st> ==> <exn v, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <exn v, st2>
  
<e1 && e2, env, st> ==> <r2, st2>
  if <e1, env, st> ==> <v1, st1>
  and v1 is truthy
  and <e2, env, st1> ==> <r2, st2>
  
<e1 && e2, env, st> ==> <v1, st1>
  if <e1, env, st> ==> <v1, st1>
  and v1 is falsy

<e1 && e2, env, st> ==> <exn v, st1>
  if <e1, env, st> ==> <exn v, st1>
  
<e1 || e2, env, st> ==> <r2, st2>
  if <e1, env, st> ==> <v1, st1>
  and v1 is falsy
  and <e2, env, st1> ==> <r2, st2>
  
<e1 || e2, env, st> ==> <v1, st1>
  if <e1, env, st> ==> <v1, st1>
  and v1 is truthy

<e1 || e2, env, st> ==> <exn v, st1>
  if <e1, env, st> ==> <exn v, st1>

***********************************************************
REFERENCES
***********************************************************

<ref e, env, st> ==> <loc, st'>
  if <e, env, st> ==> <v1, st1>
  and loc is a new location not bound in st1
  and st' = st1[loc -> v1]
  
<ref e, env, st> ==> <exn v, st'>
  if <e, env, st> ==> <exn v, st'>
  
<!e, env, st> ==> <v, st'> 
  if <e, env, st> ==> <v', st'>
  and v' is a location bound in st'
  and st' binds v' to v
  
<!e, env, st> ==> <undefined, st'> 
  if <e, env, st> ==> <v, st'>
  and v is not a location

<!e, env, st> ==> <exn v, st'> 
  if <e, env, st> ==> <exn v, st'>
  
<e1 := e2, env, st> ==> <v2, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and v1 is a location bound in st2
  and st' = st2[v1 -> v2]
  
<e1 := e2, env, st> ==> <exn "Assignment to non-location", st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and v1 is not a location
  
<e1 := e2, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <exn v, st'>

<e1 := e2, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>

***********************************************************
EXCEPTIONS
*********************************************************** 

<throw e, env, st> ==> <exn v, st'>
  if <e, env, st> ==> <v, st'>
  
<throw e, env, st> ==> <exn v', st'>
  if <e, env, st> ==> <exn v', st'>
  
<try e1 catch x handle e2, env, st> ==> <v1, st1>
  if <e1, env, st> ==> <v1, st1>
  
<try e1 catch x handle e2, env, st> ==> <r, st2>
  if <e1, env, st> ==> <exn v, st1>
  and <e2, env[x -> v], st1> ==> <r, st2>
  
<try e1 catch x handle e2 finally e3, env, st> ==> <r, st3>
  if <try e1 catch x handle e2, env, st> ==> <r, st'>
  and <e3, env, st'> ==> <v3, st3>

<try e1 catch x handle e2 finally e3, env, st> ==> <exn v, st3>
  if <try e1 catch x handle e2, env, st> ==> <r, st'>
  and <e3, env, st'> ==> <exn v, st3>  

***********************************************************
OBJECTS
***********************************************************

<{s1:e1, ..., sn:en}, env, st0> ==> <{s1:v1, ..., sn:vn}, stn>
  if <e1, env, st0> ==> <v1, st1>
  and ...
  and <en, env, st(n-1) ==> <vn, stn>
  
<{s1:e1, ..., sn:en}, env, st0> ==> <exn v, st'>
  if there exists a j in 1..n such that
     for all i in 1..j-1, <ei, env, st(i-1)> ==> <vi, sti>
     and <ej, env, st(j-1)> ==> <exn v, st'>
       
<e1[e2], env, st> ==> <v, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and s = to_string (to_prim v2)
  and v1 = {..., s:v, ...}

<e1[e2], env, st> ==> <undefined, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and s = to_string (to_prim v2)
  and v1 is not an object, or is an object without a field named s
  
<e1[e2], env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <exn v, st'>

<e1[e2], env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>
  
<e1[e2] <- e3, env, st> ==> <v', st3>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and <e3, env, st2> ==> <v3, st3>
  and s = to_string (to_prim v2)
  and v1 = {s:v, other fields and values}
  and v' = {s:v3, other fields and values}
  
<e1[e2] <- e3, env, st> ==> <v', st3>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and <e3, env, st2> ==> <v3, st3>
  and s = to_string (to_prim v2)
  and v1 = {fields and values} but none of the fields is named s
  and v' = {s:v3, fields and values}
  
<e1[e2] <- e3, env, st> ==> <v3, st3>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and <e3, env, st2> ==> <v3, st3>
  and v1 is not an object
  
<e1[e2] <- e3, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and <e3, env, st2> ==> <exn v, st'>
  
<e1[e2] <- e3, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <exn v, st'>
  
<e1[e2] <- e3, env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>
  
<delete e1[e2], env, st> ==> <v', st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and s = to_string (to_prim v2)
  and v1 = {s:v, other fields and values}
  and v' = {other fields and values}
  
<delete e1[e2], env, st> ==> <v1, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and s = to_string (to_prim v2)
  and v1 = {fields and values} but none of the fields is named s

<delete e1[e2], env, st> ==> <v1, st2>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <v2, st2>
  and v1 is not an object
  
<delete e1[e2], env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <v1, st1>
  and <e2, env, st1> ==> <exn v, st'>
  
<delete e1[e2], env, st> ==> <exn v, st'>
  if <e1, env, st> ==> <exn v, st'>
  
***********************************************************
PRIMITIVE OPERATIONS
*********************************************************** 

to_prim(v) =
  v if v is undefined, int, bool, or string
  undefined if v is location, closure, extern, or object

to_bool(v) =
  false if v is undefined, false, 0, ""
  true otherwise
  
to_int(v) =
  undefined if v is undefined, location, closure, extern, or object
  i if v is the integer i
  1 if v is true
  0 if v is false
  i if v is a string s and i = int_of_string s  (that is OCaml's int_of_string)
  undefined if v is a string s and int_of_string s raises Failure

to_string(v) =
  s if v is the string s
  s if v is the integer i and s = string_of_int i  (that is OCaml's string_of_int)
  "true" if v is true
  "false" if v is false
  "undefined" if v is undefined, location, closure, extern, or object

primop(not, v) = 
  not (to_bool v) 
    where not is OCaml's unary Boolean negation function

primop(-, v) = 
  ~- i if i = to_int v 
       and i is not undefined,
       where ~- is OCaml's unary integer negation operator
  undefined if to_int v is undefined

primop(typeof, v) =
  "undefined" if v is undefined
  "bool" if v is a bool
  "int" if v is an int
  "string" if v is a string
  "object" if v is an object
  "location" if v is a location
  "closure" if v is a closure or an extern

primop(+, v1, v2) =
  s1 ^ s2 if p1 = to_prim v1 and p2 = to_prim v2
          and at least one of p1 and p2 is a string, 
          and s1 = to_string p1 and s2 = to_string p2,
          where ^ is OCaml's string append
  i1 + i2 if p1 = to_prim v1 and p2 = to_prim v2
          and neither p1 nor p2 is a string,
          and i1 = to_int p1 and i2 = to_int p2,
          and neither i1 nor i2 is undefined,
          where + is OCaml's integer +
  undefined if p1 = to_prim v1 and p2 = to_prim v2
            and neither p1 nor p2 is a string,
            and at least one of to_int p1 and to_int p2 is undefined

primop(-, v1, v2) =
  i1 - i2 if i1 = to_int v1 and i2 = to_int v2,
          and neither i1 nor i2 is undefined,
          where - is OCaml's integer -
  undefined if at least one of to_int v1 and to_int v2 is undefined

primop(*, v1, v2) =
  i1 * i2 if i1 = to_int v1 and i2 = to_int v2,
          and neither i1 nor i2 is undefined,
          where * is OCaml's integer *
  undefined if at least one of to_int v1 and to_int v2 is undefined

primop(/, v1, v2) = 
  i1 / i2 if i1 = to_int v1 and i2 = to_int v2,
          and neither i1 nor i2 is undefined,
          and i2 is not 0,
          where / is OCaml's integer /
  undefined if at least one of to_int v1 and to_int v2 is undefined
  exn "Division by zero" if to_int v1 is not undefined 
                         and to_vint v2 is zero

primop(mod, v1, v2) =
  i1 mod i2 if i1 = to_int v1 and i2 = to_int v2,
            and neither i1 nor i2 is undefined,
            and i2 is not 0,
            where mod is OCaml's integer mod
  undefined if at least one of to_int v1 and to_int v2 is undefined
  exn "Division by zero" if to_int v1 is not undefined 
                         and to_vint v2 is zero

primop(cmp, v1, v2) =     (* where cmp is one of <=, <, >, or >= *)
  p1 cmp p2 if p1 = to_prim v1 and p2 = to_prim v2
            and p1 and p2 are both strings,
            where cmp is OCaml's <=, <, >, or >=
  i1 cmp i2 if p1 = to_prim v1 and p2 = to_prim v2
            and at least one of p1 and p2 is not a string
            and i1 = to_int p1 and i2 = to_int p2
            and neither i1 nor i2 is undefined,
            where cmp is OCaml's <=, <, >, or >=
  false     if p1 = to_prim v1 and p2 = to_prim v2
            and at least one of to_int p1 and to_int p2 is undefined

primop(=, v1, v2) =
  true if v1 and v2 are both undefined
  true if v1 and v2 are both ints, or both strings, or both bools,
       and they are the same int, string, or bool according to OCaml's =
  true if v1 and v2 are both locations
       and primop(=, !v1, !v2) is true
  true if v1 and v2 are both objects
       and they have the same set of fields
       and for each field f, primop(=, v1.f, v2.f) is true
  true if exactly one of v1 and v2 is an int i 
       and the other is a value v that is either a string or a bool 
       and primop(=, i, to_int v) is true
  false if none of the cases above applies      
          
primop(==, v1, v2) =
  true if v1 and v2 are both undefined
  true if v1 and v2 are both ints, or both strings, or both bools,
       and they are the same int, string, or bool according to OCaml's =
  true if v1 and v2 are both objects,
       and they have the same set of fields
       and for each field f, primop(==, v1.f, v2.f) is true
  true if v1 and v2 are both locations
       and they are the same location
  false if none of the cases above applies

primop(!=, v1, v2) =
  primop(not, primop(=, v1, v2))

primop(!==, v1, v2) =
  primop(not, primop(==, v1, v2))