ast.lem

(*
  Definition of CakeML abstract syntax (AST).
*)

open import Pervasives_extra
open import Pervasives
open import Lib
open import Namespace
open import FpValTree
open import FpSem
open import RealOps

(* Literal constants *)
type lit =
  | IntLit of integer
  | Char of char
  | StrLit of string
  | Word8 of word8
  | Word64 of word64

(* Built-in binary operations *)
type opn = Plus | Minus | Times | Divide | Modulo
type opb = Lt | Gt | Leq | Geq
type opw = Andw | Orw | Xor | Add | Sub
type shift = Lsl | Lsr | Asr | Ror

(* Module names *)
type modN = string

(* Variable names *)
type varN = string

(* Constructor names (from datatype definitions) *)
type conN = string

(* Type names *)
type typeN = string

(* Type variable names *)
type tvarN = string

type word_size = W8 | W64

type op =
  (* Operations on integers *)
  | Opn of opn
  | Opb of opb
  (* Operations on words *)
  | Opw of word_size * opw
  | Shift of word_size * shift * nat
  | Equality
  (* FP operations *)
  | FP_cmp of fp_cmp
  | FP_uop of fp_uop
  | FP_bop of fp_bop
  | FP_top of fp_top
  (* Floating-point <-> word translations *)
  | FpFromWord
  | FpToWord
  (* Real ops for verification *)
  | Real_cmp of real_cmp
  | Real_uop of real_uop
  | Real_bop of real_bop
  (* Translation from floating-points to reals for verification *)
  | RealFromFP
  (* Function application *)
  | Opapp
  (* Reference operations *)
  | Opassign
  | Opref
  | Opderef
  (* Word8Array operations *)
  | Aw8alloc
  | Aw8sub
  | Aw8length
  | Aw8update
  (* Word/integer conversions *)
  | WordFromInt of word_size
  | WordToInt of word_size
  (* string/bytearray conversions *)
  | CopyStrStr
  | CopyStrAw8
  | CopyAw8Str
  | CopyAw8Aw8
  (* Char operations *)
  | Ord
  | Chr
  | Chopb of opb
  (* String operations *)
  | Implode
  | Explode
  | Strsub
  | Strlen
  | Strcat
  (* Vector operations *)
  | VfromList
  | Vsub
  | Vlength
  (* Array operations *)
  | Aalloc
  | AallocEmpty
  | Asub
  | Alength
  | Aupdate
  (* Unsafe array accesses *)
  | Asub_unsafe
  | Aupdate_unsafe
  | Aw8sub_unsafe
  | Aw8update_unsafe
  (* List operations *)
  | ListAppend
  (* Configure the GC *)
  | ConfigGC
  (* Call a given foreign function *)
  | FFI of string
  (* Evaluate new code in a given env *)
  | Eval
  (* Get the identifier of an env object *)
  | Env_id

(* Define operator classes, that allow to group their behavior later *)
type op_class =
  | EvalOp (* Eval primitive *)
  | FunApp (* function application *)
  | Simple (* arithmetic operation, no finite-precision/reals *)
  | Icing (* 64-bit floating-points *)
  | Reals (* real numbers *)

val getOpClass : op -> op_class
let getOpClass op =
  match op with
  | FP_cmp _ -> Icing
  | FP_top _ -> Icing
  | FP_bop _ -> Icing
  | FP_uop _ -> Icing
  | Real_cmp _ -> Reals
  | Real_bop _ -> Reals
  | Real_uop _ -> Reals
  | RealFromFP -> Reals
  | Opapp -> FunApp
  | Eval -> EvalOp
  | _ -> Simple
end

val isFpBool: op -> bool
let isFpBool op =
  match op with
  | FP_cmp _ -> true
  | _ -> false
  end

(* Logical operations *)
type lop =
  | And
  | Or

(* Types *)
type ast_t =
  (* Type variables that the user writes down ('a, 'b, etc.) *)
  | Atvar of tvarN
  (* Function type *)
  | Atfun of ast_t * ast_t
  (* Tuple type *)
  | Attup of list ast_t
  (* Type constructor applications.
    0-ary type applications represent unparameterised types (e.g., num or string) *)
  | Atapp of list ast_t * id modN typeN

(* Patterns *)
type pat =
  | Pany
  | Pvar of varN
  | Plit of lit
  (* Constructor applications.
     A Nothing constructor indicates a tuple pattern. *)
  | Pcon of maybe (id modN conN) * list pat
  | Pref of pat
  (* Pattern alias. *)
  | Pas of pat * varN
  | Ptannot of pat * ast_t

(* Expressions *)
type exp =
  | Raise of exp
  | Handle of exp * list (pat * exp)
  | Lit of lit
  (* Constructor application.
     A Nothing constructor indicates a tuple pattern. *)
  | Con of maybe (id modN conN) * list exp
  | Var of id modN varN
  | Fun of varN * exp
  (* Application of a primitive operator to arguments.
     Includes function application. *)
  | App of op * list exp
  (* Logical operations (and, or) *)
  | Log of lop * exp * exp
  | If of exp * exp * exp
  (* Pattern matching *)
  | Mat of exp * list (pat * exp)
  (* A let expression
     A Nothing value for the binding indicates that this is a
     sequencing expression, that is: (e1; e2). *)
  | Let of maybe varN * exp * exp
  (* Local definition of (potentially) mutually recursive
     functions.
     The first varN is the function's name, and the second varN
     is its parameter. *)
  | Letrec of list (varN * varN * exp) * exp
  | Tannot of exp * ast_t
  (* Location annotated expressions, not expected in source programs *)
  | Lannot of exp * locs
  (* Floating-point optimisations *)
  | FpOptimise of fp_opt * exp

type type_def = list (list tvarN * typeN * list (conN * list ast_t))

(* Declarations *)
type dec =
  (* Top-level bindings
   * The pattern allows several names to be bound at once *)
  | Dlet of locs * pat * exp
  (* Mutually recursive function definition *)
  | Dletrec of locs * list (varN * varN * exp)
  (* Type definition
     Defines several data types, each of which has several
     named variants, which can in turn have several arguments.
   *)
  | Dtype of locs * type_def
  (* Type abbreviations *)
  | Dtabbrev of locs * list tvarN * typeN * ast_t
  (* New exceptions *)
  | Dexn of locs * conN * list ast_t
  (* Module *)
  | Dmod of modN * list dec
  (* Local: local part, visible part *)
  | Dlocal of list dec * list dec
  (* Store current lexical env in an env value *)
  | Denv of tvarN

(*
(* Specifications
   For giving the signature of a module *)
type spec =
  | Sval of varN * ast_t
  | Stype of type_def
  | Stabbrev of list tvarN * typeN * ast_t
  | Stype_opq of list tvarN * typeN
  | Sexn of conN * list ast_t

type specs = list spec

*)

(* Accumulates the bindings of a pattern *)
val pat_bindings : pat -> list varN -> list varN
let rec
pat_bindings Pany already_bound =
  already_bound
and
pat_bindings (Pvar n) already_bound =
  n::already_bound
and
pat_bindings (Plit l) already_bound =
  already_bound
and
pat_bindings (Pcon _ ps) already_bound =
  pats_bindings ps already_bound
and
pat_bindings (Pref p) already_bound =
  pat_bindings p already_bound
and
pat_bindings (Pas p i) already_bound =
  pat_bindings p (i::already_bound)
and
pat_bindings (Ptannot p _) already_bound =
  pat_bindings p already_bound
and
pats_bindings [] already_bound =
  already_bound
and
pats_bindings (p::ps) already_bound =
  pats_bindings ps (pat_bindings p already_bound)