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).

typing.ml 1.62 KB
Newer Older
1

2 3
open Util
open Format
4 5
open Term

6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
(** 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

24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
module M = Map.Make(String)

type env = {
  tysymbols : tysymbol M.t;
  fsymbols  : fsymbol M.t;
  psymbols  : psymbol M.t;
  tyvars    : vsymbol M.t;
  vars      : vsymbol M.t;
}

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

42 43 44 45 46 47 48 49 50 51 52
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
53 54 55
let fmla env f =
  assert false (*TODO*)

56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
(** 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
  let ty = Ty.create_tysymbol (Name.from_string s) vl None in
  { 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*)