typing.ml 41.1 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 37 38
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
39

40 41 42
let error = Loc.error

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

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

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

75
let debug_parse_only = Debug.register_flag "parse_only"
76
  ~desc:"Stop@ after@ the@ parsing."
77
let debug_type_only  = Debug.register_flag "type_only"
78
  ~desc:"Stop@ after@ the@ typing."
79

80 81
(** Environments *)

82
(** typing using destructive type variables
83

84 85 86 87 88 89
    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
90

91 92
*)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
98 99 100
let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

101 102 103 104
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

105
let create_user_tv =
106 107
  let hs = Hstr.create 17 in
  fun s -> try Hstr.find hs s with Not_found ->
108
  let tv = create_tvsymbol (id_fresh s) in
109
  Hstr.add hs s tv;
110 111 112 113 114 115
  tv

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

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

121 122
let denv_empty = { dvars = Mstr.empty; gvars = Util.const None }
let denv_empty_with_globals gv = { dvars = Mstr.empty; gvars = gv }
123

124 125
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
126
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
127

128 129 130
let print_denv fmt denv =
  Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars

131 132 133 134 135 136 137 138 139 140 141 142
(* 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

let specialize_tysymbol loc p uc =
  let sl = string_list_of_qualid [] p in
143 144
  try ns_find_ts (get_namespace uc) sl
  with Not_found -> error ~loc (UnboundType sl)
145 146 147

(* lazy declaration of tuples *)

148 149 150
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)
151
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
152
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
153
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
154

155
let rec dty uc = function
156
  | PPTtyvar {id=x} ->
157
      create_user_type_var x
158 159
  | PPTtyapp (p, x) ->
      let loc = qloc x in
160
      let ts = specialize_tysymbol loc x uc in
161
      let tyl = List.map (dty uc) p in
162
      Loc.try2 loc tyapp ts tyl
163 164
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
165
      tyapp ts (List.map (dty uc) tyl)
166

167
let find_ns get_id find p ns =
168 169
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
170 171 172 173
  try
    let r = find ns sl in
    if Debug.test_flag Glob.flag then Glob.use loc (get_id r);
    r
174 175
  with Not_found -> error ~loc (UnboundSymbol sl)

176 177
let get_id_prop p = p.pr_name
let find_prop_ns = find_ns get_id_prop ns_find_pr
178 179
let find_prop p uc = find_prop_ns p (get_namespace uc)

180 181
let get_id_ts ts = ts.ts_name
let find_tysymbol_ns = find_ns get_id_ts ns_find_ts
182 183
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

184 185
let get_id_ls ls = ls.ls_name
let find_lsymbol_ns = find_ns get_id_ls ns_find_ls
186 187
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

188 189 190 191 192 193 194 195 196 197 198
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)

199 200
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
201
(* dead code
202
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
203
*)
204

205 206
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
207 208
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
209

210
let specialize_fsymbol p uc =
211
  let s,tl,ty = specialize_lsymbol p uc in
212
  match ty with
213
    | None -> let loc = qloc p in error ~loc TermExpected
214
    | Some ty -> s, tl, ty
215

216
let specialize_psymbol p uc =
217
  let s,tl,ty = specialize_lsymbol p uc in
218 219
  match ty with
    | None -> s, tl
220 221
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

222
let is_psymbol p uc =
223 224
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225

226
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
227 228 229 230 231 232 233 234 235 236 237 238
(* [is_projection uc ls] returns
   - [Some (ts, lsc, i)] if [ls] is the i-th projection of an
     algebraic datatype [ts] with only one constructor [lcs]
   - [None] otherwise
 *)
let is_projection uc ls =
  try
    let ts,tl = match ls.ls_args, ls.ls_value with
      | [{ty_node = Ty.Tyapp (ts, tl)}], Some _ -> ts,tl
      | _ -> (* not a function with 1 argument *) raise Exit
    in
    ignore (List.fold_left (fun tvs t -> match t.ty_node with
239
      | Ty.Tyvar tv -> Stv.add_new Exit tv tvs
Andrei Paskevich's avatar
Andrei Paskevich committed
240 241 242 243 244 245 246 247 248 249
      | _ -> (* not a generic type *) raise Exit) Stv.empty tl);
    let kn = get_known uc in
    let lsc = match Decl.find_constructors kn ts with
      | [lsc] -> lsc
      | _ -> (* 0 or several constructors *) raise Exit
    in
    let def = match Decl.find_logic_definition kn ls with
      | Some def -> def
      | None -> (* no definition *) raise Exit
    in
