typing.ml 8.63 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
  | PredicateExpected
  | TermExpected
32 33 34 35 36 37 38 39 40 41 42 43

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
44 45 46 47 48 49 50
  | 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
51 52 53 54 55 56
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"

(** typing environments *)
57

58 59 60 61 62 63
module M = Map.Make(String)

type env = {
  tysymbols : tysymbol M.t;
  fsymbols  : fsymbol M.t;
  psymbols  : psymbol M.t;
64
  tyvars    : tvsymbol M.t;
65 66 67 68 69 70 71 72 73 74 75
  vars      : vsymbol M.t;
}

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

76 77 78 79 80 81
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
82 83 84
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 }

85

86
(** typing using destructive type variables 
87

88 89 90 91 92 93
    parsed trees        intermediate trees       typed trees
      (Ptree)               (D below)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
      lexpr      --dfmla-->   dfmla     --fmla-->    fmla
94

95 96 97 98 99 100 101 102 103 104 105 106 107 108
*)

(** types with destructive type variables *)

type dty =
  | Tyvar of type_var
  | Tyapp of tysymbol * dty list
      
and type_var = { 
  tag : int; 
  user : bool;
  tvsymbol : tvsymbol;
  mutable type_val : dty option;
}
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 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
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

(** environment + destructive type variables environment *)

type denv = { 
  env : env;
  dvars : (string, type_var) Hashtbl.t;
}

let create_denv 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
 
(** typing types *)

(* 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)
	
(** typing terms and formulas *)

type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
  | Tbvar of int
  | Tvar of vsymbol
  | Tapp of fsymbol * dterm list
  | Tlet of dterm * string * dterm
(*   | Tcase of dterm * tbranch list *)
  | Teps of string * dfmla

and dfmla = 
  | Fapp of psymbol * dterm list
  | Fquant of quant * string * dfmla
  | Fbinop of binop * dfmla * dfmla
  | Fnot of dfmla
  | Ftrue
  | Ffalse
  | Fif of dfmla * dfmla * dfmla
(*   | Flet of dterm * string * dfmla *)
(*   | Fcase of dterm * (pattern * dfmla) list *)

let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff
  | _ -> assert false 

let rec dterm env t = match t.pp_desc with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214 215 216
  | _ ->
      assert false (*TODO*)

217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233
and dfmla env e = match e.pp_desc with
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
  | PPprefix (PPnot, a) ->
      Fnot (dfmla env a)
  | PPinfix (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
      Fbinop (binop op, dfmla env a, dfmla env b)
  | PPinfix _ ->
      error ~loc:e.pp_loc PredicateExpected
  | PPif (a, b, c) ->
      Fif (dfmla env a, dfmla env b, dfmla env c)  
  | PPforall (id, pt, _, a) -> (* TODO: triggers *)
      assert false (*TODO*)
  | _ ->
      assert false (*TODO*)
234

235
let rec term env t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236 237
  assert false (*TODO*)

238 239 240 241 242 243 244 245 246 247 248 249 250 251
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
      f_false 
  | Fnot f ->
      f_not (fmla env f)
  | Fbinop (op, f1, f2) ->
      f_binary op (fmla env f1) (fmla env f2)
  | Fif (f1, f2, f3) ->
      f_if (fmla env f1) (fmla env f2) (fmla env f3)
  | _ ->
      assert false (*TODO*)

252 253 254 255 256 257 258 259 260
(** 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
261
    add_tyvar x v env, v
262 263
  in
  let _, vl = map_fold_left add_ty_var env sl in
264
  let ty = Ty.create_tysymbol (Name.from_string s) vl None in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
  add_tysymbol s ty env
266

267 268
let add_function loc pl t env id =
  if M.mem id env.fsymbols then error ~loc (Clash id);
269 270 271
  let denv = create_denv env in
  let pl = List.map (dty denv) pl and t = dty denv t in
  let pl = List.map (ty denv) pl and t = ty denv t in
272 273 274 275 276
  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);
277 278 279
  let denv = create_denv env in
  let pl = List.map (dty denv) pl in
  let pl = List.map (ty denv) pl in
280 281 282
  let s = create_psymbol (Name.from_string id) pl in
  { env with psymbols = M.add id s env.psymbols }

283 284 285 286 287 288 289 290 291 292 293 294 295 296
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
  fmla denv f

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
  term denv t

let axiom loc s f env =
  ignore (fmla env f);
  env

297 298 299
let add env = function
  | TypeDecl (loc, ext, sl, s) ->
      add_type loc ext sl s env
300 301 302 303
  | 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
304 305
  | Axiom (loc, s, f) ->
      axiom loc s f env
306 307
  | _ ->
      assert false (*TODO*)