typing.ml 40.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Format
14
open Ident
15
open Ptree
16
open Ty
17
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
18
open Decl
19
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
20
open Env
21
open Denv
Andrei Paskevich's avatar
Andrei Paskevich committed
22

23 24
(** errors *)

25
exception DuplicateVar of string
26 27 28
exception DuplicateTypeVar of string
exception PredicateExpected
exception TermExpected
29 30
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
31
exception ClashTheory of string
32
(* dead code
33
exception UnboundTheory of qualid
34
*)
35
exception UnboundTypeVar of string
36
(* dead code
37
exception UnboundType of string list
38
*)
39
exception UnboundSymbol of qualid
40

41 42 43
let error = Loc.error

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

45
let rec print_qualid fmt = function
46
  | Qident s -> fprintf fmt "%s" s.id
47
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
48

49
let () = Exn_printer.register (fun fmt e -> match e with
50
  | DuplicateTypeVar s ->
51 52 53
      fprintf fmt "Duplicate type parameter %s" s
  | DuplicateVar s ->
      fprintf fmt "Duplicate variable %s" s
54 55 56 57
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
58 59 60 61
  | 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
62
  | ClashTheory s ->
63
      fprintf fmt "Clash with previous theory %s" s
64
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65 66
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
67
*)
68 69
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
70
(* dead code
71 72
  | UnboundType sl ->
       fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
73
*)
74 75
  | UnboundSymbol q ->
       fprintf fmt "Unbound symbol '%a'" print_qualid q
76
  | _ -> raise e)
77

78
let debug_parse_only = Debug.register_flag "parse_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
79
  ~desc:"Stop@ after@ parsing."
80
let debug_type_only  = Debug.register_flag "type_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  ~desc:"Stop@ after@ type-checking."
82

83 84
(** Environments *)

85
(** typing using destructive type variables
86

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

94 95
*)

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

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

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

108
let create_user_tv =
109 110
  let hs = Hstr.create 17 in
  fun s -> try Hstr.find hs s with Not_found ->
111
  let tv = create_tvsymbol (id_fresh s) in
112
  Hstr.add hs s tv;
113 114 115 116 117 118
  tv

(* TODO: shouldn't we localize this ident? *)
let create_user_type_var x =
  tyuvar (create_user_tv x)

119
type denv = {
120 121
  dvars : dty Mstr.t;    (* local variables, to be bound later *)
  gvars : qualid -> vsymbol option; (* global variables, for programs *)
122 123
}

124 125
let denv_empty = { dvars = Mstr.empty; gvars = Util.const None }
let denv_empty_with_globals gv = { dvars = Mstr.empty; gvars = gv }
126

127
(* dead code
128 129
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
130
*)
131
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
132

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

138 139 140 141 142 143 144 145 146 147
(* 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

148 149
(* lazy declaration of tuples *)

150 151 152
let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl)
let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls)
153
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
154
let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
155
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
156

157
let find_ns get_id find p ns =
158 159
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
160 161 162 163
  try
    let r = find ns sl in
    if Debug.test_flag Glob.flag then Glob.use loc (get_id r);
    r
164
  with Not_found -> error ~loc (UnboundSymbol p)
165

166 167
let get_id_prop p = p.pr_name
let find_prop_ns = find_ns get_id_prop ns_find_pr
168 169
let find_prop p uc = find_prop_ns p (get_namespace uc)

170 171
let get_id_ts ts = ts.ts_name
let find_tysymbol_ns = find_ns get_id_ts ns_find_ts
172 173
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

174 175
let get_id_ls ls = ls.ls_name
let find_lsymbol_ns = find_ns get_id_ls ns_find_ls
176 177
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

178 179 180 181 182 183 184 185 186 187 188
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)

189 190
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
191
(* dead code
192
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
193
*)
194

195
let rec dty uc = function
196
  | PPTtyvar ({id=x}, _) ->
197
      create_user_type_var x
198
  | PPTtyapp (x, p) ->
199 200
      let ts = find_tysymbol x uc in
      let tyl = List.map (dty uc) p in
201
      Loc.try2 ~loc:(qloc x) tyapp ts tyl
202 203 204 205
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      tyapp ts (List.map (dty uc) tyl)

206
let rec ty_of_pty uc = function
207
  | PPTtyvar ({id=x}, _) ->
208
      ty_var (create_user_tv x)
209
  | PPTtyapp (x, p) ->
