typing.ml 39 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Format
14
open Pp
15
open Ident
16
open Ptree
17
open Ty
18
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
19
open Decl
20
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
21
open Env
22
open Denv
Andrei Paskevich's avatar
Andrei Paskevich committed
23

24 25
(** errors *)

26
exception DuplicateVar of string
27 28 29
exception DuplicateTypeVar of string
exception PredicateExpected
exception TermExpected
30 31
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
32
exception ClashTheory of string
33
(* dead code
34
exception UnboundTheory of qualid
35
*)
36
exception UnboundTypeVar of string
37
(* dead code
38
exception UnboundType of string list
39
*)
40
exception UnboundSymbol of qualid
41

42 43 44
let error = Loc.error

let errorm = Loc.errorm
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45

46
let rec print_qualid fmt = function
47
  | Qident s -> fprintf fmt "%s" s.id
48
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
49

50
let () = Exn_printer.register (fun fmt e -> match e with
51
  | DuplicateTypeVar s ->
52 53 54
      fprintf fmt "Duplicate type parameter %s" s
  | DuplicateVar s ->
      fprintf fmt "Duplicate variable %s" s
55 56 57 58
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
59 60 61 62
  | FSymExpected ls ->
      fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
63
  | ClashTheory s ->
64
      fprintf fmt "Clash with previous theory %s" s
65
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66 67
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
68
*)
69 70
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
71
(* dead code
72 73
  | UnboundType sl ->
       fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
74
*)
75 76
  | UnboundSymbol q ->
       fprintf fmt "Unbound symbol '%a'" print_qualid q
77
  | _ -> raise e)
78

79
let debug_parse_only = Debug.register_flag "parse_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
80
  ~desc:"Stop@ after@ parsing."
81
let debug_type_only  = Debug.register_flag "type_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
82
  ~desc:"Stop@ after@ type-checking."
83

84 85
(** Environments *)

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
97 98
let term_expected_type ~loc ty1 ty2 =
  errorm ~loc
99
    "This term has type %a@ but is expected to have type@ %a"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100 101
    print_dty ty1 print_dty ty2

Andrei Paskevich's avatar
Andrei Paskevich committed
102 103 104
let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

105 106 107 108
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

109
let create_user_tv =
110 111
  let hs = Hstr.create 17 in
  fun s -> try Hstr.find hs s with Not_found ->
112
  let tv = create_tvsymbol (id_fresh s) in
113
  Hstr.add hs s tv;
114 115 116 117 118 119
  tv

(* TODO: shouldn't we localize this ident? *)
let create_user_type_var x =
  tyuvar (create_user_tv x)

120
type denv = {
121 122
  dvars : dty Mstr.t;    (* local variables, to be bound later *)
  gvars : qualid -> vsymbol option; (* global variables, for programs *)
123 124
}

125 126
let denv_empty = { dvars = Mstr.empty; gvars = Util.const None }
let denv_empty_with_globals gv = { dvars = Mstr.empty; gvars = gv }
127

128
(* dead code
129 130
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
131
*)
132
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
133

134
(* dead code
135 136
let print_denv fmt denv =
  Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars
137
*)
138

139 140 141 142 143 144 145 146 147 148
(* parsed types -> intermediate types *)

let rec qloc = function
  | Qident x -> x.id_loc
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc

let rec string_list_of_qualid acc = function
  | Qident id -> id.id :: acc
  | Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p

149 150
(* lazy declaration of tuples *)

151 152 153
let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl)
let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls)
154
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
155
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
156
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
157

158
let find_ns get_id find p ns =
159 160
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
161 162 163 164
  try
    let r = find ns sl in
    if Debug.test_flag Glob.flag then Glob.use loc (get_id r);
    r
165
  with Not_found -> error ~loc (UnboundSymbol p)
166

167 168
let get_id_prop p = p.pr_name
let find_prop_ns = find_ns get_id_prop ns_find_pr
169 170
let find_prop p uc = find_prop_ns p (get_namespace uc)

171 172
let get_id_ts ts = ts.ts_name
let find_tysymbol_ns = find_ns get_id_ts ns_find_ts
173 174
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

175 176
let get_id_ls ls = ls.ls_name
let find_lsymbol_ns = find_ns get_id_ls ns_find_ls
177 178
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

179 180 181 182 183 184 185 186 187 188 189
let find_fsymbol_ns q ns =
  let ls = find_lsymbol_ns q ns in
  if ls.ls_value = None then error ~loc:(qloc q) (FSymExpected ls) else ls

