typing.ml 40.5 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 109 110 111 112 113 114 115 116 117 118
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)

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

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

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

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

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

(* lazy declaration of tuples *)

151 152 153
let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl)
let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls)
154
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
155
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
156
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
157

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

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

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

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

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

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

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

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

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

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

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

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

303

304 305
(** Typing types *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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