210 211
      let ts = find_tysymbol x uc in
      let tyl = List.map (ty_of_pty uc) p in
212
      Loc.try2 ~loc:(qloc x) ty_app ts tyl
213 214 215 216
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      ty_app ts (List.map (ty_of_pty uc) tyl)

217 218 219 220 221 222 223 224 225 226
let rec opaque_tvs acc = function
  | Ptree.PPTtyvar (id, true) -> Stv.add (create_user_tv id.id) acc
  | Ptree.PPTtyvar (_, false) -> acc
  | Ptree.PPTtyapp (_, pl)
  | Ptree.PPTtuple pl -> List.fold_left opaque_tvs acc pl

let opaque_tvs args value =
  let acc = Opt.fold opaque_tvs Stv.empty value in
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) acc args

227 228
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
229 230
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
231

232
let specialize_fsymbol p uc =
233
  let s,tl,ty = specialize_lsymbol p uc in
234
  match ty with
235
    | None -> let loc = qloc p in error ~loc TermExpected
236
    | Some ty -> s, tl, ty
237

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

244
let is_psymbol p uc =
245 246
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247

248 249
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250 251 252 253
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

254
(** Typing terms and formulas *)
255 256

let binop = function
257 258 259 260
  | PPand -> Tand
  | PPor -> Tor
  | PPimplies -> Timplies
  | PPiff -> Tiff
261

Andrei Paskevich's avatar
Andrei Paskevich committed
262
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
263
  let s = ref Sstr.empty in
264 265
  let add { id = id; id_loc = loc } =
    s := Loc.try3 ~loc Sstr.add_new (DuplicateVar id) id !s
266 267 268 269
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
270
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
Andrei Paskevich's avatar
Andrei Paskevich committed
271
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
272
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
273
    | PPpor (p, _) -> check p
274
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
275
  check p
276

277 278
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
279 280
  env, { dp_node = n; dp_ty = ty }

281
and dpat_node loc uc env = function
282
  | PPpwild ->
283
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
284
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
285
  | PPpvar x ->
286
      let ty = fresh_type_var loc in
287
      let env = add_var x.id ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
288 289
      env, Pvar x, ty
  | PPpapp (x, pl) ->
290
      let s, tyl, ty = specialize_fsymbol x uc in
291
      let env, pl = dpat_args s loc uc env tyl pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
292
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
293 294
  | PPprec fl ->
      let renv = ref env in
295
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
296
      let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
297
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
298 299
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
300
            let loc = e.pat_loc in
301
            let env,e = dpat uc !renv e in
Andrei Paskevich's avatar
Andrei Paskevich committed
302 303 304
            unify_raise ~loc e.dp_ty ty;
            renv := env;
            e
305 306
        | None ->
            { dp_node = Pwild; dp_ty = ty }
Andrei Paskevich's avatar
Andrei Paskevich committed
307
      in
308
      let al = List.map2 get_val pjl tyl in
309
      !renv, Papp (cs, al), Opt.get ty
310 311 312 313
  | 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
314
      let env, pl = dpat_args s loc uc env tyl pl in
315
      let ty = tyapp (ts_tuple n) tyl in
316
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
317
  | PPpas (p, x) ->
318
      let env, p = dpat uc env p in
319
      let env = add_var x.id p.dp_ty env in
Andrei Paskevich's avatar
Andrei Paskevich committed
320
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
321
  | PPpor (p, q) ->
322 323
      let env, p = dpat uc env p in
      let env, q = dpat uc env q in
Andrei Paskevich's avatar
Andrei Paskevich committed
324
      unify_raise ~loc p.dp_ty q.dp_ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
325
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
326

327
and dpat_args ls loc uc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328
  let n = List.length el and m = List.length pl in
329
  if n <> m then error ~loc (BadArity (ls,m));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
330
  let rec check_arg env = function
331
    | [], [] ->
332
        env, []
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
    | a :: al, p :: pl ->
334 335 336 337 338
        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
339
    | _ ->
340
        assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
341
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
342
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
343

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
344
let rec trigger_not_a_term_exn = function
345
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
346 347 348
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

349
let param_tys uc pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
350
  let s = ref Sstr.empty in
351 352 353
  let ty_of_param (loc,id,gh,ty) =
    if gh then Loc.errorm ~loc "ghost parameters are not allowed here";
    Opt.iter (fun { id = id; id_loc = loc } ->
354
      s := Loc.try3 ~loc Sstr.add_new (DuplicateVar id) id !s) id;
