pgm_typing.ml 17.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why
22
open Util
23
open Ident
24
open Ty
25
open Term
26
open Theory
27 28 29
open Denv
open Ptree
open Pgm_ttree
30

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
type error =
  | Message 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 errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf
    (fun _ ->
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc (Message s))
    fmt f

let report fmt = function
  | Message s ->
      fprintf fmt "%s" s

55 56 57 58
let id_result = "result"

(* environments *)

59
let ts_unit uc = ns_find_ts (get_namespace uc) ["unit"]
60
let ts_ref uc = ns_find_ts (get_namespace uc) ["ref"]
61
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
62 63 64 65 66 67 68
let ts_exn uc = ns_find_ts (get_namespace uc) ["exn"]

let ls_Unit uc = ns_find_ls (get_namespace uc) ["Unit"]

let dty_bool uc = Tyapp (ns_find_ts (get_namespace uc) ["bool"], [])
let dty_unit uc = Tyapp (ts_unit uc, [])
let dty_label uc = Tyapp (ns_find_ts (get_namespace uc) ["label"], [])
69

70
type denv = {
71
  uc   : theory_uc;
72 73 74
  denv : Typing.denv;
}

75 76 77
let create_denv uc = 
  { uc   = uc;
    denv = Typing.create_denv uc;
78
  }
79

80 81 82 83
let create_type_var loc =
  let tv = Ty.create_tvsymbol (id_user "a" loc) in
  Tyvar (create_ty_decl_var ~loc ~user:false tv)

84 85
let dcurrying uc tyl ty =
  let make_arrow_type ty1 ty2 = Tyapp (ts_arrow uc, [ty1; ty2]) in
86
  List.fold_right make_arrow_type tyl ty
87

88
let uncurrying uc ty =
89
  let rec uncurry acc ty = match ty.ty_node with
90
    | Ty.Tyapp (ts, [t1; t2]) when ts == ts_arrow uc -> uncurry (t1 :: acc) t2
91 92 93 94
    | _ -> List.rev acc, ty
  in
  uncurry [] ty

95
let expected_type e ty =
96 97
  if not (Denv.unify e.dexpr_type ty) then
    errorm ~loc:e.dexpr_loc 
98
      "this expression has type %a, but is expected to have type %a"
99
      print_dty e.dexpr_type print_dty ty
100

101 102
(* phase 1: typing programs (using destructive type inference) *)

103 104
let pure_type env = Typing.dty env.denv

105 106 107 108 109 110
let rec dpurify env = function
  | DTpure ty -> 
      ty
  | DTarrow (bl, c) -> 
      dcurrying env.uc (List.map (fun (_,ty) -> dpurify env ty) bl)
	(dpurify env c.dc_result_type)
111

112 113 114 115 116
let check_reference_type uc loc ty =
  let ty_ref =Tyapp (ts_ref uc, [create_type_var loc]) in
  if not (Denv.unify ty ty_ref) then
    errorm ~loc "this expression has type %a, but is expected to be a reference"
      print_dty ty
117 118 119 120 121
  
let dreference env id =
  if Typing.mem_var id.id env.denv then
    (* local variable *)
    let ty = Typing.find_var id.id env.denv in
122
    check_reference_type env.uc id.id_loc ty;
123 124 125
    DRlocal id.id
  else 
    let p = Qident id in
126 127
    let s, _, ty = Typing.specialize_fsymbol p env.uc in
    check_reference_type env.uc id.id_loc ty;
128 129
    DRglobal s

130 131 132 133 134 135 136 137 138
let dexception env id =
  let p = Qident id in
  let _, _, ty as r = Typing.specialize_fsymbol p env.uc in
  let ty_exn = Tyapp (ts_exn env.uc, []) in
  if not (Denv.unify ty ty_exn) then
    errorm ~loc:id.id_loc
      "this expression has type %a, but is expected to be an exception"
      print_dty ty;
  r
139 140 141 142

let deffect env e =
  { de_reads  = List.map (dreference env) e.Pgm_ptree.pe_reads;
    de_writes = List.map (dreference env) e.Pgm_ptree.pe_writes;
143 144 145
    de_raises = 
      List.map (fun id -> let ls,_,_ = dexception env id in ls) 
	e.Pgm_ptree.pe_raises; }
146

