Link Search Menu Expand Document
CBS-beta

Languages-beta : OC-L-12-Core-Library.cbs | PRETTY | PDF

Outline 
Language "OCaml Light"

12 Core library 

[
Funcon ocaml-light-core-library
Funcon ocaml-light-match-failure
Funcon ocaml-light-is-structurally-equal
Funcon ocaml-light-to-string
Funcon ocaml-light-define-and-display
Funcon ocaml-light-evaluate-and-display
]
Meta-variables
  R, S, S1, S2, S3, T, U <: values
  S* <: values*
  T+ <: values+

Abbreviations

The following funcons take computations X and return (curried) functions. X refers to a single function argument as arg, or to individual arguments of a curried function of several arguments as arg-1, arg-2, arg-3.

Auxiliary Funcon
  op-1(X:S=>T) : =>functions(S,T)
    ~> function abstraction X
Auxiliary Funcon
  op-2(X:tuples(S1,S2)=>T) : =>functions(S1, functions(S2,T))
    ~> curry function abstraction X
Auxiliary Funcon
  op-3(X:tuples(S1,S2,S3)=>T) : =>functions(S1, functions(S2, functions(S3, T)))
   ~> function abstraction(
        curry partial-apply-first(function abstraction X, given))
Auxiliary Funcon
  partial-apply-first(F:functions(tuples(R,S,T+),U), V:R) :
    =>functions(tuples(S,T+),U)
    ~> function abstraction(apply(F, tuple(V, tuple-elements given)))

partial-apply-first(F, V) provides V as the first argument to a function expecting a tuple of 3 or more arguments, returning a function expecting a tuple of one fewer arguments.

Auxiliary Funcon
  arg : T=>T
    ~> given
Auxiliary Funcon
  arg-1 : tuples(S1,S*)=>S1
    ~> checked index(1, tuple-elements given)
Auxiliary Funcon
  arg-2 : tuples(S1,S2,S*)=>S2
    ~> checked index(2, tuple-elements given)
Auxiliary Funcon
  arg-3 : tuples(S1,S2,S3,S*)=>S3
    ~> checked index(3, tuple-elements given)

Library

The ocaml-light-core-library environment maps most of the names defined in OCaml Module Pervasives (the initially opened module) to funcon terms. See https://caml.inria.fr/pub/docs/manual-ocaml-4.06/core.html for further details and comments.

It also maps some other names defined in the OCaml Standard Libarary to funcon terms (to support tests using them without opening those modules).