355 356 357 358 359 360 361 362 363 364 365 366
    ty_of_dty (dty uc ty) in
  List.map ty_of_param pl

let quant_var uc env (id,ty) =
  let ty = match ty with
    | None -> Denv.fresh_type_var id.id_loc
    | Some ty -> dty uc ty in
  add_var id.id ty env, (id,ty)

let quant_vars uc env qvl =
  let s = ref Sstr.empty in
  let add env (({ id = id; id_loc = loc }, _) as qv) =
367
    s := Loc.try3 ~loc Sstr.add_new (DuplicateVar id) id !s;
368 369
    quant_var uc env qv in
  Lists.map_fold_left add env qvl
370

371
let check_highord uc env x tl = match x with
Andrei Paskevich's avatar
Andrei Paskevich committed
372
  | Qident { id = x } when Mstr.mem x env.dvars -> true
373 374
  | _ -> env.gvars x <> None ||
      List.length tl > List.length ((find_lsymbol x uc).ls_args)
Andrei Paskevich's avatar
Andrei Paskevich committed
375 376 377 378 379 380

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

381
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
382
  let n, ty = dterm_node ~localize loc uc env t in
383
  let t = { dt_node = n; dt_ty = ty } in
384 385
  let rec down loc e = match e.dt_node with
    | Tnamed (Lstr _, e) -> down loc e
386 387 388
    | Tnamed (Lpos _, _) -> t
    | _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
  in
389 390 391 392
  match localize with
    | Some (Some loc) -> down loc t
    | Some None -> down loc t
    | None -> t
393

394
and dterm_node ~localize loc uc env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
395
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
396
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
397
      let ty = Mstr.find x env.dvars in
398
      Tvar x, ty
399
  | PPvar x when env.gvars x <> None ->
400
      let vs = Opt.get (env.gvars x) in
401
      Tgvar vs, dty_of_ty vs.vs_ty
402
  | PPvar x ->
403
      (* 0-arity symbol (constant) *)
404
      let s, tyl, ty = specialize_fsymbol x uc in
405
      if tyl <> [] then error ~loc (BadArity (s,0));
406
      Tapp (s, []), ty
407
  | PPapp (x, tl) when check_highord uc env x tl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
408 409
      let tl = apply_highord loc x tl in
      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
410
      let tl = dtype_args ~localize fs_func_app loc uc env atyl tl in
411
      Tapp (fs_func_app, tl), Opt.get aty
412
  | PPapp (x, tl) ->
413
      let s, tyl, ty = specialize_fsymbol x uc in
414
      let tl = dtype_args ~localize s loc uc env tyl tl in
415
      Tapp (s, tl), ty
416 417 418 419
  | 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
420
      let tl = dtype_args ~localize s loc uc env tyl tl in
421
      let ty = tyapp (ts_tuple n) tyl in
422
      Tapp (s, tl), ty
423 424
  | PPinfix (e1, x, e2)
  | PPinnfix (e1, x, e2) ->
425
      if x.id = "infix <>" then error ~loc TermExpected;
426
      let s, tyl, ty = specialize_fsymbol (Qident x) uc in
427
      let tl = dtype_args ~localize s loc uc env tyl [e1; e2] in
428
      Tapp (s, tl), ty
429
  | PPconst (Number.ConstInt _ as c) ->
430
      Tconst c, tyapp Ty.ts_int []
431
  | PPconst (Number.ConstReal _ as c) ->
432
      Tconst c, tyapp Ty.ts_real []
Andrei Paskevich's avatar
Andrei Paskevich committed
433
  | PPlet (x, e1, e2) ->
434
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435
      let ty = e1.dt_ty in
436
      let env = add_var x.id ty env in
437
      let e2 = dterm ~localize uc env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
438
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
439
  | PPmatch (e1, bl) ->
440
      let t1 = dterm ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
441
      let ty1 = t1.dt_ty in
442
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
443
      let branch (p, e) =
444
        let env, p = dpat_list uc env ty1 p in
445
        let loc = e.pp_loc in
446 447
        let e = dterm ~localize uc env e in
        unify_raise ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
448
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
449 450
      in
      let bl = List.map branch bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
451
      Tmatch (t1, bl), tb
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
452
  | PPnamed (x, e1) ->
453
      let localize = match x with
454
        | Lpos l -> Some (Some l)
455
        | Lstr _ -> localize
456
      in
457
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
458
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459 460
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
461
      let e1 = dterm ~localize uc env e1 in
