Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

typing.ml 16.4 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

20 21
open Util
open Format
22
open Pp
23
open Ty
24
open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25
open Ptree
26
open Theory
27

28 29 30
(** errors *)

type error = 
31
  | Message of string
32 33
  | ClashType of string
  | BadTypeArity of string
34
  | UnboundType of string
35
  | TypeArity of qualid * int * int
36
  | Clash of string
37 38
  | PredicateExpected
  | TermExpected
39
  | UnboundSymbol of string
40 41 42
  | TermExpectedType of (formatter -> unit) * (formatter -> unit) 
      (* actual / expected *)
  | BadNumberOfArguments of Name.t * int * int 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  | ClashTheory of string
44
  | ClashNamespace of string
45
  | UnboundTheory of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
  | AlreadyTheory of string
47
  | UnboundNamespace of string
48 49 50 51 52 53 54

exception Error of error

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

55
let rec print_qualid fmt = function
56
  | Qident s -> fprintf fmt "%s" s.id
57
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
58

59
let report fmt = function
60 61
  | Message s ->
      fprintf fmt "%s" s
62 63 64 65
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
  | BadTypeArity s ->
      fprintf fmt "duplicate type parameter %s" s
66
  | UnboundType s ->
67
       fprintf fmt "Unbound type '%s'" s
68
  | TypeArity (id, a, n) ->
69
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
70 71 72
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
      fprintf fmt "Clash with previous constant %s" id
73 74 75 76
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
77
  | UnboundSymbol s ->
78
       fprintf fmt "Unbound symbol '%s'" s
79 80 81 82 83 84
  | BadNumberOfArguments (s, n, m) ->
      fprintf fmt "@[Symbol `%a' is aplied to %d terms,@ " Name.print s n;
      fprintf fmt "but is expecting %d arguments@]" m
  | TermExpectedType (ty1, ty2) ->
      fprintf fmt "@[This term has type "; ty1 fmt; 
      fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85 86
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
87 88
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
89 90
  | UnboundTheory s ->
      fprintf fmt "unbound theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91 92
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  | UnboundNamespace s ->
      fprintf fmt "unbound namespace %s" s

(** Environments *)

module M = Map.Make(String)

type env = {
  loadpath : string list;
  theories : Theory.t M.t; (* local theories *)
}

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
109 110

(** typing using destructive type variables 
111

112 113 114 115 116 117
    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
118

119 120 121 122 123 124 125 126 127 128 129 130 131 132
*)

(** types with destructive type variables *)

type dty =
  | Tyvar of type_var
  | Tyapp of tysymbol * dty list
      
and type_var = { 
  tag : int; 
  user : bool;
  tvsymbol : tvsymbol;
  mutable type_val : dty option;
}
133

134 135 136 137 138 139 140 141 142 143 144 145 146
let rec print_dty fmt = function
  | Tyvar { type_val = Some t } ->
      print_dty fmt t
  | Tyvar { type_val = None; tvsymbol = v } ->
      fprintf fmt "'%a" Name.print v
  | Tyapp (s, []) ->
      fprintf fmt "%a" Name.print s.Ty.ts_name
  | Tyapp (s, [t]) -> 
      fprintf fmt "%a %a" print_dty t Name.print s.Ty.ts_name
  | Tyapp (s, l) -> 
      fprintf fmt "(%a) %a" 
	(print_list comma print_dty) l Name.print s.Ty.ts_name

147 148
let create_type_var =
  let t = ref 0 in
149
  fun ~user tv -> 
150
    incr t; 
151
    { tag = !t; user = user; tvsymbol = tv; type_val = None }
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

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

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

180
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181
    environment + local variables.
182
    It is only local to this module and created with [create_denv] below. *)
183 184

type denv = { 
185
  th : Theory.th; (* the theory under construction *)
186 187
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty M.t; (* local variables, to be bound later *)
188 189
}