let find_psymbol_ns q ns =
  let ls = find_lsymbol_ns q ns in
  if ls.ls_value <> None then error ~loc:(qloc q) (PSymExpected ls) else ls

let find_fsymbol q uc = find_fsymbol_ns q (get_namespace uc)
let find_psymbol q uc = find_psymbol_ns q (get_namespace uc)

190 191
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
192
(* dead code
193
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
194
*)
195

196
let rec dty uc = function
197
  | PPTtyvar ({id=x}, _) ->
198
      create_user_type_var x
199
  | PPTtyapp (x, p) ->
200 201 202 203 204 205 206
      let ts = find_tysymbol x uc in
      let tyl = List.map (dty uc) p in
      Loc.try2 (qloc x) tyapp ts tyl
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      tyapp ts (List.map (dty uc) tyl)

207
let rec ty_of_pty uc = function
208
  | PPTtyvar ({id=x}, _) ->
209
      ty_var (create_user_tv x)
210
  | PPTtyapp (x, p) ->
211 212 213 214 215 216 217
      let ts = find_tysymbol x uc in
      let tyl = List.map (ty_of_pty uc) p in
      Loc.try2 (qloc x) ty_app ts tyl
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      ty_app ts (List.map (ty_of_pty uc) tyl)

218 219 220 221 222 223 224 225 226 227
let rec opaque_tvs acc = function
  | Ptree.PPTtyvar (id, true) -> Stv.add (create_user_tv id.id) acc
  | Ptree.PPTtyvar (_, false) -> acc
  | Ptree.PPTtyapp (_, pl)
  | Ptree.PPTtuple pl -> List.fold_left opaque_tvs acc pl

let opaque_tvs args value =
  let acc = Opt.fold opaque_tvs Stv.empty value in
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) acc args

228 229
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
230 231
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
232

233
let specialize_fsymbol p uc =
234
  let s,tl,ty = specialize_lsymbol p uc in
235
  match ty with
236
    | None -> let loc = qloc p in error ~loc TermExpected
237
    | Some ty -> s, tl, ty
238

239
let specialize_psymbol p uc =
240
  let s,tl,ty = specialize_lsymbol p uc in
241 242
  match ty with
    | None -> s, tl
243 244
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

245
let is_psymbol p uc =
246 247
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248

249 250
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251 252 253 254
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

255
(** Typing terms and formulas *)
256 257

let binop = function
258 259 260 261
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
262

Andrei Paskevich's avatar
Andrei Paskevich committed
263
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
264
  let s = ref Sstr.empty in
265
  let add id =
266
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
267 268 269 270
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
271
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
272
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
273
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
274
    | PPpor (p, _) -> check p
275
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
276
  check p
277

278 279
let rec dpat uc env pat =
  let env, n, ty = dpat_node pat.pat_loc uc env pat.pat_desc in
Andrei Paskevich's avatar
Andrei Paskevich committed
280 281
  env, { dp_node = n; dp_ty = ty }

282
and dpat_node loc uc env = function
283
  | PPpwild ->
284
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
285
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
286
  | PPpvar x ->
287
      let ty = fresh_type_var loc in
288
      let env = add_var x.id ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
289 290
      env, Pvar x, ty
  | PPpapp (x, pl) ->
291
      let s, tyl, ty = specialize_fsymbol x uc in
292
      let env, pl = dpat_args s loc uc env tyl pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
293
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
294 295
  | PPprec fl ->
      let renv = ref env in
296 297
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
298
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
299 300
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
301
            let loc = e.pat_loc in
302
            let env,e = dpat uc !renv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
303 304 305
            unify_raise ~loc e.dp_ty ty;
            renv := env;
            e
306 307
        | None ->
            { dp_node = Pwild; dp_ty = ty }
Andrei Paskevich's avatar
Andrei Paskevich committed
308
      in
309
      let al = List.map2 get_val pjl tyl in
310
      !renv, Papp (cs, al), Opt.get ty
311 312 313 314
  | PPptuple pl ->
      let n = List.length pl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) pl in
315
      let env, pl = dpat_args s loc uc env tyl pl in
316
      let ty = tyapp (ts_tuple n) tyl in
317
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
318
  | PPpas (p, x) ->
319
      let env, p = dpat uc env p in
320
      let env = add_var x.id p.dp_ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
321
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
322
  | PPpor (p, q) ->
323 324
      let env, p = dpat uc env p in
      let env, q = dpat uc env q in
Andrei Paskevich's avatar
Andrei Paskevich committed
325
      unify_raise ~loc p.dp_ty q.dp_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
326
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
327

328
and dpat_args ls loc uc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
329
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
330
  if n <> m then error ~loc (BadArity (ls,n,m));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331
  let rec check_arg env = function
