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/

typing.ml 2.75 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) Francois Bobot, Jean-Christophe Filliatre,              *)
(*  Johannes Kanig and 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.                  *)
(*                                                                        *)
(**************************************************************************)
16

17 18
open Util
open Format
19 20
open Term

21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
(** errors *)

type error = 
  | ClashType of string
  | BadTypeArity of string

exception Error of error

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

let report fmt = function
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
  | BadTypeArity s ->
      fprintf fmt "duplicate type parameter %s" s

39 40 41 42 43 44
module M = Map.Make(String)

type env = {
  tysymbols : tysymbol M.t;
  fsymbols  : fsymbol M.t;
  psymbols  : psymbol M.t;
45
  tyvars    : tvsymbol M.t;
46 47 48 49 50 51 52 53 54 55 56
  vars      : vsymbol M.t;
}

let empty = {
  tysymbols = M.empty;
  fsymbols  = M.empty;
  psymbols  = M.empty;
  tyvars    = M.empty;
  vars      = M.empty;
}

57 58 59 60 61 62 63 64 65 66 67
let find_tysymbol s env = M.find s env.tysymbols
let find_fsymbol s env = M.find s env.fsymbols
let find_psymbol s env = M.find s env.psymbols
let find_tyvar s env = M.find s env.tyvars
let find_var s env = M.find s env.vars

(** typing *)

let term env t =
  assert false (*TODO*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68 69 70
let fmla env f =
  assert false (*TODO*)

71 72 73 74 75 76 77 78 79 80 81 82
(** building environments *)

open Ptree

let add_type loc ext sl s env =
  if M.mem s env.tysymbols then error ~loc (ClashType s);
  let add_ty_var env x =
    if M.mem x env.tyvars then error ~loc (BadTypeArity x);
    let v = Name.from_string x in
    { env with tyvars = M.add x v env.tyvars}, v
  in
  let _, vl = map_fold_left add_ty_var env sl in
83
  let ty = Ty.create_tysymbol (Name.from_string s) vl None in
84 85 86 87 88 89 90
  { env with tysymbols = M.add s ty env.tysymbols }

let add env = function
  | TypeDecl (loc, ext, sl, s) ->
      add_type loc ext sl s env
  | _ ->
      assert false (*TODO*)