diff --git a/vocal/proofs/why3/Makefile b/vocal/proofs/why3/Makefile index ee804d1..6891def 100644 --- a/vocal/proofs/why3/Makefile +++ b/vocal/proofs/why3/Makefile @@ -3,7 +3,7 @@ SRC=../../src/ WHY3=Vector UnionFind PriorityQueue Arrays ZipperList PairingHeap \ - Mjrty RingBuffer CountingSort #Queue + Mjrty RingBuffer CountingSort Queue WHY3ML=$(addsuffix .ml, $(WHY3)) WHY3IMPL=$(addsuffix _impl, $(WHY3)) @@ -19,8 +19,8 @@ all: $(WHY3GEN) %.prove: why3 prove -L . -L $(SRC) $*.mlw -WHY3EXTRACT=why3 extract -D ocaml64 -D uf.drv\ - --modular --recursive-deps #-D queue.drv +WHY3EXTRACT=why3 extract -D ocaml64 -D uf.drv -D queue.drv\ + --modular --recursive-deps WHY3EXTRACTNR=why3 extract -D ocaml64 -D uf.drv\ --modular diff --git a/vocal/proofs/why3/Queue_impl.mlw b/vocal/proofs/why3/Queue_impl.mlw index 127a984..e93a1e0 100644 --- a/vocal/proofs/why3/Queue_impl.mlw +++ b/vocal/proofs/why3/Queue_impl.mlw @@ -9,9 +9,9 @@ (**************************************************************************) (* Authors: - Mário Pereira (LRI, Univ Paris-Saclay then + Mário Pereira (LRI, Univ Paris-Saclay then NOVA-LINCS, Universidade Nova de Lisboa) - Jean-Christophe Filliâtre (CNRS, LRI, Univ Paris-Saclay) *) + Jean-Christophe Filliâtre (CNRS, LRI, Univ Paris-Saclay) *) (* Mutable queue implementation, following OCaml's queue implementation *) @@ -34,8 +34,8 @@ module Impl mutable ghost view : seq 'a; mutable ghost list : seq (loc 'a); mutable ghost used_mem : mem 'a - } invariant { length > 0 -> first = list[0] /\ last = list[length - 1] /\ - used_mem.next last = Some null } + } invariant { length > 0 -> first = list[0] /\ last = list[length - 1] /\ + used_mem.next last = Some null } invariant { length = 0 -> first = last = null } invariant { length = Seq.length view = Seq.length list } invariant { forall i. 0 <= i < length -> list[i] <> null } @@ -52,6 +52,8 @@ module Impl (* OCaml code starts here *) + exception Empty + lemma mem_tail: forall x: 'a, s: seq 'a. Seq.length s > 0 -> mem x s <-> (x = s[0] \/ mem x s[1 .. ]) @@ -66,7 +68,7 @@ module Impl ensures { result <-> q.view == empty } = q.first == null - let push (x: 'a) (q: t 'a) : unit + let add (x: 'a) (q: t 'a) : unit ensures { q.view == snoc (old q.view) x } = let c = mk_cell q.used_mem x null in if q.last == null then begin @@ -83,13 +85,17 @@ module Impl q.list <- snoc q.list c; end - (*TODO: Subspecification: we must ensure that the returned value is indeed the - first element of the queue *) - let pop (q: t 'a) : 'a - requires { Seq.length q.view > 0 } - ensures { q.view == (old q.view)[1 .. ] } - ensures { old q.view == cons result q.view } - = let x = get_content q.used_mem q.first in + let push = add + + let take_opt (q: t 'a) : option 'a + ensures { old q.view == empty -> result = None } + ensures { not (old q.view == empty) -> result = Some (old q.view)[0] } + ensures { old q.view == empty -> q.view == old q.view } + ensures { not old q.view == empty -> q.view == (old q.view)[1 .. ] } + = + if is_empty q then None + else + let x = get_content q.used_mem q.first in if get_next q.used_mem q.first == null then begin free q.used_mem q.first; q.first <- null; @@ -105,13 +111,63 @@ module Impl q.list <- q.list[1 .. ]; free q.used_mem oldfirst end; - x + Some x + + let take (q: t 'a) : 'a + raises { Empty -> (old q.view) == empty } + ensures { q.view == (old q.view)[1 .. ] } + ensures { result = (old q.view)[0] } + ensures { old q.view == cons result q.view } + = + match take_opt q with + | None -> raise Empty + | Some e -> e + end + + let pop = take + + let peek (q: t 'a) : 'a + raises { Empty -> q.view == empty } + ensures { result = q.view[0] } + = + if is_empty q then raise Empty; + get_content q.used_mem q.first + + let top = peek + + let peek_opt (q: t 'a) : option 'a + ensures { old q.view == empty -> result = None } + ensures { not (old q.view == empty) -> result = Some q.view[0] } + = + if is_empty q then None else Some (get_content q.used_mem q.first) + + let clear (q: t 'a) : unit + ensures { q.view == empty } + = + q.length <- 0; + q.first <- null; + q.last <- null; + q.view <- empty; + q.list <- empty; + q.used_mem <- empty_memory () + + predicate disjoint_queue (q1 q2: t 'a) = + disjoint_mem q1.used_mem q2.used_mem + + (* lemma aux: forall q1 q2: t 'a. *) + (* disjoint_queue q1 q2 -> forall i. 0 <= i < Seq.length q1.list -> *) + (* not (mem q1.list[i] q2.list) *) let transfer (q1 q2: t 'a) : unit requires { disjoint_mem q1.used_mem q2.used_mem } ensures { q2.view == (old q2.view) ++ (old q1.view) } ensures { q1.view == empty } - = if not (is_empty q1) then + = let lemma disjoint_mem_disjoint_list (q1 q2: t 'a) + requires { disjoint_queue q1 q2 } + ensures { forall i. 0 <= i < Seq.length q1.list -> + not (mem q1.list[i] q2.list) } + = () in + if not (is_empty q1) then if is_empty q2 then begin q2.length, q1.length <- q1.length, 0; q2.first, q2.last <- q1.first, q1.last; @@ -121,13 +177,14 @@ module Impl (* clear q1 is inlined, since type invariant for q1 is now broken *) q1.first, q1.last, q1.list, q1.view <- null, null, Seq.empty, Seq.empty; end else begin - let len = q2.length + q1.length in - q2.length, q1.length <- len, 0; + q2.length <- q2.length + q1.length; + q1.length <- 0; set_next q2.used_mem q2.last q1.first; - q2.last, q2.list, q2.view <- - q1.last, q2.list ++ q1.list, q2.view ++ q1.view; - q2.used_mem, q1.used_mem <- - mem_union q2.used_mem q1.used_mem, empty_memory (); + q2.last <- q1.last; + q2.list <- q2.list ++ q1.list; + q2.view <- q2.view ++ q1.view; + q2.used_mem <- mem_union q1.used_mem q2.used_mem; + q1.used_mem <- empty_memory (); (* clear q1 is inlined, since type invariant for q1 is now broken *) q1.first, q1.last, q1.list, q1.view <- null, null, Seq.empty, Seq.empty end @@ -139,7 +196,9 @@ module Correct use Impl clone Queue.Sig with - type t, - val create, val is_empty, val push, val pop, val transfer + type t, predicate disjoint_t = disjoint_queue, + val create, val add, val push, val take, val take_opt, val pop, + val peek, val peek_opt, val top, val is_empty, + val clear, val transfer end diff --git a/vocal/proofs/why3/Queue_impl/why3session.xml b/vocal/proofs/why3/Queue_impl/why3session.xml index 7e12f06..14c26ea 100644 --- a/vocal/proofs/why3/Queue_impl/why3session.xml +++ b/vocal/proofs/why3/Queue_impl/why3session.xml @@ -1,365 +1,332 @@ - - - - - - + + + + + - + - + - + - + - + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - - + + - - + + - - + + - - + + - - - - - - - - - + + - - + + - - + + - - + + - - - - - - - - - - - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + - - - + + + - + - + - + - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - - + + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - + - + + + + - + - + + + + - + + + + + + + - + + + + + + + + + + + + + - + - - - - - - - - - - - - - - - - - + + diff --git a/vocal/proofs/why3/Queue_impl/why3shapes.gz b/vocal/proofs/why3/Queue_impl/why3shapes.gz index 8a70564..2ae9761 100644 Binary files a/vocal/proofs/why3/Queue_impl/why3shapes.gz and b/vocal/proofs/why3/Queue_impl/why3shapes.gz differ diff --git a/vocal/src/Queue.ml b/vocal/src/Queue.ml new file mode 100644 index 0000000..65e07dd --- /dev/null +++ b/vocal/src/Queue.ml @@ -0,0 +1,65 @@ +type 'a t = { + mutable first: 'a SinglyLL.cell; + mutable last: 'a SinglyLL.cell; + } + +exception Empty + +let create : type a. unit -> (a t) = + fun _ -> { first = SinglyLL.Nil ; last = SinglyLL.Nil } + +let is_empty : type a. (a t) -> (bool) = + fun q -> ((q.first) == (SinglyLL.Nil )) + +let add : type a. a -> (a t) -> unit = + fun x q -> let c = (SinglyLL.Cons { content = x; next = (SinglyLL.Nil ) }) in + if ((q.last) == (SinglyLL.Nil )) + then begin q.first <- c; q.last <- c end + else begin (SinglyLL.set_next (q.last) c); q.last <- c end + +let take_opt : type a. (a t) -> (a option) = + fun q -> if is_empty q + then None + else + begin + let x = (SinglyLL.get_content (q.first)) in + if ((SinglyLL.get_next (q.first)) == (SinglyLL.Nil )) + then + begin q.first <- SinglyLL.Nil ; q.last <- SinglyLL.Nil end + else q.first <- (SinglyLL.get_next (q.first)); + Some x end + +let take : type a. (a t) -> a = + fun q -> match take_opt q with + | None -> raise Empty + | Some e -> e + +let peek : type a. (a t) -> a = + fun q -> if is_empty q then raise Empty; (SinglyLL.get_content (q.first)) + +let peek_opt : type a. (a t) -> (a option) = + fun q -> if is_empty q + then None + else Some (SinglyLL.get_content (q.first)) + +let clear : type a. (a t) -> unit = + fun q -> q.first <- SinglyLL.Nil ; q.last <- SinglyLL.Nil + +let transfer : type a. (a t) -> (a t) -> unit = + fun q1 q2 -> if not (is_empty q1) + then begin + if is_empty q2 + then + begin + begin q2.first <- q1.first; q2.last <- q1.last end; + begin q1.first <- SinglyLL.Nil ; + q1.last <- SinglyLL.Nil end + end + else + begin + (SinglyLL.set_next (q2.last) (q1.first)); + q2.last <- q1.last; + begin q1.first <- SinglyLL.Nil ; + q1.last <- SinglyLL.Nil end + end end + diff --git a/vocal/src/Queue.mli b/vocal/src/Queue.mli new file mode 100644 index 0000000..d88c315 --- /dev/null +++ b/vocal/src/Queue.mli @@ -0,0 +1,115 @@ +(**************************************************************************) +(* *) +(* VOCaL -- A Verified OCaml Library *) +(* *) +(* Copyright (c) 2020 The VOCaL Project *) +(* *) +(* This software is free software, distributed under the MIT license *) +(* (as described in file LICENSE enclosed). *) +(**************************************************************************) + +(** First-in first-out queues. + + This module implements queues (FIFOs), with in-place modification, following + OCaml's implementation. + + Missing functions: + - [copy] + - [length] + - [fold] + - [iter] +*) + +(*@ open Seq *) + +type 'a t +(** The type of queues containing elements of type ['a]. *) +(*@ mutable model view: 'a seq *) + + +exception Empty +(** Raised when {!Queue.take} or {!Queue.peek} is applied to an empty queue. *) + + +val create : unit -> 'a t +(** Return a new queue, initially empty. *) +(*@ q = create () + ensures q.view == empty *) + +val add : 'a -> 'a t -> unit +(** [add x q] adds the element [x] at the end of the queue [q]. *) +(*@ add x q + modifies q + ensures q.view == Seq.snoc (old q.view) x *) + +val push : 'a -> 'a t -> unit +(** [push] is a synonym for [add]. *) +(*@ push x q + modifies q + ensures q.view == Seq.snoc (old q.view) x *) + +val take : 'a t -> 'a +(** [take q] removes and returns the first element in queue [q], + or raises {!Empty} if the queue is empty. *) +(*@ r = take q + modifies q + ensures old q.view == Seq.cons r q.view + ensures old q.view == empty -> q.view == empty + raises Empty -> (old q.view) == empty *) + +val take_opt : 'a t -> 'a option +(** [take_opt q] removes and returns the first element in queue [q], + or returns [None] if the queue is empty. 4.08 *) +(*@ r = take_opt q + modifies q + ensures q.view == if old q.view == empty then old q.view + else (old q.view)[1 ..] + ensures r = if old q.view == empty then None + else Some ((old q.view)[0]) *) + +val pop : 'a t -> 'a +(** [pop] is a synonym for [take]. *) +(*@ r = pop q + modifies q + ensures old q.view == Seq.cons r q.view + ensures old q.view == empty -> q.view == empty + raises Empty -> (old q.view) == empty *) + +val peek : 'a t -> 'a +(** [peek q] returns the first element in queue [q], without removing + it from the queue, or raises {!Empty} if the queue is empty. *) +(*@ r = peek q + ensures r = q.view[0] + raises Empty -> q.view == empty *) + +val peek_opt : 'a t -> 'a option +(** [peek_opt q] returns the first element in queue [q], without removing + it from the queue, or returns [None] if the queue is empty. *) +(*@ r = peek_opt q + ensures r = if old q.view == empty then None else Some q.view[0] *) + +val top : 'a t -> 'a +(** [top] is a synonym for [peek]. *) +(*@ r = top q + ensures r = q.view[0] + raises Empty -> q.view == empty *) + +val clear : 'a t -> unit +(** Discard all elements from a queue. *) +(*@ clear q + ensures q.view = empty *) + +val is_empty : 'a t -> bool +(** Return [true] if the given queue is empty, [false] otherwise. *) +(*@ b = is_empty q + ensures b <-> q.view = empty *) + +val transfer : 'a t -> 'a t -> unit +(** [transfer q1 q2] adds all of [q1]'s elements at the end of + the queue [q2], then clears [q1]. It is equivalent to the + sequence [iter (fun x -> add x q2) q1; clear q1], but runs + in constant time. *) +(*@ transfer q1 q2 + modifies q1.view, q2.view + ensures q1.view == empty + ensures q2.view == old q2.view ++ old q1.view *) diff --git a/vocal/src/Queue.mlibak b/vocal/src/Queue.mlibak deleted file mode 100644 index 7827453..0000000 --- a/vocal/src/Queue.mlibak +++ /dev/null @@ -1,45 +0,0 @@ -(**************************************************************************) -(* *) -(* VOCaL -- A Verified OCaml Library *) -(* *) -(* Copyright (c) 2020 The VOCaL Project *) -(* *) -(* This software is free software, distributed under the MIT license *) -(* (as described in file LICENSE enclosed). *) -(**************************************************************************) - -(*@ open Seq *) - -type 'a t -(*@ mutable model view: 'a seq *) - -val create : unit -> 'a t -(** Return a new queue, initially empty. *) -(*@ q = create () - ensures q.view == empty *) - -val push : 'a -> 'a t -> unit -(** [add x q] adds the element [x] at the end of the queue [q]. *) -(*@ push x q - modifies q - ensures q.view == Seq.snoc (old q.view) x *) - -val pop : 'a t -> 'a -(** [pop q] removes and returns the first element in queue [q]. *) -(*@ r = pop q - requires q.view <> empty - modifies q - ensures old q.view == Seq.cons r q.view *) - -val is_empty : 'a t -> bool -(** Return [true] if the given queue is empty, [false] otherwise. *) -(*@ b = is_empty q - ensures b <-> q.view = empty *) - -val transfer : 'a t -> 'a t -> unit -(** [transfer q1 q2] adds all of [q1]'s elements at the end of - the queue [q2], then clears [q1]. *) -(*@ transfer q1 q2 - modifies q1.view, q2.view - ensures q1.view == empty - ensures q2.view == old q2.view ++ old q1.view *) diff --git a/vocal/src/UnionFind.mli b/vocal/src/UnionFind.mli index de35bd1..a0a665f 100644 --- a/vocal/src/UnionFind.mli +++ b/vocal/src/UnionFind.mli @@ -107,7 +107,7 @@ val union : 'a elem -> 'a elem -> unit else old (img uf x) *) -(*@ val join: 'a uf -> 'a uf -> unit *) +(* @ val join: 'a uf -> 'a uf -> unit *) (* @ join uf1 uf2 (*? requires disjoint (dom uf1) (dom uf2) *) modifies uf1 diff --git a/why3gospel/why3gospel_trans.ml b/why3gospel/why3gospel_trans.ml index f35c484..2014731 100644 --- a/why3gospel/why3gospel_trans.ml +++ b/why3gospel/why3gospel_trans.ml @@ -12,6 +12,7 @@ module T = Gospel.Tast module Tm = Gospel.Tmodule module Ot = Gospel.Oparsetree open Why3 +open Wstdlib open Ptree open Why3gospel_driver @@ -56,6 +57,10 @@ module Term = struct let ident_of_lsymbol Tt.{ls_name = name} = mk_id name.I.id_str ~id_loc:(location name.I.id_loc) + let ident_of_qualid = function Qident x | Qdot (_, x) -> x + let cmp_id_qualid q1 q2 = + (ident_of_qualid q1).id_str = (ident_of_qualid q2).id_str + let quant = function | Tt.Tforall -> Dterm.DTforall | Tt.Texists -> Dterm.DTexists @@ -173,7 +178,7 @@ let td_params (tvs, _) = (** Visibility of type declarations. An alias type cannot be private, so we check whether or not the GOSPEL type manifest is [None]. *) let td_vis_from_manifest = function - | None -> Private + | None -> Private | Some _ -> Public (** Convert a GOSPEL type definition into a Why3's Ptree [type_def]. If the @@ -190,7 +195,7 @@ let td_def td_spec td_manifest = | None -> td_def_of_ty_fields td_spec.T.ty_fields | Some ty -> TDalias (Term.ty ty) -let type_decl (T.{td_ts = {ts_ident}; td_spec; td_manifest} as td) = T.{ +let type_decl (T.{td_ts = {ts_ident}; td_spec; td_manifest} as td) = { td_loc = location td.td_loc; td_ident = mk_id ts_ident.id_str ~id_loc:(location td.td_loc); td_params = List.map td_params td.td_params; @@ -212,6 +217,50 @@ let loc_of_vs vs = Term.(location vs.Tt.vs_name.I.id_loc) let ident_of_lb_arg lb = Term.ident_of_vsymbol (T.vs_of_lb_arg lb) let loc_of_lb_arg lb = loc_of_vs (T.vs_of_lb_arg lb) +(** Global environment of represented types to their disjoint predicate. *) +(* TODO: can we have something better than this global hashtbl? I know we could + fill up our functions with an extra argument [env], but I would really like + to avoid the pain of redifining every functions because of the extra arg. *) +let env_represented : logic_decl Hstr.t = Hstr.create 64 + +(** Check if a given type declaration is represented, i.e., if it is ephemeral + or contains at least a mutable model field. *) +let is_represented T.{td_spec} = + td_spec.ty_ephemeral || List.exists (fun (_, mut) -> mut) td_spec.ty_fields + +(** Build a predicate of the form [predicate disjoint_t t t] for a represented + type declaration [t]. *) +let disjoint_represented T.{td_ts = {ts_ident}; td_params} = + let id_pred = mk_id ("disjoint_" ^ ts_ident.id_str) in + let id_pty = mk_id ts_ident.id_str in + let mk_tyvar (v, _) = PTtyvar (Term.ident_of_tvsymbol v) in + let pty = PTtyapp (Qident id_pty, List.map mk_tyvar td_params) in + let param = (dummy_loc, None, false, pty) in + mk_logic_decl dummy_loc id_pred [param; param] None None + +(** [disjoint tdl] returns a list of predicate declarations, each of the form + [predicate disjoint_t t t] for all represented type declarations [t] that + are in the list [tdl]. *) +let disjoint tdl = + let mk_disjoint acc (T.{td_ts} as td) = + if is_represented td then begin let decl = disjoint_represented td in + (* while generating the [disjoint] predicate, also fill [env_type_decl] *) + Hstr.add env_represented td_ts.ts_ident.id_str decl; + decl :: acc end + else acc in + let predl = List.fold_left mk_disjoint [] tdl in + Dlogic (List.rev predl) + +let mk_disjoint_term id_left id_right id_represented = + let decl_disjoint = Hstr.find env_represented id_represented.id_str in + let qualid_app = Qident decl_disjoint.ld_ident in + let tid_left = Tident (Qident id_left) in + let tid_right = Tident (Qident id_right) in + let arg_left = Term.mk_term tid_left id_left.id_loc in + let arg_right = Term.mk_term tid_right id_right.id_loc in + let term_desc = Tidapp (qualid_app, [arg_left; arg_right]) in + Term.mk_term term_desc dummy_loc + (** Given the result type [sp_ret] of a function and a GOSPEL postcondition [post] (represented as a [term]), convert it into a Why3's Ptree postcondition of the form [Loc.position * (pattern * term)]. *) @@ -273,6 +322,38 @@ let spec_with_checks val_spec pre checks = sp_partial = false; } +let empty_spec = { + sp_pre = []; + sp_post = []; + sp_xpost = []; + sp_reads = []; + sp_writes = []; + sp_alias = []; + sp_variant = []; + sp_checkrw = false; + sp_diverge = false; + sp_partial = false; +} + +let variant_union v1 v2 = match v1, v2 with + | _, [] -> v1 + | [], _ -> v2 + | _, ({term_loc = loc},_)::_ -> + Loc.errorm ~loc "multiple `variant' clauses are not allowed" + +let spec_union s1 s2 = { + sp_pre = s1.sp_pre @ s2.sp_pre; + sp_post = s1.sp_post @ s2.sp_post; + sp_xpost = s1.sp_xpost @ s2.sp_xpost; + sp_reads = s1.sp_reads @ s2.sp_reads; + sp_writes = s1.sp_writes @ s2.sp_writes; + sp_alias = s1.sp_alias @ s2.sp_alias; + sp_variant = variant_union s1.sp_variant s2.sp_variant; + sp_checkrw = s1.sp_checkrw || s2.sp_checkrw; + sp_diverge = s1.sp_diverge || s2.sp_diverge; + sp_partial = s1.sp_partial || s2.sp_partial; +} + let spec val_spec = { sp_pre = List.map (fun (t, _) -> term t) val_spec.T.sp_pre; sp_post = sp_post val_spec.sp_ret val_spec.sp_post; @@ -292,19 +373,6 @@ let split_on_checks sp_pre = let pre, checks = List.fold_left mk_split ([], []) sp_pre in List.rev pre, List.rev checks -let empty_spec = { - sp_pre = []; - sp_post = []; - sp_xpost = []; - sp_reads = []; - sp_writes = []; - sp_alias = []; - sp_variant = []; - sp_checkrw = false; - sp_diverge = false; - sp_partial = false; -} - let rec core_type Ot.{ ptyp_desc; ptyp_loc } = match ptyp_desc with | Ptyp_var x -> @@ -327,13 +395,13 @@ let rec core_type Ot.{ ptyp_desc; ptyp_loc } = | _ -> assert false (* TODO *) (** Convert GOSPEL [val] declarations into Why3's Ptree [val] declarations. *) -let val_decl vd g = +let val_decl vd ghost = let rec flat_ptyp_arrow ct = match ct.Ot.ptyp_desc with | Ot.Ptyp_var _ | Ptyp_tuple _ | Ptyp_constr _ -> [ct] - | Ot.Ptyp_arrow (_, t1, t2) -> - begin match t1.ptyp_desc with - | Ot.Ptyp_arrow (lbl, t11, t12) -> t1 :: flat_ptyp_arrow t2 - | _ -> flat_ptyp_arrow t1 @ flat_ptyp_arrow t2 end + | Ot.Ptyp_arrow (_, t1, t2) -> (* creative indentation *) + begin match t1.ptyp_desc with + | Ot.Ptyp_arrow (lbl, t11, t12) -> t1 :: flat_ptyp_arrow t2 + | _ -> flat_ptyp_arrow t1 @ flat_ptyp_arrow t2 end | _ -> assert false (* TODO *) in let mk_single_param lb_arg ct = let add_at_id at id = { id with id_ats = ATstr at :: id.id_ats } in @@ -371,16 +439,40 @@ let val_decl vd g = let mk_val id params ret pat mask spec = let e_any = Eany (params, Expr.RKnone, ret, pat, mask, spec) in let e_any = mk_expr e_any (location vd.T.vd_loc) in - Dlet (id, g, Expr.RKnone, e_any) in - match vd.T.vd_spec with - | None -> [mk_val (mk_id vd_str) params ret pat mask empty_spec] - | Some s -> (* creative indentation *) - begin match split_on_checks s.sp_pre with - | pre, [] -> [mk_val (mk_id vd_str) params ret pat mask (spec s)] - | pre, checks -> let id_unsafe = mk_id ("unsafe_" ^ vd_str) in - let spec_checks = spec_with_checks s pre (List.map term checks) in - [mk_val id_unsafe params ret pat mask (spec s); - mk_val (mk_id vd_str) params ret pat mask spec_checks] end in + Dlet (id, ghost, Expr.RKnone, e_any) in + let mk_disjoint_pre params = + let mk_disjoint = function + | [(_, id, _, PTtyapp (q, _)); (_, id', _, PTtyapp (q', _))] + when cmp_id_qualid q q' -> let id_q = Term.ident_of_qualid q in + [mk_disjoint_term (Opt.get id) (Opt.get id') id_q] + | _ -> [] (* TODO *) in + let represented_param (_, _, _, pty) = match pty with + | PTtyapp (Qident {id_str}, _) -> Hstr.mem env_represented id_str + | _ -> false in + let represented_params = List.filter represented_param params in + { empty_spec with sp_pre = mk_disjoint represented_params } in + let spec_disjoint = mk_disjoint_pre params in + let mk_spec = function + | None -> empty_spec, None + | Some s -> (* creative indentation *) + begin match split_on_checks s.T.sp_pre with + | _, [] -> spec_union (spec s) spec_disjoint, None + | pre, checks -> + let spec_checks = spec_with_checks s pre (List.map term checks) in + let spec_checks = spec_union spec_checks spec_disjoint in + let spec_regular = spec_union (spec s) spec_disjoint in + spec_regular, Some spec_checks end in + let mk_val_checks pre checks = + mk_val (mk_id vd_str) params ret pat mask checks in + let mk_val_unsafe spec = let id_unsafe = mk_id ("unsafe_" ^ vd_str) in + mk_val id_unsafe params ret pat mask spec in + let (spec_regular, spec_checks) = mk_spec vd.T.vd_spec in + let mk_val_final spec_regular = function + | None -> [mk_val (mk_id vd_str) params ret pat mask spec_regular] + | Some spec_checks -> + [mk_val_unsafe spec_regular; + mk_val_checks spec_regular spec_checks] in + mk_val_final spec_regular spec_checks in let params, ret, pat, mask = let core_tys = flat_ptyp_arrow vd.T.vd_type in let core_tys, last = Lists.chop_last core_tys in @@ -444,7 +536,7 @@ let sig_open file mm loc = Duseimport (loc, false, [dot_name, None]) let signature = - let mod_type_table: (string, gdecl list) Hashtbl.t = Hashtbl.create 16 in + let mod_type_table: gdecl list Hstr.t = Hstr.create 16 in (* Convert a GOSPEL module declaration into a Why3 scope. *) let rec module_declaration T.{md_name; md_type; md_loc} = @@ -456,7 +548,7 @@ let signature = | T.Mod_ident s -> begin match s with | [s] -> (* retrieve the list of declarations corresponding to module type [s] *) - Hashtbl.find mod_type_table s (* TODO: catch Not_found *) + Hstr.find mod_type_table s (* TODO: catch Not_found *) | _ -> assert false end | T.Mod_signature s -> List.flatten (signature s) @@ -477,13 +569,15 @@ let signature = and module_type_declaration mtd = let decls = match mtd.T.mtd_type with | None -> [] | Some mt -> module_type mt in - Hashtbl.add mod_type_table mtd.mtd_name.I.id_str decls + Hstr.add mod_type_table mtd.mtd_name.I.id_str decls and signature_item i = match i.T.sig_desc with | T.Sig_val (vd, g) -> List.map (fun d -> Gdecl d) (val_decl vd g) | T.Sig_type (_rec_flag, tdl, _gh) -> - [Gdecl (Dtype (List.map type_decl tdl))] + let tdlw = Gdecl (Dtype (List.map type_decl tdl)) in + let pdlw = Gdecl (disjoint tdl) in + [tdlw; pdlw] | T.Sig_typext _ (* of Oparsetree.type_extension *) -> assert false (*TODO*) | T.Sig_module md -> @@ -522,4 +616,5 @@ let signature = [Gdecl (axiom ax)] (*TODO*) and signature s = List.map signature_item s in + signature