typing.ml 40.2 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)
19

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

32 33
(** errors *)

34 35 36 37 38
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
exception PredicateExpected
exception TermExpected
39 40
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
41 42 43 44 45 46 47
exception BadNumberOfArguments of Ident.ident * int * int
exception ClashTheory of string
exception UnboundTheory of qualid
exception CyclicTypeDef
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
      fprintf fmt "duplicate type parameter %s" s
60
  | TypeArity (id, a, n) ->
61
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
62 63
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64
      fprintf fmt "Clash with previous symbol %s" id
65 66 67 68
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
69 70 71 72
  | 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
73
  | BadNumberOfArguments (s, n, m) ->
74
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
75
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76 77
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78 79
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
80 81 82 83
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
84 85 86 87
  | 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
88
  | _ -> raise e)
89

90 91
let debug_parse_only = Debug.register_stop_flag "parse_only"
let debug_type_only  = Debug.register_stop_flag "type_only"
92

93 94
(** Environments *)

95
(** typing using destructive type variables
96

97 98 99 100 101 102
    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
103

104 105
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106 107 108 109 110
let term_expected_type ~loc ty1 ty2 =
  errorm ~loc
    "@[This term has type %a@ but is expected to have type@ %a@]"
    print_dty ty1 print_dty ty2

Andrei Paskevich's avatar
Andrei Paskevich committed
111 112 113
let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

114 115 116 117
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

118
type denv = {
119
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
120
  dvars   : dty Mstr.t;    (* local variables, to be bound later *)
121 122
}

123
let create_denv () = {
124
  utyvars = Hashtbl.create 17;
125 126 127
  dvars = Mstr.empty;
}

128 129 130 131 132
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

133 134 135 136
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
137
    let v = create_user_type_var x in
138 139
    Hashtbl.add env.utyvars x v;
    v
140

141 142 143 144
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 }

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

148 149 150 151 152 153 154 155 156 157 158 159
(* 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
160
  let ts =
161 162 163
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
164 165 166 167
  ts, List.length ts.ts_args

(* lazy declaration of tuples *)

168 169 170 171
let add_ty_decl uc dl = add_decl_with_tuples uc (create_ty_decl dl)
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)
172

173
let rec dty uc env = function
174
  | PPTtyvar {id=x} ->
175
      tyvar (find_user_type_var x env)
176 177
  | PPTtyapp (p, x) ->
      let loc = qloc x in
178
      let ts, a = specialize_tysymbol loc x uc in
179 180
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
181
      let tyl = List.map (dty uc env) p in
182
      tyapp ts tyl
183 184
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
185
      tyapp ts (List.map (dty uc env) tyl)
186 187 188 189

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
190
  try find ns sl
191 192
  with Not_found -> error ~loc (UnboundSymbol sl)

193
let find_prop_ns = find_ns ns_find_pr
194 195 196 197 198 199 200 201
let find_prop p uc = find_prop_ns p (get_namespace uc)

let find_tysymbol_ns = find_ns ns_find_ts
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

let find_lsymbol_ns = find_ns ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

202 203 204 205 206 207 208 209 210 211 212
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)

213 214 215
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

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

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

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

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

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

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
    if Sstr.mem id.id !s then
330
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
331
    s := Sstr.add id.id !s
332 333 334 335
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
336
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
337
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
338
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
339
    | PPpor (p, _) -> check p
340
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
341
  check p
342

343 344
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
345
  tyvar (create_ty_decl_var ~loc ~user:false tv)
346

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

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

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

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

416
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
417
  let s = ref Sstr.empty in
418
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
419 420
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add 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
  | _ -> List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
427 428 429 430 431 432

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

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

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

638
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
639
  let f = dfmla_node ~localize loc uc env f in
640 641
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
642 643 644
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
645 646 647 648
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
649

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

739
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
740 741
  check_pat_linearity p;
  let loc = p.pat_loc in
742
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
743
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
744
  env, p
745

746
and dtype_args ~localize s loc uc env el tl =
747 748 749
  let n = List.length el and m = List.length tl in
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
  let rec check_arg = function
750
    | [], [] ->
751
        []
752
    | a :: al, t :: bl ->
753
        let loc = t.pp_loc in
754
        let t = dterm ~localize uc env t in
755 756
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
757
    | _ ->
758
        assert false
759 760 761
  in
  check_arg (el, tl)

762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777
(** Add projection functions for the algebraic types *)

let add_projection cl p (fs,tyarg,tyval) th =
  let vs = create_vsymbol (id_fresh p) tyval