typing.ml 29.6 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
Andrei Paskevich's avatar
Andrei Paskevich committed
23
open Ptree
24
open Ident
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 34
(** errors *)

type error = 
35
  | Message of string
36
  | ClashType of string
37
  | DuplicateTypeVar of string
38
  | TypeArity of qualid * int * int
39
  | Clash of string
40 41
  | PredicateExpected
  | TermExpected
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 48 49 50
  | UnboundFile of string
  | UnboundDir of string
  | AmbiguousPath of string * string
  | NotInLoadpath of string
51 52
  | CyclicTypeDef
  | UnboundTypeVar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
53
  | AnyMessage of string
54 55 56 57 58 59 60

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
61 62 63 64 65 66 67 68 69 70 71
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

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

76
let report fmt = function
77 78
  | Message s ->
      fprintf fmt "%s" s
79 80
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
81
  | DuplicateTypeVar s ->
82
      fprintf fmt "duplicate type parameter %s" s
83
  | TypeArity (id, a, n) ->
84
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
85 86
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
      fprintf fmt "Clash with previous symbol %s" id
88 89 90 91
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
92
  | BadNumberOfArguments (s, n, m) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
93
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
94
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95 96
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
97 98
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99 100
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101 102
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
103 104 105 106 107 108 109 110
  | 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
111 112 113 114
  | 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
115 116
  | AnyMessage s ->
      fprintf fmt "%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
117

118 119
(** Environments *)