250
    let v, t = match Decl.open_ls_defn def with
Andrei Paskevich's avatar
Andrei Paskevich committed
251 252 253 254 255 256 257 258 259 260 261 262 263 264
      | [v], t -> v, t
      | _ -> assert false
    in
    let b = match t.t_node with
      | Tcase ({t_node=Term.Tvar v'}, [b]) when vs_equal v' v -> b
      | _ -> raise Exit
    in
    let p, t = t_open_branch b in
    let pl = match p with
      | { pat_node = Term.Papp (lsc', pl) } when ls_equal lsc lsc' -> pl
      | _ -> raise Exit
    in
    let i = match t.t_node with
      | Term.Tvar xi ->
265 266 267 268 269 270
          let rec index i = function
            | [] -> raise Exit
            | { pat_node = Term.Pvar v} :: _ when vs_equal v xi -> i
            | _ :: l -> index (i+1) l
          in
          index 0 pl
Andrei Paskevich's avatar
Andrei Paskevich committed
271
      | _ ->
272
          raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
    in
    Some (ts, lsc, i)
  with Exit ->
    None

let list_fields uc fl =
  let type_field (q, e) =
    let loc = qloc q in
    let ls = find_lsymbol q uc in
    match is_projection uc ls with
      | None -> errorm ~loc "this is not a record field"
      | Some pr -> pr, loc, e
  in
  let fl = List.map type_field fl in
  let (ts,cs,_),_,_ = List.hd fl in
  let n = List.length cs.ls_args in
  let args = Array.create n None in
  let check_field ((ts',_,i),loc,e) =
    if not (ts_equal ts' ts) then
      errorm ~loc "this should be a field for type %a" Pretty.print_ts ts;
    assert (0 <= i && i < n);
    if args.(i) <> None then
      errorm ~loc "this record field is defined several times";
    args.(i) <- Some (loc,e);
  in
  List.iter check_field fl;
  ts,cs,Array.to_list args
300
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
301

302

303 304
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305 306 307 308
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

309
(** Typing terms and formulas *)
310 311

let binop = function
312 313 314 315
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
316

Andrei Paskevich's avatar
Andrei Paskevich committed
317
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
318
  let s = ref Sstr.empty in
319
  let add id =
320
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
321 322 323 324
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
325
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
326
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
327
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
328
    | PPpor (p, _) -> check p
329
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
330
  check p
331

332 333
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
334
  tyvar (create_ty_decl_var ~loc tv)
335

336 337
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
338 339
  env, { dp_node = n; dp_ty = ty }

340
and dpat_node loc uc env = function
341
  | PPpwild ->
342
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
343
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
344
  | PPpvar x ->
345
      let ty = fresh_type_var loc in
346
      let env = add_var x.id ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
347 348
      env, Pvar x, ty
  | PPpapp (x, pl) ->
349
      let s, tyl, ty = specialize_fsymbol x uc in
350
      let env, pl = dpat_args s loc uc env tyl pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
351
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
352 353
  | PPprec fl ->
      let renv = ref env in
354 355
      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
356
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
357 358
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
359
            let loc = e.pat_loc in
360
            let env,e = dpat uc !renv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
361 362 363
            unify_raise ~loc e.dp_ty ty;
            renv := env;
            e
364 365
        | None ->
            { dp_node = Pwild; dp_ty = ty }
Andrei Paskevich's avatar
Andrei Paskevich committed
366
      in
367
      let al = List.map2 get_val pjl tyl in
368
      !renv, Papp (cs, al), Opt.get ty
369 370 371 372
  | 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
373
      let env, pl = dpat_args s loc uc env tyl pl in
374
      let ty = tyapp (ts_tuple n) tyl in
375
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
376
  | PPpas (p, x) ->
377
      let env, p = dpat uc env p in
378
      let env = add_var x.id p.dp_ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
379
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
380
  | PPpor (p, q) ->
381 382
      let env, p = dpat uc env p in
      let env, q = dpat uc env q in
Andrei Paskevich's avatar
Andrei Paskevich committed
383
      unify_raise ~loc p.dp_ty q.dp_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
384
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
385

386
and dpat_args ls loc uc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
388
  if n <> m then error ~loc (BadArity (ls,n,m));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389
  let rec check_arg env = function
390
    | [], [] ->
391
        env, []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
392
    | a :: al, p :: pl ->
393 394 395 396 397
        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
398
    | _ ->
399
        assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
400
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
401
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
402

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403
let rec trigger_not_a_term_exn = function
404
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
405 406 407
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

408
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
409
  let s = ref Sstr.empty in
410
  let check id =
411
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
412
  in
413
  List.iter (fun (idl, _) -> Opt.iter check idl) uqu
414

415
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
416
  | Qident { id = x } when Mstr.mem x env.dvars -> true
417 418
  | _ -> env.gvars x <> None ||
      List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
419 420 421 422 423 424

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

425
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
426
  let n, ty = dterm_node ~localize loc uc env t in
427
  let t = { dt_node = n; dt_ty = ty } in
428 429
  let rec down loc e = match e.dt_node with
    | Tnamed (Lstr _, e) -> down loc e
430 431 432
    | Tnamed (Lpos _, _) -> t
    | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
  in
433 434 435 436
  match localize with
    | Some (Some loc) -> down loc t
    | Some None -> down loc t
    | None -> t
437

438
and dterm_node ~localize loc uc env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
439
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
440
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
441
      let ty = Mstr.find x env.dvars in
442
      Tvar x, ty
443
  | PPvar x when env.gvars x <> None ->
444
      let vs = Opt.get (env.gvars x) in
445 446 447
      assert (ty_closed vs.vs_ty);
      let ty = specialize_ty ~loc (Htv.create 0) vs.vs_ty in
      Tgvar vs, ty
448
  | PPvar x ->
449
      (* 0-arity symbol (constant) *)
450
      let s, tyl, ty = specialize_fsymbol x uc in
451
      let n = List.length tyl in
Andrei Paskevich's avatar
Andrei Paskevich committed
452
      if n > 0 then error ~loc (BadArity (s,n,0));
453
      Tapp (s, []), ty
454
  | PPapp (x, tl) when check_highord uc env x tl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
455 456
      let tl = apply_highord loc x tl in
      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
457
      let tl = dtype_args ~localize fs_func_app loc uc env atyl tl in
458
      Tapp (fs_func_app, tl), Opt.get aty
459
  | PPapp (x, tl) ->
460
      let s, tyl, ty = specialize_fsymbol x uc in
461
      let tl = dtype_args ~localize s loc uc env tyl tl in
462
      Tapp (s, tl), ty
463 464 465 466
  | 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
467
      let tl = dtype_args ~localize s loc uc env tyl tl in
468
      let ty = tyapp (ts_tuple n) tyl in
469
      Tapp (s, tl), ty
470
  | PPinfix (e1, x, e2) ->
471
      let s, tyl, ty = specialize_fsymbol (Qident x) uc in
472
      let tl = dtype_args ~localize s loc uc env tyl [e1; e2] in
473
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474
  | PPconst (ConstInt _ as c) ->
475
      Tconst c, tyapp Ty.ts_int []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476
  | PPconst (ConstReal _ as c) ->
477
      Tconst c, tyapp Ty.ts_real []
Andrei Paskevich's avatar
Andrei Paskevich committed
478
  | PPlet (x, e1, e2) ->
479
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
480
      let ty = e1.dt_ty in
481
      let env = add_var x.id ty env in
482
      let e2 = dterm ~localize uc env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
484
  | PPmatch (e1, bl) ->
485
      let t1 = dterm ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
486
      let ty1 = t1.dt_ty in
487
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
488
      let branch (p, e) =
489
        let env, p = dpat_list uc env ty1 p in
490
        let loc = e.pp_loc in
491 492
        let e = dterm ~localize uc env e in
        unify_raise ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
493
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
494 495
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
496
      Tmatch (t1, bl), tb
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
497
  | PPnamed (x, e1) ->
498
      let localize = match x with
499
        | Lpos l -> Some (Some l)
500
        | Lstr _ -> localize
501
      in
502
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
504 505
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
506
      let e1 = dterm ~localize uc env e1 in
507
      let ty = dty uc ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
508
      unify_raise ~loc e1.dt_ty ty;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
509
      e1.dt_node, ty
510 511
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
512 513
      let e2 = dterm ~localize uc env e2 in
      let e3 = dterm ~localize uc env e3 in
Andrei Paskevich's avatar
Andrei Paskevich committed
514
      unify_raise ~loc e3.dt_ty e2.dt_ty;
515
      Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
516
  | PPeps (x, ty, e1) ->
517
      let ty = dty uc ty in
518
      let env = add_var x.id ty env in
519
      let e1 = dfmla ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
520
      Teps (x, ty, e1), ty
521
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
522 523
      check_quant_linearity uqu;
      let uquant env (idl,ty) =
524
        let ty = dty uc ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
525 526 527 528
        let id = match idl with
          | Some id -> id
          | None -> assert false
        in
529
        add_var id.id ty env, (id,ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
530
      in
531
      let env, uqu = Lists.map_fold_left uquant env uqu in
Andrei Paskevich's avatar
Andrei Paskevich committed
532
      let trigger e =
533 534 535 536
        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
537 538
      in
      let trl = List.map (List.map trigger) trl in
539
      let e = match q with
540 541
        | PPfunc -> TRterm (dterm ~localize uc env a)
        | PPpred -> TRfmla (dfmla ~localize uc env a)
542 543 544 545
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
Andrei Paskevich's avatar
Andrei Paskevich committed
546
        | TRterm t ->
547
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
548
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
549
              let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty)
Andrei Paskevich's avatar
Andrei Paskevich committed
550 551 552 553 554 555 556 557 558
              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
559
        | TRfmla f ->
560
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
561 562 563 564 565
            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) ->
566 567
              let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty)
              uqu ([], tyapp ts_pred [uty])
Andrei Paskevich's avatar
Andrei Paskevich committed
568 569 570 571 572 573 574 575
            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
576
            id, ty, Fbinop (Tiff, Fapp (ps_pred_app, [h;u]), f)
Andrei Paskevich's avatar
Andrei Paskevich committed
577
      in
578
      Teps (id, ty, Fquant (Tforall, uqu, trl, f)), ty
579
  | PPrecord fl ->
580 581
      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
582
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
583 584
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
585
            let loc = e.pp_loc in
586
            let e = dterm ~localize uc env e in
Andrei Paskevich's avatar
Andrei Paskevich committed
587 588
            unify_raise ~loc e.dt_ty ty;
            e
589
        | None -> error ~loc (RecordFieldMissing (cs,pj))
590
      in
591
      let al = List.map2 get_val pjl tyl in
592
      Tapp (cs,al), Opt.get ty
Andrei Paskevich's avatar
Andrei Paskevich committed
593
  | PPupdate (e,fl) ->
594
      let e = dterm ~localize uc env e in
595 596
      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
597
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
598 599
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
600
            let loc = e.pp_loc in
601
            let e = dterm ~localize uc env e in
602
            unify_raise ~loc e.dt_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
603 604
            e
        | None ->
605
            let ptyl,pty = Denv.specialize_lsymbol ~loc pj in
606
            unify_raise ~loc (Opt.get pty) ty;
607 608 609
            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
610
      in
611
      let al = List.map2 get_val pjl tyl in
612
      Tapp (cs,al), Opt.get ty
Andrei Paskevich's avatar
Andrei Paskevich committed
613
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
614
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
615

616
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
617
  let f = dfmla_node ~localize loc uc env f in
618 619
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
620 621 622
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
623 624 625 626
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
627

628
and dfmla_node ~localize loc uc env = function
629 630 631 632
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
633
  | PPunop (PPnot, a) ->
634
      Fnot (dfmla ~localize uc env a)
635
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
636
      Fbinop (binop op, dfmla ~localize uc env a, dfmla ~localize uc env b)
637
  | PPif (a, b, c) ->
638
      Fif (dfmla ~localize uc env a,
639
           dfmla ~localize uc env b, dfmla ~localize uc env c)
640
  | PPquant (q, uqu, trl, a) ->
641
      check_quant_linearity uqu;
642
      let uquant env (idl,ty) =
643
        let ty = dty uc ty in
644
        let id = match idl with
Andrei Paskevich's avatar
Andrei Paskevich committed
645
          | Some id -> id
646
          | None -> assert false
647
        in
648
        add_var id.id ty env, (id,ty)
649
      in
650
      let env, uqu = Lists.map_fold_left uquant env uqu in
651
      let trigger e =
652 653 654 655
        try
          TRterm (dterm ~localize uc env e)
        with exn when trigger_not_a_term_exn exn ->
          TRfmla (dfmla ~localize uc env e)
656 657
      in
      let trl = List.map (List.map trigger) trl in
658
      let q = match q with
659 660
        | PPforall -> Tforall
        | PPexists -> Texists
661
        | _ -> error ~loc PredicateExpected
662
      in
663 664
      Fquant (q, uqu, trl, dfmla ~localize uc env a)
  | PPapp (x, tl) when check_highord uc env x tl ->
665 666
      let tl = apply_highord loc x tl in
      let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in
667
      let tl = dtype_args ~localize ps_pred_app loc uc env atyl tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
668
      Fapp (ps_pred_app, tl)
669
  | PPapp (x, tl) ->
670
      let s, tyl = specialize_psymbol x uc in
671
      let tl = dtype_args ~localize s loc uc env tyl tl in
672
      Fapp (s, tl)
673 674
  | PPinfix (e12, op2, e3) ->
      begin match e12.pp_desc with
675 676 677 678 679 680
        | PPinfix (_, op1, e2) when is_psymbol (Qident op1) uc ->
            let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
            Fbinop (Tand, dfmla ~localize uc env e12,
                    dfmla ~localize uc env e23)
        | _ ->
            let s, tyl = specialize_psymbol (Qident op2) uc in
681
            let tl = dtype_args ~localize s loc uc env tyl [e12;e3] in
682
            Fapp (s, tl)
683
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
684
  | PPlet (x, e1, e2) ->
685
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
686
      let ty = e1.dt_ty in
687
      let env = add_var x.id ty env in
688
      let e2 = dfmla ~localize uc env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
689
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
690
  | PPmatch (e1, bl) ->
691
      let t1 = dterm ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
692 693
      let ty1 = t1.dt_ty in
      let branch (p, e) =
694 695
        let env, p = dpat_list uc env ty1 p in
        p, dfmla ~localize uc env e
Andrei Paskevich's avatar
Andrei Paskevich committed
696
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
697
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
698
  | PPnamed (x, f1) ->
699
      let localize = match x with
700
        | Lpos l -> Some (Some l)
701
        | Lstr _ -> localize
702
      in
703
      let f1 = dfmla ~localize uc env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704
      Fnamed (x, f1)
705
(*
706
  | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
707 708
      let pr = find_prop x uc in
      Fvar (Decl.find_prop (Theory.get_known uc) pr)
709
*)
710
  | PPvar x ->
711
      let s, tyl = specialize_psymbol x uc in
712
      let tl = dtype_args ~localize s loc uc env tyl [] in
713
      Fapp (s, tl)
Andrei Paskevich's avatar
Andrei Paskevich committed
714
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ | PPupdate _ ->
715
      error ~loc PredicateExpected
716

717
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
718 719
  check_pat_linearity p;
  let loc = p.pat_loc in
720
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
721
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
722
  env, p
723

724
and dtype_args ~localize ls loc uc env el tl =
725
  let n = List.length el and m = List.length tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
726
  if n <> m then error ~loc (BadArity (ls,n,m));
727
  let rec check_arg = function
728
    | [], [] ->
729
        []
730
    | a :: al, t :: bl ->
731
        let loc = t.pp_loc in
732
        let t = dterm ~localize uc env t in
733 734
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
735
    | _ ->
736
        assert false
737 738 739
  in
  check_arg (el, tl)