332
    | [], [] ->
333
        env, []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
334
    | a :: al, p :: pl ->
335 336 337 338 339
        let loc = p.pat_loc in
        let env, p = dpat uc env p in
        unify_raise ~loc p.dp_ty a;
        let env, pl = check_arg env (al, pl) in
        env, p :: pl
Andrei Paskevich's avatar
Andrei Paskevich committed
340
    | _ ->
341
        assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
342
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
344

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345
let rec trigger_not_a_term_exn = function
346
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347 348 349
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

350
let param_tys uc pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
351
  let s = ref Sstr.empty in
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
  let ty_of_param (loc,id,gh,ty) =
    if gh then Loc.errorm ~loc "ghost parameters are not allowed here";
    Opt.iter (fun { id = id; id_loc = loc } ->
      s := Loc.try3 loc Sstr.add_new (DuplicateVar id) id !s) id;
    ty_of_dty (dty uc ty) in
  List.map ty_of_param pl

let quant_var uc env (id,ty) =
  let ty = match ty with
    | None -> Denv.fresh_type_var id.id_loc
    | Some ty -> dty uc ty in
  add_var id.id ty env, (id,ty)

let quant_vars uc env qvl =
  let s = ref Sstr.empty in
  let add env (({ id = id; id_loc = loc }, _) as qv) =
    s := Loc.try3 loc Sstr.add_new (DuplicateVar id) id !s;
    quant_var uc env qv in
  Lists.map_fold_left add env qvl
371

372
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
373
  | Qident { id = x } when Mstr.mem x env.dvars -> true
374 375
  | _ -> env.gvars x <> None ||
      List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
376 377 378 379 380 381

let apply_highord loc x tl = match List.rev tl with
  | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a]
  | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
  | [] -> assert false

382
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
383
  let n, ty = dterm_node ~localize loc uc env t in
384
  let t = { dt_node = n; dt_ty = ty } in
385 386
  let rec down loc e = match e.dt_node with
    | Tnamed (Lstr _, e) -> down loc e
387 388 389
    | Tnamed (Lpos _, _) -> t
    | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
  in
390 391 392 393
  match localize with
    | Some (Some loc) -> down loc t
    | Some None -> down loc t
    | None -> t
394

395
and dterm_node ~localize loc uc env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
396
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
397
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
398
      let ty = Mstr.find x env.dvars in
399
      Tvar x, ty
400
  | PPvar x when env.gvars x <> None ->
401
      let vs = Opt.get (env.gvars x) in
402
      Tgvar vs, dty_of_ty vs.vs_ty
403
  | PPvar x ->
404
      (* 0-arity symbol (constant) *)
405
      let s, tyl, ty = specialize_fsymbol x uc in
406
      let n = List.length tyl in
Andrei Paskevich's avatar
Andrei Paskevich committed
407
      if n > 0 then error ~loc (BadArity (s,n,0));
408
      Tapp (s, []), ty
409
  | PPapp (x, tl) when check_highord uc env x tl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
410 411
      let tl = apply_highord loc x tl in
      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
412
      let tl = dtype_args ~localize fs_func_app loc uc env atyl tl in
413
      Tapp (fs_func_app, tl), Opt.get aty
414
  | PPapp (x, tl) ->
415
      let s, tyl, ty = specialize_fsymbol x uc in
416
      let tl = dtype_args ~localize s loc uc env tyl tl in
417
      Tapp (s, tl), ty
418 419 420 421
  | PPtuple tl ->
      let n = List.length tl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) tl in
422
      let tl = dtype_args ~localize s loc uc env tyl tl in
423
      let ty = tyapp (ts_tuple n) tyl in
424
      Tapp (s, tl), ty
425 426
  | PPinfix (e1, x, e2)
  | PPinnfix (e1, x, e2) ->
427
      if x.id = "infix <>" then error ~loc TermExpected;
428
      let s, tyl, ty = specialize_fsymbol (Qident x) uc in
429
      let tl = dtype_args ~localize s loc uc env tyl [e1; e2] in
430
      Tapp (s, tl), ty
431
  | PPconst (Number.ConstInt _ as c) ->
432
      Tconst c, tyapp Ty.ts_int []
433
  | PPconst (Number.ConstReal _ as c) ->
434
      Tconst c, tyapp Ty.ts_real []
Andrei Paskevich's avatar
Andrei Paskevich committed
435
  | PPlet (x, e1, e2) ->
436
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
      let ty = e1.dt_ty in
438
      let env = add_var x.id ty env in
439
      let e2 = dterm ~localize uc env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