120
(** typing using destructive type variables 
121

122 123 124 125 126 127
    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
128

129 130
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131 132 133 134 135
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

136 137 138 139 140
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
141

142 143 144 145 146
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
147

148

149 150
(** Typing types *)

151
let rec qloc = function
152
  | Qident x -> x.id_loc
153
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
154

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
155 156 157 158 159 160 161 162
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

163
(** Typing terms and formulas *)
164

Andrei Paskevich's avatar
Andrei Paskevich committed
165 166 167 168 169 170 171 172
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

173 174
type uquant = string list * dty

175 176 177
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
178
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179
  | Tconst of constant
180
  | Tapp of lsymbol * dterm list
181
  | Tlet of dterm * string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
182
  | Tmatch of dterm * (dpattern * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183
  | Tnamed of string * dterm
184 185 186
  | Teps of string * dfmla

and dfmla = 
187
  | Fapp of lsymbol * dterm list
188
  | Fquant of quant * uquant list * dtrigger list list * dfmla
189 190 191 192 193
  | 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
194
  | Flet of dterm * string * dfmla
Andrei Paskevich's avatar
Andrei Paskevich committed
195
  | Fmatch of dterm * (dpattern * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
197
  | Fvar of fmla
198

199 200 201 202
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

203 204 205 206 207 208
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

209
let check_pat_linearity pat =
Andrei Paskevich's avatar
Andrei Paskevich committed
210
  let s = ref Sstr.empty in
211
  let add id =
Andrei Paskevich's avatar
Andrei Paskevich committed
212 213
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
214 215 216 217 218 219 220 221 222
  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
223 224 225 226 227 228 229
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
230
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
231 232 233
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
234
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
235
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
236 237 238 239 240 241 242 243
      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
Andrei Paskevich's avatar
Andrei Paskevich committed
244
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
245 246
      env, Pas (p,x), p.dp_ty

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247 248
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
249
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250
  let rec check_arg env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
251
    | [], [] -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
252 253 254 255 256 257 258
	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
259 260 261
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
262
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
263

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264
let rec trigger_not_a_term_exn = function
265
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
266 267 268
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

269
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
270
  let s = ref Sstr.empty in
271
  let check id = 
Andrei Paskevich's avatar
Andrei Paskevich committed
272 273
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
274 275 276
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

277 278 279 280 281
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
Andrei Paskevich's avatar
Andrei Paskevich committed
282
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
283
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
284
      let ty = Mstr.find x env.dvars in
285 286 287
      Tvar x, ty
  | PPvar x -> 
      (* 0-arity symbol (constant) *)
288
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289
      let s, tyl, ty = specialize_fsymbol ~loc s in
290
      let n = List.length tyl in
291
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
292
      Tapp (s, []), ty
293
  | PPapp (x, tl) ->
294
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295
      let s, tyl, ty = specialize_fsymbol ~loc s in
296
      let tl = dtype_args s.ls_name loc env tyl tl in
297
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
298
  | PPconst (ConstInt _ as c) ->
299
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300
  | PPconst (ConstReal _ as c) ->
301
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
302 303 304
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
305
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
306 307
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
308
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
309 310 311 312
      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
313
	Tyvar (create_ty_decl_var ~loc ~user:false tv) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
314
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
315
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316
	let loc = pat.pat_loc in
317
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
318
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319 320 321 322 323
	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
324 325 326
      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
327
      Tmatch (e1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328 329 330
  | 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
331 332 333 334 335 336
  | 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
337
  | PPquant _ | PPif _ 
338 339
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
340

341 342 343 344 345 346 347 348 349 350 351
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)  
352
  | PPquant (q, uqu, trl, a) ->
353
      check_quant_linearity uqu;
354 355 356 357
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let env, idl = 
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
358
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
359 360 361
            env idl
        in
        env, (idl,ty)
362
      in
363
      let env, uqu = map_fold_left uquant env uqu in
364
      let trigger e =
365 366
	try 
	  TRterm (dterm env e) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
367 368
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla env e) 
369 370
      in
      let trl = List.map (List.map trigger) trl in
371 372 373 374 375
      let q = match q with 
        | PPforall -> Fforall 
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
376
  | PPapp (x, tl) ->
377
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
378
      let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
379
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
380
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
381 382 383
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
384
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
385 386
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
387
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388 389
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
390
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391
	let loc = pat.pat_loc in
392
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
393
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
394
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
395 396
        pat, dfmla env e
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
397
      Fmatch (e1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398 399 400
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
401
  | PPvar x -> 
402
      Fvar (snd (find_prop x env.th))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403
  | PPconst _ | PPcast _ ->
404
      error ~loc:e.pp_loc PredicateExpected
405

406 407 408 409 410 411 412 413 414
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
415
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
416 417 418 419 420 421
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
422 423 424 425 426
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 -> 
Andrei Paskevich's avatar
Andrei Paskevich committed
427
      if Mstr.mem x env then assert false; (* FIXME? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
428
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
429
      Mstr.add x v env, pat_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
430 431 432 433
  | Papp (s, pl) -> 
      let env, pl = map_fold_left pattern env pl in
      env, pat_app s pl ty
  | Pas (p, x) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
434
      if Mstr.mem x env then assert false; (* FIXME? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
435
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
436
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
437 438
      env, pat_as p v

439 440
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
441 442
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
443
  | Tconst c ->
444
      t_const c (ty_of_dty t.dt_ty)
445
  | Tapp (s, tl) ->
446
      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
447 448 449 450
  | 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
Andrei Paskevich's avatar
Andrei Paskevich committed
451
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
452 453
      let e2 = term env e2 in
      t_let v e1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
454 455 456 457 458 459 460 461
  | 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
462 463 464
  | 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
465 466
  | Teps _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
467

468 469 470 471 472 473 474 475 476 477 478
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)
479
  | Fquant (q, uqu, trl, f1) ->
480
      (* TODO: shouldn't we localize this ident? *)
481 482 483 484
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
          (fun env x -> 
Andrei Paskevich's avatar
Andrei Paskevich committed
485
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v) 
486
          env xl 
487
      in
488
      let env, vl = map_fold_left uquant env uqu in
489
      let trigger = function
490 491
	| TRterm t -> Term (term env t) 
	| TRfmla f -> Fmla (fmla env f) 
492 493 494
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
495 496
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
497
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498 499 500
      let ty = ty_of_dty e1.dt_ty in
      let e1 = term env e1 in 
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
501
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
502 503
      let f2 = fmla env f2 in
      f_let v e1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
504 505 506 507 508 509
  | 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
510
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
511
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
512
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
513 514
  | Fvar f ->
      f
515

516
(** Typing declarations, that is building environments. *)
517 518 519

open Ptree

520
let add_types dl th =
521
  let ns = get_namespace th in
522 523 524 525
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
526
	 if Mstr.mem id.id def || Mnm.mem id.id ns.ns_ts then 
527
	   error ~loc:id.id_loc (ClashType id.id);
Andrei Paskevich's avatar
Andrei Paskevich committed
528 529
	 Mstr.add id.id d def) 
      Mstr.empty dl 
530
  in
531 532 533 534 535 536 537 538
  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;
Andrei Paskevich's avatar
Andrei Paskevich committed
539
      let d = Mstr.find x def in
540 541 542 543 544 545 546
      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);
547
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
548 549 550 551
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
552
      let id = id_user id d.td_loc in
553 554 555 556 557 558 559 560 561 562
      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
Andrei Paskevich's avatar
Andrei Paskevich committed
563
		    | Qident x when Mstr.mem x.id def ->
564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580
			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
581 582
  let th' = 
    let tsl = 
Andrei Paskevich's avatar
Andrei Paskevich committed
583
      Mstr.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
584
    in
585
    add_decl th (create_ty_decl tsl)
586
  in
587
  let decl d = 
588 589 590 591 592 593 594 595
    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 -> 
596
	       Hashtbl.add vars v.tv_name.id_short 
597
                  (create_ty_decl_var ~user:true v)) 
598 599 600 601 602 603 604 605 606 607 608
	    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
609
	    create_fconstr (id_user id.id loc) tyl ty
610 611 612 613
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
614 615
  in
  let dl = List.map decl dl in
616
  List.fold_left add_decl th (create_ty_decls dl)
617

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
618
let env_of_vsymbol_list vl =
Andrei Paskevich's avatar
Andrei Paskevich committed
619
  List.fold_left (fun env v -> Mstr.add v.vs_name.id_short v env) Mstr.empty vl
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
620

621
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
622
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
623 624
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
625
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
626 627 628
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
629 630
    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
631
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
632
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
633
    Hashtbl.add denvs id denv;
634
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
635 636 637 638 639
    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;
640
	  add_decl th (create_logic_decl [ps, None])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
641 642
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
643
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
644
	  Hashtbl.add fsymbols id fs;
645
	  add_decl th (create_logic_decl [fs, None])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
646 647 648 649 650 651 652
  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
Andrei Paskevich's avatar
Andrei Paskevich committed
653
      | Some id -> { denv with dvars = Mstr.add id.id (dty denv ty) denv.dvars }
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
654
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
655 656 657
    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
658 659
    let create_var (x, _) ty = 
      let id = match x with 
660 661
	| 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
662 663 664
      in
      create_vsymbol id ty
    in
665
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
666 667 668
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
669 670
        begin match d.ld_def with
	  | None -> ps,None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
671 672
	  | Some f -> 
	      let f = dfmla denv f in
673 674 675 676
              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
677
	      let env = env_of_vsymbol_list vl in
678 679
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
680
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
681
	let fs = Hashtbl.find fsymbols id in
682 683
        begin match d.ld_def with
	  | None -> fs,None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
684
	  | Some t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
685
	      let loc = t.pp_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
686
	      let t = dterm denv t in
687 688 689 690
              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
691
	      let env = env_of_vsymbol_list vl in
692
              try make_fs_defn fs vl (term env t)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
693
	      with _ -> term_expected_type ~loc t.dt_ty (dty denv ty)
694
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
695 696
  in
  let dl = List.map type_decl dl in
697
  List.fold_left add_decl th (create_logic_decls dl)
698 699 700 701

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
Andrei Paskevich's avatar
Andrei Paskevich committed
702
  term Mstr.empty t
703

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
704 705 706
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
Andrei Paskevich's avatar
Andrei Paskevich committed
707
  fmla Mstr.empty f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
708

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
709 710 711
let add_prop k loc s f th =
  let f = fmla th f in
  try
712
    add_decl th (create_prop_decl k (create_prsymbol (id_user s.id loc)) f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
713 714
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
715

Andrei Paskevich's avatar
Andrei Paskevich committed
716
(*
717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771
(** [check_clausal_form loc ps f] checks whether the formula [f] 
    has a valid clausal form 
      \forall x_1,.., x_k. P1 -> ... -> P_n -> P
    where P is headed by ps and ps has only positive occurrences in P1 .. Pn *)

let rec occurrences ps f = match f.f_node with
  | Term.Ftrue | Term.Ffalse -> 
      0, 0
  | Term.Fapp (ps', _) -> 
      (if ps'.ls_name == ps.ls_name then 1 else 0), 0
  | Term.Fbinop (Fimplies, f1, f2) -> 
      let pos1, neg1 = occurrences ps f1 in
      let pos2, neg2 = occurrences ps f2 in
      neg1+pos2, pos1+neg2
  | Term.Fbinop ((Fand | For), f1, f2) -> 
      let pos1, neg1 = occurrences ps f1 in
      let pos2, neg2 = occurrences ps f2 in
      pos1+pos2, neg1+neg2
  | Term.Fbinop (Fiff, f1, f2) -> 
      let pos1, neg1 = occurrences ps f1 in
      let pos2, neg2 = occurrences ps f2 in
      let n = pos1+pos2+neg1+neg2 in
      n, n
  | Term.Fnot p1 -> 
      let pos1, neg1 = occurrences ps p1 in neg1, pos1
  | Term.Fquant (_, qf) ->
      assert false (* TODO *)
      (* occurrences pi p *)
  | Term.Flet (t, bf) ->
      let _, f = f_open_bound bf in
      occurrences ps f
  | Term.Fif (f1, f2, f3) ->
      let pos1, neg1 = occurrences ps f1 in
      let pos2, neg2 = occurrences ps f2 in
      let pos3, neg3 = occurrences ps f3 in
      pos1+pos2+pos3, neg1+neg2+neg3
  | Term.Fcase (_, bl) ->
      List.fold_left
	(fun (pos, neg) br ->
	   let _, _, f1 = f_open_branch br in
	   let pos1, neg1 = occurrences ps f1 in
	   pos+pos1, neg+neg1)
	(0, 0) bl
      
let rec check_unquantified_clausal_form loc ps f = match f.f_node with
  | Term.Fbinop (Fimplies, f1, f2) -> 
      check_unquantified_clausal_form loc ps f2;
      let _, neg1 = occurrences ps f1 in
      if neg1 > 0 then 
	errorm ~loc 
	  "inductive predicate has a negative occurrence in this case"
  | Term.Fapp (ps', _) -> 
      (* TODO: vrifier galement que les arguments de ps' ont exactement
	 les mmes types que ceux de la dclaration de ps (et non plus 
	 prcis) *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
772
      if ps'.ls_name != ps.ls_name then
773 774 775 776 777 778 779 780 781 782
	errorm ~loc "head of clause does not contain the inductive predicate"
  | _ -> 
      errorm ~loc "this case is not in clausal form"

let rec check_clausal_form loc ps f = match f.f_node with
  | Term.Fquant (Fforall, qf) ->
      let vl, _, f = f_open_quant qf in
      check_clausal_form loc ps f
  | _ -> 
      check_unquantified_clausal_form loc ps f
Andrei Paskevich's avatar
Andrei Paskevich committed
783 784 785 786 787
*)

let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false
788

789 790 791 792 793 794 795 796
let add_inductives dl th =
  let ns = get_namespace th in
  let psymbols = Hashtbl.create 17 in
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.in_ident.id in
    if Hashtbl.mem psymbols id || Mnm.mem id ns.ns_ls 
      then error ~loc:d.in_loc (Clash id);
Andrei Paskevich's avatar
Andrei Paskevich committed
797
    let v = id_user id d.in_loc in
798 799 800 801 802
    let denv = create_denv th in
    let type_ty t = ty_of_dty (dty denv t) in
    let pl = List.map type_ty d.in_params in
    let ps = create_psymbol v pl in
    Hashtbl.add psymbols id ps;
803
    add_decl th (create_logic_decl [ps, None])
804
  in
805 806 807 808 809
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
  let type_decl d = 
    let id = d.in_ident.id in
    let ps = Hashtbl.find psymbols id in
Andrei Paskevich's avatar
Andrei Paskevich committed
810
    let clause (loc, id, f) = 
811
      create_prsymbol (id_user id.id loc), fmla th' f
812 813 814 815
    in
    ps, List.map clause d.in_def
  in
  let dl = List.map type_decl dl in
Andrei Paskevich's avatar
Andrei Paskevich committed
816 817 818
  try
    List.fold_left add_decl th (create_ind_decls dl)
  with
819
  | InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
820
      "not a clausal form"
821
  | NonPositiveIndDecl (_,pr,s) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
822
      "non-positive occurrence of %a" Pretty.print_ls s
823
  | TooSpecificIndDecl (_,pr,t) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
824
      "term @[%a@] is too specific" Pretty.print_term t
825

826
(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
827 828

let load_channel file c =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
829 830
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
831 832 833 834 835
  Lexer.parse_logic_file lb

let load_file file =
  let c = open_in file in
  let tl = load_channel file c in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
836 837
  close_in c;
  tl
838

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
839
let prop_kind = function
840 841 842
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
843

844
let find_theory env lenv q id = match q with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
845
  | [] -> 
846
      (* local theory *)
847
      begin try Mnm.find id lenv 
Andrei Paskevich's avatar
Andrei Paskevich committed
848
      with Not_found -> find_theory env [] id end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
849
  | _ :: _ ->
850
      (* theory in file f *)
Andrei Paskevich's avatar
Andrei Paskevich committed
851
      find_theory env q id
852 853 854

let rec type_theory env lenv id pt =
  let n = id_user id.id id.id_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
855
  let th = create_theory n in
856
  let th = add_decls env lenv th pt.pt_decl in
857 858
  close_theory th

859
and add_decls env lenv th = List.fold_left (add_decl env lenv) th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
860