typing.ml 39.7 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

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

32 33
(** errors *)

34
exception DuplicateVar of string
35 36 37
exception DuplicateTypeVar of string
exception PredicateExpected
exception TermExpected
38 39
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
40 41 42 43 44
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
45

46 47 48
let error = Loc.error

let errorm = Loc.errorm
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
49

50
let rec print_qualid fmt = function
51
  | Qident s -> fprintf fmt "%s" s.id
52
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
53

54
let () = Exn_printer.register (fun fmt e -> match e with
55
  | DuplicateTypeVar s ->
56 57 58
      fprintf fmt "Duplicate type parameter %s" s
  | DuplicateVar s ->
      fprintf fmt "Duplicate variable %s" s
59 60 61 62
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
63 64 65 66
  | FSymExpected ls ->
      fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
67
  | ClashTheory s ->
68
      fprintf fmt "Clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69 70
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
71 72
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
73 74 75 76
  | 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
77
  | _ -> raise e)
78

79 80
let debug_parse_only = Debug.register_stop_flag "parse_only"
let debug_type_only  = Debug.register_stop_flag "type_only"
81

82 83
(** Environments *)

84
(** typing using destructive type variables
85

86 87 88 89 90 91
    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
92

93 94
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95 96
let term_expected_type ~loc ty1 ty2 =
  errorm ~loc
97
    "This term has type %a@ but is expected to have type@ %a"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
98 99
    print_dty ty1 print_dty ty2

Andrei Paskevich's avatar
Andrei Paskevich committed
100 101 102
let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

103 104 105 106
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

107
type denv = {
108
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
109
  dvars   : dty Mstr.t;    (* local variables, to be bound later *)
110 111
}

112
let create_denv () = {
113
  utyvars = Hashtbl.create 17;
114 115 116
  dvars = Mstr.empty;
}

117 118 119 120 121
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

122 123 124 125
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
126
    let v = create_user_type_var x in
127 128
    Hashtbl.add env.utyvars x v;
    v
129

130 131 132 133
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 }

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

