summaryrefslogblamecommitdiff
path: root/frontend/ast.ml
blob: b2451191d6896d26013c44028656440924318539 (plain) (tree)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16















                                                         
                            



                

                
                          





               

                         

            
                           




            

                             


             
           

















                                                                

          
                                                  




                                                  


                  


                        


                        




                     

               
                                     


                                      
open Lexing

type position = Lexing.position
let position_unknown = Lexing.dummy_pos

type extent = position * position
let extent_unknown = (position_unknown, position_unknown)

type 'a ext = 'a * extent

type id = string

type typ =
    | AST_TINT
    | AST_TBOOL
    | AST_TREAL
    | AST_TGROUP of typ list

type unary_op =
    | AST_UPLUS
    | AST_UMINUS

type binary_op =
    (* num * num -> num *)
    | AST_PLUS
    | AST_MINUS
    | AST_MUL
    | AST_DIV
    | AST_MOD

type binary_rel_op =
    (* 'a * 'a -> bool *)
    | AST_EQ
    | AST_NE
    (* num * num -> bool *)
    | AST_LT
    | AST_LE
    | AST_GT
    | AST_GE

type bin_bool_op =
    (* bool * bool -> bool *)
    | AST_AND
    | AST_OR

type expr =
    | AST_identifier  of id ext
    (* on numerical values *)
    | AST_int_const   of string ext
    | AST_real_const  of string ext
    | AST_unary       of unary_op * (expr ext)
    | AST_binary      of binary_op * (expr ext) * (expr ext)
    (* on boolean values *)
    | AST_bool_const  of bool
    | AST_binary_rel  of binary_rel_op * (expr ext) * (expr ext)
    | AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
    | AST_not         of expr ext
    (* temporal primitives *)
    | AST_pre         of expr ext
    | AST_arrow       of (expr ext) * (expr ext)
    (* other *)
    | AST_if          of (expr ext) * (expr ext) * (expr ext)
    | AST_instance    of (id ext) * (expr ext list)
    (* (TODO) and more : when, merge, activate instances, ... *)

type eqn =
    | AST_assign     of (id ext list) * (expr ext)
    | AST_guarantee  of (id ext) * (expr ext)
    | AST_assume     of (id ext) * (expr ext)
    (* (TODO) and more : automaton, activate... *)

type var_def = bool * (id ext) * typ

type node_decl = {
    name : id;
    args : var_def list;
    ret  : var_def list;
    var  : var_def list;
    body : eqn ext list;
}

type const_decl = {
    name  : id;
    typ   : typ;
    value : expr ext;
}

type toplevel =
    | AST_node_decl  of node_decl ext
    | AST_const_decl of const_decl ext

type prog = toplevel list