440
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
441
  | PPmatch (e1, bl) ->
442
      let t1 = dterm ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
443
      let ty1 = t1.dt_ty in
444
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
445
      let branch (p, e) =
446
        let env, p = dpat_list uc env ty1 p in
447
        let loc = e.pp_loc in
448 449
        let e = dterm ~localize uc env e in
        unify_raise ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
450
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
451 452
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
453
      Tmatch (t1, bl), tb
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
454
  | PPnamed (x, e1) ->
455
      let localize = match x with
456
        | Lpos l -> Some (Some l)
457
        | Lstr _ -> localize
458
      in
459
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
460
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461 462
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
463
      let e1 = dterm ~localize uc env e1 in
464
      let ty = dty uc ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
465
      unify_raise ~loc e1.dt_ty ty;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466
      e1.dt_node, ty
467 468
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
469 470
      let e2 = dterm ~localize uc env e2 in
      let e3 = dterm ~localize uc env e3 in
Andrei Paskevich's avatar
Andrei Paskevich committed
471
      unify_raise ~loc e3.dt_ty e2.dt_ty;
472
      Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty
473 474
  | PPeps (b, e1) ->
      let env, (x, ty) = quant_var uc env b in
475
      let e1 = dfmla ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
476
      Teps (x, ty, e1), ty
477
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
478
      let env, uqu = quant_vars uc env uqu in
Andrei Paskevich's avatar
Andrei Paskevich committed
479
      let trigger e =
480 481 482 483
        try
          TRterm (dterm ~localize uc env e)
        with exn when trigger_not_a_term_exn exn ->
          TRfmla (dfmla ~localize uc env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
484 485
      in
      let trl = List.map (List.map trigger) trl in
486
      let e = match q with
487 488
        | PPfunc -> TRterm (dterm ~localize uc env a)
        | PPpred -> TRfmla (dfmla ~localize uc env a)
489 490 491 492
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
Andrei Paskevich's avatar
Andrei Paskevich committed
493
        | TRterm t ->
494
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
495
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
496
              let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty)
Andrei Paskevich's avatar
Andrei Paskevich committed
497 498 499 500 501 502 503 504 505
              uqu ([],t.dt_ty)
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            id, ty, Fapp (ps_equ, [h;t])
Andrei Paskevich's avatar
Andrei Paskevich committed
506
        | TRfmla f ->
507
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
508 509 510 511 512
            let (uid,uty),uqu = match List.rev uqu with
              | uq :: uqu -> uq, List.rev uqu
              | [] -> assert false
            in
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
513 514
              let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty)
              uqu ([], tyapp ts_pred [uty])
Andrei Paskevich's avatar
Andrei Paskevich committed
515 516 517 518 519 520 521 522
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
523
            id, ty, Fbinop (Tiff, Fapp (ps_pred_app, [h;u]), f)
Andrei Paskevich's avatar
Andrei Paskevich committed
524
      in
525
      Teps (id, ty, Fquant (Tforall, uqu, trl, f)), ty
526
  | PPrecord fl ->
527 528
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
529
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
530 531
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
532
            let loc = e.pp_loc in
533
            let e = dterm ~localize uc env e in
Andrei Paskevich's avatar
Andrei Paskevich committed
534 535
            unify_raise ~loc e.dt_ty ty;
            e
536
        | None -> error ~loc (RecordFieldMissing (cs,pj))
537
      in
538
      let al = List.map2 get_val pjl tyl in
539
      Tapp (cs,al), Opt.get ty
Andrei Paskevich's avatar
Andrei Paskevich committed
540
  | PPupdate (e,fl) ->
541
      let e = dterm ~localize uc env e in
542 543
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
544
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
545 546
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
547
            let loc = e.pp_loc in
548
            let e = dterm ~localize uc env e in
549
            unify_raise ~loc e.dt_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
550 551
            e
        | None ->
552
            let ptyl,pty = Denv.specialize_lsymbol ~loc pj in
553
            unify_raise ~loc (Opt.get pty) ty;
554 555 556
            unify_raise ~loc (List.hd ptyl) e.dt_ty;
            (* FIXME? if e is a complex expression, use let *)
            { dt_node = Tapp (pj,[e]) ; dt_ty = ty }
Andrei Paskevich's avatar
Andrei Paskevich committed
557
      in
558
      let al = List.map2 get_val pjl tyl in
559
      Tapp (cs,al), Opt.get ty
Andrei Paskevich's avatar
Andrei Paskevich committed
560
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
561
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
562

563
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
564
  let f = dfmla_node ~localize loc uc env f in
565 566
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
567 568 569
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
570 571 572 573
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
574