147 148 149 150 151 152 153 154 155 156 157 158
let rec dtype_v env = function
  | Pgm_ptree.Tpure pt -> 
      DTpure (pure_type env pt)
  | Pgm_ptree.Tarrow (bl, c) -> 
      let env, bl = map_fold_left dbinder env bl in
      let c = dtype_c env c in
      DTarrow (bl, c) 

and dtype_c env c = 
  let ty = dtype_v env c.Pgm_ptree.pc_result_type in
  { dc_result_name = c.Pgm_ptree.pc_result_name.id;
    dc_result_type = ty;
159
    dc_effect      = deffect env c.Pgm_ptree.pc_effect;
160 161 162 163 164
    dc_pre         = env.denv, c.Pgm_ptree.pc_pre;
    dc_post        =   
      let denv = Typing.add_var id_result (dpurify env ty) env.denv in
      denv, c.Pgm_ptree.pc_post;
  }
165

166
and dbinder env ({id=x; id_loc=loc}, v) =
167 168 169 170 171 172 173 174
  let v = match v with
    | Some v -> dtype_v env v 
    | None -> DTpure (create_type_var loc)
  in
  let ty = dpurify env v in
  let env = { env with denv = Typing.add_var x ty env.denv } in
  env, (x, v)

175
let rec dexpr env e = 
176
  let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
177 178
  { dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
    dexpr_denv = env.denv; dexpr_type = ty;  }
179

180
and dexpr_desc env loc = function
181
  | Pgm_ptree.Econstant (ConstInt _ as c) ->
182
      DEconstant c, Tyapp (Ty.ts_int, [])
183
  | Pgm_ptree.Econstant (ConstReal _ as c) ->
184 185
      DEconstant c, Tyapp (Ty.ts_real, [])
  | Pgm_ptree.Eident (Qident {id=x}) when Typing.mem_var x env.denv ->
186
      (* local variable *)
187 188
      let ty = Typing.find_var x env.denv in
      DElocal x, ty
189
  | Pgm_ptree.Eident p ->
190 191
      let s, tyl, ty = Typing.specialize_fsymbol p env.uc in
      DEglobal s, dcurrying env.uc tyl ty
192
  | Pgm_ptree.Eapply (e1, e2) ->
193 194
      let e1 = dexpr env e1 in
      let e2 = dexpr env e2 in
195
      let ty2 = create_type_var loc and ty = create_type_var loc in
196 197
      if not (Denv.unify e1.dexpr_type (Tyapp (ts_arrow env.uc, [ty2; ty]))) 
      then
198 199 200
	errorm ~loc:e1.dexpr_loc "this expression is not a function";
      expected_type e2 ty2;
      DEapply (e1, e2), ty
201 202 203 204
  | Pgm_ptree.Efun (bl, t) ->
      let env, bl = map_fold_left dbinder env bl in
      let (_,e,_) as t = dtriple env t in
      let tyl = List.map (fun (x,_) -> Typing.find_var x env.denv) bl in
205
      let ty = dcurrying env.uc tyl e.dexpr_type in
206
      DEfun (bl, t), ty
207
  | Pgm_ptree.Elet ({id=x}, e1, e2) ->
208 209 210 211 212
      let e1 = dexpr env e1 in
      let ty1 = e1.dexpr_type in
      let env = { env with denv = Typing.add_var x ty1 env.denv } in
      let e2 = dexpr env e2 in
      DElet (x, e1, e2), e2.dexpr_type
213 214 215 216
  | Pgm_ptree.Eletrec (dl, e1) ->
      let env, dl = dletrec env dl in
      let e1 = dexpr env e1 in
      DEletrec (dl, e1), e1.dexpr_type
217

218
  | Pgm_ptree.Esequence (e1, e2) ->
219
      let e1 = dexpr env e1 in
220
      expected_type e1 (dty_unit env.uc);
221 222
      let e2 = dexpr env e2 in
      DEsequence (e1, e2), e2.dexpr_type
223
  | Pgm_ptree.Eif (e1, e2, e3) ->
224
      let e1 = dexpr env e1 in
225
      expected_type e1 (dty_bool env.uc);
226 227 228 229
      let e2 = dexpr env e2 in
      let e3 = dexpr env e3 in
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
230
  | Pgm_ptree.Ewhile (e1, a, e2) ->
231
      let e1 = dexpr env e1 in
232
      expected_type e1 (dty_bool env.uc);
233
      let e2 = dexpr env e2 in
234 235
      expected_type e2 (dty_unit env.uc);
      DEwhile (e1, a, e2), (dty_unit env.uc)
