typing.ml 39.1 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3
(*  Copyright (C) 2010-                                                   *)
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
Andrei Paskevich's avatar
Andrei Paskevich committed
23
open Ptree
24
open Ident
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 128 129 130 131
  uc : theory_uc; (* the theory under construction *)
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty Mstr.t; (* local variables, to be bound later *)
}

132 133 134
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
135 136 137 138 139 140 141 142 143 144 145 146
  dvars = Mstr.empty;
}

let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    (* TODO: shouldn't we localize this ident? *)
    let v = create_tvsymbol (id_fresh x) in
    let v = create_ty_decl_var ~user:true v in
    Hashtbl.add env.utyvars x v;
    v
147

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

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

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

(* lazy declaration of tuples *)

let tuples_needed = Hashtbl.create 17

let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n

let add_tuple_decls uc =
181
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
182 183 184 185 186 187 188 189
    tuples_needed uc

let with_tuples ?(reset=false) f uc x =
  let uc = f (add_tuple_decls uc) x in
  if reset then Hashtbl.clear tuples_needed;
  uc

let add_ty_decl  = with_tuples add_ty_decl
190
let add_ty_decls = with_tuples ~reset:true add_ty_decl
191 192

let add_logic_decl  = with_tuples add_logic_decl
193
let add_logic_decls = with_tuples ~reset:true add_logic_decl
194 195

let add_ind_decl  = with_tuples add_ind_decl
196
let add_ind_decls = with_tuples ~reset:true add_ind_decl
197

198 199
let add_prop_decl = with_tuples ~reset:true add_prop_decl

200 201
let rec type_inst s ty = match ty.ty_node with
  | Ty.Tyvar n -> Mtv.find n s
202
  | Ty.Tyapp (ts, tyl) -> tyapp (ts, List.map (type_inst s) tyl)
203 204

let rec dty env = function
205
  | PPTtyvar {id=x} ->
206
      tyvar (find_user_type_var x env)
207 208
  | PPTtyapp (p, x) ->
      let loc = qloc x in
209
      let ts, a = specialize_tysymbol loc x env.uc in
210 211 212
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
213
      begin match ts.ts_def with
214
	| None ->
215
	    tyapp (ts, tyl)
216
	| Some ty ->
217 218 219
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    type_inst s ty
220 221 222
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
223
      tyapp (ts, List.map (dty env) tyl)
224 225 226 227

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
228
  try find ns sl
229 230
  with Not_found -> error ~loc (UnboundSymbol sl)

231
let find_prop_ns = find_ns ns_find_pr
232 233 234 235 236 237 238 239
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)

240 241 242
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

243 244
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
245 246
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
247

248
let specialize_fsymbol p uc =
249
  let s,tl,ty = specialize_lsymbol p uc in
250
  match ty with
251
    | None -> let loc = qloc p in error ~loc TermExpected
252
    | Some ty -> s, tl, ty
253

254
let specialize_psymbol p uc =
255
  let s,tl,ty = specialize_lsymbol p uc in
256 257
  match ty with
    | None -> s, tl
258 259
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

260
let is_psymbol p uc =
261 262
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263

