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

typing.ml 6.35 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
open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
20
open Ptree
21

22 23 24 25 26
(** errors *)

type error = 
  | ClashType of string
  | BadTypeArity of string
27 28 29
  | UnboundType of string
  | TypeArity of string * int * int
  | Clash of string
30 31 32 33 34 35 36 37 38 39 40 41

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
42 43 44 45 46 47 48
  | UnboundType s ->
       fprintf fmt "Unbound type '%s'" s
  | TypeArity (id, a, n) ->
      fprintf fmt "@[The type %s expects %d argument(s),@ " id a;
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
      fprintf fmt "Clash with previous constant %s" id
49

50 51 52 53 54 55
module M = Map.Make(String)

type env = {
  tysymbols : tysymbol M.t;
  fsymbols  : fsymbol M.t;
  psymbols  : psymbol M.t;
56
  tyvars    : tvsymbol M.t;
57 58 59 60 61 62 63 64 65 66 67
  vars      : vsymbol M.t;
}

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

68 69 70 71 72 73
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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74 75 76
let add_tyvar x v env = { env with tyvars = M.add x v env.tyvars}
let add_tysymbol x ty env = { env with tysymbols = M.add x ty env.tysymbols }

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166

(** typing using destructive type variables *)

module D = struct

  (* types with destructive type variables *)
  type ty =
    | Tyvar of type_var
    | Tyapp of tysymbol * ty list

  and type_var = { 
    tag : int; 
    user : bool;
    tvsymbol : tvsymbol;
    mutable type_val : ty option;
  }

  let create_type_var =
    let t = ref 0 in
    fun ~user x -> 
      incr t; 
      { tag = !t; user = user; tvsymbol = Name.from_string x; type_val = None }

  let rec occurs v = function
    | Tyvar { type_val = Some t } -> occurs v t
    | Tyvar { tag = t; type_val = None } -> v.tag = t
    | Tyapp (_, l) -> List.exists (occurs v) l

  (* destructive type unification *)
  let rec unify t1 t2 = match t1, t2 with
    | Tyvar { type_val = Some t1 }, _ ->
	unify t1 t2
    | _, Tyvar { type_val = Some t2 } ->
	unify t1 t2
    | Tyvar v1, Tyvar v2 when v1.tag = v2.tag ->
	true
    (* instantiable variables *)
    | Tyvar ({user=false} as v), t
    | t, Tyvar ({user=false} as v) ->
	not (occurs v t) && (v.type_val <- Some t; true)
    (* recursive types *)
    | Tyapp (s1, l1), Tyapp (s2, l2) ->
	s1 == s2 && List.length l1 = List.length l2 &&
	List.for_all2 unify l1 l2
    | Tyapp _, _ | _, Tyapp _ ->
	false
    (* other cases *)
    | Tyvar {user=true; tag=t1}, Tyvar {user=true; tag=t2} -> 
	t1 = t2

  (* env + destructive type variables environment *)
  type denv = { 
    env : env;
    dvars : (string, type_var) Hashtbl.t;
  }

  let create env = { env = env; dvars = Hashtbl.create 17 }

  let find_type_var x env =
    try
      Hashtbl.find env.dvars x
    with Not_found ->
      let v = create_type_var ~user:true x in
      Hashtbl.add env.dvars x v;
      v
 
  (* parsed types -> intermediate types *)
  let rec dty env = function
    | PPTvarid (x, _) -> 
	Tyvar (find_type_var x env)
    | PPTexternal (p, id, loc) ->
	if not (M.mem id env.env.tysymbols) then error ~loc (UnboundType id);
	let s = M.find id env.env.tysymbols in
	let np = List.length p in
	let a = List.length s.Ty.ts_args in
	if np <> a then error ~loc (TypeArity (id, a, np));
	Tyapp (s, List.map (dty env) p)

  (* intermediate types -> types *)
  let rec ty env = function
    | Tyvar { type_val = Some t } ->
	ty env t
    | Tyvar { tvsymbol = tv } ->
	Ty.ty_var tv
    | Tyapp (s, tl) ->
	Ty.ty_app s (List.map (ty env) tl)
	

end

167 168
(** typing *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169 170 171 172
let term env t = match t.pp_desc with
  | _ ->
      assert false (*TODO*)

173

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174 175 176
let fmla env f =
  assert false (*TODO*)

177 178 179 180 181 182 183 184 185
(** 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
186
    add_tyvar x v env, v
187 188
  in
  let _, vl = map_fold_left add_ty_var env sl in
189
  let ty = Ty.create_tysymbol (Name.from_string s) vl None in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
190
  add_tysymbol s ty env
191

192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
let add_function loc pl t env id =
  if M.mem id env.fsymbols then error ~loc (Clash id);
  let denv = D.create env in
  let pl = List.map (D.dty denv) pl and t = D.dty denv t in
  let pl = List.map (D.ty denv) pl and t = D.ty denv t in
  let s = create_fsymbol (Name.from_string id) (pl, t) false in
  { env with fsymbols = M.add id s env.fsymbols }

let add_predicate loc pl env id =
  if M.mem id env.psymbols then error ~loc (Clash id);
  let denv = D.create env in
  let pl = List.map (D.dty denv) pl in
  let pl = List.map (D.ty denv) pl in
  let s = create_psymbol (Name.from_string id) pl in
  { env with psymbols = M.add id s env.psymbols }

208 209 210
let add env = function
  | TypeDecl (loc, ext, sl, s) ->
      add_type loc ext sl s env
211 212 213 214
  | Logic (loc, ext, ids, PPredicate pl) ->
      List.fold_left (add_predicate loc pl) env ids
  | Logic (loc, ext, ids, PFunction (pl, t)) ->
      List.fold_left (add_function loc pl t) env ids
215 216
  | _ ->
      assert false (*TODO*)