236
  | Pgm_ptree.Elazy (op, e1, e2) ->
237
      let e1 = dexpr env e1 in
238
      expected_type e1 (dty_bool env.uc);
239
      let e2 = dexpr env e2 in
240 241
      expected_type e2 (dty_bool env.uc);
      DElazy (op, e1, e2), (dty_bool env.uc)
242 243 244 245 246 247 248 249 250 251 252 253 254
  | Pgm_ptree.Ematch (el, bl) ->
      let el = List.map (dexpr env) el in
      let tyl = List.map (fun e -> e.dexpr_type) el in
      let ty = create_type_var loc in (* the type of all branches *)
      let branch (pl, e) =
	let denv, pl = Typing.dpat_list env.denv tyl pl in
	let env = { env with denv = denv } in
	let e = dexpr env e in
	expected_type e ty;
	pl, e
      in
      let bl = List.map branch bl in
      DEmatch (el, bl), ty
255
  | Pgm_ptree.Eskip ->
256
      DEskip, (dty_unit env.uc)
257 258
  | Pgm_ptree.Eabsurd ->
      DEabsurd, create_type_var loc
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
  | Pgm_ptree.Eraise (id, e) ->
      let ls, tyl, _ = dexception env id in
      let e = match e, tyl with
	| None, [] ->  
	    None
	| Some _, [] ->
	    errorm ~loc "expection %s has no argument" id.id
	| None, [ty] ->
	    errorm ~loc "exception %s is expecting an argument of type %a"
	      id.id print_dty ty;
	| Some e, [ty] -> 
	    let e = dexpr env e in
	    expected_type e ty;
	    Some e
	| _ -> 
	    assert false
      in
      DEraise (ls, e), create_type_var loc
277 278

  | Pgm_ptree.Eassert (k, le) ->
279
      DEassert (k, le), (dty_unit env.uc) 
280 281 282 283
  | Pgm_ptree.Eghost e1 ->
      let e1 = dexpr env e1 in
      DEghost e1, e1.dexpr_type
  | Pgm_ptree.Elabel ({id=l}, e1) ->
284
      let ty = dty_label env.uc in
285
      let env = { env with denv = Typing.add_var l ty env.denv } in
286 287
      let e1 = dexpr env e1 in
      DElabel (l, e1), e1.dexpr_type
288 289 290 291 292
  | Pgm_ptree.Ecast (e1, ty) ->
      let e1 = dexpr env e1 in
      let ty = pure_type env ty in
      expected_type e1 ty;
      e1.dexpr_desc, ty
293

294 295
and dletrec env dl =
  (* add all functions into environment *)
296
  let add_one env (id, bl, var, t) = 
297
    let ty = create_type_var id.id_loc in
298 299
    let env = { env with denv = Typing.add_var id.id ty env.denv } in
    env, ((id, ty), bl, var, t)
300
  in
301
  let env, dl = map_fold_left add_one env dl in
302
  (* then type-check all of them and unify *)
303
  let type_one ((id, tyres), bl, v, t) = 
304 305 306 307 308 309 310 311
    let env, bl = map_fold_left dbinder env bl in
    let (_,e,_) as t = dtriple env t in
    let tyl = List.map (fun (x,_) -> Typing.find_var x env.denv) bl in
    let ty = dcurrying env.uc tyl e.dexpr_type in
    if not (Denv.unify ty tyres) then 
      errorm ~loc:id.id_loc
	"this expression has type %a, but is expected to have type %a"
	print_dty ty print_dty tyres;
312
    ((id.id, tyres), bl, v, t)
313 314 315
  in
  env, List.map type_one dl

316 317 318 319 320 321 322 323
and dtriple env (p, e, q) =     
  let p = env.denv, p in
  let e = dexpr env e in
  let ty = e.dexpr_type in
  let denvq = Typing.add_var id_result ty env.denv in
  let q = denvq, q in
  (p, e, q)

324 325
(* phase 2: typing annotations *)

326 327 328
let currying uc tyl ty =
  let make_arrow_type ty1 ty2 = Ty.ty_app (ts_arrow uc) [ty1; ty2] in
  List.fold_right make_arrow_type tyl ty
329

330 331 332 333
let purify uc = function
  | Tpure ty -> 
      ty
  | Tarrow (bl, c) -> 
334
      currying uc (List.map (fun (v,_) -> v.vs_ty) bl) c.c_result_name.vs_ty
