MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

env.ml 4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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 Ident
21
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
22
23
24
25
26
27

(** Environment *)

type env = {
  env_retrieve : retrieve_theory;
  env_memo     : (string list, theory Mnm.t) Hashtbl.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
28
  env_tag      : Hashweak.tag;
Andrei Paskevich's avatar
Andrei Paskevich committed
29
30
31
32
}

and retrieve_theory = env -> string list -> theory Mnm.t

Andrei Paskevich's avatar
Andrei Paskevich committed
33
let create_env = let c = ref (-1) in fun retrieve ->
34
35
36
  let env = {
    env_retrieve = retrieve;
    env_memo     = Hashtbl.create 17;
Andrei Paskevich's avatar
Andrei Paskevich committed
37
    env_tag      = (incr c; Hashweak.create_tag !c) }
38
39
40
41
  in
  let add th m = Mnm.add th.th_name.id_string th m in
  let m = Mnm.empty in
  let m = add builtin_theory m in
42
  let m = add highord_theory m in
43
44
45
46
47
  let m = add (tuple_theory 0) m in
  let m = add (tuple_theory 1) m in
  let m = add (tuple_theory 2) m in
  Hashtbl.add env.env_memo [] m;
  env
Andrei Paskevich's avatar
Andrei Paskevich committed
48
49
50
51

exception TheoryNotFound of string list * string

let find_theory env sl s =
Andrei Paskevich's avatar
Andrei Paskevich committed
52
  try
53
54
55
56
57
58
59
60
61
62
    let m =
      try
	Hashtbl.find env.env_memo sl
      with Not_found ->
	Hashtbl.add env.env_memo sl Mnm.empty;
	let m = env.env_retrieve env sl in
	Hashtbl.replace env.env_memo sl m;
	m
    in
    Mnm.find s m
Andrei Paskevich's avatar
Andrei Paskevich committed
63
  with Not_found ->
64
    raise (TheoryNotFound (sl, s))
Andrei Paskevich's avatar
Andrei Paskevich committed
65

Andrei Paskevich's avatar
Andrei Paskevich committed
66
let env_tag env = env.env_tag
Andrei Paskevich's avatar
Andrei Paskevich committed
67

68
69
70

(** Parsers *)

71
type read_channel = env -> string -> in_channel -> theory Mnm.t
72

73
74
75
let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)

76
let register_format name suffixes rc =
77
78
79
  Hashtbl.add read_channel_table name rc;
  List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes

80
exception UnknownFormat of string (* parser name *)
81
82

let parser_for_file ?name file = match name with
83
84
85
  | None ->
      begin try
	let ext =
86
87
88
89
90
	  let s = Filename.chop_extension file in
	  let n = String.length s in
	  String.sub file n (String.length file - n)
	in
	Hashtbl.find suffixes_table ext
91
      with Invalid_argument _ | Not_found ->
92
93
	"why"
      end
94
  | Some n ->
95
96
97
98
      n

let find_parser table n =
  try Hashtbl.find table n
99
  with Not_found -> raise (UnknownFormat n)
100

101
let read_channel ?name env file ic =
102
  let n = parser_for_file ?name file in
103
  let rc = find_parser read_channel_table n in
104
  rc env file ic
105

106
107
let list_formats () =
  let h = Hashtbl.create 17 in
108
  let add s p =
109
110
111
112
113
114
    let l = try Hashtbl.find h p with Not_found -> [] in
    Hashtbl.replace h p (s :: l)
  in
  Hashtbl.iter add suffixes_table;
  Hashtbl.fold (fun p l acc -> (p, l) :: acc) h []

115
(* Exception reporting *)
116
117

let () = Exn_printer.register
118
119
120
121
122
123
124
125
  begin fun fmt exn -> match exn with
  | TheoryNotFound (sl, s) ->
      Format.fprintf fmt "Theory not found: %a.%s"
        (Pp.print_list Pp.dot Format.pp_print_string) sl s
  | UnknownFormat s ->
      Format.fprintf fmt "Unknown input format: %s" s
  | _ -> raise exn
  end
126