mltree.ml 2.17 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
open Expr
open Ident
open Ty
open Ity
open Term

type ty =
  | Tvar    of tvsymbol
  | Tapp    of ident * ty list
  | Ttuple  of ty list

type is_ghost = bool

type var = ident * ty * is_ghost

type for_direction = To | DownTo

type pat =
  | Pwild
  | Pident  of ident
  | Papp    of lsymbol * pat list
  | Ptuple  of pat list
  | Por     of pat * pat
  | Pas     of pat * ident

type is_rec = bool

type binop = Band | Bor | Beq

type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)

type expr = {
  e_node   : expr_node;
  e_ity    : ity;
  e_effect : effect;
}

and expr_node =
39
  | Econst  of Number.integer_constant
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
  | Evar    of pvsymbol
  | Eapp    of rsymbol * expr list
  | Efun    of var list * expr
  | Elet    of let_def * expr
  | Eif     of expr * expr * expr
  | Eassign of (pvsymbol * rsymbol * pvsymbol) list
  | Ematch  of expr * (pat * expr) list
  | Eblock  of expr list
  | Ewhile  of expr * expr
  (* For loop for Why3's type int *)
  | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
  | Eraise  of xsymbol * expr option
  | Eexn    of xsymbol * ty option * expr
  | Etry    of expr * (xsymbol * pvsymbol list * expr) list
  | Eignore of expr
  | Eabsurd
  | Ehole

and let_def =
  | Lvar of pvsymbol * expr
  | Lsym of rsymbol * ty * var list * expr
  | Lrec of rdef list

and rdef = {
  rec_sym  : rsymbol; (* exported *)
  rec_rsym : rsymbol; (* internal *)
  rec_args : var list;
  rec_exp  : expr;
  rec_res  : ty;
  rec_svar : Stv.t; (* set of type variables *)
}

type is_mutable = bool

type typedef =
  | Ddata     of (ident * ty list) list
  | Drecord   of (is_mutable * ident * ty) list
  | Dalias    of ty

type its_defn = {
  its_name    : ident;
  its_args    : tvsymbol list;
  its_private : bool;
  its_def     : typedef option;
}

type decl =
  | Dtype   of its_defn list
  | Dlet    of let_def
  | Dexn    of xsymbol * ty option
  | Dclone  of ident * decl list
(*
    | Dfunctor of ident * (ident * decl list) list * decl list
*)

type known_map = decl Mid.t

type from_module = {
  from_mod: Pmodule.pmodule option;
  from_km : Pdecl.known_map;
}

type pmodule = {
  mod_from  : from_module;
  mod_decl  : decl list;
  mod_known : known_map;
}