190 191
let create_denv th = { 
  th = th; 
192 193 194
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
195

196 197 198 199 200 201 202 203
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    let v = create_type_var ~user:true (Name.from_string x) in
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204 205 206 207
(* Specialize *)

module Htv = Hashtbl.Make(Name)

208
let find_type_var env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
209 210 211 212 213 214 215
  try
    Htv.find env tv
  with Not_found ->
    let v = create_type_var ~user:false tv in
    Htv.add env tv v;
    v
 
216 217
let rec specialize env t = match t.Ty.ty_node with
  | Ty.Tyvar tv -> 
218
      Tyvar (find_type_var env tv)
219 220
  | Ty.Tyapp (s, tl) ->
      Tyapp (s, List.map (specialize env) tl)
221

222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
  try find_namespace ns x 
  with Not_found -> error ~loc (UnboundNamespace x)

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

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

(** specific find functions using a path *)

let find_tysymbol {id=x; id_loc=loc} ns = 
  try find_tysymbol ns x 
  with Not_found -> error ~loc (UnboundType x)

let find_tysymbol p th = 
  find find_tysymbol p (get_namespace th)

245
let specialize_tysymbol x env =
246
  let s = find_tysymbol x env.th in
247 248
  let env = Htv.create 17 in
  s, List.map (find_type_var env) s.Ty.ts_args
249
	
250 251 252 253 254 255 256
let find_fsymbol {id=x; id_loc=loc} ns = 
  try find_fsymbol ns x 
  with Not_found -> error ~loc (UnboundSymbol x)

let find_fsymbol p th = 
  find find_fsymbol p (get_namespace th)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257
let specialize_fsymbol x env =
258
  let s = find_fsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259 260 261 262
  let tl, t = s.fs_scheme in
  let env = Htv.create 17 in
  s, List.map (specialize env) tl, specialize env t

263 264 265 266 267 268 269
let find_psymbol {id=x; id_loc=loc} ns = 
  try find_psymbol ns x 
  with Not_found -> error ~loc (UnboundSymbol x)

let find_psymbol p th =
  find find_psymbol p (get_namespace th)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
270
let specialize_psymbol x env =
271
  let s = find_psymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
272 273 274
  let env = Htv.create 17 in
  s, List.map (specialize env) s.ps_scheme

275 276
(** Typing types *)

277
let rec qloc = function
278
  | Qident x -> x.id_loc
279
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
280 281 282

(* parsed types -> intermediate types *)
let rec dty env = function
283
  | PPTtyvar {id=x} -> 
284
      Tyvar (find_user_type_var x env)
285
  | PPTtyapp (p, x) ->
286
      let loc = qloc x in
287
      let s, tv = specialize_tysymbol x env in
288 289 290 291 292 293 294 295 296 297 298 299 300 301
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
      Tyapp (s, List.map (dty env) p)

(* intermediate types -> types *)
let rec ty = function
  | Tyvar { type_val = Some t } ->
      ty t
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
      Ty.ty_app s (List.map ty tl)

302
(** Typing terms and formulas *)
303 304 305 306

type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
307
  | Tvar of string
308 309 310 311 312 313 314
  | Tapp of fsymbol * dterm list
  | Tlet of dterm * string * dterm
(*   | Tcase of dterm * tbranch list *)
  | Teps of string * dfmla

and dfmla = 
  | Fapp of psymbol * dterm list
315
  | Fquant of quant * string * dty * dfmla
316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
  | Fbinop of binop * dfmla * dfmla
  | Fnot of dfmla
  | Ftrue
  | Ffalse
  | Fif of dfmla * dfmla * dfmla
(*   | Flet of dterm * string * dfmla *)
(*   | Fcase of dterm * (pattern * dfmla) list *)

let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff
  | _ -> assert false 

331 332 333 334 335
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
336 337 338 339 340 341
  | PPvar (Qident {id=x}) when M.mem x env.dvars ->
      (* local variable *)
      let ty = M.find x env.dvars in
      Tvar x, ty
  | PPvar x -> 
      (* 0-arity symbol (constant) *)
342 343 344 345
      let s, tyl, ty = specialize_fsymbol x env in
      let n = List.length tyl in
      if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
      Tapp (s, []), ty
346
  | PPapp (x, tl) ->
347 348 349
      let s, tyl, ty = specialize_fsymbol x env in
      let tl = dtype_args s.fs_name loc env tyl tl in
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350 351 352
  | _ ->
      assert false (*TODO*)

353 354 355 356 357 358 359 360 361 362 363 364 365
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)
  | PPinfix _ ->
      error ~loc:e.pp_loc PredicateExpected
  | PPif (a, b, c) ->
      Fif (dfmla env a, dfmla env b, dfmla env c)  
366
  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
367
      let ty = dty env ty in
368 369 370
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fforall, x, ty, dfmla env a)
  | PPexists ({id=x}, ty, a) -> (* TODO: triggers *)
371
      let ty = dty env ty in
372 373
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fexists, x, ty, dfmla env a)
374
  | PPapp (x, tl) ->
375
      let s, tyl = specialize_psymbol x env in
376 377
      let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
      Fapp (s, tl)
378 379
  | _ ->
      assert false (*TODO*)
380

381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
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
	if not (unify a t.dt_ty) then
	  error ~loc (TermExpectedType ((fun f -> print_dty f t.dt_ty),
					(fun f -> print_dty f a)));
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

let rec term env t = match t.dt_node with
  | Tvar x ->
      assert (M.mem x env);
      t_var (M.find x env)
  | Tapp (s, tl) ->
      t_app s (List.map (term env) tl) (ty t.dt_ty)
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
405 406
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407

408 409 410 411 412 413 414 415 416 417 418
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)
419 420 421 422 423 424 425
  | Fquant (q, x, t, f1) ->
      let v = create_vsymbol (Name.from_string x) (ty t) in
      let env = M.add x v env in
      f_quant q v (fmla env f1)
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)

