add function contracts as one kind of annotation, to be parsed either…

… from s-expressions or directly from code

src/annot/annot.ml

@@ -1,17 +1,26 @@
 open Fmt
+open Types
 
 type t =
   { annotid : string
   ; items : Sexp.t
   }
 
-let pp_annot fmt annot =
-  pf fmt "(@%a@\n  @[<b 2>%a@]@\n)" string annot.annotid Sexp.pp_sexp
-    annot.items
+type 'a annot =
+  | Contract of 'a Contract.t
+  | Annot of t
 
-let annot_recorder : (string, t) Hashtbl.t = Hashtbl.create 17
+let pp_annot fmt = function
+  | Contract contract ->
+    pf fmt "(@%a@\n  @[<v>%a@]@\n)" string "contract" Contract.pp_contract
+      contract
+  | Annot annot ->
+    pf fmt "(@%a@\n  @[<hv>%a@]@\n)" string annot.annotid Sexp.pp_sexp
+      annot.items
 
-let record_annot annot = Hashtbl.add annot_recorder annot.annotid annot
+let annot_recorder : (string, text annot) Hashtbl.t = Hashtbl.create 17
+
+let record_annot annotid annot = Hashtbl.add annot_recorder annotid annot
 
 let get_annots ?name () =
   match name with

src/annot/annot.mli

@@ -1,12 +1,17 @@
 open Fmt
+open Types
 
 type t =
   { annotid : string
   ; items : Sexp.t
   }
 
-val pp_annot : formatter -> t -> unit
+type 'a annot =
+  | Contract of 'a Contract.t
+  | Annot of t
 
-val record_annot : t -> unit
+val pp_annot : formatter -> text annot -> unit
 
-val get_annots : ?name:string -> unit -> t list
+val record_annot : string -> text annot -> unit
+
+val get_annots : ?name:string -> unit -> text annot list

src/annot/contract.ml

@@ -1,34 +1,16 @@
+open Fmt
 open Types
-
-type nonrec binpred =
-  | Ge
-  | Gt
-  | Le
-  | Lt
-  | Eq
-  | Neq
-
-type nonrec unconnect = Neg
-
-type nonrec binconnect =
-  | And
-  | Or
-  | Imply
-  | Equiv
-
-type 'a prop =
-  | Const of bool
-  | BinPred of binpred * 'a term * 'a term
-  | UnConnect of unconnect * 'a prop
-  | BinConnect of binconnect * 'a prop * 'a prop
-
-and 'a term =
-  | Int of int
-  | Global of 'a indice
-  | Result
+open Spec
 
 type 'a t =
   { func : 'a indice
   ; preconditions : 'a prop list
   ; postconditions : 'a prop list
   }
+
+let pp_contract fmt { func; preconditions; postconditions } =
+  pf fmt "%a@,%a@,%a@," pp_indice func
+    (list ~sep:pp_newline pp_prop)
+    preconditions
+    (list ~sep:pp_newline pp_prop)
+    postconditions

src/annot/contract.mli

@@ -1,34 +1,11 @@
+open Fmt
 open Types
-
-type nonrec binpred =
-  | Ge
-  | Gt
-  | Le
-  | Lt
-  | Eq
-  | Neq
-
-type nonrec unconnect = Neg
-
-type nonrec binconnect =
-  | And
-  | Or
-  | Imply
-  | Equiv
-
-type 'a prop =
-  | Const of bool
-  | BinPred of binpred * 'a term * 'a term
-  | UnConnect of unconnect * 'a prop
-  | BinConnect of binconnect * 'a prop * 'a prop
-
-and 'a term =
-  | Int of int
-  | Global of 'a indice
-  | Result
+open Spec
 
 type 'a t =
   { func : 'a indice
   ; preconditions : 'a prop list
   ; postconditions : 'a prop list
   }
+
+val pp_contract : formatter -> 'a t -> unit

src/annot/spec.ml

