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 40.4 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 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
let rec dty uc env = function
202
  | PPTtyvar {id=x} ->
203
      tyvar (find_user_type_var x env)
204 205
  | PPTtyapp (p, x) ->
      let loc = qloc x in
206
      let ts, a = specialize_tysymbol loc x uc in
207 208
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
209
      let tyl = List.map (dty uc env) p in
210
      tyapp ts tyl
211 212
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
213
      tyapp ts (List.map (dty uc env) tyl)
214 215 216 217

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
218
  try find ns sl
219 220
  with Not_found -> error ~loc (UnboundSymbol sl)

221
let find_prop_ns = find_ns ns_find_pr
222 223 224 225 226 227 228 229
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)

230 231 232
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

233 234
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
235 236
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
237

238
let specialize_fsymbol p uc =
239
  let s,tl,ty = specialize_lsymbol p uc in
240
  match ty with
241
    | None -> let loc = qloc p in error ~loc TermExpected
242
    | Some ty -> s, tl, ty
243

244
let specialize_psymbol p uc =
245
  let s,tl,ty = specialize_lsymbol p uc in
246 247
  match ty with
    | None -> s, tl
248 249
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

250
let is_psymbol p uc =
251 252
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
253

Andrei Paskevich's avatar
Andrei Paskevich committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
(* [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
277
    let v, t = match Decl.open_ls_defn def with
Andrei Paskevich's avatar
Andrei Paskevich committed
278 279 280 281 282 283 284 285 286 287 288 289 290 291
      | [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 ->
292 293 294 295 296 297
          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
298
      | _ ->
299
          raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
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
    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

328

329 330
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331 332 333 334
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

335
(** Typing terms and formulas *)
336 337

let binop = function
338 339 340 341
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
342

Andrei Paskevich's avatar
Andrei Paskevich committed
343
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
344
  let s = ref Sstr.empty in
345
  let add id =
346
    if Sstr.mem id.id !s then
347
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
348
    s := Sstr.add id.id !s
349 350 351 352
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
353
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
354
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
355
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
356
    | PPpor (p, _) -> check p
357
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
358
  check p
359

360 361
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
362
  tyvar (create_ty_decl_var ~loc ~user:false tv)
363

364 365
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
366 367
  env, { dp_node = n; dp_ty = ty }

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

411
and dpat_args s loc uc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
413
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
414
  let rec check_arg env = function
415
    | [], [] ->
416
        env, []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
417
    | a :: al, p :: pl ->
418 419 420 421 422
        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
423
    | _ ->
424
        assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
425
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
426
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
427

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
428
let rec trigger_not_a_term_exn = function
429
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
430 431 432
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

433
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
434
  let s = ref Sstr.empty in
435
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
436 437
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
438
  in
439
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
440

441
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
442
  | Qident { id = x } when Mstr.mem x env.dvars -> true
443
  | _ -> List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
444 445 446 447 448 449

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

450 451
let rec dterm ?(localize=false) uc env { pp_loc = loc; pp_desc = t } =
  let n, ty = dterm_node ~localize loc uc env t in
452
  let t = { dt_node = n; dt_ty = ty } in
453 454 455 456 457 458
  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
459

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

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

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

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

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