137 138 139 140 141 142 143 144 145 146 147 148
(* 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
149 150
  try ns_find_ts (get_namespace uc) sl
  with Not_found -> error ~loc (UnboundType sl)
151 152 153

(* lazy declaration of tuples *)

154 155 156 157
let add_ty_decl uc dl = add_decl_with_tuples uc (create_ty_decl dl)
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
let add_ind_decl uc dl = add_decl_with_tuples uc (create_ind_decl dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
158

159
let rec dty uc env = function
160
  | PPTtyvar {id=x} ->
161
      tyvar (find_user_type_var x env)
162 163
  | PPTtyapp (p, x) ->
      let loc = qloc x in
164
      let ts = specialize_tysymbol loc x uc in
165
      let tyl = List.map (dty uc env) p in
166
      Loc.try2 loc tyapp ts tyl
167 168
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
169
      tyapp ts (List.map (dty uc env) tyl)
170 171 172 173

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
174
  try find ns sl
175 176
  with Not_found -> error ~loc (UnboundSymbol sl)

177
let find_prop_ns = find_ns ns_find_pr
178 179 180 181 182 183 184 185
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)

186 187 188 189 190 191 192 193 194 195 196
let find_fsymbol_ns q ns =
  let ls = find_lsymbol_ns q ns in
  if ls.ls_value = None then error ~loc:(qloc q) (FSymExpected ls) else ls

let find_psymbol_ns q ns =
  let ls = find_lsymbol_ns q ns in
  if ls.ls_value <> None then error ~loc:(qloc q) (PSymExpected ls) else ls

let find_fsymbol q uc = find_fsymbol_ns q (get_namespace uc)
let find_psymbol q uc = find_psymbol_ns q (get_namespace uc)

197 198 199
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

200 201
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
202 203
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
204

205
let specialize_fsymbol p uc =
206
  let s,tl,ty = specialize_lsymbol p uc in
207
  match ty with
208
    | None -> let loc = qloc p in error ~loc TermExpected
209
    | Some ty -> s, tl, ty
210

211
let specialize_psymbol p uc =
212
  let s,tl,ty = specialize_lsymbol p uc in
213 214
  match ty with
    | None -> s, tl
215 216
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

217
let is_psymbol p uc =
218 219
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220

221
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
222 223 224 225 226 227 228 229 230 231 232 233
(* [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
234
      | Ty.Tyvar tv -> Stv.add_new Exit tv tvs
Andrei Paskevich's avatar
Andrei Paskevich committed
235 236 237 238 239 240 241 242 243 244
      | _ -> (* 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
245
    let v, t = match Decl.open_ls_defn def with
Andrei Paskevich's avatar
Andrei Paskevich committed
246 247 248 249 250 251 252 253 254 255 256 257 258 259
      | [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 ->
260 261 262 263 264 265
          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
266
      | _ ->
267
          raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
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
    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
295
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
296

297

298 299
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300 301 302 303
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

304
(** Typing terms and formulas *)
305 306

let binop = function
307 308 309 310
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
311

Andrei Paskevich's avatar
Andrei Paskevich committed
312
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
313
  let s = ref Sstr.empty in
314
  let add id =
315
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
316 317 318 319
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
320
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
321
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
322
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
323
    | PPpor (p, _) -> check p
324
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
325
  check p
326

327 328
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
329
  tyvar (create_ty_decl_var ~loc ~user:false tv)
330

331 332
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
333 334
  env, { dp_node = n; dp_ty = ty }

335
and dpat_node loc uc env = function
336
  | PPpwild ->
337
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
338
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
339
  | PPpvar x ->
340
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
341
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
342 343
      env, Pvar x, ty
  | PPpapp (x, pl) ->
344
      let s, tyl, ty = specialize_fsymbol x uc in
345
      let env, pl = dpat_args s loc uc env tyl pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
346
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
347 348
  | PPprec fl ->
      let renv = ref env in
349 350
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
351
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
352 353
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
354
            let loc = e.pat_loc in
355
            let env,e = dpat uc !renv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
356 357 358
            unify_raise ~loc e.dp_ty ty;
            renv := env;
            e
359 360
        | None ->
            { dp_node = Pwild; dp_ty = ty }
Andrei Paskevich's avatar
Andrei Paskevich committed
361
      in
362 363
      let al = List.map2 get_val pjl tyl in
      !renv, Papp (cs, al), Util.of_option ty
364 365 366 367
  | 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
368
      let env, pl = dpat_args s loc uc env tyl pl in
369
      let ty = tyapp (ts_tuple n) tyl in
370
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
371
  | PPpas (p, x) ->
372
      let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
373
      let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
374
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
375
  | PPpor (p, q) ->
376 377
      let env, p = dpat uc env p in
      let env, q = dpat uc env q in
Andrei Paskevich's avatar
Andrei Paskevich committed
378
      unify_raise ~loc p.dp_ty q.dp_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
379
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
380

381
and dpat_args ls loc uc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
382
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
383
  if n <> m then error ~loc (BadArity (ls,n,m));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
384
  let rec check_arg env = function
385
    | [], [] ->
386
        env, []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387
    | a :: al, p :: pl ->
388 389 390 391 392
        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
393
    | _ ->
394
        assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
395
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
396
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
397

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398
let rec trigger_not_a_term_exn = function
399
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400 401 402
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

403
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
404
  let s = ref Sstr.empty in
405
  let check id =
406
    s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
407
  in
408
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
409

410
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
411
  | Qident { id = x } when Mstr.mem x env.dvars -> true
412
  | _ -> List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
413 414 415 416 417 418

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

419
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
420
  let n, ty = dterm_node ~localize loc uc env t in
421
  let t = { dt_node = n; dt_ty = ty } in
422 423
  let rec down loc e = match e.dt_node with
    | Tnamed (Lstr _, e) -> down loc e
424 425 426
    | Tnamed (Lpos _, _) -> t
    | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
  in
427 428 429 430
  match localize with
    | Some (Some loc) -> down loc t
    | Some None -> down loc t
    | None -> t
431

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

605
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
606
  let f = dfmla_node ~localize loc uc env f in
607 608
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
609 610 611
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
612 613 614 615
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
616

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

706
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
707 708
  check_pat_linearity p;
  let loc = p.pat_loc in
709
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
710
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
711
  env, p
712

713
and dtype_args ~localize ls loc uc env el tl =
714
  let n = List.length el and m = List.length tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
715
  if n <> m then error ~loc (BadArity (ls,n,m));
716
  let rec check_arg = function
717
    | [], [] ->
718
        []
719
    | a :: al, t :: bl ->
720
        let loc = t.pp_loc in
721
        let t = dterm ~localize uc env t in
722 723
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
724
    | _ ->
725
        assert false
726 727 728
  in
  check_arg (el, tl)

729 730
(** Add projection functions for the algebraic types *)

731
(*
732 733 734 735 736 737 738 739 740 741 742 743 744 745
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
746
    t_close_branch (pat_app cs al tyarg) (t_var vs)
747 748
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
749
  let t = t_case (t_var vs) (List.map per_cs cl) in
750
  let d = make_ls_defn fs [vs] t in
751 752 753 754
  add_logic_decl th [d]

let add_projections th d = match d.td_def with
  | TDabstract | TDalias _ -> th
755
  | TDrecord _ -> assert false
756 757 758 759 760 761 762 763
  | 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
764 765
          | Some id when not (Mstr.mem id.id acc) ->
              let fn = create_user_id id in
766
              let fs = create_fsymbol fn [tc] ty in
767
              Mstr.add id.id (fs,tc,ty) acc
768 769 770 771 772 773 774
          | _ -> 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))
775
*)
776

777
(** Typing declarations, that is building environments. *)
778 779 780

open Ptree

781
let add_types dl th =
782
  let def = List.fold_left
783
    (fun def d ->
Andrei Paskevich's avatar