typing.ml 35.1 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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 Ty
25
open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26
open Ptree
27
open Theory
28
open TheoryUC
Andrei Paskevich's avatar
Andrei Paskevich committed
29

30 31 32
(** errors *)

type error = 
33
  | Message of string
34
  | ClashType of string
35
  | DuplicateTypeVar of string
36
  | UnboundType of string
37
  | TypeArity of qualid * int * int
38
  | Clash of string
39 40
  | PredicateExpected
  | TermExpected
41
  | UnboundSymbol of string
42
  | BadNumberOfArguments of Ident.ident * int * int 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  | ClashTheory of string
44
  | ClashNamespace of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
  | UnboundTheory of qualid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
  | AlreadyTheory of string
47
  | UnboundNamespace of string
48 49 50 51
  | UnboundFile of string
  | UnboundDir of string
  | AmbiguousPath of string * string
  | NotInLoadpath of string
52 53
  | CyclicTypeDef
  | UnboundTypeVar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
54
  | AnyMessage of string
55 56 57 58 59 60 61

exception Error of error

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62 63 64 65 66 67 68 69 70 71 72
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf 
    (fun _ -> 
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc (AnyMessage s))
    fmt f

73
let rec print_qualid fmt = function
74
  | Qident s -> fprintf fmt "%s" s.id
75
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
76

77
let report fmt = function
78 79
  | Message s ->
      fprintf fmt "%s" s
80 81
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
82
  | DuplicateTypeVar s ->
83
      fprintf fmt "duplicate type parameter %s" s
84
  | UnboundType s ->
85
       fprintf fmt "Unbound type '%s'" s
86
  | TypeArity (id, a, n) ->
87
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
88 89
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90
      fprintf fmt "Clash with previous symbol %s" id
91 92 93 94
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
95
  | UnboundSymbol s ->
96
       fprintf fmt "Unbound symbol '%s'" s
97
  | BadNumberOfArguments (s, n, m) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
98
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
99
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100 101
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
102 103
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104 105
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106 107
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
108 109
  | UnboundNamespace s ->
      fprintf fmt "unbound namespace %s" s
110 111 112 113 114 115 116 117
  | UnboundFile s ->
      fprintf fmt "no such file %s" s
  | UnboundDir s ->
      fprintf fmt "no such directory %s" s
  | AmbiguousPath (f1, f2) ->
      fprintf fmt "@[ambiguous path:@ both `%s'@ and `%s'@ match@]" f1 f2
  | NotInLoadpath f ->
      fprintf fmt "cannot find `%s' in loadpath" f
118 119 120 121
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
122 123
  | AnyMessage s ->
      fprintf fmt "%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
124

125 126
(** Environments *)

127
module S = Set.Make(String)
128 129
module M = Map.Make(String)

130
(** typing using destructive type variables 
131

132 133 134 135 136 137
    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
138

139 140 141 142 143 144 145 146 147 148 149 150 151
*)

(** types with destructive type variables *)

type dty =
  | Tyvar of type_var
  | Tyapp of tysymbol * dty list
      
and type_var = { 
  tag : int; 
  user : bool;
  tvsymbol : tvsymbol;
  mutable type_val : dty option;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
152
  type_var_loc : loc option;
153
}
154

155 156 157 158
let rec print_dty fmt = function
  | Tyvar { type_val = Some t } ->
      print_dty fmt t
  | Tyvar { type_val = None; tvsymbol = v } ->
159
      fprintf fmt "'%s" (tv_name v).id_short
160
  | Tyapp (s, []) ->
161
      fprintf fmt "%s" s.ts_name.id_short
162
  | Tyapp (s, [t]) -> 
163
      fprintf fmt "%a %s" print_dty t s.ts_name.id_short
164
  | Tyapp (s, l) -> 
165 166
      fprintf fmt "(%a) %s" 
	(print_list comma print_dty) l s.ts_name.id_short
167

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
168 169 170 171 172
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

173
let create_ty_decl_var =
174
  let t = ref 0 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175
  fun ?loc ~user tv -> 
176
    incr t; 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177 178
    { tag = !t; user = user; tvsymbol = tv; type_val = None;
      type_var_loc = loc }
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206

let rec occurs v = function
  | Tyvar { type_val = Some t } -> occurs v t
  | Tyvar { tag = t; type_val = None } -> v.tag = t
  | Tyapp (_, l) -> List.exists (occurs v) l