462
      let ty = dty uc ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
463
      unify_raise ~loc e1.dt_ty ty;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
464
      e1.dt_node, ty
465 466
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
467 468
      let e2 = dterm ~localize uc env e2 in
      let e3 = dterm ~localize uc env e3 in
Andrei Paskevich's avatar
Andrei Paskevich committed
469
      unify_raise ~loc e3.dt_ty e2.dt_ty;
470
      Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty
471 472
  | PPeps (b, e1) ->
      let env, (x, ty) = quant_var uc env b in
473
      let e1 = dfmla ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
474
      Teps (x, ty, e1), ty
475
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
476
      let env, uqu = quant_vars uc env uqu in
Andrei Paskevich's avatar
Andrei Paskevich committed
477
      let trigger e =
478 479 480 481
        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
482 483
      in
      let trl = List.map (List.map trigger) trl in
484
      let e = match q with
485 486
        | PPfunc -> TRterm (dterm ~localize uc env a)
        | PPpred -> TRfmla (dfmla ~localize uc env a)
487 488 489 490
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
Andrei Paskevich's avatar
Andrei Paskevich committed
491
        | TRterm t ->
492
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
493
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
494
              let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty)
Andrei Paskevich's avatar
Andrei Paskevich committed
495 496 497 498 499 500 501 502 503
              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
504
        | TRfmla f ->
505
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
506 507 508 509 510
            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) ->
511 512
              let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty)
              uqu ([], tyapp ts_pred [uty])
Andrei Paskevich's avatar
Andrei Paskevich committed
513 514 515 516 517 518 519 520
            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
521
            id, ty, Fbinop (Tiff, Fapp (ps_pred_app, [h;u]), f)
Andrei Paskevich's avatar
Andrei Paskevich committed
522
      in
523
      Teps (id, ty, Fquant (Tforall, uqu, trl, f)), ty
524
  | PPrecord fl ->
525
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
526
      let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
527
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
528 529
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
530
            let loc = e.pp_loc in
531
            let e = dterm ~localize uc env e in
Andrei Paskevich's avatar
Andrei Paskevich committed
532 533
            unify_raise ~loc e.dt_ty ty;
            e
534
        | None -> error ~loc (RecordFieldMissing (cs,pj))
535
      in
536
      let al = List.map2 get_val pjl tyl in
537
      Tapp (cs,al), Opt.get ty
Andrei Paskevich's avatar
Andrei Paskevich committed
538
  | PPupdate (e,fl) ->
539
      let e = dterm ~localize uc env e in
540
      let fl = List.map (fun (q,e) -> find_lsymbol q uc,e) fl in
541
      let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
542
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
543 544
      let get_val pj ty = match Mls.find_opt pj flm with
        | Some e ->
Andrei Paskevich's avatar
Andrei Paskevich committed
545
            let loc = e.pp_loc in
546
            let e = dterm ~localize uc env e in
547
            unify_raise ~loc e.dt_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
548 549
            e
        | None ->
550
            let ptyl,pty = Denv.specialize_lsymbol ~loc pj in
551
            unify_raise ~loc (Opt.get pty) ty;
552 553 554
            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
555
      in
556
      let al = List.map2 get_val pjl tyl in
557
      Tapp (cs,al), Opt.get ty
Andrei Paskevich's avatar
Andrei Paskevich committed
558
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
559
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
560

561
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
562
  let f = dfmla_node ~localize loc uc env f in
563 564
  let rec down loc e = match e with
    | Fnamed (Lstr _, e) -> down loc e
565 566 567
    | Fnamed (Lpos _, _) -> f
    | _ -> Fnamed (Lpos loc, f)
  in
568 569 570 571
  match localize with
    | Some (Some loc) -> down loc f
    | Some None -> down loc f
    | None -> f
572

573
and dfmla_node ~localize loc uc env = function
574 575 576 577
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
578
  | PPunop (PPnot, a) ->
579
      Fnot (dfmla ~localize uc env a)
580
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
581
      Fbinop (binop op, dfmla ~localize uc env a, dfmla ~localize uc env b)
582
  | PPif (a, b, c) ->
583
      Fif (dfmla ~localize uc env a,
584
           dfmla ~localize uc env b, dfmla ~localize uc env c)
585
  | PPquant (q, uqu, trl, a) ->
586
      let env, uqu = quant_vars uc env uqu in
587
      let trigger e =
