Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

mlw_dty.mli 1.94 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16 17 18 19

(* destructive types for program type inference *)

open Ident
open Ty
open Term
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
20
open Mlw_module
21

22
type dreg
23
type dity
24
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
25

26 27
type tvars (* a set of type variables *)
val empty_tvars: tvars
28 29
val add_dity: tvars -> dity -> tvars
val add_dvty: tvars -> dvty -> tvars
30

31
val create_type_variable: unit -> dity
32
val create_user_type_variable: Ptree.ident -> (* opaque *) bool -> dity
33
val its_app: itysymbol -> dity list -> dity
34 35
val ts_app: tysymbol -> dity list -> dity

36 37
val opaque_tvs: Stv.t -> dity -> Stv.t

38 39 40 41 42
val is_chainable: dvty -> bool
  (* non-bool * non-bool -> bool *)

val free_user_vars: tvars -> dvty -> Stv.t
  (* user type variables not bound in the context *)
43

Andrei Paskevich's avatar
Andrei Paskevich committed
44 45
exception DTypeMismatch of dity * dity

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
46 47
val unify: ?weak:bool -> dity -> dity -> unit
  (* when [weak] is true, don't unify regions *)
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49
val ity_of_dity: dity -> ity
50
  (* only use once all unification is done *)
51

52
val specialize_scheme: tvars -> dvty -> dvty
53

54
val specialize_lsymbol: lsymbol -> dvty
55
val specialize_pvsymbol: pvsymbol -> dity
56 57
val specialize_psymbol: psymbol -> dvty
val specialize_plsymbol: plsymbol -> dvty
Andrei Paskevich's avatar
Andrei Paskevich committed
58
val specialize_xsymbol: xsymbol -> dity
Andrei Paskevich's avatar
Andrei Paskevich committed
59 60

val print_dity : Format.formatter -> dity -> unit