typing.ml 40.9 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 81
let debug_parse_only = Debug.register_stop_flag "parse_only"
let debug_type_only  = Debug.register_stop_flag "type_only"
82

83 84
(** Environments *)

85
(** typing using destructive type variables
86

87 88 89 90 91 92
    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
93

94 95
*)

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

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

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

108
type denv = {
109
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
110
  dvars   : dty Mstr.t;    (* local variables, to be bound later *)
111 112
}

113
let create_denv () = {
114
  utyvars = Hashtbl.create 17;
115 116 117
  dvars = Mstr.empty;
}

118 119 120 121 122
let create_user_type_var x =
  (* TODO: shouldn't we localize this ident? *)
  let v = create_tvsymbol (id_fresh x) in
  create_ty_decl_var ~user:true v

123 124 125 126
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
127
    let v = create_user_type_var x in
128 129
    Hashtbl.add env.utyvars x v;
    v
130

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

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

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

(* lazy declaration of tuples *)

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

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

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

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

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

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

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

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

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

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

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

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

231
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
232 233 234 235 236 237 238 239 240 241 242 243
(* [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
244
      | Ty.Tyvar tv -> Stv.add_new Exit tv tvs
Andrei Paskevich's avatar
Andrei Paskevich committed
245 246 247 248 249 250 251 252 253 254
      | _ -> (* 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
255
    let v, t = match Decl.open_ls_defn def with
Andrei Paskevich's avatar
Andrei Paskevich committed
256 257 258 259 260 261 262 263 264 265 266 267 268 269
      | [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 ->
270 271 272 273 274 275
          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
276
      | _ ->
277
          raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
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 303 304
    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
305
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
306

307

308 309
(** Typing types *)

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

314
(** Typing terms and formulas *)
315 316

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

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

337 338
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
339
  tyvar (create_ty_decl_var ~loc ~user:false tv)
340

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

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

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

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

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

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

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

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

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

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

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

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

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