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

861
and add_decl env lenv th = function
862
863
864
865
866
867
868
  | TypeDecl dl ->
      add_types dl th
  | LogicDecl dl ->
      add_logics dl th
  | IndDecl dl ->
      add_inductives dl th
  | PropDecl (loc, k, s, f) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
869
      add_prop (prop_kind k) loc s f th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
870
  | UseClone (loc, use, subst) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
871
872
873
      let q, id = split_qualid use.use_theory in
      let t = 
	try
874
	  find_theory env lenv q id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
875
	with 
876
	  | TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
877
878
	  | Error (AmbiguousPath _ as e) -> error ~loc e
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
879
880
881
882
      let use_or_clone th = match subst with
	| None -> 
	    use_export th t
	| Some s -> 
883
884
885
886
            let add_inst s = function
              | CStsym (p,q) ->
                  let ts1 = find_tysymbol_ns p t.th_export in
                  let ts2 = find_tysymbol q th in
887
888
                  if Mts.mem ts1 s.inst_ts
                  then error ~loc (Clash ts1.ts_name.id_short);
889
890
891
892
                  { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
              | CSlsym (p,q) ->
                  let ls1 = find_lsymbol_ns p t.th_export in
                  let ls2 = find_lsymbol q th in
893
894
                  if Mls.mem ls1 s.inst_ls
                  then error ~loc (Clash ls1.ls_name.id_short);
895
896
                  { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
              | CSlemma p ->
897
                  let pr,_ = find_prop_ns p t.th_export in
898
                  if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
899
                  then error ~loc (Clash pr.pr_name.id_short);
900
901
                  { s with inst_lemma = Spr.add pr s.inst_lemma }
              | CSgoal p ->
902
                  let pr,_ = find_prop_ns p t.th_export in
903
                  if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
904
                  then error ~loc (Clash pr.pr_name.id_short);
905
                  { s with inst_goal = Spr.add pr s.inst_goal }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
906
	    in
907
            let s = List.fold_left add_inst empty_inst s in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
908
909
	    clone_export th t s
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
910
      let n = match use.use_as with 
911
912
913
	| None -> Some t.th_name.id_short
	| Some (Some x) -> Some x.id
	| Some None -> None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
914
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
915
      begin try match use.use_imp_exp with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
916
917
918
	| Nothing ->
	    (* use T = namespace T use_export T end *)
	    let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
919
	    let th = use_or_clone th in
920
	    close_namespace th false n
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
921
922
923
	| Import ->
	    (* use import T = namespace T use_export T end import T *)
	    let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
924
	    let th = use_or_clone th in
925
	    close_namespace th true n
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
926
	| Export ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
927
	    use_or_clone th 
928
      with ClashSymbol s ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
929
	error ~loc (Clash s)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
930
      end
931
  | Namespace (_, import, name, dl) ->
932
      let ns = get_namespace th in
933
934
935
936
937
938
939
      let id = match name with
        | Some { id=id; id_loc=loc } ->
            if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
            Some id
        | None ->
            None
      in
940
      let th = open_namespace th in
941
      let th = add_decls env lenv th dl in
942
      close_namespace th import id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
943

944
and type_and_add_theory env lenv pt =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
945
  let id = pt.pt_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
946
947
  if Mnm.mem id.id lenv || id.id = builtin_theory.th_name.id_short 
    then error (ClashTheory id.id);
948
949
  let th = type_theory env lenv id pt in
  Mnm.add id.id th lenv
Jean-Christophe Filliâtre's avatar