Andrei Paskevich's avatar
Andrei Paskevich committed
264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337
(* [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
    let v, t = match Decl.open_fs_defn def with
      | [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 ->
	  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
      | _ ->
	  raise Exit
    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

338

339 340
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
341 342 343 344
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

345
(** Typing terms and formulas *)
346 347 348 349 350 351 352

let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

Andrei Paskevich's avatar
Andrei Paskevich committed
353
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
354
  let s = ref Sstr.empty in
355
  let add id =
356
    if Sstr.mem id.id !s then
357
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
358
    s := Sstr.add id.id !s
359 360 361 362
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
363
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
364
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
365
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
366
    | PPpor (p, _) -> check p
367
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
368
  check p
369

370 371
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
372
  tyvar (create_ty_decl_var ~loc ~user:false tv)
373

Andrei Paskevich's avatar
Andrei Paskevich committed
374 375 376 377 378
let rec dpat env pat =
  let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
  env, { dp_node = n; dp_ty = ty }

and dpat_node loc env = function
379
  | PPpwild ->
380
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
381
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
382
  | PPpvar x ->
383
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
384
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
385 386
      env, Pvar x, ty
  | PPpapp (x, pl) ->
387
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
388 389
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
390 391 392 393 394 395 396 397 398 399 400 401 402 403
  | PPprec fl ->
      let renv = ref env in
      let _,cs,fl = list_fields env.uc fl in
      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
            let env,e = dpat !renv e in
            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
404 405 406 407 408
  | 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
      let env, pl = dpat_args s.ls_name loc env tyl pl in
409
      let ty = tyapp (ts_tuple n, tyl) in
410
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
411
  | PPpas (p, x) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
412
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
413
      let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
414
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
415 416 417
  | PPpor (p, q) ->
      let env, p = dpat env p in
      let env, q = dpat env q in
Andrei Paskevich's avatar
Andrei Paskevich committed
418
      unify_raise ~loc p.dp_ty q.dp_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
419
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
420

421
and dpat_args s loc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
423
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
  let rec check_arg env = function
425
    | [], [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
426 427 428 429
	env, []
    | a :: al, p :: pl ->
	let loc = p.pat_loc in
	let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
430
	unify_raise ~loc p.dp_ty a;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431 432
	let env, pl = check_arg env (al, pl) in
	env, p :: pl
Andrei Paskevich's avatar
Andrei Paskevich committed
433 434 435
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
436
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
437

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
let rec trigger_not_a_term_exn = function
439
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
440 441 442
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

443
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
444
  let s = ref Sstr.empty in
445
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
446 447
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
448
  in
449
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
450

Andrei Paskevich's avatar
Andrei Paskevich committed
451 452 453 454 455 456 457 458 459
let check_highord env x tl = match x with
  | Qident { id = x } when Mstr.mem x env.dvars -> true
  | _ -> List.length tl > List.length ((find_lsymbol x env.uc).ls_args)

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

460 461 462 463 464 465 466 467 468 469
let rec dterm ?(localize=false) env { pp_loc = loc; pp_desc = t } =
  let n, ty = dterm_node ~localize loc env t in
  let t = { dt_node = n; dt_ty = ty } in
  if localize then
    let n = Tnamed (Ident.label ~loc "", t) in
    { dt_node = n; dt_ty = ty }
  else
    t

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

649 650 651 652 653
and dfmla ?(localize=false) env { pp_loc = loc; pp_desc = f } =
  let n = dfmla_node ~localize loc env f in
  if localize then Fnamed (Ident.label ~loc "", n) else n

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

Andrei Paskevich's avatar
Andrei Paskevich committed
734 735 736 737
and dpat_list env ty p =
  check_pat_linearity p;
  let loc = p.pat_loc in
  let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
738
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
739
  env, p
740

741 742 743 744
and dtype_args s loc env el tl =
  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
745
    | [], [] ->
746 747 748 749
	[]
    | a :: al, t :: bl ->
	let loc = t.pp_loc in
	let t = dterm env t in
Andrei Paskevich's avatar
Andrei Paskevich committed
750
	unify_raise ~loc t.dt_ty a;
751 752 753 754 755 756
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772
(** 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
773
    t_close_branch (pat_app cs al tyarg) (t_var vs)
774 775
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
776
  let t = t_case (t_var vs) (List.map per_cs cl) in
777 778 779 780 781
  let d = make_fs_defn fs [vs] t in
  add_logic_decl th [d]

let add_projections th d = match d.td_def with
  | TDabstract | TDalias _ -> th
782
  | TDrecord _ -> assert false
783 784 785 786 787 788 789 790
  | TDalgebraic cl ->
      let per_cs acc (_,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 per_param acc ty (n,_) = match n with
791 792 793
          | Some { id = id ; id_lab = labels ; id_loc = loc }
            when not (Mstr.mem id acc) ->
              let fn = id_user ~labels id loc in
794
              let fs = create_fsymbol fn [tc] ty in
795
              Mstr.add id (fs,tc,ty) acc
796 797 798 799 800 801 802 803
          | _ -> acc
        in
        List.fold_left2 per_param acc cs.ls_args pl
      in
      let ps = List.fold_left per_cs Mstr.empty cl in
      try Mstr.fold (add_projection cl) ps th
      with e -> raise (Loc.Located (d.td_loc, e))

804
(** Typing declarations, that is building environments. *)
805 806 807

open Ptree

808
let add_types dl th =
809
  let def = List.fold_left
810
    (fun def d ->
811
      let id = d.td_ident.id in
812
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
813 814
      Mstr.add id d def)
    Mstr.empty dl
815
  in
816
  let tysymbols = Hashtbl.create 17 in
817
  let rec visit x =
818 819 820 821 822 823
    try
      match Hashtbl.find tysymbols x with
	| None -> error CyclicTypeDef
	| Some ts -> ts
    with Not_found ->
      Hashtbl.add tysymbols x None;
Andrei Paskevich's avatar
Andrei Paskevich committed
824
      let d = Mstr.find x def in
825 826
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
827 828
      let vl =
	List.map
829 830 831 832
	  (fun { id = v ; id_lab = labels ; id_loc = loc } ->
	     if Hashtbl.mem vars v then error ~loc (DuplicateTypeVar v);
	     let i = create_tvsymbol (id_user ~labels v loc) in
	     Hashtbl.add vars v i;