335

336 337 338 339 340 341 342 343 344
let reference _uc env = function
  | DRlocal x -> Rlocal (Mstr.find x env)
  | DRglobal ls -> Rglobal ls

let effect uc env e =
  { e_reads  = List.map (reference uc env) e.de_reads;
    e_writes = List.map (reference uc env) e.de_writes;
    e_raises = e.de_raises; }

345 346 347 348 349 350 351 352 353 354 355 356 357
let rec type_v uc env = function
  | DTpure ty -> 
      Tpure (Denv.ty_of_dty ty)
  | DTarrow (bl, c) -> 
      let env, bl = map_fold_left (binder uc) env bl in
      Tarrow (bl, type_c uc env c)

and type_c uc env c = 
  let tyv = type_v uc env c.dc_result_type in
  let ty = purify uc tyv in
  let v = create_vsymbol (id_fresh c.dc_result_name) ty in
  { c_result_name = v;
    c_result_type = tyv;
358
    c_effect      = effect uc env c.dc_effect;
359 360 361 362 363 364 365 366 367 368 369 370
    c_pre         = 
      (let denv, l = c.dc_pre in Typing.type_fmla denv env l);
    c_post        =
	  let denv, l = c.dc_post in 
	  let v_result = create_vsymbol (id_fresh id_result) ty in
	  let env = Mstr.add id_result v_result env in
 	  Typing.type_fmla denv env l;
  }
    
and binder uc env (x, tyv) = 
  let tyv = type_v uc env tyv in
  let v = create_vsymbol (id_fresh x) (purify uc tyv) in
371 372 373
  let env = Mstr.add x v env in
  env, (v, tyv)

374 375
let rec expr uc env e =
  let d = expr_desc uc env e.dexpr_denv e.dexpr_desc in
376 377 378
  let ty = Denv.ty_of_dty e.dexpr_type in
  { expr_desc = d; expr_type = ty; expr_loc = e.dexpr_loc }

379
and expr_desc uc env denv = function
380 381 382
  | DEconstant c ->
      Econstant c
  | DElocal x ->
383
      Elocal (Mstr.find x env)
384 385 386
  | DEglobal ls ->
      Eglobal ls
  | DEapply (e1, e2) ->
387
      Eapply (expr uc env e1, expr uc env e2)
388
  | DEfun (bl, e1) ->
389 390
      let env, bl = map_fold_left (binder uc) env bl in
      Efun (bl, triple uc env e1)
391
  | DElet (x, e1, e2) ->
392
      let e1 = expr uc env e1 in
393 394
      let v = create_vsymbol (id_fresh x) e1.expr_type in
      let env = Mstr.add x v env in
395
      Elet (v, e1, expr uc env e2)
396 397 398 399
  | DEletrec (dl, e1) ->
      let env, dl = letrec uc env dl in
      let e1 = expr uc env e1 in
      Eletrec (dl, e1)
400 401

  | DEsequence (e1, e2) ->
402
      Esequence (expr uc env e1, expr uc env e2)
403
  | DEif (e1, e2, e3) ->
404
      Eif (expr uc env e1, expr uc env e2, expr uc env e3)
405
  | DEwhile (e1, la, e2) ->
406 407
      let la = 
	{ loop_invariant = 
408
	    option_map (Typing.type_fmla denv env) la.Pgm_ptree.loop_invariant;
409
	  loop_variant   = 
410
	    option_map (Typing.type_term denv env) la.Pgm_ptree.loop_variant; }
411
      in
412
      Ewhile (expr uc env e1, la, expr uc env e2)
413
  | DElazy (op, e1, e2) ->
414
      Elazy (op, expr uc env e1, expr uc env e2)
415 416 417 418 419 420 421 422
  | DEmatch (el, bl) ->
      let el = List.map (expr uc env) el in
      let branch (pl, e) = 
        let env, pl = map_fold_left Typing.pattern env pl in
        (pl, expr uc env e)
      in
      let bl = List.map branch bl in
      Ematch (el, bl)
423 424
  | DEskip ->
      Eskip
425 426
  | DEabsurd ->
      Eabsurd
427 428
  | DEraise (ls, e) ->
      Eraise (ls, option_map (expr uc env) e)
429 430

  | DEassert (k, f) ->
431
      let f = Typing.type_fmla denv env f in
432
      Eassert (k, f)
433
  | DEghost e1 -> 
434
      Eghost (expr uc env e1)