Funcon
  ocaml-light-core-library : =>environments 
   ~>
   {// Predefined exceptions
    "Match_failure" |->
      op-1(variant("Match_failure", arg)),
    "Invalid_argument" |->
      op-1(variant("Invalid_argument", arg)),
    "Division_by_zero" |->
      variant("Division_by_zero", tuple( )),

    // Exceptions   
    "raise" |->
      op-1(throw(arg)),

    //Comparisons
    "(=)" |->
      op-2(ocaml-light-is-structurally-equal(arg-1, arg-2)),
    "(<>)" |->
      op-2(not(ocaml-light-is-structurally-equal(arg-1, arg-2))),
    "(<)" |->
      op-2(is-less(arg-1, arg-2)),
    "(>)" |->
      op-2(is-greater(arg-1, arg-2)),
    "(<=)" |->
      op-2(is-less-or-equal(arg-1, arg-2)),
    "(>=)" |->
      op-2(is-greater-or-equal(arg-1, arg-2)),
    "min" |->
      op-2(if-true-else(is-less(arg-1, arg-2), arg-1, arg-2)),
    "max" |->
      op-2(if-true-else(is-greater(arg-1, arg-2), arg-1, arg-2)),
    "(==)" |->
      op-2(if-true-else(
        and(is-in-type(arg-1, ground-values), is-in-type(arg-2, ground-values)),
        is-equal(arg-1, arg-2),
        throw(variant("Invalid_argument", "equal: functional value")))),
    "(!=)" |->
      op-2(if-true-else(
        and(is-in-type(arg-1, ground-values), is-in-type(arg-2, ground-values)),
        not is-equal(arg-1, arg-2),
        throw(variant("Invalid_argument", "equal: functional value")))),
 
    // Boolean operations (excluding lazy conditionals)
    "not" |->
      op-1(not(arg)),

    // Integer arithmetic
    "(~-)" |->
      op-1(implemented-integer integer-negate(arg)),
    "(~+)" |->
      op-1(implemented-integer arg),
    "succ" |->
      op-1(implemented-integer integer-add(arg, 1)),
    "pred" |->
      op-1(implemented-integer integer-subtract(arg, 1)),
    "(+)" |->
      op-2(implemented-integer integer-add(arg-1, arg-2)),
    "(-)" |->
      op-2(implemented-integer integer-subtract(arg-1, arg-2)),
    "(*)" |->
      op-2(implemented-integer integer-multiply(arg-1, arg-2)),
    "(/)" |->
      op-2(implemented-integer if-true-else(is-equal(arg-2, 0),
                    throw(variant("Division_by_zero", tuple( ))),
                    checked integer-divide(arg-1, arg-2))),
    "(mod)" |->
      op-2(implemented-integer checked integer-modulo(arg-1, arg-2)),
    "abs" |->
      op-1(implemented-integer integer-absolute-value(arg)),
    "max_int" |->
      op-1(signed-bit-vector-maximum(implemented-integers-width)),
    "min_int" |->
      op-1(signed-bit-vector-minimum(implemented-integers-width)),

    // Bitwise operations
    "(land)" |->
      op-2(bit-vector-to-integer
        bit-vector-and(implemented-bit-vector arg-1, 
          implemented-bit-vector arg-2)),
    "(lor)" |->
      op-2(bit-vector-to-integer
        bit-vector-or(implemented-bit-vector arg-1, 
          implemented-bit-vector arg-2)),
    "(lxor)" |->
      op-2(bit-vector-to-integer
        bit-vector-xor(implemented-bit-vector arg-1, 
          implemented-bit-vector arg-2)),
    "lnot" |->
      op-1(bit-vector-to-integer
        bit-vector-not(implemented-bit-vector arg)),
    "(lsl)" |->
      op-2(bit-vector-to-integer
        bit-vector-shift-left(implemented-bit-vector arg-1, arg-2)),
    "(lsr)" |->
      op-2(bit-vector-to-integer
        bit-vector-logical-shift-right(implemented-bit-vector arg-1, arg-2)),
    "(asr)" |->
      op-2(bit-vector-to-integer
        bit-vector-arithmetic-shift-right(implemented-bit-vector arg-1, arg-2)),

    // Floating-point arithmetic
    "(~-.)" |->
      op-1(float-negate(implemented-floats-format, arg)),
    "(~+.)" |->
      op-1(arg),
    "(+.)" |->
      op-2(float-add(implemented-floats-format, arg-1, arg-2)),
    "(-.)" |->
      op-2(float-subtract(implemented-floats-format, arg-1, arg-2)),
    "(*.)" |->
      op-2(float-multiply(implemented-floats-format, arg-1, arg-2)),
    "(/.)" |->
      op-2(float-divide(implemented-floats-format, arg-1, arg-2)),
    "(**)" |->
      op-2(float-float-power(implemented-floats-format, arg-1, arg-2)),
    "sqrt" |->
      op-1(float-sqrt(implemented-floats-format, arg)),
    "exp" |->
      op-1(float-exp(implemented-floats-format, arg)),
    "log" |->
      op-1(float-log(implemented-floats-format, arg)),
    "log10" |->
      op-1(float-log10(implemented-floats-format, arg)),
    "cos" |->
      op-1(float-cos(implemented-floats-format, arg)),
    "sin" |->
      op-1(float-sin(implemented-floats-format, arg)),
    "tan" |->
      op-1(float-tan(implemented-floats-format, arg)),
    "acos" |->
      op-1(float-acos(implemented-floats-format, arg)),
    "asin" |->
      op-1(float-asin(implemented-floats-format, arg)),
    "atan" |->
      op-1(float-atan(implemented-floats-format, arg)),
    "atan2" |->
      op-2(float-atan2(implemented-floats-format, arg-1, arg-2)),
    "cosh" |->
      op-1(float-cosh(implemented-floats-format, arg)),
    "sinh" |->
      op-1(float-sinh(implemented-floats-format, arg)),
    "tanh" |->
      op-1(float-tanh(implemented-floats-format, arg)),
    "ceil" |->
      op-1(implemented-integer float-ceiling(implemented-floats-format, arg)),
    "floor" |->
      op-1(implemented-integer float-floor(implemented-floats-format, arg)),
    "abs_float" |->
      op-1(float-absolute-value(implemented-floats-format, arg)),
    "mod_float" |->
      op-2(float-remainder(implemented-floats-format, arg-1, arg-2)),
    "int_of_float" |->
      op-1(implemented-integer float-truncate(implemented-floats-format, arg)),
    "float_of_int" |->
      op-1(implemented-float-literal(string-append(to-string(arg), ".0"))),

    // String operations
    "(^)" |->
      op-2(string-append(arg-1, arg-2)),

    // String conversion operations
    "string_of_int" |->
      op-1(to-string(arg)),
    "int_of_string" |->
      op-1(implemented-integer implemented-integer-literal(arg)),
    "string_of_float" |->
      op-1(to-string(arg)),
    "float_of_string" |->
      op-1(implemented-float-literal(arg)), 

    // List operations
    "(@)" |->
      op-2(list-append(arg-1, arg-2)),

    // Input/output
    //   Output functions on standard output
    "print_char" |->
      op-1(print(to-string(arg))),
    "print_string" |->
      op-1(print(arg)),
    "print_int" |->
      op-1(print(to-string(arg))),
    "print_float" |->
      op-1(print(to-string(arg))),
    "print_newline" |->
      op-1(print "\n"),
    //   Input functions on standard input
    "read_line" |->
      op-1(read),
    "read_int" |->
      op-1(implemented-integer-literal(read)),
    "read_float" |->
      op-1(implemented-float-literal(read)),

    // References (not represented as mutable records)
    "ref" |->
      op-1(allocate-initialised-variable(implemented-values, arg)),
    "(!)" |->
      op-1(assigned(arg)),
    "(:=)" |->
      op-2(assign(arg-1, arg-2)),

    // Module List
    "length" |->
      op-1(implemented-integer list-length(arg)),
    "cons" |->
      op-2(cons(arg-1, arg-2)),
    "hd" |->
      op-1(else(head(arg), throw(variant("Failure", "hd")))),
    "tl" |->
      op-1(else(tail(arg), throw(variant("Failure", "tl")))),
    "rev" |->
      op-1(list(reverse(list-elements(arg)))),
    
    // Module Array
    "array_length" |->
      op-1(implemented-integer length(vector-elements(arg))),
    "array_make" |->
      op-2(if-true-else(is-greater-or-equal(arg-1, 0),
             vector(interleave-map(
               allocate-initialised-variable(values, arg),
               n-of(arg-1, arg-2))),
             throw(variant("Invalid_argument", "array_make")))),
    "array_append" |->
      op-2(vector(vector-elements(arg-1), vector-elements(arg-2))),
    "array_get" |->
      op-2(else(assigned(checked index(nat-succ arg-2, vector-elements(arg-1))),
                throw(variant("Invalid_argument", "array_get")))),
    "array_set" |->
      op-3(else(assign(checked index(nat-succ arg-2, vector-elements(arg-1)), arg-3),
                throw(variant("Invalid_argument", "array_set"))))
   }

