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
exception ClashTheory of string
42
(* dead code
43
exception UnboundTheory of qualid
44
*)
45 46 47
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
48

49 50 51
let error = Loc.error

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

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

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

84
let debug_parse_only = Debug.register_flag "parse_only"
85
  ~desc:"Stop@ after@ the@ parsing."
86
let debug_type_only  = Debug.register_flag "type_only"
87
  ~desc:"Stop@ after@ the@ typing."
88

89 90
(** Environments *)

91
(** typing using destructive type variables
92

93 94 95 96 97 98
    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
99

100 101
*)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
107 108 109
let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

110 111 112 113
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

114 115 116 117 118 119 120 121 122 123 124
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)

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

130 131
let denv_empty = { dvars = Mstr.empty; gvars = Util.const None }
let denv_empty_with_globals gv = { dvars = Mstr.empty; gvars = gv }
132

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

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

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

(* lazy declaration of tuples *)

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

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

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

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

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

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

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

208 209
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
210
(* dead code
211
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
212
*)
213

214 215
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
216 217
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
218

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

225
let specialize_psymbol p uc =
226
  let s,tl,ty = specialize_lsymbol p uc in
227 228
  match ty with
    | None -> s, tl
229 230
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

231
let is_psymbol p uc =
232 233
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
234

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

311

312 313
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
314 315 316 317
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

318
(** Typing terms and formulas *)
319 320

let binop = function
321 322 323 324
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
325

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

341 342
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
343
  tyvar (create_ty_decl_var ~loc tv)
344

345 346
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
347 348
  env, { dp_node = n; dp_ty = ty }

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
let rec trigger_not_a_term_exn = function
413
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414 415 416
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

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

424
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
425
  | Qident { id = x } when Mstr.mem x env.dvars -> true
426 427
  | _ -> env.gvars x <> None ||
      List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
428 429 430 431 432 433

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

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

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

625
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
626
  let f = dfmla_node ~localize loc uc env f in
627 628
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
629 630 631
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
632 633 634 635
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
636

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