575
and dfmla_node ~localize loc uc env = function
576 577 578 579
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
580
  | PPunop (PPnot, a) ->
581
      Fnot (dfmla ~localize uc env a)
582
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
583
      Fbinop (binop op, dfmla ~localize uc env a, dfmla ~localize uc env b)
584
  | PPif (a, b, c) ->
585
      Fif (dfmla ~localize uc env a,
586
           dfmla ~localize uc env b, dfmla ~localize uc env c)
587
  | PPquant (q, uqu, trl, a) ->
588
      let env, uqu = quant_vars uc env uqu in
589
      let trigger e =
590 591 592 593
        try
          TRterm (dterm ~localize uc env e)
        with exn when trigger_not_a_term_exn exn ->
          TRfmla (dfmla ~localize uc env e)
594 595
      in
      let trl = List.map (List.map trigger) trl in
596
      let q = match q with
597 598
        | PPforall -> Tforall
        | PPexists -> Texists
599
        | _ -> error ~loc PredicateExpected
600
      in
601 602
      Fquant (q, uqu, trl, dfmla ~localize uc env a)
  | PPapp (x, tl) when check_highord uc env x tl ->
603 604
      let tl = apply_highord loc x tl in
      let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in
605
      let tl = dtype_args ~localize ps_pred_app loc uc env atyl tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
606
      Fapp (ps_pred_app, tl)
607
  | PPapp (x, tl) ->
608
      let s, tyl = specialize_psymbol x uc in
609
      let tl = dtype_args ~localize s loc uc env tyl tl in
610
      Fapp (s, tl)
611 612
  | PPinfix (e12, op2, e3)
  | PPinnfix (e12, op2, e3) ->
613
      begin match e12.pp_desc with
614 615
        | PPinfix (_, op1, e2)
          when op1.id = "infix <>" || is_psymbol (Qident op1) uc ->
616 617 618
            let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
            Fbinop (Tand, dfmla ~localize uc env e12,
                    dfmla ~localize uc env e23)
619 620 621 622
        | _ when op2.id = "infix <>" ->
            let op2 = { op2 with id = "infix =" } in
            let e0 = { pp_desc = PPinfix (e12, op2, e3); pp_loc = loc } in
            Fnot (dfmla ~localize uc env e0)
623 624
        | _ ->
            let s, tyl = specialize_psymbol (Qident op2) uc in
625
            let tl = dtype_args ~localize s loc uc env tyl [e12;e3] in
626
            Fapp (s, tl)
627
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
628
  | PPlet (x, e1, e2) ->
629
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
630
      let ty = e1.dt_ty in
631
      let env = add_var x.id ty env in
632
      let e2 = dfmla ~localize uc env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
633
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
634
  | PPmatch (e1, bl) ->
635
      let t1 = dterm ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
636 637
      let ty1 = t1.dt_ty in
      let branch (p, e) =
638 639
        let env, p = dpat_list uc env ty1 p in
        p, dfmla ~localize uc env e
Andrei Paskevich's avatar
Andrei Paskevich committed
640
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
641
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
642
  | PPnamed (x, f1) ->
643
      let localize = match x with
644
        | Lpos l -> Some (Some l)
645
        | Lstr _ -> localize
646
      in
647
      let f1 = dfmla ~localize uc env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
648
      Fnamed (x, f1)
649
(*
650
  | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
651 652
      let pr = find_prop x uc in
      Fvar (Decl.find_prop (Theory.get_known uc) pr)
653
*)
654
  | PPvar x ->
655
      let s, tyl = specialize_psymbol x uc in
656
      let tl = dtype_args ~localize s loc uc env tyl [] in
657
      Fapp (s, tl)
Andrei Paskevich's avatar
Andrei Paskevich committed
658
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ | PPupdate _ ->
659
      error ~loc PredicateExpected
660

661
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
662 663
  check_pat_linearity p;
  let loc = p.pat_loc in
664
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
665
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
666
  env, p
667

668
and dtype_args ~localize ls loc uc env el tl =
669
  let n = List.length el and m = List.length tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
670
  if n <> m then error ~loc (BadArity (ls,n,m));
671
  let rec check_arg = function
672
    | [], [] ->
673
        []
674
    | a :: al, t :: bl ->
675
        let loc = t.pp_loc in
676
        let t = dterm ~localize uc env t in
677 678
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
679
    | _ ->
680
        assert false
681 682 683
  in
  check_arg (el, tl)

684
(** Typing declarations, that is building environments. *)
685 686 687

open Ptree

688
let add_types dl th =
689
  let def = List.fold_left
<