(* destructive type unification *)
let rec unify t1 t2 = match t1, t2 with
  | Tyvar { type_val = Some t1 }, _ ->
      unify t1 t2
  | _, Tyvar { type_val = Some t2 } ->
      unify t1 t2
  | Tyvar v1, Tyvar v2 when v1.tag = v2.tag ->
      true
	(* instantiable variables *)
  | Tyvar ({user=false} as v), t
  | t, Tyvar ({user=false} as v) ->
      not (occurs v t) && (v.type_val <- Some t; true)
	(* recursive types *)
  | Tyapp (s1, l1), Tyapp (s2, l2) ->
      s1 == s2 && List.length l1 = List.length l2 &&
	  List.for_all2 unify l1 l2
  | Tyapp _, _ | _, Tyapp _ ->
      false
	(* other cases *)
  | Tyvar {user=true; tag=t1}, Tyvar {user=true; tag=t2} -> 
      t1 = t2

207
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
208
    environment + local variables.
209
    It is only local to this module and created with [create_denv] below. *)
210 211

type denv = { 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212
  th : theory_uc; (* the theory under construction *)
213 214
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty M.t; (* local variables, to be bound later *)
215 216
}

217 218
let create_denv th = { 
  th = th; 
219 220 221
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
222

223 224 225 226
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
227
    (* TODO: shouldn't we localize this ident? *)
228
    let v = create_tvsymbol (id_fresh x) in
229
    let v = create_ty_decl_var ~user:true v in
230 231 232
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233 234
(* Specialize *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
235
let find_type_var ~loc env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236 237 238
  try
    Htv.find env tv
  with Not_found ->
239
    let v = create_ty_decl_var ~loc ~user:false tv in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240 241 242
    Htv.add env tv v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243
let rec specialize ~loc env t = match t.ty_node with
244
  | Ty.Tyvar tv -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245
      Tyvar (find_type_var ~loc env tv)
246
  | Ty.Tyapp (s, tl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247
      Tyapp (s, List.map (specialize ~loc env) tl)
248

249 250 251
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
252
  try Mnm.find x ns.ns_ns
253 254 255 256 257 258 259 260 261 262 263 264
  with Not_found -> error ~loc (UnboundNamespace x)

let rec find_namespace q ns = match q with
  | Qident t -> find_local_namespace t ns
  | Qdot (q, t) -> let ns = find_namespace q ns in find_local_namespace t ns

let rec find f q ns = match q with
  | Qident x -> f x ns
  | Qdot (m, x) -> let ns = find_namespace m ns in f x ns

(** specific find functions using a path *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
let find_local_tysymbol {id=x; id_loc=loc} ns = 
266
  try Mnm.find x ns.ns_ts
267 268
  with Not_found -> error ~loc (UnboundType x)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
269 270 271
let find_tysymbol_ns p ns =
  find find_local_tysymbol p ns

272
let find_tysymbol p th = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
273
  find_tysymbol_ns p (get_namespace th)
274

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
275
let specialize_tysymbol ~loc x env =
276
  let s = find_tysymbol x env.th in
277
  let env = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
278
  s, List.map (find_type_var ~loc env) s.ts_args
279
	
280 281
let find_lsymbol {id=x; id_loc=loc} ns = 
  try Mnm.find x ns.ns_ls
282 283
  with Not_found -> error ~loc (UnboundSymbol x)

284 285
let find_lsymbol_ns p ns = 
  find find_lsymbol p ns
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286

287 288
let find_lsymbol p th = 
  find_lsymbol_ns p (get_namespace th)
289

290
let find_prop {id=x; id_loc=loc} ns = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
291 292 293
  try Mnm.find x ns.ns_pr
  with Not_found -> errorm ~loc "unbound formula %s" x

294 295 296
let find_prop_ns p ns =
  find find_prop p ns

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
297
let find_prop p th =
298
  find_prop_ns p (get_namespace th)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
299

300 301 302
let specialize_lsymbol ~loc s =
  let tl = s.ls_args in
  let t = s.ls_value in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303
  let env = Htv.create 17 in
304
  s, List.map (specialize ~loc env) tl, option_map (specialize ~loc env) t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305

306 307 308 309 310
let specialize_fsymbol ~loc s = 
  let s, tl, ty = specialize_lsymbol ~loc s in
  match ty with
    | None -> error ~loc TermExpected
    | Some ty -> s, tl, ty
311

312 313 314 315 316
let specialize_psymbol ~loc s = 
  let s, tl, ty = specialize_lsymbol ~loc s in
  match ty with
    | None -> s, tl
    | Some _ -> error ~loc PredicateExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
317

318 319
(** Typing types *)

320
let rec qloc = function
321
  | Qident x -> x.id_loc
322
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
323

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324 325 326 327 328 329 330 331
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 split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

332
(* parsed types -> intermediate types *)
333 334

let rec type_inst s ty = match ty.ty_node with
335
  | Ty.Tyvar n -> Mtv.find n s
336 337
  | Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl)

338
let rec dty env = function
339
  | PPTtyvar {id=x} -> 
340
      Tyvar (find_user_type_var x env)
341
  | PPTtyapp (p, x) ->
342
      let loc = qloc x in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343
      let ts, tv = specialize_tysymbol ~loc x env in
344 345 346
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
347 348 349 350 351
      let tyl = List.map (dty env) p in
      match ts.ts_def with
	| None -> 
	    Tyapp (ts, tyl)
	| Some ty -> 
352 353
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
354
	    type_inst s ty
355 356

(* intermediate types -> types *)
357
let rec ty_of_dty = function
358
  | Tyvar { type_val = Some t } ->
359
      ty_of_dty t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360 361
  | Tyvar { type_val = None; user = false; type_var_loc = loc } ->
      errorm ?loc "undefined type variable"
362 363 364
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
365
      Ty.ty_app s (List.map ty_of_dty tl)
366

367
(** Typing terms and formulas *)
368

Andrei Paskevich's avatar
Andrei Paskevich committed
369 370 371 372 373 374 375 376
type dpattern = { dp_node : dpattern_node; dp_ty : dty }

and dpattern_node =
  | Pwild
  | Pvar of string
  | Papp of lsymbol * dpattern list
  | Pas of dpattern * string

377 378
type uquant = string list * dty

379 380 381
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
382
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383
  | Tconst of constant
384
  | Tapp of lsymbol * dterm list
385
  | Tlet of dterm * string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
386
  | Tmatch of dterm * (dpattern * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387
  | Tnamed of string * dterm
388 389 390
  | Teps of string * dfmla

and dfmla = 
391
  | Fapp of lsymbol * dterm list
392
  | Fquant of quant * uquant list * dtrigger list list * dfmla
393 394 395 396 397
  | Fbinop of binop * dfmla * dfmla
  | Fnot of dfmla
  | Ftrue
  | Ffalse
  | Fif of dfmla * dfmla * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398
  | Flet of dterm * string * dfmla
Andrei Paskevich's avatar
Andrei Paskevich committed
399
  | Fmatch of dterm * (dpattern * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
401
  | Fvar of fmla
402

403 404 405 406
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

407 408 409 410 411 412
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

413 414 415 416 417 418 419 420 421 422 423 424 425 426
let check_pat_linearity pat =
  let s = ref S.empty in
  let add id =
    if S.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := S.add id.id !s
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
    | PPpapp (_, pl) -> List.iter check pl
    | PPpas (p, id) -> check p; add id
  in
  check pat

Andrei Paskevich's avatar
Andrei Paskevich committed
427 428 429 430 431 432 433
let rec dpat env pat =
  let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
  env, { dp_node = n; dp_ty = ty }

and dpat_node loc env = function
  | PPpwild -> 
      let tv = create_tvsymbol (id_user "a" loc) in
434
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
435 436 437
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
438
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
439 440 441 442 443 444 445 446 447 448 449 450
      let env = { env with dvars = M.add x ty env.dvars } in
      env, Pvar x, ty
  | PPpapp (x, pl) ->
      let s = find_lsymbol x env.th in
      let s, tyl, ty = specialize_fsymbol ~loc s in
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
  | PPpas (p, {id=x}) ->
      let env, p = dpat env p in
      let env = { env with dvars = M.add x p.dp_ty env.dvars } in
      env, Pas (p,x), p.dp_ty

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
451 452
and dpat_args s loc env el pl = 
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
453
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
454
  let rec check_arg env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
455
    | [], [] -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456 457 458 459 460 461 462
	env, []
    | a :: al, p :: pl ->
	let loc = p.pat_loc in
	let env, p = dpat env p in
	if not (unify a p.dp_ty) then term_expected_type ~loc p.dp_ty a;
	let env, pl = check_arg env (al, pl) in
	env, p :: pl
Andrei Paskevich's avatar
Andrei Paskevich committed
463 464 465
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
467

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
468
let rec trigger_not_a_term_exn = function
469
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
470 471 472
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

473
let check_quant_linearity uqu =
474 475 476 477 478 479 480
  let s = ref S.empty in
  let check id = 
    if S.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := S.add id.id !s
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

481 482 483 484 485
let rec dterm env t = 
  let n, ty = dterm_node t.pp_loc env t.pp_desc in
  { dt_node = n; dt_ty = ty }

and dterm_node loc env = function
486 487 488 489 490 491
  | PPvar (Qident {id=x}) when M.mem x env.dvars ->
      (* local variable *)
      let ty = M.find x env.dvars in
      Tvar x, ty
  | PPvar x -> 
      (* 0-arity symbol (constant) *)
492
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
493
      let s, tyl, ty = specialize_fsymbol ~loc s in
494
      let n = List.length tyl in
495
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
496
      Tapp (s, []), ty
497
  | PPapp (x, tl) ->
498
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
499
      let s, tyl, ty = specialize_fsymbol ~loc s in
500
      let tl = dtype_args s.ls_name loc env tyl tl in
501
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
502
  | PPconst (ConstInt _ as c) ->
503
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
504
  | PPconst (ConstReal _ as c) ->
505
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
506 507 508 509 510 511
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
      let env = { env with dvars = M.add x ty env.dvars } in
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
512
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
513 514 515 516
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
      let tb = (* the type of all branches *)
	let tv = create_tvsymbol (id_user "a" loc) in
517
	Tyvar (create_ty_decl_var ~loc ~user:false tv) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
518
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
519
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
520
	let loc = pat.pat_loc in
521
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
522
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
523 524 525 526 527
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
	let loc = e.pp_loc in
	let e = dterm env e in
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
        pat, e
Andrei Paskevich's avatar
Andrei Paskevich committed
528 529 530
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
531
      Tmatch (e1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532 533 534
  | PPnamed (x, e1) ->
      let e1 = dterm env e1 in
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
535 536 537 538 539 540
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
      let e1 = dterm env e1 in
      let ty = dty env ty in
      if not (unify e1.dt_ty ty) then term_expected_type ~loc e1.dt_ty ty;
      e1.dt_node, ty
541
  | PPquant _ | PPif _ 
542 543
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
544

545 546 547 548 549 550 551 552 553 554 555
and dfmla env e = match e.pp_desc with
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
  | PPprefix (PPnot, a) ->
      Fnot (dfmla env a)
  | PPinfix (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
      Fbinop (binop op, dfmla env a, dfmla env b)
  | PPif (a, b, c) ->
      Fif (dfmla env a, dfmla env b, dfmla env c)  
556
  | PPquant (q, uqu, trl, a) ->
557
      check_quant_linearity uqu;
558 559 560 561 562 563 564 565
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let env, idl = 
          map_fold_left
            (fun env {id=x} -> { env with dvars = M.add x ty env.dvars }, x)
            env idl
        in
        env, (idl,ty)
566
      in
567
      let env, uqu = map_fold_left uquant env uqu in
568
      let trigger e =
569 570
	try 
	  TRterm (dterm env e) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
571 572
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla env e) 
573 574
      in
      let trl = List.map (List.map trigger) trl in
575 576 577 578 579
      let q = match q with 
        | PPforall -> Fforall 
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
580
  | PPapp (x, tl) ->
581
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582
      let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
583
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
584
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
585 586 587 588 589 590
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
      let env = { env with dvars = M.add x ty env.dvars } in
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
591
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
592 593
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
594
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595
	let loc = pat.pat_loc in
596
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
597
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
598
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
599 600
        pat, dfmla env e
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
601
      Fmatch (e1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
602 603 604
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
605
  | PPvar x -> 
606
      Fvar (snd (find_prop x env.th))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
607
  | PPconst _ | PPcast _ ->
608
      error ~loc:e.pp_loc PredicateExpected
609

610 611 612 613 614 615 616 617 618
and dtype_args s loc env el tl =
  let n = List.length el and m = List.length tl in
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
  let rec check_arg = function
    | [], [] -> 
	[]
    | a :: al, t :: bl ->
	let loc = t.pp_loc in
	let t = dterm env t in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
619
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
620 621 622 623 624 625
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
let rec pattern env p = 
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
  | Pvar x -> 
      if M.mem x env then assert false; (* FIXME? *)
      let v = create_vsymbol (id_fresh x) ty in
      M.add x v env, pat_var v
  | Papp (s, pl) -> 
      let env, pl = map_fold_left pattern env pl in
      env, pat_app s pl ty
  | Pas (p, x) ->
      if M.mem x env then assert false; (* FIXME? *)
      let v = create_vsymbol (id_fresh x) ty in
      let env, p = pattern (M.add x v env) p in
      env, pat_as p v

643 644 645 646
let rec term env t = match t.dt_node with
  | Tvar x ->
      assert (M.mem x env);
      t_var (M.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
647
  | Tconst c ->
648
      t_const c (ty_of_dty t.dt_ty)
649
  | Tapp (s, tl) ->
650
      t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
651 652 653 654 655 656 657
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
      let e1 = term env e1 in 
      let v = create_vsymbol (id_fresh x) ty in
      let env = M.add x v env in
      let e2 = term env e2 in
      t_let v e1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
658 659 660 661 662 663 664 665
  | Tmatch (e1, bl) ->
      let branch (pat,e) =
        let env, pat = pattern env pat in
        (pat, term env e)
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
      t_case (term env e1) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
666 667 668
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
669 670
  | Teps _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
671

672 673 674 675 676 677 678 679 680 681 682
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
      f_false 
  | Fnot f ->
      f_not (fmla env f)
  | Fbinop (op, f1, f2) ->
      f_binary op (fmla env f1) (fmla env f2)
  | Fif (f1, f2, f3) ->
      f_if (fmla env f1) (fmla env f2) (fmla env f3)
683
  | Fquant (q, uqu, trl, f1) ->
684
      (* TODO: shouldn't we localize this ident? *)
685 686 687 688 689 690
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
          (fun env x -> 
             let v = create_vsymbol (id_fresh x) ty in M.add x v env, v) 
          env xl 
691
      in
692
      let env, vl = map_fold_left uquant env uqu in
693
      let trigger = function
694 695
	| TRterm t -> Term (term env t) 
	| TRfmla f -> Fmla (fmla env f) 
696 697 698
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
699 700
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
701
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
702 703 704 705
      let ty = ty_of_dty e1.dt_ty in
      let e1 = term env e1 in 
      let v = create_vsymbol (id_fresh x) ty in
      let env = M.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
706 707
      let f2 = fmla env f2 in
      f_let v e1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
708 709 710 711 712 713
  | Fmatch (e1, bl) ->
      let branch (pat,e) =
        let env, pat = pattern env pat in
        (pat, fmla env e)
      in
      f_case (term env e1) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
714
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
715
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
716
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
717 718
  | Fvar f ->
      f
719

720
(** Typing declarations, that is building environments. *)
721 722 723

open Ptree

724
let add_types dl th =
725
  let ns = get_namespace th in
726 727 728 729
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
730 731
	 if M.mem id.id def || Mnm.mem id.id ns.ns_ts then 
	   error ~loc:id.id_loc (ClashType id.id);
732 733
	 M.add id.id d def) 
      M.empty dl 
734
  in
735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750
  let tysymbols = Hashtbl.create 17 in
  let rec visit x = 
    try
      match Hashtbl.find tysymbols x with
	| None -> error CyclicTypeDef
	| Some ts -> ts
    with Not_found ->
      Hashtbl.add tysymbols x None;
      let d = M.find x def in
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
      let vl = 
	List.map 
	  (fun v -> 
	     if Hashtbl.mem vars v.id then 
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
751
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
752 753 754 755
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
756
      let id = id_user id d.td_loc in
757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784
      let ts = match d.td_def with
	| TDalias ty -> 
	    let rec apply = function
	      | PPTtyvar v -> 
		  begin 
		    try ty_var (Hashtbl.find vars v.id)
		    with Not_found -> error ~loc:v.id_loc (UnboundTypeVar v.id)
		  end
	      | PPTtyapp (tyl, q) ->
		  let ts = match q with
		    | Qident x when M.mem x.id def ->
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
		  try
		    ty_app ts (List.map apply tyl)
		  with Ty.BadTypeArity ->
		    error ~loc:(qloc q) (TypeArity (q, List.length ts.ts_args,
						    List.length tyl))
	    in
	    create_tysymbol id vl (Some (apply ty))
	| TDabstract | TDalgebraic _ -> 
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
785 786 787 788
  let th' = 
    let tsl = 
      M.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
    in
789
    add_decl th (create_ty_decl tsl)
790
  in
791
  let decl d = 
792 793 794 795 796 797 798 799
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
      | None -> 
	  assert false
      | Some ts -> 
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
	  List.iter 
	    (fun v -> 
800 801
	       Hashtbl.add vars (tv_name v).id_short 
                  (create_ty_decl_var ~user:true v)) 
802 803 804 805 806 807 808 809 810 811 812
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
      | TDabstract | TDalias _ -> 
	  Tabstract
      | TDalgebraic cl -> 
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
	  let constructor (loc, id, pl) = 
	    let param (_, t) = ty_of_dty (dty th' t) in
	    let tyl = List.map param pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
813
	    create_fconstr (id_user id.id loc) tyl ty
814 815 816 817
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
818 819
  in
  let dl = List.map decl dl in
820
  List.fold_left add_decl th (create_ty_decls dl)
821

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
822 823 824
let env_of_vsymbol_list vl =
  List.fold_left (fun env v -> M.add v.vs_name.id_short v env) M.empty vl

825
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
826
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
827 828
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
829
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
830 831 832
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
833 834
    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls 
      then error ~loc:d.ld_loc (Clash id);
Andrei Paskevich's avatar
Andrei Paskevich committed
835
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
836
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
837
    Hashtbl.add denvs id denv;
838
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
839 840 841 842 843
    let pl = List.map type_ty d.ld_params in
    match d.ld_type with
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
844
	  add_decl th (create_logic_decl [ps, None])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
845 846
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
847
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
848
	  Hashtbl.add fsymbols id fs;
849
	  add_decl th (create_logic_decl [fs, None])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
850 851 852 853 854 855 856 857 858
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
  let type_decl d = 
    let id = d.ld_ident.id in
    let dadd_var denv (x, ty) = match x with
      | None -> denv
      | Some id -> { denv with dvars = M.add id.id (dty denv ty) denv.dvars }
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
859 860 861
    let denv = Hashtbl.find denvs id in
    let denv = { denv with th = th' } in
    let denv = List.fold_left dadd_var denv d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
862 863
    let create_var (x, _) ty = 
      let id = match x with 
864 865
	| None -> id_fresh "%x"
	| Some id -> id_user id.id id.id_loc
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
866 867 868
      in
      create_vsymbol id ty
    in
869
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
870 871 872
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
873 874
        begin match d.ld_def with
	  | None -> ps,None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
875 876
	  | Some f -> 
	      let f = dfmla denv f in
877 878 879 880
              let vl = match ps.ls_value with
                | None -> mk_vlist ps.ls_args
                | _ -> assert false
              in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
881
	      let env = env_of_vsymbol_list vl in
882 883
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
884
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
885
	let fs = Hashtbl.find fsymbols id in
886 887
        begin match d.ld_def with
	  | None -> fs,None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
888
	  | Some t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
889
	      let loc = t.pp_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
890
	      let t = dterm denv t in
891 892 893 894
              let vl = match fs.ls_value with
                | Some _ -> mk_vlist fs.ls_args
                | _ -> assert false
              in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
895
	      let env = env_of_vsymbol_list vl in
896
              try make_fs_defn fs vl (term env t)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
897
	      with _ -> term_expected_type ~loc t.dt_ty (dty denv ty)
898
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
899 900
  in
  let dl = List.map type_decl dl in
901
  List.fold_left add_decl th (create_logic_decls dl)
902 903 904 905

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
906
  term M.empty t
907

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
908 909 910 911 912
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
  fmla M.empty f

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
913 914 915
let add_prop k loc s f th =
  let f = fmla th f in
  try
916
    add_decl th (create_prop_decl k (create_prop (id_user s.id loc)) f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
917 918
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
919

Andrei Paskevich's avatar
Andrei Paskevich committed
920
(*
921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975
(** [check_clausal_form loc ps f] checks whether the formula [f] 
    has a valid clausal form 
      \forall x_1,.., x_k. P1 -> ... ->