typing.ml 39.8 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 check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
341
  let s = ref Sstr.empty in
342
  let check id =
343
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
344
  in
345
  List.iter (fun (idl, _) -> Opt.iter check idl) uqu
346

347
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
348
  | Qident { id = x } when Mstr.mem x env.dvars -> true
349 350
  | _ -> env.gvars x <> None ||
      List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
351 352 353 354 355 356

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

357
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
358
  let n, ty = dterm_node ~localize loc uc env t in
359
  let t = { dt_node = n; dt_ty = ty } in
360 361
  let rec down loc e = match e.dt_node with
    | Tnamed (Lstr _, e) -> down loc e
362 363 364
    | Tnamed (Lpos _, _) -> t
    | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
  in
365 366 367 368
  match localize with
    | Some (Some loc) -> down loc t
    | Some None -> down loc t
    | None -> t
369

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

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

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

655
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
656 657
  check_pat_linearity p;
  let loc = p.pat_loc in