Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

mlw_module.mli 3.25 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
open Ident
open Ty
25 26
open Term
open Decl
27 28
open Theory
open Mlw_ty
29
open Mlw_ty.T
30 31 32
open Mlw_expr
open Mlw_decl

33 34 35 36 37
type type_symbol =
  | PT of itysymbol
  | TS of tysymbol

type prog_symbol =
38 39 40
  | PV of pvsymbol
  | PS of psymbol
  | PL of plsymbol
41 42
  | XS of xsymbol
  | LS of lsymbol
43

44 45 46 47
type namespace = {
  ns_ts : type_symbol Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
48 49
}

50 51
val ns_find_ts : namespace -> string list -> type_symbol
val ns_find_ps : namespace -> string list -> prog_symbol
52 53 54 55 56 57 58 59 60 61
val ns_find_ns : namespace -> string list -> namespace

(** Module *)

type modul = private {
  mod_theory: theory;			(* pure theory *)
  mod_decls : pdecl list;		(* module declarations *)
  mod_export: namespace;		(* exported namespace *)
  mod_known : known_map;		(* known identifiers *)
  mod_local : Sid.t;			(* locally declared idents *)
62
  mod_used  : Sid.t;			(* used modules *)
63 64 65 66 67 68 69 70 71 72 73 74
}

(** Module under construction *)

type module_uc (* a module under construction *)

val create_module : ?path:string list -> preid -> module_uc
val close_module  : module_uc -> modul

val open_namespace  : module_uc -> module_uc
val close_namespace : module_uc -> bool -> string option -> module_uc

75
val get_theory : module_uc -> theory_uc
76 77 78 79 80
val get_namespace : module_uc -> namespace
val get_known : module_uc -> known_map

(** Use *)

81
val use_export : module_uc -> modul -> module_uc
82

83
(** Clone *)
84

85
val clone_export : module_uc -> modul -> th_inst -> module_uc
86 87 88 89 90 91 92 93 94 95 96

(** Logic decls *)

val add_decl : module_uc -> decl -> module_uc
val use_export_theory: module_uc -> theory -> module_uc
val clone_export_theory: module_uc -> theory -> th_inst -> module_uc
val add_meta : module_uc -> meta -> meta_arg list -> module_uc

(** Program decls *)

val add_pdecl : module_uc -> pdecl -> module_uc