426

427
(** Typing declarations, that is building environments. *)
428 429 430

open Ptree

431 432 433
let add_type loc sl s th =
  let ns = get_namespace th in
  if mem_tysymbol ns s.id then error ~loc (ClashType s.id);
434
  let tyvars = ref M.empty in
435
  let add_ty_var {id=x} =
436
    if M.mem x !tyvars then error ~loc (BadTypeArity x);
437
    let v = Name.from_string x in
438 439
    tyvars := M.add x v !tyvars;
    v
440
  in
441
  let vl = List.map add_ty_var sl in
442
  let ty = Ty.create_tysymbol (Name.from_string s.id) vl None in
443
  add_decl th (Dtype [ty, Ty_abstract])
444

445 446 447 448
let add_function loc pl t th {id=id} =
  let ns = get_namespace th in
  if mem_fsymbol ns id then error ~loc (Clash id);
  let denv = create_denv th in
449
  let pl = List.map (dty denv) pl and t = dty denv t in
450
  let pl = List.map ty pl and t = ty t in
451
  let s = create_fsymbol (Name.from_string id) (pl, t) false in
452
  add_decl th (Dlogic [Lfunction (s, None)])
453

454 455 456 457
let add_predicate loc pl th {id=id} =
  let ns = get_namespace th in
  if mem_psymbol ns id then error ~loc (Clash id);
  let denv = create_denv th in
458
  let pl = List.map (dty denv) pl in
459
  let pl = List.map ty pl in
460
  let s = create_psymbol (Name.from_string id) pl in
461
  add_decl th (Dlogic [Lpredicate (s, None)])
462

463 464 465
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
466
  fmla M.empty f
467 468 469 470

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
471
  term M.empty t
472 473 474 475 476

let axiom loc s f env =
  ignore (fmla env f);
  env

477
(***
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
478 479 480 481
let uses_theory env (as_t, q) =
  let loc = qloc q in
  let rec find_theory q = match q with
    | Qident t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
482
	t.id, find_local_theory t env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483 484 485 486 487
    | Qdot (q, t) -> 
	let _, env = find_theory q in t.id, find_local_theory t env
  in
  let id, th = find_theory q in
  let id = match as_t with None -> id | Some x -> x.id in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
488
  if M.mem id (self env).theories then error ~loc (AlreadyTheory id);
489
  add_theory id th env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
490 491 492 493

let open_theory t env =
  let loc = t.id_loc and id = t.id in
  if not (M.mem id env.theories) then error ~loc (UnboundTheory id);
494 495 496 497 498 499
  let th = M.find id env.theories in
  let open_map m1 m2 = M.fold M.add m1 m2 in
  { tysymbols = open_map th.tysymbols env.tysymbols;
    fsymbols  = open_map th.fsymbols  env.fsymbols;
    psymbols  = open_map th.psymbols  env.psymbols;
    theories  = open_map th.theories  env.theories }
500
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
501

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
502 503 504 505
let find_theory env q =
  assert false (* TODO *)

let rec add_decl env th = function
506
  | TypeDecl (loc, sl, s) ->
507
      add_type loc sl s th
508
  | Logic (loc, ids, PPredicate pl) ->
509
      List.fold_left (add_predicate loc pl) th ids
510
  | Logic (loc, ids, PFunction (pl, t)) ->
511
      List.fold_left (add_function loc pl t) th ids
512
  | Axiom (loc, s, f) ->
513
      axiom loc s f th
514
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
	| None -> t.t_name
	| Some x -> Name.from_string x.id
      in
      begin match use.use_imp_exp with
	| Nothing ->
	    (* use T = namespace T use_export T end *)
	    let th = open_namespace th in
	    let th = use_export th t in
	    close_namespace th n ~import:false
	| Import ->
	    (* use import T = namespace T use_export T end import T *)
	    let th = open_namespace th in
	    let th = use_export th t in
	    close_namespace th n ~import:true
	| Export ->
	    use_export th t
      end
534 535 536 537
  | Namespace (_, {id=id; id_loc=loc}, dl) ->
      let ns = get_namespace th in
      if mem_namespace ns id then error ~loc (ClashNamespace id);
      let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538
      let th = add_decls env th dl in
539 540
      let n = Name.from_string id in
      close_namespace th n ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
541 542 543 544 545
  | AlgType _ 
  | Goal _ 
  | Function_def _ 
  | Predicate_def _ 
  | Inductive_def _ ->
546
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
547

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

550 551 552 553 554
let add_theory env pt =
  let id = pt.th_name.id in
  if M.mem id env.theories then error ~loc:pt.th_loc (ClashTheory id);
  let n = Name.from_string id in
  let th = create_theory n in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
555
  let th = add_decls env th pt.th_decl in
556 557
  let t = close_theory th in
  { env with theories = M.add id t env.theories }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
558

559 560 561 562 563
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)