diff --git a/src/annot/annot.ml b/src/annot/annot.ml index 24cdb944f..645ba793b 100644 --- a/src/annot/annot.ml +++ b/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 @[%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 @[%a@]@\n)" string "contract" Contract.pp_contract + contract + | Annot annot -> + pf fmt "(@%a@\n @[%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 diff --git a/src/annot/annot.mli b/src/annot/annot.mli index b55a4a2fd..f6d878cf6 100644 --- a/src/annot/annot.mli +++ b/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 diff --git a/src/annot/contract.ml b/src/annot/contract.ml index 820b6eb5a..5bb2d754c 100644 --- a/src/annot/contract.ml +++ b/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 diff --git a/src/annot/contract.mli b/src/annot/contract.mli index 820b6eb5a..1c8607d88 100644 --- a/src/annot/contract.mli +++ b/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 diff --git a/src/annot/spec.ml b/src/annot/spec.ml new file mode 100644 index 000000000..eefd4ff57 --- /dev/null +++ b/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 "@[%a@ %a@ %a@]" pp_term tm1 pp_binpred b pp_term tm2 + | UnConnect (u, pr1) -> pf fmt "@[%a@ %a@]" pp_unconnect u pp_prop pr1 + | BinConnect (b, pr1, pr2) -> + pf fmt "@[%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 "@[%a@ %a@ %a, %a@]" pp_binder b pp_binder_type bt pp_id id + pp_prop pr1 + | None -> + pf fmt "@[%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|} diff --git a/src/ast/binary.ml b/src/ast/binary.ml index 81871c39c..e7dd01f3f 100644 --- a/src/ast/binary.ml +++ b/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 diff --git a/src/ast/text.ml b/src/ast/text.ml index 891d2251e..bf72f9f9e 100644 --- a/src/ast/text.ml +++ b/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) = diff --git a/src/dune b/src/dune index 6875570d1..346298546 100644 --- a/src/dune +++ b/src/dune @@ -50,6 +50,7 @@ interpret interpret_intf kind + spec link link_env log diff --git a/src/parser/binary_parser.ml b/src/parser/binary_parser.ml index 396f5c300..95816c742 100644 --- a/src/parser/binary_parser.ml +++ b/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 diff --git a/src/parser/text_lexer.ml b/src/parser/text_lexer.ml index 6dc78d983..095d537cf 100644 --- a/src/parser/text_lexer.ml +++ b/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 *)