Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

typing.ml 39.4 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
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 176 177 178 179 180 181
  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 =
182
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
183 184 185 186 187 188 189 190
    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
191
let add_ty_decls = with_tuples ~reset:true add_ty_decl
192 193

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

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

199 200
let add_prop_decl = with_tuples ~reset:true add_prop_decl

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

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

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

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
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 338
(* [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

339

340 341
(** Typing types *)

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

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

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

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

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

375 376
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
377 378
  env, { dp_node = n; dp_ty = ty }

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

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

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

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

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

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

461 462
let rec dterm ?(localize=false) uc env { pp_loc = loc; pp_desc = t } =
  let n, ty = dterm_node ~localize loc uc env t in
463
  let t = { dt_node = n; dt_ty = ty } in
464 465 466 467 468 469
  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
470

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

655 656
and dfmla ?(localize=false) uc env { pp_loc = loc; pp_desc = f } =
  let f = dfmla_node ~localize loc uc env f in
657 658 659 660 661 662
  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
663

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

751
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
752 753
  check_pat_linearity p;
  let loc = p.pat_loc in
754
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
755
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
756
  env, p
757

758
and dtype_args s loc uc env el tl =
759 760 761
  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
762
    | [], [] ->
763 764 765
	[]
    | a :: al, t :: bl ->
	let loc = t.p