Language-specific funcons

Exception values 

Funcon
  ocaml-light-match-failure : =>variants(tuples(strings, integers, integers))
    ~> variant("Match_failure", tuple("", 0, 0))

ocaml-light-match-failure gives a value to be thrown when a match fails. The variant value should consist of the source program text, line, and column, but these are currently not included in the translation of OCaml Light.

Funcon
  ocaml-light-assert-failure : =>variants(tuples(strings, integers, integers))
    ~> variant("Assert_failure", tuple("", 0, 0))

ocaml-light-assert-failure gives a value to be thrown when an assertion fails. The variant value should consist of the source program text, line, and column, but these are currently not included in the translation of OCaml Light.

Structural equality 

Funcon
  ocaml-light-is-structurally-equal(_:implemented-values, _:implemented-values) : 
                                                                       =>booleans

ocaml-light-is-structurally-equal(V1, V2) is false whenever V1 or V2 contains a function. For vectors, it compares all their respective assigned values. It is equality on primitive values, and defined inductively on composite values.

Unit Type

Rule
  ocaml-light-is-structurally-equal(null-value, null-value) ~> true

Booleans

Rule
  ocaml-light-is-structurally-equal(B1:booleans, B2:booleans) ~> is-equal(B1,B2)

Integers

Rule
  ocaml-light-is-structurally-equal(I1:implemented-integers, I2:implemented-integers) ~>
    is-equal(I1,I2)

Floats

Rule
  ocaml-light-is-structurally-equal(F1:implemented-floats, F2:implemented-floats) ~>
    is-equal(F1,F2)

Characters

Rule
  ocaml-light-is-structurally-equal(C1:implemented-characters, C2:implemented-characters) ~>
    is-equal(C1,C2)

Strings

Rule
  ocaml-light-is-structurally-equal(S1:implemented-strings, S2:implemented-strings) ~>
    is-equal(S1,S2)

Tuples

Rule
  ocaml-light-is-structurally-equal(tuple(), tuple()) ~> true
Rule
  ocaml-light-is-structurally-equal(tuple(), tuple(V+)) ~> false
Rule
  ocaml-light-is-structurally-equal(tuple(V+), tuple()) ~> false
Rule
  ocaml-light-is-structurally-equal(tuple(V, V*), tuple(W, W*)) ~>
    and(ocaml-light-is-structurally-equal(V, W), 
        ocaml-light-is-structurally-equal(tuple(V*), tuple(W*)))

Lists

