typing.ml 39.9 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
MARCHE Claude's avatar
MARCHE Claude committed
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 39 40 41 42 43 44 45 46
exception Message of string
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
exception PredicateExpected
exception TermExpected
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
47 48

let error ?loc e = match loc with
49 50
  | None -> raise e
  | Some loc -> raise (Loc.Located (loc,e))
51

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52 53 54
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
55 56
  Format.kfprintf
    (fun _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
57 58 59
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
60
       error ?loc (Message s))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
61 62
    fmt f

63
let rec print_qualid fmt = function
64
  | Qident s -> fprintf fmt "%s" s.id
65
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
66

67
let () = Exn_printer.register (fun fmt e -> match e with
68 69
  | Message s ->
      fprintf fmt "%s" s
70
  | DuplicateTypeVar s ->
71
      fprintf fmt "duplicate type parameter %s" s
72
  | TypeArity (id, a, n) ->
73
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
74 75
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76
      fprintf fmt "Clash with previous symbol %s" id
77 78 79 80
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
81
  | BadNumberOfArguments (s, n, m) ->
82
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
83
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84 85
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86 87
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
88 89 90 91
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
92 93 94 95
  | 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
96
  | _ -> raise e)
97

98 99 100
let debug_parse_only = Debug.register_flag "parse_only"
let debug_type_only  = Debug.register_flag "type_only"

101 102
(** Environments *)

103
(** typing using destructive type variables
104

105 106 107 108 109 110
    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
111

112 113
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114 115 116 117 118
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
119 120 121
let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

122 123 124 125
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

126
type denv = {
127
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
128
  dvars   : dty Mstr.t;    (* local variables, to be bound later *)
129 130
}

131
let create_denv () = {
132
  utyvars = Hashtbl.create 17;
133 134 135
  dvars = Mstr.empty;
}

136 137 138 139 140
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

141 142 143 144
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
145
    let v = create_user_type_var x in
146 147
    Hashtbl.add env.utyvars x v;
    v
148

149 150 151 152
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 }

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

156 157 158 159 160 161 162 163 164 165 166 167
(* 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
168
  let ts =
169 170 171
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
172 173 174 175
  ts, List.length ts.ts_args

(* lazy declaration of tuples *)

176 177 178 179
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)
180

181
let rec dty uc env = function
182
  | PPTtyvar {id=x} ->
183
      tyvar (find_user_type_var x env)
184 185
  | PPTtyapp (p, x) ->
      let loc = qloc x in
186
      let ts, a = specialize_tysymbol loc x uc in
187 188
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
189
      let tyl = List.map (dty uc env) p in
190
      tyapp ts tyl
191 192
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
193
      tyapp ts (List.map (dty uc env) tyl)
194 195 196 197

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
198
  try find ns sl
199 200
  with Not_found -> error ~loc (UnboundSymbol sl)

201
let find_prop_ns = find_ns ns_find_pr
202 203 204 205 206 207 208 209
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)

210 211 212
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

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

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

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

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

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

308

309 310
(** Typing types *)

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
323
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
324
  let s = ref Sstr.empty in
325
  let add id =
326
    if Sstr.mem id.id !s then
327
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
328
    s := Sstr.add id.id !s
329 330 331 332
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
333
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
334
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
335
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
336
    | PPpor (p, _) -> check p
337
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
338
  check p
339

340 341
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
342
  tyvar (create_ty_decl_var ~loc ~user:false tv)
343

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

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

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

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

413
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  let s = ref Sstr.empty in
415
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
416 417
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
418
  in
419
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
420

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

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

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

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

632 633
and dfmla ?(localize=false) uc env { pp_loc = loc; pp_desc = f } =
  let f = dfmla_node ~localize loc uc env f in
634 635 636 637 638 639
  let rec down e = match e with
    | Fnamed (Lstr _, e) -> down e
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
  if localize then down f else f
640

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

730
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
731 732
  check_pat_linearity p;
  let loc = p.pat_loc in
733
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
734
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
735
  env, p
736

737
and dtype_args s loc uc env el tl =
738 739 740
  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
741
    | [], [] ->
742
        []
743
    | a :: al, t :: bl ->
744 745 746 747
        let loc = t.pp_loc in
        let t = dterm uc env t in
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
748
    | _ ->
749
        assert false
750 751 752
  in
  check_arg (el, tl)

753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768
(** Add projection functions for the algebraic types *)

let add_projection cl p (fs,tyarg,tyval) th =
  let vs = create_vsymbol (id_fresh p) tyval in
  let per_cs (_,id,pl) =
    let cs = find_lsymbol (Qident id) th in
    let tc = match cs.ls_value with
      | None -> assert false
      | Some t -> t
    in
    let m = ty_match Mtv.empty tc tyarg in
    let per_param ty (n,_) = match n with
      | Some id when id.id = p -> pat_var vs
      | _ -> pat_wild (ty_inst m ty)
    in
    let al = List.map2 per_param cs.ls_args pl in
<