mlw_typing.ml 46.7 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
23
open Ident
24 25 26
open Ty
open Term
open Decl
27 28 29
open Theory
open Env
open Ptree
30
open Mlw_dtree
31
open Mlw_ty
32
open Mlw_ty.T
33 34
open Mlw_expr
open Mlw_decl
35
open Mlw_pretty
36
open Mlw_module
Andrei Paskevich's avatar
Andrei Paskevich committed
37
open Mlw_wp
38
open Mlw_dty
39

40 41
(** errors *)

42
exception DuplicateProgVar of string
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
exception DuplicateTypeVar of string
(*
exception PredicateExpected
exception TermExpected
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundType of string list
*)
exception UnboundTypeVar of string
exception UnboundSymbol of string list

let error = Loc.error
let errorm = Loc.errorm

59 60
let qloc = Typing.qloc
let print_qualid = Typing.print_qualid
61 62 63

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
64 65 66
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
(*
  | PredicateExpected ->
      Format.fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      Format.fprintf fmt "syntax error: term expected"
  | FSymExpected ls ->
      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
  | ClashTheory s ->
      Format.fprintf fmt "Clash with previous theory %s" s
  | UnboundTheory q ->
      Format.fprintf fmt "unbound theory %a" print_qualid q
  | UnboundType sl ->
      Format.fprintf fmt "Unbound type '%a'"
        (Pp.print_list Pp.dot Pp.pp_print_string) sl
*)
  | UnboundTypeVar s ->
      Format.fprintf fmt "unbound type variable '%s" s
  | UnboundSymbol sl ->
      Format.fprintf fmt "Unbound symbol '%a'"
        (Pp.print_list Pp.dot Format.pp_print_string) sl
  | _ -> raise e)

(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)

93 94 95 96
type denv = {
  uc     : module_uc;
  locals : (tvars * dity) Mstr.t;
  tvars  : tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
97
  uloc   : Ptree.loc option;
98
}
99

100 101 102 103
let create_denv uc = {
  uc     = uc;
  locals = Mstr.empty;
  tvars  = empty_tvars;
Andrei Paskevich's avatar
Andrei Paskevich committed
104
  uloc   = None;
105
}
106

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
(** Typing type expressions *)

let rec dity_of_pty ~user denv = function
  | Ptree.PPTtyvar id ->
      create_user_type_variable id
  | Ptree.PPTtyapp (pl, p) ->
      let dl = List.map (dity_of_pty ~user denv) pl in
      let x = Typing.string_list_of_qualid [] p in
      begin
        try
          let its = ns_find_it (get_namespace denv.uc) x in
          its_app ~user its dl
        with Not_found -> try
          let ts = ns_find_ts (Theory.get_namespace (get_theory denv.uc)) x in
          ts_app ts dl
        with Not_found ->
123
          errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
124 125 126
      end
  | Ptree.PPTtuple pl ->
      ts_app (ts_tuple (List.length pl)) (List.map (dity_of_pty ~user denv) pl)
127 128 129

