typing.ml 39.6 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 string list
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 sl ->
       fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
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 166
  with Not_found -> error ~loc (UnboundSymbol sl)

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 197 198
let rec dty uc = function
  | PPTtyvar {id=x} ->
      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 208 209
let rec ty_of_pty uc = function
  | PPTtyvar {id=x} ->
      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
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
220 221
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
222

223
let specialize_fsymbol p uc =
224
  let s,tl,ty = specialize_lsymbol p uc in
225
  match ty with
226
    | None -> let loc = qloc p in error ~loc TermExpected
227
    | Some ty -> s, tl, ty
228

229
let specialize_psymbol p uc =
230
  let s,tl,ty = specialize_lsymbol p uc in
231 232
  match ty with
    | None -> s, tl
233 234
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

235
let is_psymbol p uc =
236 237
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
238

239 240
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241 242 243 244
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

245
(** Typing terms and formulas *)
246 247

let binop = function
248 249 250 251
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
252

Andrei Paskevich's avatar
Andrei Paskevich committed
253
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
254
  let s = ref Sstr.empty in
255
  let add id =
256
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
257 258 259 260
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
261
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
262
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
263
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
264
    | PPpor (p, _) -> check p
265
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
266
  check p
267

268 269
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
270 271
  env, { dp_node = n; dp_ty = ty }

272
and dpat_node loc uc env = function
273
  | PPpwild ->
274
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
275
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
276
  | PPpvar x ->
277
      let ty = fresh_type_var loc in
278
      let env = add_var x.id ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
279 280
      env, Pvar x, ty
  | PPpapp (x, pl) ->
281
      let s, tyl, ty = specialize_fsymbol x uc in
282
      let env, pl = dpat_args s loc uc env tyl pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
283
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
284 285
  | PPprec fl ->
      let renv = ref env in
286 287
      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
288
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
289 290
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
291
            let loc = e.pat_loc in
292
            let env,e = dpat uc !renv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
293 294 295
            unify_raise ~loc e.dp_ty ty;
            renv := env;
            e
296 297
        | None ->
            { dp_node = Pwild; dp_ty = ty }
Andrei Paskevich's avatar
Andrei Paskevich committed
298
      in
299
      let al = List.map2 get_val pjl tyl in
300
      !renv, Papp (cs, al), Opt.get ty
301 302 303 304
  | 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
305
      let env, pl = dpat_args s loc uc env tyl pl in
306
      let ty = tyapp (ts_tuple n) tyl in
307
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
308
  | PPpas (p, x) ->
309
      let env, p = dpat uc env p in
310
      let env = add_var x.id p.dp_ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
311
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
312
  | PPpor (p, q) ->
313 314
      let env, p = dpat uc env p in
      let env, q = dpat uc env q in
Andrei Paskevich's avatar
Andrei Paskevich committed
315
      unify_raise ~loc p.dp_ty q.dp_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
316
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
317

318
and dpat_args ls loc uc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
320
  if n <> m then error ~loc (BadArity (ls,n,m));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321
  let rec check_arg env = function
322
    | [], [] ->
323
        env, []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
    | a :: al, p :: pl ->
325 326 327 328 329
        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
330
    | _ ->
331
        assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
332
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
334

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335
let rec trigger_not_a_term_exn = function
336
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337 338 339
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

340
let param_tys uc pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
341
  let s = ref Sstr.empty in
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
  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
361

362
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
363
  | Qident { id = x } when Mstr.mem x env.dvars -> true
364 365
  | _ -> env.gvars x <> None ||
      List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
366 367 368 369 370 371

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

372
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
373
  let n, ty = dterm_node ~localize loc uc env t in
374
  let t = { dt_node = n; dt_ty = ty } in
375 376
  let rec down loc e = match e.dt_node with
    | Tnamed (Lstr _, e) -> down loc e
377 378 379
    | Tnamed (Lpos _, _) -> t
    | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
  in
380 381 382 383
  match localize with
    | Some (Some loc) -> down loc t
    | Some None -> down loc t
    | None -> t
384

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

553
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
554
  let f = dfmla_node ~localize loc uc env f in
555 556
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
557 558 559
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
560 561 562 563
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
564

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

651
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
652 653
  check_pat_linearity p;
  let loc = p.pat_loc in
654
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
655
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
656
  env, p
657

658
and dtype_args ~localize ls loc uc env el tl =
659
  let n = List.length el and m = List.length tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
660
  if n <> m then error ~loc (BadArity (ls,n,m));
661
  let rec check_arg = function
662
    | [], [] ->
663
        []
664
    | a :: al, t :: bl ->
665
        let loc = t.pp_loc in
666
        let t = dterm ~localize uc env t in
667 668
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
669
    | _ ->
670
        assert false
671 672 673
  in
  check_arg (el, tl)

674 675
(** Add projection functions for the algebraic types *)

676
(*
677 678 679 680 681 682 683 684 685 686 687 688 689 690
let add_projection cl p (fs,tyarg,tyval) th =
  let vs = create_vsymbol (id_fresh p) tyval in
  let per_cs (_,id,pl) =
    let cs = find_lsymbol (Qident id) th in
    let tc = match cs.ls_value with
      | None -> assert false
      | Some t -> t
    in
    let m = ty_match Mtv.empty tc tyarg in
    let per_param ty (n,_) = match n with
      | Some id when id.id = p -> pat_var vs
      | _ -> pat_wild (ty_inst m ty)
    in
    let al = List.map2 per_param cs.ls_args pl in
691
    t_close_branch (pat_app cs al tyarg) (t_var vs)
692 693
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
694
  let t = t_case (t_var vs) (List.map per_cs cl) in
695
  let d = make_ls_defn fs [vs] t in
696 697 698 699
  add_logic_decl th [d]

let add_projections th d = match d.td_def with
  | TDabstract | TDalias _ -> th