typing.ml 32 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
53 54
  | UnboundType of string list
  | UnboundSymbol of string list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
55
  | AnyMessage of string
56 57 58 59 60 61 62

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

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

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

124 125
(** Environments *)

126
(** typing using destructive type variables 
127

128 129 130 131 132 133
    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
134

135 136
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137 138 139 140 141
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

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 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 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

type denv = { 
  uc : theory_uc; (* the theory under construction *)
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty Mstr.t; (* local variables, to be bound later *)
}

let create_denv uc = { 
  uc = uc; 
  utyvars = Hashtbl.create 17; 
  dvars = Mstr.empty;
}

let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    (* TODO: shouldn't we localize this ident? *)
    let v = create_tvsymbol (id_fresh x) in
    let v = create_ty_decl_var ~user:true v in
    Hashtbl.add env.utyvars x v;
    v
 
(* parsed types -> intermediate types *)

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

let rec string_list_of_qualid acc = function
  | Qident id -> id.id :: acc
  | Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p

let specialize_tysymbol loc p uc =
  let sl = string_list_of_qualid [] p in
  let ts = 
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
  ts, specialize_tysymbol ~loc ts

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

let rec dty env = function
  | PPTtyvar {id=x} -> 
      Tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
      let ts, tv = specialize_tysymbol loc x env.uc in
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
      match ts.ts_def with
	| None -> 
	    Tyapp (ts, tyl)
	| Some ty -> 
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    type_inst s ty

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

let find_prop_ns = find_ns ns_find_prop
let find_prop p uc = find_prop_ns p (get_namespace uc)

let find_tysymbol_ns = find_ns ns_find_ts
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

let find_lsymbol_ns = find_ns ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
  s, specialize_lsymbol (qloc p) s

let specialize_fsymbol p uc = 
  let loc = qloc p in
  let s, (tl, ty) = specialize_lsymbol p uc in
230 231 232
  match ty with
    | None -> error ~loc TermExpected
    | Some ty -> s, tl, ty
233

234 235 236
let specialize_psymbol p uc = 
  let loc = qloc p in
  let s, (tl, ty) = specialize_lsymbol p uc in
237 238 239
  match ty with
    | None -> s, tl
    | Some _ -> error ~loc PredicateExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240

241

242 243
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
244 245 246 247
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

248
(** Typing terms and formulas *)
249

Andrei Paskevich's avatar
Andrei Paskevich committed
250 251 252 253 254 255 256 257
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

258 259
type uquant = string list * dty

260 261 262
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
263
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264
  | Tconst of constant
265
  | Tapp of lsymbol * dterm list
266
  | Tlet of dterm * string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
267
  | Tmatch of dterm * (dpattern * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
268
  | Tnamed of string * dterm
269 270 271
  | Teps of string * dfmla

and dfmla = 
272
  | Fapp of lsymbol * dterm list
273
  | Fquant of quant * uquant list * dtrigger list list * dfmla
274 275 276 277 278
  | 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
279
  | Flet of dterm * string * dfmla
Andrei Paskevich's avatar
Andrei Paskevich committed
280
  | Fmatch of dterm * (dpattern * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282
  | Fvar of fmla
283

284 285 286 287
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

288 289 290 291 292 293
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

294
let check_pat_linearity pat =
Andrei Paskevich's avatar
Andrei Paskevich committed
295
  let s = ref Sstr.empty in
296
  let add id =
297 298
    if Sstr.mem id.id !s then 
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
299
    s := Sstr.add id.id !s
300 301 302 303 304 305 306 307 308
  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
309 310 311 312 313 314 315
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
316
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
317 318 319
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
320
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
321
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
322 323
      env, Pvar x, ty
  | PPpapp (x, pl) ->
324
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
325 326 327 328
      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
329
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
330 331
      env, Pas (p,x), p.dp_ty

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332 333
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
334
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335
  let rec check_arg env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
336
    | [], [] -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337 338 339 340 341 342 343
	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
344 345 346
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
348

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
349
let rec trigger_not_a_term_exn = function
350
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
351 352 353
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

354
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
355
  let s = ref Sstr.empty in
356
  let check id = 
Andrei Paskevich's avatar
Andrei Paskevich committed
357 358
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
359 360 361
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

362 363 364 365 366
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
367
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
368
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
369
      let ty = Mstr.find x env.dvars in
370 371 372
      Tvar x, ty
  | PPvar x -> 
      (* 0-arity symbol (constant) *)
373
      let s, tyl, ty = specialize_fsymbol x env.uc in
374
      let n = List.length tyl in
375
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
376
      Tapp (s, []), ty
377
  | PPapp (x, tl) ->
378
      let s, tyl, ty = specialize_fsymbol x env.uc in
379
      let tl = dtype_args s.ls_name loc env tyl tl in
380
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
381
  | PPconst (ConstInt _ as c) ->
382
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
383
  | PPconst (ConstReal _ as c) ->
384
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
385 386 387
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
388
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389 390
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
391
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
392 393 394 395
      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
396
	Tyvar (create_ty_decl_var ~loc ~user:false tv) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
397
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
398
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
399
	let loc = pat.pat_loc in
400
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
401
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402 403 404 405 406
	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
407 408 409
      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
410
      Tmatch (e1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411 412 413
  | 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
414 415 416 417 418 419
  | 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
420
  | PPquant _ | PPif _ 
421 422
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
423

424 425 426 427 428 429 430 431 432 433 434
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)  
435
  | PPquant (q, uqu, trl, a) ->
436
      check_quant_linearity uqu;
437 438 439 440
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let env, idl = 
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
441
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
442 443 444
            env idl
        in
        env, (idl,ty)
445
      in
446
      let env, uqu = map_fold_left uquant env uqu in
447
      let trigger e =
448 449
	try 
	  TRterm (dterm env e) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
450 451
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla env e) 
452 453
      in
      let trl = List.map (List.map trigger) trl in
454 455 456 457 458
      let q = match q with 
        | PPforall -> Fforall 
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
459
  | PPapp (x, tl) ->
460
      let s, tyl = specialize_psymbol x env.uc in
461
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
462
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
463 464 465
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
466
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
467 468
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
469
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
470 471
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
472
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
473
	let loc = pat.pat_loc in
474
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
475
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
477 478
        pat, dfmla env e
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
479
      Fmatch (e1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
480 481 482
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483
  | PPvar x -> 
484
      Fvar (snd (find_prop x env.uc))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485
  | PPconst _ | PPcast _ ->
486
      error ~loc:e.pp_loc PredicateExpected
487

488 489 490 491 492 493 494 495 496
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
497
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
498 499 500 501 502 503
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
504 505 506 507 508
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
509
      if Mstr.mem x env then assert false; (* FIXME? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
510
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
511
      Mstr.add x v env, pat_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
512 513 514 515
  | 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
516
      if Mstr.mem x env then assert false; (* FIXME? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
517
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
518
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
519 520
      env, pat_as p v

521 522
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
523 524
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525
  | Tconst c ->
526
      t_const c (ty_of_dty t.dt_ty)
527
  | Tapp (s, tl) ->
528
      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
529 530 531 532
  | 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
533
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
534 535
      let e2 = term env e2 in
      t_let v e1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
536 537 538
  | Tmatch (e1, bl) ->
      let branch (pat,e) =
        let env, pat = pattern env pat in
Andrei Paskevich's avatar
Andrei Paskevich committed
539
        ([pat], term env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
540 541 542
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
543
      t_case [term env e1] bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
544 545 546
  | 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
547 548
  | Teps _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
549

550 551 552 553 554 555 556 557 558 559 560
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)
561
  | Fquant (q, uqu, trl, f1) ->
562
      (* TODO: shouldn't we localize this ident? *)
563 564 565 566
      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
567
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v) 
568
          env xl 
569
      in
570
      let env, vl = map_fold_left uquant env uqu in
571
      let trigger = function
572 573
	| TRterm t -> Term (term env t) 
	| TRfmla f -> Fmla (fmla env f) 
574 575 576
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
577 578
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
580 581 582
      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
583
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
584 585
      let f2 = fmla env f2 in
      f_let v e1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
586 587 588
  | Fmatch (e1, bl) ->
      let branch (pat,e) =
        let env, pat = pattern env pat in
Andrei Paskevich's avatar
Andrei Paskevich committed
589
        ([pat], fmla env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
590
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
591
      f_case [term env e1] (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
592
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
593
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
594
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595 596
  | Fvar f ->
      f
597

598
(** Typing declarations, that is building environments. *)
599 600 601

open Ptree

602
let add_types dl th =
603
  let ns = get_namespace th in
604 605 606 607
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
608
	 if Mstr.mem id.id def || Mnm.mem id.id ns.ns_ts then 
609
	   error ~loc:id.id_loc (ClashType id.id);
Andrei Paskevich's avatar
Andrei Paskevich committed
610 611
	 Mstr.add id.id d def) 
      Mstr.empty dl 
612
  in
613 614 615 616 617 618 619 620
  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
621
      let d = Mstr.find x def in
622 623 624 625 626 627 628
      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);
629
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
630 631 632 633
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
634
      let id = id_user id d.td_loc in
635 636 637 638 639 640 641 642 643 644
      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
645
		    | Qident x when Mstr.mem x.id def ->
646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
			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
663 664
  let th' = 
    let tsl = 
Andrei Paskevich's avatar
Andrei Paskevich committed
665
      Mstr.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
666
    in
667
    add_decl th (create_ty_decl tsl)
668
  in
669
  let decl d = 
670 671 672 673 674 675 676 677
    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 -> 
678
	       Hashtbl.add vars v.tv_name.id_short 
679
                  (create_ty_decl_var ~user:true v)) 
680 681 682 683 684 685 686 687 688 689 690
	    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
691
	    create_fconstr (id_user id.id loc) tyl ty
692 693 694 695
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
696 697
  in
  let dl = List.map decl dl in
698
  List.fold_left add_decl th (create_ty_decls dl)
699

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
700
let env_of_vsymbol_list vl =
Andrei Paskevich's avatar
Andrei Paskevich committed
701
  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
702

703
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
705 706
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
707
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
708 709 710
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
711 712
    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
713
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
714
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
715
    Hashtbl.add denvs id denv;
716
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
717 718 719 720 721
    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;
722
	  add_decl th (create_logic_decl [ps, None])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
723 724
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
725
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
726
	  Hashtbl.add fsymbols id fs;
727
	  add_decl th (create_logic_decl [fs, None])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
728 729 730 731 732 733 734
  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
735
      | 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
736
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
737
    let denv = Hashtbl.find denvs id in
738
    let denv = { denv with uc = th' } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
739
    let denv = List.fold_left dadd_var denv d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
740 741
    let create_var (x, _) ty = 
      let id = match x with 
742 743
	| 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
744 745 746
      in
      create_vsymbol id ty
    in
747
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
748 749 750
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
751 752
        begin match d.ld_def with
	  | None -> ps,None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
753 754
	  | Some f -> 
	      let f = dfmla denv f in
755 756 757 758
              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
759
	      let env = env_of_vsymbol_list vl in
760 761
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
762
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
763
	let fs = Hashtbl.find fsymbols id in
764 765
        begin match d.ld_def with
	  | None -> fs,None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
766
	  | Some t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
767
	      let loc = t.pp_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
768
	      let t = dterm denv t in
769 770 771 772
              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
773
	      let env = env_of_vsymbol_list vl in
774
              try make_fs_defn fs vl (term env t)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
775
	      with _ -> term_expected_type ~loc t.dt_ty (dty denv ty)
776
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
777 778
  in
  let dl = List.map type_decl dl in
779
  List.fold_left add_decl th (create_logic_decls dl)
780 781 782 783

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

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
786 787 788
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
Andrei Paskevich's avatar
Andrei Paskevich committed
789
  fmla Mstr.empty f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
790

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
791 792 793
let add_prop k loc s f th =
  let f = fmla th f in
  try
794
    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
795 796
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
797

Andrei Paskevich's avatar
Andrei Paskevich committed
798
(*
799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853
(** [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
854
      if ps'.ls_name != ps.ls_name then
855 856 857 858 859 860 861 862 863 864
	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
865 866 867 868 869
*)

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

871 872 873 874 875 876 877 878
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
879
    let v = id_user id d.in_loc in
880 881 882 883 884
    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;
885
    add_decl th (create_logic_decl [ps, None])
886
  in
887 888 889 890 891
  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
892
    let clause (loc, id, f) = 
893
      create_prsymbol (id_user id.id loc), fmla th' f
894 895 896 897
    in
    ps, List.map clause d.in_def
  in
  let dl = List.map type_decl dl in
Andrei Paskevich's avatar
Andrei Paskevich committed
898 899 900
  try
    List.fold_left add_decl th (create_ind_decls dl)
  with
901
  | InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
902
      "not a clausal form"
903
  | NonPositiveIndDecl (_,pr,s) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
904
      "non-positive occurrence of %a" Pretty.print_ls s
905
  | TooSpecificIndDecl (_,pr,t) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
906
      "term @[%a@] is too specific" Pretty.print_term t
907

908
(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
909 910

let load_channel file c =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
911 912
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
913 914 915 916 917
  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
918 919
  close_in c;
  tl
920

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
921
let prop_kind = function
922 923 924
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
925

926
let find_theory env lenv q id = match q with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
927
  | [] -> 
928
      (* local theory *)
929
      begin try Mnm.find id lenv 
Andrei Paskevich's avatar
Andrei Paskevich committed
930
      with Not_found -> find_theory env [] id end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
931
  | _ :: _ ->
932
      (* theory in file f *)
Andrei Paskevich's avatar