@@ -0,0 +1,98 @@
+open Types
+open Fmt
+
+(*
+  text:
+    (local index)
+    (global index)
+    (binder index)
+    string_id
+
+  binary:
+    (local index)
+    (global index)
+    (binder index)
+*)
+
+type nonrec binpred =
+  | Ge
+  | Gt
+  | Le
+  | Lt
+  | Eq
+  | Neq
+
+type nonrec unconnect = Neg
+
+type nonrec binconnect =
+  | And
+  | Or
+  | Imply
+  | Equiv
+
+type nonrec binder =
+  | Forall
+  | Exists
+
+type nonrec binder_type = num_type
+
+type 'a prop =
+  | Const : bool -> 'a prop
+  | BinPred : binpred * 'a term * 'a term -> 'a prop
+  | UnConnect : unconnect * 'a prop -> 'a prop
+  | BinConnect : binconnect * 'a prop * 'a prop -> 'a prop
+  | Binder : binder * binder_type * string option * 'a prop -> 'a prop
+
+and 'a term =
+  | Int32 : int32 -> 'a term
+  | Var : text indice -> text term
+  | GlobalVar : 'a indice -> 'a term
+  | BinderVar : 'a indice -> 'a term
+  | Result : 'a term
+
+let pp_bool fmt = function true -> pf fmt "true" | false -> pf fmt "false"
+
+let pp_binpred fmt = function
+  | Ge -> pf fmt ">="
+  | Gt -> pf fmt ">"
+  | Le -> pf fmt "<="
+  | Lt -> pf fmt "<"
+  | Eq -> pf fmt "="
+  | Neq -> pf fmt "!="
+
+let pp_unconnect fmt = function Neg -> pf fmt "!"
+
+let pp_binconnect fmt = function
+  | And -> pf fmt "&&"
+  | Or -> pf fmt "||"
+  | Imply -> pf fmt "==>"
+  | Equiv -> pf fmt "<==>"
+
+let pp_binder fmt = function
+  | Forall -> pf fmt {|\forall|}
+  | Exists -> pf fmt {|\exists|}
+
+let pp_binder_type = pp_num_type
+
+let rec pp_prop fmt = function
+  | Const bool -> pf fmt {|"\%a"|} pp_bool bool
+  | BinPred (b, tm1, tm2) ->
+    pf fmt "@[<hv 2>%a@ %a@ %a@]" pp_term tm1 pp_binpred b pp_term tm2
+  | UnConnect (u, pr1) -> pf fmt "@[<hv 2>%a@ %a@]" pp_unconnect u pp_prop pr1
+  | BinConnect (b, pr1, pr2) ->
+    pf fmt "@[<hv 2>%a@ %a@ %a@]" pp_prop pr1 pp_binconnect b pp_prop pr2
+  | Binder (b, bt, id_opt, pr1) -> (
+    match id_opt with
+    | Some id ->
+      pf fmt "@[<hv 2>%a@ %a@ %a, %a@]" pp_binder b pp_binder_type bt pp_id id
+        pp_prop pr1
+    | None ->
+      pf fmt "@[<hv 2>%a@ %a@, %a@]" pp_binder b pp_binder_type bt pp_prop pr1 )
+
+and pp_term (type e) fmt (tm : e term) =
+  match tm with
+  | Int32 i -> pf fmt "%i" (Int32.to_int i)
+  | Var ind -> pf fmt "%a" pp_indice ind
+  | GlobalVar ind -> pf fmt "global.%a" pp_indice ind
+  | BinderVar ind -> pf fmt "binder.%a" pp_indice ind
+  | Result -> pf fmt {|\result|}

src/ast/binary.ml

@@ -49,8 +49,8 @@ type elem =
   }
 
 type custom =
-  | Uninterpreted of (string, Sexp.t) Either.t
-  | Contract of binary Contract.t
+  | Uninterpreted of string
+  | From_annot of binary Annot.annot
 
 type modul =
   { id : string option

src/ast/text.ml

@@ -95,7 +95,7 @@ let pp_module_field fmt = function
 type modul =
   { id : string option
   ; fields : module_field list
-  ; annots : Annot.t list
+  ; annots : text Annot.annot list
   }
 
 let pp_modul fmt (m : modul) =

src/dune

@@ -50,6 +50,7 @@
   interpret
   interpret_intf
   kind
+  spec
   link
   link_env
   log

src/parser/binary_parser.ml

@@ -1211,9 +1211,7 @@ let sections_iterate (input : Input.t) =
 
   (* Custom *)
   let custom =
-    List.filter_map
-      (Option.map (fun x -> Uninterpreted (Either.Left x)))
-      custom_sections
+    List.filter_map (Option.map (fun x -> Uninterpreted x)) custom_sections
   in
 
   { id = None

src/parser/text_lexer.ml

@@ -452,14 +452,14 @@ let rec token buf =
     if String.equal "" annotid then Log.err "empty annotation id"
     else
       let items = Sexp.List (annot buf) in
-      Annot.(record_annot { annotid; items });
+      Annot.(record_annot annotid (Annot { annotid; items }));
       token buf
   | "(@", Plus id_char ->
     let annotid = Utf8.lexeme buf in
     let annotid = String.sub annotid 2 (String.length annotid - 2) in
     let annotid = mk_string buf annotid in
     let items = Sexp.List (annot buf) in
-    Annot.(record_annot { annotid; items });
+    Annot.(record_annot annotid (Annot { annotid; items }));
     token buf
   | "(@" -> Log.err "empty annotation id"
   (* 1 *)