Rule
  ocaml-light-is-structurally-equal([], []) ~> true
Rule
  ocaml-light-is-structurally-equal([], [V+]) ~> false
Rule
  ocaml-light-is-structurally-equal([V+], []) ~> false
Rule
  ocaml-light-is-structurally-equal([V,V*], [W,W*]) ~>
    and(ocaml-light-is-structurally-equal(V,W),
        ocaml-light-is-structurally-equal([V*], [W*]))

Records

Rule
                       dom(Map1) == dom(Map2)
  ----------------------------------------------------------------------
  ocaml-light-is-structurally-equal(record(Map1:maps(_,_)), record(Map2:maps(_,_)))
    ~> not(is-in-set(false, 
         set(interleave-map(
           ocaml-light-is-structurally-equal(
             checked lookup(Map1, given), 
             checked lookup(Map2, given)),
           set-elements(dom(Map1))))))

References

Rule
  ocaml-light-is-structurally-equal(V1:variables, V2:variables) ~>
    ocaml-light-is-structurally-equal(assigned(V1), assigned(V2))

Vectors

Rule
  ocaml-light-is-structurally-equal(Vec1:vectors(values), Vec2:vectors(values)) ~>
    ocaml-light-is-structurally-equal([vector-elements(Vec1)], [vector-elements(Vec2)])

Variants

Rule
  ocaml-light-is-structurally-equal(variant(Con1,V1), variant(Con2,V2)) ~>
    if-true-else(
      is-equal(Con1, Con2),
      if-true-else(
        or(is-equal(tuple( ), V1), is-equal(tuple( ), V2)),
        and(is-equal(tuple( ), V1), is-equal(tuple( ), V2)),
        ocaml-light-is-structurally-equal(V1, V2)),
      false)

Functions

Rule
  ocaml-light-is-structurally-equal(_:functions(_,_), _:functions(_,_)) ~>
    throw(variant("Invalid_argument", "equal: functional value"))

Console display 

Funcon
  ocaml-light-to-string(_:values) : =>strings

ocaml-light-to-string(V) gives the string represention of OCaml Light values as implemented by the ocaml interpreter.

Rule // Unit
  ocaml-light-to-string(null-value) ~> "()"
Rule // Booleans
  ocaml-light-to-string(B:booleans) ~> to-string(B)
Rule // Integers
  ocaml-light-to-string(I:integers) ~> to-string(I)
Rule // Floats
  ocaml-light-to-string(F:implemented-floats) ~> to-string(F)
Rule // Characters
  ocaml-light-to-string(C:implemented-characters) ~>
    string-append("'", to-string(C), "'")
Rule // Strings
  S =/= []
  ----------------------------------------------------------------
  ocaml-light-to-string(S:implemented-strings) ~> string-append("\"", S, "\"")
Rule // Functions
  ocaml-light-to-string(_:functions(_,_)) ~> "<fun>"
Rule // References
  ocaml-light-to-string(V:variables) ~>
    string-append("ref ", ocaml-light-to-string(assigned(V)))
Rule // Variants
  ocaml-light-to-string(variant(Con,Arg)) ~>
    if-true-else(is-equal(tuple( ),Arg), Con,
      string-append(Con, " ", ocaml-light-to-string(Arg)))
Rule // Tuples
  ocaml-light-to-string(tuple(V:values, V+:values+)) ~>
    string-append(
      "(",
      intersperse(", ", interleave-map(ocaml-light-to-string(given), V, V+)),
      ")")
Rule // Lists
  ocaml-light-to-string([V*:values*]) ~>
    string-append(
      "[",
      intersperse("; ", interleave-map(ocaml-light-to-string(given), V*)),
      "]")
Rule // Vectors
  ocaml-light-to-string(V:implemented-vectors) ~>
    string-append(
      "[|",
      intersperse("; ", interleave-map(
        ocaml-light-to-string(assigned(given)), 
        vector-elements(V))),
      "|]")
Rule // Records
  ocaml-light-to-string(record(M:maps(_,_))) ~>
    string-append(
      "{",
      intersperse("; ", interleave-map(
            string-append(arg-1," = ",ocaml-light-to-string(arg-2)),
            map-elements(M))),
      "}")
Funcon
  ocaml-light-define-and-display(Env:envs) : =>envs
   ~> sequential(
        effect left-to-right-map(
          print(arg-1, " = ", ocaml-light-to-string arg-2, "\n"),
          map-elements Env), 
        Env)
Funcon
  ocaml-light-evaluate-and-display(V:implemented-values) : =>envs
   ~> sequential(
        print("- = ", ocaml-light-to-string V, "\n"), 
        map())
From the PLanCompS Project CBS-beta issues… Suggest an improvement…

← ↑ →