(** Typing program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
130
let dity_int  = ts_app ts_int  []
131
let dity_real = ts_app ts_real []
132
let dity_bool = ts_app ts_bool []
Andrei Paskevich's avatar
Andrei Paskevich committed
133 134
let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
135

136
let expected_type ?(weak=false) e dity =
137
  unify ~weak e.de_type dity
138

139 140 141 142 143 144 145 146
let rec extract_labels labs loc e = match e.Ptree.expr_desc with
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (s :: labs) loc e
  | Ptree.Enamed (Ptree.Lpos p, e) -> extract_labels labs (Some p) e
  | Ptree.Ecast  (e, ty) ->
      let labs, loc, d = extract_labels labs loc e in
      labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
  | e -> List.rev labs, loc, e

147 148 149
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
150

151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
    | [{ vtv_ity = { ity_node = Ityapp (its,_,_) }}] -> its
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
    | [cs,pjl] -> cs, List.map (exn_option (BadRecordField pl.pl_ls)) pjl
    | _ -> raise (BadRecordField pl.pl_ls) in
  let pjs = List.fold_left (fun s pj -> Sls.add pj.pl_ls s) Sls.empty pjl in
  let flm = List.fold_left (fun m (pj,v) -> let pj = pj.pl_ls in
    if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
      Mls.add_new (DuplicateRecordField (cs.pl_ls,pj)) pj v m)
    Mls.empty fll
  in
  cs,pjl,flm

171
let find_field uc (p,e) =
172 173 174
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PL pl -> (pl,e)
175 176
    | _ -> errorm ~loc:(qloc p) "bad record field %a" print_qualid p
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
177

178
let find_pure_field uc (p,e) =
179 180
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ls (Theory.get_namespace (get_theory uc)) x, e
181
  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
182

183 184
let pure_record uc = function
  | [] -> raise Decl.EmptyRecord
185 186 187 188 189 190
  | (p,_)::_ ->
      let x = Typing.string_list_of_qualid [] p in
      begin try ignore (ns_find_ps (get_namespace uc) x); false
      with Not_found -> true end

let hidden_pl ~loc pl =
191 192 193
  { de_desc = DEglobal_pl pl;
    de_type = specialize_plsymbol pl;
    de_loc  = loc; de_lab = [] }
194 195

let hidden_ls ~loc ls =
196 197 198
  { de_desc = DEglobal_ls ls;
    de_type = specialize_lsymbol ls;
    de_loc  = loc; de_lab = [] }
199 200

(* helper functions for let-expansion *)
201
let test_var e = match e.de_desc with
202 203 204 205 206
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
207 208 209 210
  { de_desc = DElocal "q";
    de_type = e.de_type;
    de_loc  = e.de_loc;
    de_lab  = [] }
211

212 213 214 215
let mk_id s loc =
  { id = s; id_loc = loc; id_lab = [] }

let mk_dexpr desc dity loc labs =
216
  { de_desc = desc; de_type = dity; de_loc = loc; de_lab = labs }
217

Andrei Paskevich's avatar
Andrei Paskevich committed
218
let mk_let ~loc ~uloc e (desc,dity) =
219
  if test_var e then desc, dity else
Andrei Paskevich's avatar
Andrei Paskevich committed
220
  let loc = def_option loc uloc in
221 222
  let e1 = mk_dexpr desc dity loc [] in
  DElet (mk_id "q" loc, e, e1), dity
223

224 225 226 227 228 229 230
(* patterns *)

let add_var id dity denv =
  let tvars = add_tvars denv.tvars dity in
  let locals = Mstr.add id.id (tvars,dity) denv.locals in
  { denv with locals = locals; tvars = tvars }

231
let specialize_qualid uc p =
232 233 234 235 236
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
    | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
    | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
237 238
    | PX xs ->
        errorm ~loc:(qloc p) "unexpected exception symbol %a" print_xs xs
239 240 241 242
  with Not_found -> try
    let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
    DEglobal_ls ls, specialize_lsymbol ls
  with Not_found ->
243
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
244

245
let find_xsymbol uc p =
Andrei Paskevich's avatar
Andrei Paskevich committed
246 247
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
248
    | PX xs -> xs
249
    | _ -> errorm ~loc:(qloc p) "exception symbol expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
250
  with Not_found ->
251
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
Andrei Paskevich's avatar
Andrei Paskevich committed
252

253
let find_variant_ls uc p =
254 255
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
256
    | _ -> errorm ~loc:(qloc p) "%a is not a binary relation" print_qualid p
257 258 259
  with Not_found -> try
    match ns_find_ls (Theory.get_namespace (get_theory uc)) x with
      | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
260 261
      | ls ->
          errorm ~loc:(qloc p) "%a is not a binary relation" Pretty.print_ls ls
262
  with Not_found ->
263
    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
264

265 266 267 268 269
let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
  | Ptree.PPpwild ->
      PPwild, create_type_variable (), denv
  | Ptree.PPpvar id ->
      let dity = create_type_variable () in
270
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
271
  | Ptree.PPpapp (q,ppl) ->
272
      let sym, dity = specialize_qualid denv.uc q in
273
      dpat_app denv (mk_dexpr sym dity loc []) ppl
274
  | Ptree.PPprec fl when pure_record denv.uc fl ->
275
      let kn = Theory.get_known (get_theory denv.uc) in
276
      let fl = List.map (find_pure_field denv.uc) fl in
277 278 279 280 281
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj flm in
      dpat_app denv (hidden_ls ~loc cs) (List.map get_val pjl)
  | Ptree.PPprec fl ->
282
      let fl = List.map (find_field denv.uc) fl in
283 284 285 286 287 288 289 290 291 292 293 294 295 296
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj.pl_ls flm in
      dpat_app denv (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
      dpat_app denv (hidden_ls ~loc cs) ppl
  | Ptree.PPpor (pp1, pp2) ->
      let pp1, dity1, denv = dpattern denv pp1 in
      let pp2, dity2, denv = dpattern denv pp2 in
      Loc.try2 loc unify dity1 dity2;
      PPor (pp1, pp2), dity1, denv
  | Ptree.PPpas (pp, id) ->
      let pp, dity, denv = dpattern denv pp in
297
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
298

299
and dpat_app denv ({ de_loc = loc } as de) ppl =
300 301 302
  let add_pp pp (ppl, tyl, denv) =
    let pp,ty,denv = dpattern denv pp in pp::ppl,ty::tyl,denv in
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
303
  let pp = match de.de_desc with
304 305
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> PPlapp (ls, ppl)
306 307
    | DEglobal_pv pv -> errorm ~loc "%a is not a constructor" print_pv pv
    | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
308 309 310
    | _ -> assert false
  in
  let res = create_type_variable () in
311
  Loc.try2 loc unify de.de_type (make_arrow_type tyl res);
312 313
  pp, res, denv

314 315
(* specifications *)

316 317 318 319 320 321 322 323
let dbinders denv bl =
  let dbinder (id,pty) (denv,bl,tyl) =
    let dity = match pty with
      | Some pty -> dity_of_pty ~user:true denv pty
      | None -> create_type_variable () in
    add_var id dity denv, (id,false,dity)::bl, dity::tyl
  in
  List.fold_right dbinder bl (denv,[],[])
324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343

let deff_of_peff uc pe =
  { deff_reads  = List.map (fun le -> false, le) pe.pe_reads;
    deff_writes = List.map (fun le -> false, le) pe.pe_writes;
    deff_raises = List.map (fun q -> false, find_xsymbol uc q) pe.pe_raises; }

let dxpost uc ql = List.map (fun (q,f) -> find_xsymbol uc q, f) ql

let rec dtype_c denv tyc =
  let tyv, dity = dtype_v denv tyc.pc_result_type in
  { dc_result = tyv;
    dc_effect = deff_of_peff denv.uc tyc.pc_effect;
    dc_pre    = tyc.pc_pre;
    dc_post   = fst tyc.pc_post;
    dc_xpost  = dxpost denv.uc (snd tyc.pc_post); },
  dity

and dtype_v denv = function
  | Tpure pty ->
      let dity = dity_of_pty ~user:true denv pty in
344
      DSpecV (false,dity), dity
345 346 347 348
  | Tarrow (bl,tyc) ->
      let denv,bl,tyl = dbinders denv bl in
      let tyc,dity = dtype_c denv tyc in
      DSpecA (bl,tyc), make_arrow_type tyl dity
349

350 351 352 353 354 355 356 357
let dvariant uc = function
  | Some (le, Some q) -> [le, Some (find_variant_ls uc q)]
  | Some (le, None) -> [le, None]
  | None -> []
(* TODO: accept a list of variants in the surface language
  List.map (fun (le,q) -> le, Util.option_map (find_variant_ls uc) q) var
*)

358
(* expressions *)
359

360 361 362
let de_unit ~loc = hidden_ls ~loc (fs_tuple 0)

let de_app e el =
363
  let res = create_type_variable () in
364
  let tyl = List.map (fun a -> a.de_type) el in
365 366 367
  expected_type e (make_arrow_type tyl res);
  DEapply (e, el), res

Andrei Paskevich's avatar
Andrei Paskevich committed
368
let rec dexpr denv e =
369
  let loc = e.Ptree.expr_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
370 371
  let labs, uloc, d = extract_labels [] denv.uloc e in
  let denv = { denv with uloc = uloc } in
372
  let d, ty = de_desc denv loc d in
Andrei Paskevich's avatar
Andrei Paskevich committed
373
  let loc = def_option loc uloc in
374
  mk_dexpr d ty loc labs
375

376
and de_desc denv loc = function
377 378
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
379 380 381
      let tvs, dity = Mstr.find x denv.locals in
      let dity = specialize_scheme tvs dity in
      DElocal x, dity
382
  | Ptree.Eident p ->
383
      specialize_qualid denv.uc p
384 385
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
386
      let el = List.map (dexpr denv) el in
387
      de_app (dexpr denv e) el
388
  | Ptree.Elet (id, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
389
      let e1 = dexpr denv e1 in
390 391
      let dity = e1.de_type in
      let tvars = match e1.de_desc with
Andrei Paskevich's avatar
Andrei Paskevich committed
392 393
        | DEfun _ -> denv.tvars
        | _ -> add_tvars denv.tvars dity in
394 395
      let locals = Mstr.add id.id (tvars, dity) denv.locals in
      let denv = { denv with locals = locals; tvars = tvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
396
      let e2 = dexpr denv e2 in
397
      DElet (id, e1, e2), e2.de_type
Andrei Paskevich's avatar
Andrei Paskevich committed
398
  | Ptree.Eletrec (rdl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
399
      let rdl = dletrec denv rdl in
400
      let add_one denv ({ id = id }, dity, _) =
401 402
        { denv with locals = Mstr.add id (denv.tvars, dity) denv.locals } in
      let denv = List.fold_left add_one denv rdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
403
      let e1 = dexpr denv e1 in
404
      DEletrec (rdl, e1), e1.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
405
  | Ptree.Efun (bl, tr) ->
406
      let lam, dity = dlambda denv bl None tr in
407
      DEfun lam, dity
408
  | Ptree.Ecast (e1, pty) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
409
      let e1 = dexpr denv e1 in
410
      expected_type e1 (dity_of_pty ~user:false denv pty);
411
      e1.de_desc, e1.de_type
412 413
  | Ptree.Enamed _ ->
      assert false
414
  | Ptree.Esequence (e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
415
      let e1 = dexpr denv e1 in
416
      expected_type e1 dity_unit;
Andrei Paskevich's avatar
Andrei Paskevich committed
417
      let e2 = dexpr denv e2 in
418
      DElet (mk_id "_" loc, e1, e2), e2.de_type
419
  | Ptree.Eif (e1, e2, e3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
420
      let e1 = dexpr denv e1 in
421
      expected_type e1 dity_bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
422 423
      let e2 = dexpr denv e2 in
      let e3 = dexpr denv e3 in
424 425
      expected_type e3 e2.de_type;
      DEif (e1, e2, e3), e2.de_type
426 427
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
Andrei Paskevich's avatar
Andrei Paskevich committed
428
      let el = List.map (dexpr denv) el in
429 430
      de_app (hidden_ls ~loc ls) el
  | Ptree.Erecord fl when pure_record denv.uc fl ->
431
      let kn = Theory.get_known (get_theory denv.uc) in
432
      let fl = List.map (find_pure_field denv.uc) fl in
433 434
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
435
        | Some e -> dexpr denv e
436
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
437
      de_app (hidden_ls ~loc cs) (List.map get_val pjl)
438
  | Ptree.Erecord fl ->
439
      let fl = List.map (find_field denv.uc) fl in
440 441
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
442
        | Some e -> dexpr denv e
443
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
444 445
      de_app (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.Eupdate (e1, fl) when pure_record denv.uc fl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
446
      let e1 = dexpr denv e1 in
447 448
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
449
      let fl = List.map (find_pure_field denv.uc) fl in
450 451
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
452
        | Some e -> dexpr denv e
453
        | None ->
454
            let d, dity = de_app (hidden_ls ~loc pj) [e0] in
455
            mk_dexpr d dity loc [] in
456
      let res = de_app (hidden_ls ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
457
      mk_let ~loc ~uloc:denv.uloc e1 res
458
  | Ptree.Eupdate (e1, fl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
459
      let e1 = dexpr denv e1 in
460
      let e0 = mk_var e1 in
461
      let fl = List.map (find_field denv.uc) fl in
462 463
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
Andrei Paskevich's avatar
Andrei Paskevich committed
464
        | Some e -> dexpr denv e
465
        | None ->
466
            let d, dity = de_app (hidden_pl ~loc pj) [e0] in
467
            mk_dexpr d dity loc [] in
468
      let res = de_app (hidden_pl ~loc cs) (List.map get_val pjl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
469
      mk_let ~loc ~uloc:denv.uloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
470
  | Ptree.Eassign (e1, q, e2) ->
471 472
      let fl = { expr_desc = Eident q; expr_loc = loc } in
      let e1 = { expr_desc = Eapply (fl,e1); expr_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
473 474
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
475
      expected_type ~weak:true e2 e1.de_type;
Andrei Paskevich's avatar
Andrei Paskevich committed
476
      DEassign (e1, e2), dity_unit
477 478 479 480 481
  | Ptree.Econstant (ConstInt _ as c) ->
      DEconstant c, dity_int
  | Ptree.Econstant (ConstReal _ as c) ->
      DEconstant c, dity_real
  | Ptree.Enot e1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
482
      let e1 = dexpr denv e1 in
483 484 485
      expected_type e1 dity_bool;
      DEnot e1, dity_bool
  | Ptree.Elazy (op, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
486 487
      let e1 = dexpr denv e1 in
      let e2 = dexpr denv e2 in
488 489 490
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
      DElazy (op, e1, e2), dity_bool
491
  | Ptree.Ematch (e1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
492
      let e1 = dexpr denv e1 in
493 494 495
      let res = create_type_variable () in
      let branch (pp,e) =
        let ppat, dity, denv = dpattern denv pp in
Andrei Paskevich's avatar
Andrei Paskevich committed
496
        let e = dexpr denv e in
497
        Loc.try2 pp.pat_loc unify dity e1.de_type;
498 499 500
        expected_type e res;
        ppat, e in
      DEmatch (e1, List.map branch bl), res
Andrei Paskevich's avatar
Andrei Paskevich committed
501 502
  | Ptree.Eraise (q, e1) ->
      let res = create_type_variable () in
503
      let xs = find_xsymbol denv.uc q in
504
      let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
505
      let e1 = match e1 with
Andrei Paskevich's avatar
Andrei Paskevich committed
506
        | Some e1 -> dexpr denv e1
507
        | None when ity_equal xs.xs_ity ity_unit -> de_unit ~loc
Andrei Paskevich's avatar
Andrei Paskevich committed
508 509 510 511
        | _ -> errorm ~loc "exception argument expected" in
      expected_type e1 dity;
      DEraise (xs, e1), res
  | Ptree.Etry (e1, cl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
512
      let e1 = dexpr denv e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
513
      let branch (q, id, e) =
514
        let xs = find_xsymbol denv.uc q in
515
        let dity = specialize_xsymbol xs in
Andrei Paskevich's avatar
Andrei Paskevich committed
516 517
        let id, denv = match id with
          | Some id -> id, add_var id dity denv
518
          | None -> mk_id "void" loc, denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
519
        xs, id, dexpr denv e
Andrei Paskevich's avatar
Andrei Paskevich committed
520 521
      in
      let cl = List.map branch cl in
522
      DEtry (e1, cl), e1.de_type
523
  | Ptree.Eabsurd ->
524
      DEabsurd, create_type_variable ()
525 526
  | Ptree.Eassert (ak, lexpr) ->
      DEassert (ak, lexpr), dity_unit
Andrei Paskevich's avatar
Andrei Paskevich committed
527 528
  | Ptree.Emark (id, e1) ->
      let e1 = dexpr denv e1 in
529
      DEmark (id, e1), e1.de_type
530
  | Ptree.Eany tyc ->
531 532
      let tyc, dity = dtype_c denv tyc in
      DEany tyc, dity
533 534 535 536 537 538 539 540 541 542 543 544 545 546
  | Ptree.Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
      let e1 = dexpr denv e1 in
      let var = dvariant denv.uc var in
      expected_type e1 dity_unit;
      DEloop (var,inv,e1), e1.de_type
  | Ptree.Efor (id, efrom, dir, eto, inv, e1) ->
      let efrom = dexpr denv efrom in
      let eto = dexpr denv eto in
      let denv = add_var id dity_int denv in
      let e1 = dexpr denv e1 in
      expected_type efrom dity_int;
      expected_type eto dity_int;
      expected_type e1 dity_unit;
      DEfor (id,efrom,dir,eto,inv,e1), e1.de_type
547
  | Ptree.Eabstract (_e1, _post) ->
548 549
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
550
and dletrec denv rdl =
Andrei Paskevich's avatar
Andrei Paskevich committed
551 552 553
  (* add all functions into environment *)
  let add_one denv (id, bl, var, tr) =
    let res = create_type_variable () in
Andrei Paskevich's avatar
Andrei Paskevich committed
554
    add_var id res denv, (id, res, bl, var, tr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
555 556 557
  let denv, rdl = Util.map_fold_left add_one denv rdl in
  (* then type-check all of them and unify *)
  let type_one (id, res, bl, var, tr) =
558
    let lam, dity = dlambda denv bl var tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
559
    Loc.try2 id.id_loc unify dity res;
560
    id, dity, lam in
561
  List.map type_one rdl
Andrei Paskevich's avatar
Andrei Paskevich committed
562

563 564
and dlambda denv bl var (p, e, (q, xq)) =
  let denv,bl,tyl = dbinders denv bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
565
  let e = dexpr denv e in
566 567 568
  let var = dvariant denv.uc var in
  let xq = dxpost denv.uc xq in
  (bl, var, p, e, q, xq), make_arrow_type tyl e.de_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569

570
(** stage 2 *)
571

Andrei Paskevich's avatar
Andrei Paskevich committed
572 573 574 575 576
type lenv = {
  mod_uc   : module_uc;
  let_vars : let_var Mstr.t;
  log_vars : vsymbol Mstr.t;
  log_denv : Typing.denv;
577 578
}

Andrei Paskevich's avatar
Andrei Paskevich committed
579
let create_lenv uc = {
580
  mod_uc   = use_export_theory uc Mlw_wp.th_mark;
581 582 583 584 585 586 587 588 589 590 591
  let_vars = Mstr.empty;
  log_vars = Mstr.empty;
  log_denv = Typing.denv_empty;
}

let rec dty_of_ty ty = match ty.ty_node with
  | Ty.Tyvar v ->
      Typing.create_user_type_var v.tv_name.id_string
  | Ty.Tyapp (ts, tyl) ->
      Denv.tyapp ts (List.map dty_of_ty tyl)

592 593 594 595
let create_post lenv x ty f =
  let res = create_vsymbol (id_fresh x) ty in
  let log_vars = Mstr.add x res lenv.log_vars in
  let log_denv = Typing.add_var x (dty_of_ty ty) lenv.log_denv in
596 597
  let f = Typing.type_fmla (get_theory lenv.mod_uc) log_denv log_vars f in
  create_post res f
598 599 600 601

let create_pre lenv f =
  Typing.type_fmla (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars f

602 603 604 605
let create_variant lenv (t,r) =
  let t =
    Typing.type_term (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars t in
  { v_term = t; v_rel = r }
Andrei Paskevich's avatar
Andrei Paskevich committed
606

Andrei Paskevich's avatar
Andrei Paskevich committed
607
let add_local x lv lenv = match lv with
608
  | LetA _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
609
      { lenv with let_vars = Mstr.add x lv lenv.let_vars }
610 611
  | LetV pv ->
      let dty = dty_of_ty pv.pv_vs.vs_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
612 613 614 615
      { mod_uc   = lenv.mod_uc;
        let_vars = Mstr.add x lv lenv.let_vars;
        log_vars = Mstr.add x pv.pv_vs lenv.log_vars;
        log_denv = Typing.add_var x dty lenv.log_denv }
616

617 618
exception DuplicateException of xsymbol

619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653
let binders lenv bl =
  let binder lenv (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
    let pv = create_pvsymbol (Denv.create_user_id id) vtv in
    add_local id.id (LetV pv) lenv, pv in
  Util.map_fold_left binder lenv bl

let xpost lenv xq =
  let add_exn m (xs,f) =
    let f = create_post lenv "result" (ty_of_ity xs.xs_ity) f in
    Mexn.add_new (DuplicateException xs) xs f m in
  List.fold_left add_exn Mexn.empty xq

let eff_of_deff _lenv _deff = eff_empty (* TODO *)

let rec type_c lenv dtyc =
  let result = type_v lenv dtyc.dc_result in
  let ty = match result with
    | SpecV v -> ty_of_ity v.vtv_ity
    | SpecA _ -> ty_unit in
  { c_pre    = create_pre lenv dtyc.dc_pre;
    c_effect = eff_of_deff lenv dtyc.dc_effect;
    c_result = result;
    c_post   = create_post lenv "result" ty dtyc.dc_post;
    c_xpost  = xpost lenv dtyc.dc_xpost; }

and type_v lenv = function
  | DSpecV (ghost,v) ->
      SpecV (vty_value ~ghost (ity_of_dity v))
  | DSpecA (bl,tyc) ->
      let lenv, pvl = binders lenv bl in
      SpecA (pvl, type_c lenv tyc)

(* expressions *)

654
let rec expr lenv de = match de.de_desc with
655
  | DElocal x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
656 657
      assert (Mstr.mem x lenv.let_vars);
      begin match Mstr.find x lenv.let_vars with
658
      | LetV pv -> e_value pv
659
      | LetA ps -> e_cast ps (vty_of_dity de.de_type)
660
      end
661
  | DElet (x, { de_desc = DEfun lam }, de2) ->
662 663
      let def = expr_fun lenv x lam in
      let lenv = add_local x.id (LetA def.rec_ps) lenv in
Andrei Paskevich's avatar
Andrei Paskevich committed
664
      let e2 = expr lenv de2 in
665 666
      e_rec [def] e2
  | DEfun lam ->
667
      let x = mk_id "fn" de.de_loc in
668
      let def = expr_fun lenv x lam in
669 670 671
      let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
      e_rec [def] e2
  | DElet (x, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
672
      let e1 = expr lenv de1 in
673
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
674 675
      let lenv = add_local x.id def1.let_var lenv in
      let e2 = expr lenv de2 in
676
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
677
  | DEletrec (rdl, de1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
678
      let rdl = expr_rec lenv rdl in
679
      let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
Andrei Paskevich's avatar
Andrei Paskevich committed
680
      let e1 = expr (List.fold_right add_rd rdl lenv) de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
681
      e_rec rdl e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682
  | DEapply (de1, del) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
683
      let el = List.map (expr lenv) del in
684 685 686
      begin match de1.de_desc with
        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.de_type)
        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
687
        | _               -> e_app (expr lenv de1) el
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
688
      end
689 690 691
  | DEglobal_pv pv ->
      e_value pv
  | DEglobal_ps ps ->
692
      e_cast ps (vty_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
693 694
  | DEglobal_pl pl ->
      assert (pl.pl_ls.ls_args = []);
695
      e_plapp pl [] (ity_of_dity de.de_type)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696
  | DEglobal_ls ls ->
Andrei Paskevich's avatar
Andrei Paskevich committed
697
      assert (ls.ls_args = []);
698
      e_lapp ls [] (ity_of_dity de.de_type)
699
  | DEif (de1, de2, de3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
700
      e_if (expr lenv de1) (expr lenv de2) (expr lenv de3)
Andrei Paskevich's avatar
Andrei Paskevich committed
701
  | DEassign (de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
702
      e_assign (expr lenv de1) (expr lenv de2)
703 704 705
  | DEconstant c ->
      e_const c
  | DElazy (LazyAnd, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
706
      e_lazy_and (expr lenv de1) (expr lenv de2)
707
  | DElazy (LazyOr, de1, de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
708
      e_lazy_or (expr lenv de1) (expr lenv de2)
709
  | DEnot de1 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
710
      e_not (expr lenv de1)
711
  | DEmatch (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
712
      let e1 = expr lenv de1 in
713 714 715
      let vtv = vtv_of_expr e1 in
      let branch (pp,de) =
        let vm, pp = make_ppattern pp vtv in
Andrei Paskevich's avatar
Andrei Paskevich committed
716 717
        let lenv = Mstr.fold (fun s pv -> add_local s (LetV pv)) vm lenv in
        pp, expr lenv de in
718
      e_case e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
719 720 721 722 723
  | DEassert (ak, f) ->
      let ak = match ak with
        | Ptree.Aassert -> Aassert
        | Ptree.Aassume -> Aassume
        | Ptree.Acheck  -> Acheck in
724
      e_assert ak (create_pre lenv f)
725
  | DEabsurd ->
726
      e_absurd (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
727
  | DEraise (xs, de1) ->
728
      e_raise xs (expr lenv de1) (ity_of_dity de.de_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
729
  | DEtry (de1, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
730
      let e1 = expr lenv de1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
731 732 733
      let branch (xs,id,de) =
        let vtv = vty_value xs.xs_ity in
        let pv = create_pvsymbol (Denv.create_user_id id) vtv in
Andrei Paskevich's avatar
Andrei Paskevich committed
734 735
        let lenv = add_local id.id (LetV pv) lenv in
        xs, pv, expr lenv de in
Andrei Paskevich's avatar
Andrei Paskevich committed
736
      e_try e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
737 738 739 740
  | DEmark (x, de1) ->
      let ld = create_let_defn (Denv.create_user_id x) e_setmark in
      let lenv = add_local x.id ld.let_var lenv in
      e_let ld (expr lenv de1)
741 742
  | DEany dtyc ->
      e_any (type_c lenv dtyc)
743 744
  | DEghost de1 ->
      e_ghost (expr lenv de1)
745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763
  | DEloop (var,inv,de1) ->
      let inv = match inv with
        | Some inv -> create_pre lenv inv
        | None -> t_true in
      let var = List.map (create_variant lenv) var in
      e_loop inv var (expr lenv de1)
  | DEfor (x,defrom,dir,deto,inv,de1) ->
      let efrom = expr lenv defrom in
      let eto = expr lenv deto in
      let pv = create_pvsymbol (Denv.create_user_id x) (vty_value ity_int) in
      let lenv = add_local x.id (LetV pv) lenv in
      let dir = match dir with
        | Ptree.To -> To
        | Ptree.Downto -> DownTo in
      let inv = match inv with
        | Some inv -> create_pre lenv inv
        | None -> t_true in
      let e1 = expr lenv de1 in
      e_for pv efrom dir eto inv e1
764

Andrei Paskevich's avatar
Andrei Paskevich committed
765
and expr_rec lenv rdl =
766
  let step1 lenv (id, dity, lam) =
Andrei Paskevich's avatar
Andrei Paskevich committed
767 768 769
    let vta = match vty_of_dity dity with
      | VTarrow vta -> vta
      | VTvalue _ -> assert false in
770
    let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
771
    add_local id.id (LetA ps) lenv, (ps, lam) in
Andrei Paskevich's avatar
Andrei Paskevich committed
772
  let lenv, rdl = Util.map_fold_left step1 lenv rdl in
773
  let step2 (ps, lam) = ps, expr_lam lenv lam in
Andrei Paskevich's avatar
Andrei Paskevich committed
774 775
  create_rec_defn (List.map step2 rdl)

776 777
and expr_fun lenv x lam =
  let lam = expr_lam lenv lam in
778
  create_fun_defn (Denv.create_user_id x) lam
Andrei Paskevich's avatar
Andrei Paskevich committed
779

780
and expr_lam lenv (bl, var, p, e, q, xq) =
781
  let lenv, pvl = binders lenv bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
782
  let e = expr lenv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
783
  let ty = match e.e_vty with
Andrei Paskevich's avatar
Andrei Paskevich committed
784
    | VTarrow _ -> ty_unit
785 786
    | VTvalue vtv -> ty_of_ity vtv.vtv_ity
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
787
  { l_args = pvl;
788
    l_variant = List.map (create_variant lenv) var;
789
    l_pre = create_pre lenv p;
Andrei Paskevich's avatar
Andrei Paskevich committed
790
    l_expr = e;
791
    l_post = create_post lenv "result" ty q;
792
    l_xpost = xpost lenv xq; }
793

794 795
(** Type declaration *)

796
type tys = ProgTS of itysymbol | PureTS of tysymbol
797 798 799 800 801 802 803 804 805

let find_tysymbol q uc =
  let loc = Typing.qloc q in
  let sl = Typing.string_list_of_qualid [] q in
  try ProgTS (ns_find_it (get_namespace uc) sl)
  with Not_found ->
  try PureTS (ns_find_ts (Theory.get_namespace (get_theory uc)) sl)
  with Not_found -> error ~loc (UnboundSymbol sl)