Theory Ast

chapter ‹Generated by Lem from ‹semantics/ast.lem›.›

theory "Ast" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives"
  "Lib"
  "Namespace"
  "FpSem"

begin 

― ‹‹open import Pervasives››
― ‹‹open import Lib››
― ‹‹open import Namespace››
― ‹‹open import FpSem››

― ‹‹ Literal constants ››
datatype lit =
    IntLit " int "
  | Char " char "
  | StrLit " string "
  | Word8 " 8 word "
  | Word64 " 64 word "

― ‹‹ Built-in binary operations ››
datatype opn = Plus | Minus | Times | Divide | Modulo
datatype opb = Lt | Gt | Leq | Geq
datatype opw = Andw | Orw | Xor | Add | Sub
datatype shift = Lsl | Lsr | Asr | Ror

― ‹‹ Module names ››
type_synonym modN =" string "

― ‹‹ Variable names ››
type_synonym varN =" string "

― ‹‹ Constructor names (from datatype definitions) ››
type_synonym conN =" string "

― ‹‹ Type names ››
type_synonym typeN =" string "

― ‹‹ Type variable names ››
type_synonym tvarN =" string "

datatype word_size = W8 | W64

datatype op0 =
  ― ‹‹ Operations on integers ››
    Opn " opn "
  | Opb " opb "
  ― ‹‹ Operations on words ››
  | Opw " word_size " " opw "
  | Shift " word_size " " shift " " nat "
  | Equality
  ― ‹‹ FP operations ››
  | FP_cmp " fp_cmp_op "
  | FP_uop " fp_uop_op "
  | FP_bop " fp_bop_op "
  ― ‹‹ Function application ››
  | Opapp
  ― ‹‹ Reference operations ››
  | Opassign
  | Opref
  | Opderef
  ― ‹‹ Word8Array operations ››
  | Aw8alloc
  | Aw8sub
  | Aw8length
  | Aw8update
  ― ‹‹ Word/integer conversions ››
  | WordFromInt " word_size "
  | WordToInt " word_size "
  ― ‹‹ string/bytearray conversions ››
  | CopyStrStr
  | CopyStrAw8
  | CopyAw8Str
  | CopyAw8Aw8
  ― ‹‹ Char operations ››
  | Ord
  | Chr
  | Chopb " opb "
  ― ‹‹ String operations ››
  | Implode
  | Strsub
  | Strlen
  | Strcat
  ― ‹‹ Vector operations ››
  | VfromList
  | Vsub
  | Vlength
  ― ‹‹ Array operations ››
  | Aalloc
  | AallocEmpty
  | Asub
  | Alength
  | Aupdate
  ― ‹‹ Configure the GC ››
  | ConfigGC
  ― ‹‹ Call a given foreign function ››
  | FFI " string "

― ‹‹ Logical operations ››
datatype lop =
    And
  | Or

― ‹‹ Type constructors.
 * 0-ary type applications represent unparameterised types (e.g., num or string)
 ››
datatype tctor =
  ― ‹‹ User defined types ››
    TC_name " (modN, typeN) id0 "
  ― ‹‹ Built-in types ››
  | TC_int
  | TC_char
  | TC_string
  | TC_ref
  | TC_word8
  | TC_word64
  | TC_word8array
  | TC_fn
  | TC_tup
  | TC_exn
  | TC_vector
  | TC_array

― ‹‹ Types ››
datatype t =
  ― ‹‹ Type variables that the user writes down ('a, 'b, etc.) ››
    Tvar " tvarN "
  ― ‹‹ deBruijn indexed type variables.
     The type system uses these internally. ››
  | Tvar_db " nat "
  | Tapp " t list " " tctor "

― ‹‹ Some abbreviations ››
definition Tint  :: " t "  where 
     " Tint = ( Tapp [] TC_int )"

definition Tchar  :: " t "  where 
     " Tchar = ( Tapp [] TC_char )"

definition Tstring  :: " t "  where 
     " Tstring = ( Tapp [] TC_string )"

definition Tref  :: " t ⇒ t "  where 
     " Tref t1 = ( Tapp [t1] TC_ref )"

fun  TC_word  :: " word_size ⇒ tctor "  where 
     " TC_word W8 = ( TC_word8 )"
|"     TC_word W64 = ( TC_word64 )"

definition Tword  :: " word_size ⇒ t "  where 
     " Tword wz = ( Tapp [] (TC_word wz))"

definition Tword8  :: " t "  where 
     " Tword8 = ( Tword W8 )"

definition Tword64  :: " t "  where 
     " Tword64 = ( Tword W64 )"

definition Tword8array  :: " t "  where 
     " Tword8array = ( Tapp [] TC_word8array )"

definition Tfn  :: " t ⇒ t ⇒ t "  where 
     " Tfn t1 t2 = ( Tapp [t1,t2] TC_fn )"

definition Texn  :: " t "  where 
     " Texn = ( Tapp [] TC_exn )"


― ‹‹ Patterns ››
datatype pat =
    Pany
  | Pvar " varN "
  | Plit " lit "
  ― ‹‹ Constructor applications.
     A Nothing constructor indicates a tuple pattern. ››
  | Pcon "  ( (modN, conN)id0)option " " pat list "
  | Pref " pat "
  | Ptannot " pat " " t "

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

type_synonym type_def =" ( tvarN list * typeN * (conN * t list) list) list "

― ‹‹ Declarations ››
datatype dec =
  ― ‹‹ Top-level bindings
   * The pattern allows several names to be bound at once ››
    Dlet " locs " " pat " " exp0 "
  ― ‹‹ Mutually recursive function definition ››
  | Dletrec " locs " " (varN * varN * exp0) list "
  ― ‹‹ Type definition
     Defines several data types, each of which has several
     named variants, which can in turn have several arguments.
   ››
  | Dtype " locs " " type_def "
  ― ‹‹ Type abbreviations ››
  | Dtabbrev " locs " " tvarN list " " typeN " " t "
  ― ‹‹ New exceptions ››
  | Dexn " locs " " conN " " t list "

type_synonym decs =" dec list "

― ‹‹ Specifications
   For giving the signature of a module ››
datatype spec =
    Sval " varN " " t "
  | Stype " type_def "
  | Stabbrev " tvarN list " " typeN " " t "
  | Stype_opq " tvarN list " " typeN "
  | Sexn " conN " " t list "

type_synonym specs =" spec list "

datatype top0 =
    Tmod " modN " "  specs option " " decs "
  | Tdec " dec "

type_synonym prog =" top0 list "

― ‹‹ Accumulates the bindings of a pattern ››
― ‹‹val pat_bindings : pat -> list varN -> list varN››
function (sequential,domintros) 
pats_bindings  :: "(pat)list ⇒(string)list ⇒(string)list "  
                   and
pat_bindings  :: " pat ⇒(string)list ⇒(string)list "  where 
     "
pat_bindings Pany already_bound = (
  already_bound )"
|"
pat_bindings (Pvar n) already_bound = (
  n # already_bound )"
|"
pat_bindings (Plit l) already_bound = (
  already_bound )"
|"
pat_bindings (Pcon _ ps) already_bound = (
  pats_bindings ps already_bound )"
|"
pat_bindings (Pref p) already_bound = (
  pat_bindings p already_bound )"
|"
pat_bindings (Ptannot p _) already_bound = (
  pat_bindings p already_bound )"
|"
pats_bindings [] already_bound = (
  already_bound )"
|"
pats_bindings (p # ps) already_bound = (
  pats_bindings ps (pat_bindings p already_bound))" 
by pat_completeness auto

end