588 589 590 591
        try
          TRterm (dterm ~localize uc env e)
        with exn when trigger_not_a_term_exn exn ->
          TRfmla (dfmla ~localize uc env e)
592 593
      in
      let trl = List.map (List.map trigger) trl in
594
      let q = match q with
595 596
        | PPforall -> Tforall
        | PPexists -> Texists
597
        | _ -> error ~loc PredicateExpected
598
      in
599 600
      Fquant (q, uqu, trl, dfmla ~localize uc env a)
  | PPapp (x, tl) when check_highord uc env x tl ->
601 602
      let tl = apply_highord loc x tl in
      let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in
603
      let tl = dtype_args ~localize ps_pred_app loc uc env atyl tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
604
      Fapp (ps_pred_app, tl)
605
  | PPapp (x, tl) ->
606
      let s, tyl = specialize_psymbol x uc in
607
      let tl = dtype_args ~localize s loc uc env tyl tl in
608
      Fapp (s, tl)
609 610
  | PPinfix (e12, op2, e3)
  | PPinnfix (e12, op2, e3) ->
611
      begin match e12.pp_desc with
612 613
        | PPinfix (_, op1, e2)
          when op1.id = "infix <>" || is_psymbol (Qident op1) uc ->
614 615 616
            let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
            Fbinop (Tand, dfmla ~localize uc env e12,
                    dfmla ~localize uc env e23)
617 618 619 620
        | _ when op2.id = "infix <>" ->
            let op2 = { op2 with id = "infix =" } in
            let e0 = { pp_desc = PPinfix (e12, op2, e3); pp_loc = loc } in
            Fnot (dfmla ~localize uc env e0)
621 622
        | _ ->
            let s, tyl = specialize_psymbol (Qident op2) uc in
623
            let tl = dtype_args ~localize s loc uc env tyl [e12;e3] in
624
            Fapp (s, tl)
625
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
626
  | PPlet (x, e1, e2) ->
627
      let e1 = dterm ~localize uc env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
628
      let ty = e1.dt_ty in
629
      let env = add_var x.id ty env in
630
      let e2 = dfmla ~localize uc env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
632
  | PPmatch (e1, bl) ->
633
      let t1 = dterm ~localize uc env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
634 635
      let ty1 = t1.dt_ty in
      let branch (p, e) =
636 637
        let env, p = dpat_list uc env ty1 p in
        p, dfmla ~localize uc env e
Andrei Paskevich's avatar
Andrei Paskevich committed
638
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
639
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
640
  | PPnamed (x, f1) ->
641
      let localize = match x with
642
        | Lpos l -> Some (Some l)
643
        | Lstr _ -> localize
644
      in
645
      let f1 = dfmla ~localize uc env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
646
      Fnamed (x, f1)
647
(*
648
  | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
649 650
      let pr = find_prop x uc in
      Fvar (Decl.find_prop (Theory.get_known uc) pr)
651
*)
652
  | PPvar x ->
653
      let s, tyl = specialize_psymbol x uc in
654
      let tl = dtype_args ~localize s loc uc env tyl [] in
655
      Fapp (s, tl)
Andrei Paskevich's avatar
Andrei Paskevich committed
656
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ | PPupdate _ ->
657
      error ~loc PredicateExpected
658

659
and dpat_list uc env ty p =
Andrei Paskevich's avatar
Andrei Paskevich committed
660 661
  check_pat_linearity p;
  let loc = p.pat_loc in
662
  let env, p = dpat uc env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
663
  unify_raise ~loc p.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
664
  env, p
665

666
and dtype_args ~localize ls loc uc env el tl =
667
  let n = List.length el and m = List.length tl in
668
  if n <> m then error ~loc (BadArity (ls,m));
669
  let rec check_arg = function
670
    | [], [] ->
671
        []
672
    | a :: al, t :: bl ->
673
        let loc = t.pp_loc in
674
        let t = dterm ~localize uc env t in
675 676
        unify_raise ~loc t.dt_ty a;
        t :: check_arg (al, bl)
677
    | _ ->
678
        assert false
679 680 681
  in
  check_arg (el, tl)

682
(** Typing declarations, that is building environments. *)
683 684 685

open Ptree

686
let add_types dl th =
687
  let def = List.fold_left
688
    (fun def d ->
689
      let id = d.td_ident.id in
690
      Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d def)
691
    Mstr.empty dl
692
  in
693
  let tysymbols = Hstr.create 17 in
694
  let rec visit x =
695
    let d = Mstr.find x def in
696
    try
697