*********************************************************** JOCALF SEMANTICS *********************************************************** *********************************************************** EVALUATION RELATIONS *********************************************************** Expressions: ==> Definitions: ==> Phrases: ==> *********************************************************** PHRASES *********************************************************** ==> if p is an expression e and ==> ==> if p is a definition d and ==> *********************************************************** DEFINITIONS *********************************************************** ==> v], st'> if ==> ==> if ==> let rec f (x1 ... xn) = e, env, st> ==> v], st> if v = (| fun (x1 ... xn) -> e, env[f -> v] |) *********************************************************** CONSTANTS *********************************************************** ==> ==> ==> ==> *********************************************************** VARIABLES and LET *********************************************************** ==> if env(x) = v ==> if x is not bound in env ==> if ==> and v1], st1> ==> ==> if ==> and v1], st1> ==> ==> if ==> ==> if v1 = (| fun (x1 ... xn) -> e1, env[f -> v1] |) and v1], st> ==> *********************************************************** FUNCTIONS and APPLICATION *********************************************************** e, env, st> ==> <(|fun (x1 ... xn) -> e, env|), st> ==> if ==> <(|fun (x1 ... xn) -> e, env_cl|), st0> and ==> and ... and ==> and v1, ..., xn->vn], stn> ==> ==> if ==> and ==> and ... and ==> and evaluating OCaml function extern in state stn on inputs v1 ... vn results in output value v ==> if ==> and v is neither a closure nor an external function ==> if ==> <(|fun (x1 ... xm) -> e, env_cl|), st'> and m <> n ==> if ==> and extern is an external function that does not take exactly n arguments ==> if ==> ==> if ==> 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, ==> and ==> *********************************************************** CONTROL FLOW: IF, SEQUENCE, WHILE *********************************************************** ==> if ==> and v1 is truthy and ==> ==> if ==> and v1 is falsy and ==> ==> if ==> ==> if ==> ==> if ==> and <...; en, env, st1> ==> where ...; en is just en if there are no expressions in the ... ==> if ==> ==> if ==> *********************************************************** OPERATORS *********************************************************** ==> if ==> and primop(uop, v) = r ==> if ==> ==> if ==> and ==> and primop(bop, v1, v2) = r ==> if ==> ==> if ==> and ==> ==> if ==> and v1 is truthy and ==> ==> if ==> and v1 is falsy ==> if ==> ==> if ==> and v1 is falsy and ==> ==> if ==> and v1 is truthy ==> if ==> *********************************************************** REFERENCES *********************************************************** ==> if ==> and loc is a new location not bound in st1 and st' = st1[loc -> v1] ==> if ==> ==> if ==> and v' is a location bound in st' and st' binds v' to v ==> if ==> and v is not a location ==> if ==> ==> if ==> and ==> and v1 is a location bound in st2 and st' = st2[v1 -> v2] ==> if ==> and ==> and v1 is not a location ==> if ==> and ==> ==> if ==> *********************************************************** EXCEPTIONS *********************************************************** ==> if ==> ==> if ==> ==> if ==> ==> if ==> and v], st1> ==> ==> if ==> and ==> ==> if ==> and ==> *********************************************************** OBJECTS *********************************************************** <{s1:e1, ..., sn:en}, env, st0> ==> <{s1:v1, ..., sn:vn}, stn> if ==> and ... and <{s1:e1, ..., sn:en}, env, st0> ==> if there exists a j in 1..n such that for all i in 1..j-1, ==> and ==> ==> if ==> and ==> and s = to_string (to_prim v2) and v1 = {..., s:v, ...} ==> if ==> and ==> and s = to_string (to_prim v2) and v1 is not an object, or is an object without a field named s ==> if ==> and ==> ==> if ==> ==> if ==> and ==> and ==> and s = to_string (to_prim v2) and v1 = {s:v, other fields and values} and v' = {s:v3, other fields and values} ==> if ==> and ==> and ==> 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} ==> if ==> and ==> and ==> and v1 is not an object ==> if ==> and ==> and ==> ==> if ==> and ==> ==> if ==> ==> if ==> and ==> and s = to_string (to_prim v2) and v1 = {s:v, other fields and values} and v' = {other fields and values} ==> if ==> and ==> and s = to_string (to_prim v2) and v1 = {fields and values} but none of the fields is named s ==> if ==> and ==> and v1 is not an object ==> if ==> and ==> ==> if ==> *********************************************************** 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))