typing.ml 42 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
8
(*    Andrei Paskevich                                                    *)
9 10 11 12 13 14 15 16 17 18 19
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
20

21 22
open Util
open Format
23
open Pp
24
open Ident
25
open Ptree
26
open Ty
27
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
28
open Decl
29
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
30
open Env
31
open Denv
Andrei Paskevich's avatar
Andrei Paskevich committed
32

33 34
(** errors *)

35
exception DuplicateVar of string
36 37 38
exception DuplicateTypeVar of string
exception PredicateExpected
exception TermExpected
39 40
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
41 42 43 44 45
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
46

47 48 49
let error = Loc.error

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

51
let rec print_qualid fmt = function
52
  | Qident s -> fprintf fmt "%s" s.id
53
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
54

55
let () = Exn_printer.register (fun fmt e -> match e with
56
  | DuplicateTypeVar s ->
57 58 59
      fprintf fmt "Duplicate type parameter %s" s
  | DuplicateVar s ->
      fprintf fmt "Duplicate variable %s" s
60 61 62 63
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
64 65 66 67
  | 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
68
  | ClashTheory s ->
69
      fprintf fmt "Clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70 71
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
72 73
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
74 75 76 77
  | 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
78
  | _ -> raise e)
79

80
let debug_parse_only = Debug.register_stop_flag "parse_only"
81
  ~desc:"Stop@ after@ the@ parsing."
82
let debug_type_only  = Debug.register_stop_flag "type_only"
83
  ~desc:"Stop@ after@ the@ typing."
84

85 86
(** Environments *)

87
(** typing using destructive type variables
88

89 90 91 92 93 94
    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
95

96 97
*)

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

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

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

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

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

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

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

129 130
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
131
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
132

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

136 137 138 139 140 141 142 143 144 145 146 147
(* 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
148 149
  try ns_find_ts (get_namespace uc) sl
  with Not_found -> error ~loc (UnboundType sl)
150 151 152

(* lazy declaration of tuples *)

153 154 155
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)
156
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
157
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
158
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
159

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

172
let find_ns get_id find p ns =
173 174
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
175 176 177 178
  try
    let r = find ns sl in
    if Debug.test_flag Glob.flag then Glob.use loc (get_id r);
    r
179 180
  with Not_found -> error ~loc (UnboundSymbol sl)

181 182
let get_id_prop p = p.pr_name
let find_prop_ns = find_ns get_id_prop ns_find_pr
183 184
let find_prop p uc = find_prop_ns p (get_namespace uc)

185 186
let get_id_ts ts = ts.ts_name
let find_tysymbol_ns = find_ns get_id_ts ns_find_ts
187 188
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

189 190
let get_id_ls ls = ls.ls_name
let find_lsymbol_ns = find_ns get_id_ls ns_find_ls
191 192
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

193 194 195 196 197 198 199 200 201 202 203
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)

204 205
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
206 207
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

208 209
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
210 211
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
212

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

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

225
let is_psymbol p uc =
226 227
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
228

229
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
230 231 232 233 234 235 236 237 238 239 240 241
(* [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
242
      | Ty.Tyvar tv -> Stv.add_new Exit tv tvs
Andrei Paskevich's avatar
Andrei Paskevich committed
243 244 245 246 247 248 249 250 251 252
      | _ -> (* 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
253
    let v, t = match Decl.open_ls_defn def with
Andrei Paskevich's avatar
Andrei Paskevich committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267
      | [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 ->
268 269 270 271 272 273
          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
274
      | _ ->
275
          raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
    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
303
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
304

305

306 307
(** Typing types *)

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

312
(** Typing terms and formulas *)
313 314

let binop = function
315 316 317 318
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
319

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

335 336
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
337
  tyvar (create_ty_decl_var ~loc tv)
338

339 340
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
341 342
  env, { dp_node = n; dp_ty = ty }

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

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

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

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

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

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

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

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

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

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