435
  | DElabel (s, e1) ->
436 437 438
      let ty = Denv.ty_of_dty (Typing.find_var s e1.dexpr_denv) in
      let v = create_vsymbol (id_fresh s) ty in
      let env = Mstr.add s v env in 
439
      Elabel (s, expr uc env e1)
440

441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459
and letrec uc env dl =
  (* add all functions into env, and compute local env *)
  let step1 env ((x, dty), bl, var, t) = 
    let ty = Denv.ty_of_dty dty in
    let v = create_vsymbol (id_fresh x) ty in
    let env = Mstr.add x v env in
    env, (v, bl, var, t)
  in
  let env, dl = map_fold_left step1 env dl in
  (* then translate variants and bodies *)
  let step2 (v, bl, var, (_,e,_ as t)) =
    let env, bl = map_fold_left (binder uc) env bl in
    let denv = e.dexpr_denv in
    let var = option_map (Typing.type_term denv env) var in
    let t = triple uc env t in
    (v, bl, var, t)
  in
  env, List.map step2 dl

460
and triple uc env ((denvp, p), e, (denvq, q)) =
461
  let p = Typing.type_fmla denvp env p in
462
  let e = expr uc env e in
463 464 465 466 467
  let v_result = create_vsymbol (id_fresh id_result) e.expr_type in
  let envq = Mstr.add id_result v_result env in
  let q = Typing.type_fmla denvq envq q in
  (p, e, q)

468 469
let type_expr uc e =
  let denv = create_denv uc in
470
  let e = dexpr denv e in
471
  expr uc Mstr.empty e
472

473 474 475 476 477
let type_type uc ty =
  let denv = create_denv uc in
  let dty = Typing.dty denv.denv ty in
  Denv.ty_of_dty dty

478 479 480 481 482 483 484 485
let add_decl uc ls =
  try
    Theory.add_decl uc (Decl.create_logic_decl [ls, None])
  with Theory.ClashSymbol _ ->
    let loc = match ls.ls_name.id_origin with
      | User loc -> Some loc
      | _ -> None (* FIXME: loc for recursive functions *)
    in
486
    errorm ?loc "clash with previous symbol %s" ls.ls_name.id_string
487
    
488 489 490 491 492 493 494
let file env uc dl =
  let uc, dl =
    List.fold_left
      (fun (uc, acc) d -> match d with
	 | Pgm_ptree.Dlogic dl -> 
	     List.fold_left (Typing.add_decl env Mnm.empty) uc dl, acc
	 | Pgm_ptree.Dlet (id, e) -> 
495 496
	     let e = type_expr uc e in
	     let tyl, ty = uncurrying uc e.expr_type in
497
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
498
	     let uc = add_decl uc ls in
499
	     uc, Dlet (ls, e) :: acc
500 501 502 503 504 505
	 | Pgm_ptree.Dletrec dl -> 
	     let denv = create_denv uc in
	     let _, dl = dletrec denv dl in
	     let _, dl = letrec uc Mstr.empty dl in
	     let one uc (v,_,_,_ as r) =
	       let tyl, ty = uncurrying uc v.vs_ty in
506
	       let id = id_fresh v.vs_name.id_string in
507
	       let ls = create_lsymbol id tyl (Some ty) in
508
	       add_decl uc ls, (ls, r)
509 510 511
	     in
	     let uc, dl = map_fold_left one uc dl in
	     uc, Dletrec dl :: acc
512 513 514 515 516 517
	 | Pgm_ptree.Dparam (id, tyv) ->
	     let denv = create_denv uc in
	     let tyv = dtype_v denv tyv in
	     let tyv = type_v uc Mstr.empty tyv in
	     let tyl, ty = uncurrying uc (purify uc tyv) in
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
518
	     let uc = add_decl uc ls in
519
	     uc, Dparam (ls, tyv) :: acc
520 521 522 523 524 525 526 527 528
	 | Pgm_ptree.Dexn (id, ty) ->
	     let tyl = match ty with
	       | None -> []
	       | Some ty -> [type_type uc ty]
	     in
	     let exn = ty_app (ts_exn uc) [] in
	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some exn) in
	     let uc = add_decl uc ls in
	     uc, acc
529
      )
530 531 532
      (uc, []) dl
  in
  uc, List.rev dl
533 534 535 536 537 538

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)
539 540 541 542 543 544 545 546

(* 

TODO:
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified

*)