tptp_typing.ml 24.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
Andrei Paskevich's avatar
Andrei Paskevich committed
11

Andrei Paskevich's avatar
Andrei Paskevich committed
12 13 14
open Format
open Tptp_ast

Andrei Paskevich's avatar
Andrei Paskevich committed
15
open Why3
16
open Wstdlib
Andrei Paskevich's avatar
Andrei Paskevich committed
17 18 19 20 21 22
open Ident
open Ty
open Term
open Decl
open Theory

23 24
let error = Loc.error
let errorm = Loc.errorm
Andrei Paskevich's avatar
Andrei Paskevich committed
25

26
exception DuplicateVar of string
Andrei Paskevich's avatar
Andrei Paskevich committed
27 28 29 30
exception TypeExpected
exception TermExpected
exception FmlaExpected
exception InvalidDummy
Andrei Paskevich's avatar
Andrei Paskevich committed
31
exception MalformedLet
32
exception DependentTy
Andrei Paskevich's avatar
Andrei Paskevich committed
33
exception NonNumeric
Andrei Paskevich's avatar
Andrei Paskevich committed
34
exception BadArity
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36

let () = Exn_printer.register (fun fmt e -> match e with
37
  | DuplicateVar s -> fprintf fmt "variable %s is used twice" s
Andrei Paskevich's avatar
Andrei Paskevich committed
38 39 40
  | TypeExpected -> fprintf fmt "type expression expected"
  | TermExpected -> fprintf fmt "term expression expected"
  | FmlaExpected -> fprintf fmt "formula expression expected"
Andrei Paskevich's avatar
Andrei Paskevich committed
41
  | InvalidDummy -> fprintf fmt "unexpected type placeholder"
Andrei Paskevich's avatar
Andrei Paskevich committed
42
  | MalformedLet -> fprintf fmt "malformed let-expression"
43
  | DependentTy  -> fprintf fmt "dependent type"
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  | NonNumeric   -> fprintf fmt "non-numeric argument"
45
  | BadArity     -> fprintf fmt "bad arity"
Andrei Paskevich's avatar
Andrei Paskevich committed
46 47
  | _ -> raise e)

Andrei Paskevich's avatar
Andrei Paskevich committed
48
type symbol =
49 50
  | STSko of ty
  | STVar of tvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
51 52
  | SVar  of vsymbol
  | SType of tysymbol
53 54 55 56
  | SFunc of tvsymbol list * tvsymbol list * Stv.t * lsymbol
  | SPred of tvsymbol list * tvsymbol list * Stv.t * lsymbol
  | SletF of tvsymbol list * Stv.t * vsymbol list * term
  | SletP of tvsymbol list * Stv.t * vsymbol list * term
Andrei Paskevich's avatar
Andrei Paskevich committed
57
  | Sdobj of lsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
58
  | Suse  of theory
Andrei Paskevich's avatar
Andrei Paskevich committed
59

60
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62
type env = symbol Mstr.t

63
type implicit = symbol Hstr.t
64
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
65

Andrei Paskevich's avatar
Andrei Paskevich committed
66 67
(** Defined symbols : arithmetic etc... *)

Andrei Paskevich's avatar
Andrei Paskevich committed
68 69
type denv = {
  de_env   : Env.env;
Andrei Paskevich's avatar
Andrei Paskevich committed
70

Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84
  th_univ  : theory;
  ts_univ  : tysymbol;
  ty_univ  : ty;

  th_ghost : theory;
  ts_ghost : tysymbol;
  fs_ghost : lsymbol;

  th_int   : theory;
  th_real  : theory;
  th_rat   : theory;
  ts_rat   : tysymbol;
}

85 86
let make_denv env =
  let get_theory s = Env.read_theory env ["tptp"] s in
Andrei Paskevich's avatar
Andrei Paskevich committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  let th_univ = get_theory "Univ" in
  let th_ghost = get_theory "Ghost" in
  let th_rat = get_theory "Rat" in
  let ts_univ = ns_find_ts th_univ.th_export ["iType"] in
  { de_env   = env;

    th_univ  = th_univ;
    ts_univ  = ts_univ;
    ty_univ  = ty_app ts_univ [];

    th_ghost = th_ghost;
    ts_ghost = ns_find_ts th_ghost.th_export ["gh"];
    fs_ghost = ns_find_ls th_ghost.th_export ["gh"];

    th_int   = get_theory "Int";
    th_real  = get_theory "Real";
    th_rat   = th_rat;
    ts_rat   = ns_find_ts th_rat.th_export ["rat"];
  }

let add_theory env impl th =
  let s = "$th$" ^ th.th_name.id_string in
109
  if not (Mstr.mem s env) then Hstr.replace impl s (Suse th)
110

Andrei Paskevich's avatar
Andrei Paskevich committed
111 112 113 114 115 116 117 118 119
let defined_ty ~loc denv env impl dw tyl =
  let ts = match dw with
    | DT DTuniv -> denv.ts_univ
    | DT DTint -> ts_int
    | DT DTreal -> ts_real
    | DT DTrat -> add_theory env impl denv.th_rat; denv.ts_rat
    | DT DTdummy -> error ~loc InvalidDummy
    | DT (DTtype|DTprop) | DF _ | DP _ -> error ~loc TypeExpected
  in
120
  Loc.try2 ~loc ty_app ts tyl
Andrei Paskevich's avatar
Andrei Paskevich committed
121 122 123 124 125 126

let defined_arith ~loc denv env impl dw tl =
  let ts = match tl with
    | { t_ty = Some {ty_node = Tyapp (ts,[]) }}::_ -> ts
    | _::_ -> error ~loc NonNumeric
    | [] -> error ~loc BadArity in
127
  let get_theory s = Env.read_theory denv.de_env ["tptp"] s in
Andrei Paskevich's avatar
Andrei Paskevich committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
  let get_int_theory = function
    | DF DFquot -> errorm ~loc "$quotient/2 is not defined on $int"
    | DF (DFquot_e|DFrem_e) -> get_theory "IntDivE"
    | DF (DFquot_t|DFrem_t) -> get_theory "IntDivT"
    | DF (DFquot_f|DFrem_f) -> get_theory "IntDivF"
    | DF (DFfloor|DFceil|DFtrunc|DFround|DFtoint)
    | DP (DPisint|DPisrat) -> get_theory "IntTrunc"
    | DF DFtorat -> get_theory "IntToRat"
    | DF DFtoreal -> get_theory "IntToReal"
    | _ -> denv.th_int in
  let get_rat_theory = function
    | DF (DFquot_e|DFrem_e) -> get_theory "RatDivE"
    | DF (DFquot_t|DFrem_t) -> get_theory "RatDivT"
    | DF (DFquot_f|DFrem_f) -> get_theory "RatDivF"
    | DF (DFfloor|DFceil|DFtrunc|DFround|DFtoint) -> get_theory "RatTrunc"
    | DF DFtoreal -> get_theory "RatToReal"
    | _ -> denv.th_rat in
  let get_real_theory = function
    | DF (DFquot_e|DFrem_e) -> get_theory "RealDivE"
    | DF (DFquot_t|DFrem_t) -> get_theory "RealDivT"
    | DF (DFquot_f|DFrem_f) -> get_theory "RealDivF"
    | DF (DFfloor|DFceil|DFtrunc|DFround|DFtoint)
    | DP (DPisint|DPisrat) -> get_theory "RealTrunc"
    | DF DFtorat -> get_theory "RealToRat"
    | _ -> denv.th_real in
  let th =
    if ts_equal ts ts_int then get_int_theory dw else
    if ts_equal ts denv.ts_rat then get_rat_theory dw else
    if ts_equal ts ts_real then get_real_theory dw else
    error ~loc NonNumeric
  in
  add_theory env impl th;
  let ls = match dw with
161 162 163 164 165
    | DF DFumin -> ns_find_ls th.th_export [op_prefix "-"]
    | DF DFsum -> ns_find_ls th.th_export [op_infix "+"]
    | DF DFdiff -> ns_find_ls th.th_export [op_infix "-"]
    | DF DFprod -> ns_find_ls th.th_export [op_infix "*"]
    | DF DFquot -> ns_find_ls th.th_export [op_infix "/"]
Andrei Paskevich's avatar
Andrei Paskevich committed
166 167 168 169 170 171 172
    | DF DFquot_e -> ns_find_ls th.th_export ["div"]
    | DF DFquot_t -> ns_find_ls th.th_export ["div_t"]
    | DF DFquot_f -> ns_find_ls th.th_export ["div_f"]
    | DF DFrem_e -> ns_find_ls th.th_export ["mod"]
    | DF DFrem_t -> ns_find_ls th.th_export ["mod_t"]
    | DF DFrem_f -> ns_find_ls th.th_export ["mod_f"]
    | DF DFfloor -> ns_find_ls th.th_export ["floor"]
Andrei Paskevich's avatar
Andrei Paskevich committed
173
    | DF DFceil -> ns_find_ls th.th_export ["ceiling"]
Andrei Paskevich's avatar
Andrei Paskevich committed
174 175 176 177 178
    | DF DFtrunc -> ns_find_ls th.th_export ["truncate"]
    | DF DFround -> ns_find_ls th.th_export ["round"]
    | DF DFtoint -> ns_find_ls th.th_export ["to_int"]
    | DF DFtorat -> ns_find_ls th.th_export ["to_rat"]
    | DF DFtoreal -> ns_find_ls th.th_export ["to_real"]
179 180 181 182
    | DP DPless -> ns_find_ls th.th_export [op_infix "<"]
    | DP DPlesseq -> ns_find_ls th.th_export [op_infix "<="]
    | DP DPgreater -> ns_find_ls th.th_export [op_infix ">"]
    | DP DPgreatereq -> ns_find_ls th.th_export [op_infix ">="]
Andrei Paskevich's avatar
Andrei Paskevich committed
183 184 185 186
    | DP DPisint -> ns_find_ls th.th_export ["is_int"]
    | DP DPisrat -> ns_find_ls th.th_export ["is_rat"]
    | DP (DPtrue|DPfalse|DPdistinct) | DT _ -> assert false
  in
187
  Loc.try2 ~loc t_app_infer ls tl
Andrei Paskevich's avatar
Andrei Paskevich committed
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202

let defined_expr ~loc is_fmla denv env impl dw tl = match dw, tl with
  | (DT DTdummy), _ -> error ~loc InvalidDummy
  | (DF _|DT _), _ when is_fmla -> error ~loc FmlaExpected
  | (DP _|DT _), _ when not is_fmla -> error ~loc TermExpected
  | (DP DPtrue|DP DPfalse), _::_ -> error ~loc BadArity
  | DP DPtrue, [] -> t_true
  | DP DPfalse, [] -> t_false
  | DP DPdistinct, _ ->
      let rec dist acc = function
        | t::tl ->
            let add acc s = t_and_simp acc (t_neq t s) in
            dist (List.fold_left add acc tl) tl
        | _ -> acc
      in
203
      Loc.try2 ~loc dist t_true tl
Andrei Paskevich's avatar
Andrei Paskevich committed
204 205 206 207
  | _ -> defined_arith ~loc denv env impl dw tl

(** TPTP environment *)

Andrei Paskevich's avatar
Andrei Paskevich committed
208
let find_tv ~loc env impl s =
Andrei Paskevich's avatar
Andrei Paskevich committed
209
  let tv = try Mstr.find s env with Not_found ->
210
    try Hstr.find impl s with Not_found ->
211
      let tv = STVar (create_tvsymbol (id_user s loc)) in
212
      Hstr.add impl s tv;
Andrei Paskevich's avatar
Andrei Paskevich committed
213 214
      tv in
  match tv with
215 216 217
    | STVar tv -> ty_var tv
    | STSko ty -> ty
    | _ -> error ~loc TypeExpected
Andrei Paskevich's avatar
Andrei Paskevich committed
218

Andrei Paskevich's avatar
Andrei Paskevich committed
219
let find_vs ~loc denv env impl s =
Andrei Paskevich's avatar
Andrei Paskevich committed
220
  let vs = try Mstr.find s env with Not_found ->
221
    try Hstr.find impl s with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
222
      let vs = SVar (create_vsymbol (id_user s loc) denv.ty_univ) in
223
      Hstr.add impl s vs;
Andrei Paskevich's avatar
Andrei Paskevich committed
224 225
      vs in
  match vs with
226 227
    | SVar vs -> t_var vs
    | _ -> error ~loc TermExpected
Andrei Paskevich's avatar
Andrei Paskevich committed
228

Andrei Paskevich's avatar
Andrei Paskevich committed
229
let find_ts ~loc env impl s args =
230
  let ts = try Mstr.find s env with Not_found ->
231
    try Hstr.find impl s with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
232
      let args = List.map (fun _ -> create_tvsymbol (id_fresh "a")) args in
Andrei Paskevich's avatar
Andrei Paskevich committed
233
      let ss = if s = "int" || s = "real" then "_" ^ s else s in
Clément Fumex's avatar
Clément Fumex committed
234
      let ts = SType (create_tysymbol (id_user ss loc) args NoDef) in
235
      Hstr.add impl s ts;
236 237 238 239
      ts in
  match ts with
    | SType ts -> ts
    | _ -> error ~loc TypeExpected
Andrei Paskevich's avatar
Andrei Paskevich committed
240

Andrei Paskevich's avatar
Andrei Paskevich committed
241
let find_fs ~loc denv env impl s args =
Andrei Paskevich's avatar
Andrei Paskevich committed
242
  try Mstr.find s env with Not_found ->
243
    try Hstr.find impl s with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
244 245
      let args = List.map (fun _ -> denv.ty_univ) args in
      let fs = create_fsymbol (id_user s loc) args denv.ty_univ in
246
      let fs = SFunc ([],[],Stv.empty,fs) in
247
      Hstr.add impl s fs;
Andrei Paskevich's avatar
Andrei Paskevich committed
248 249
      fs

Andrei Paskevich's avatar
Andrei Paskevich committed
250
let find_ps ~loc denv env impl s args =
Andrei Paskevich's avatar
Andrei Paskevich committed
251
  try Mstr.find s env with Not_found ->
252
    try Hstr.find impl s with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
253
      let args = List.map (fun _ -> denv.ty_univ) args in
254
      let ps = create_psymbol (id_user s loc) args in
255
      let ps = SPred ([],[],Stv.empty,ps) in
256
      Hstr.add impl s ps;
Andrei Paskevich's avatar
Andrei Paskevich committed
257
      ps
Andrei Paskevich's avatar
Andrei Paskevich committed
258

Andrei Paskevich's avatar
Andrei Paskevich committed
259 260 261
let find_dobj ~loc denv env impl s =
  let ds = "$do$" ^ s in
  let fs = try Mstr.find ds env with Not_found ->
262
    try Hstr.find impl ds with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
263 264
      let id = id_user ("do_" ^ s) loc in
      let fs = Sdobj (create_fsymbol id [] denv.ty_univ) in
265
      Hstr.add impl ds fs;
Andrei Paskevich's avatar
Andrei Paskevich committed
266 267 268 269 270
      fs in
  match fs with
    | Sdobj fs -> fs_app fs [] denv.ty_univ
    | _ -> assert false (* impossible *)

271
let ty_check loc s ty1 t =
272
  Loc.try3 ~loc ty_match s ty1 (Opt.get t.t_ty)
273

Andrei Paskevich's avatar
Andrei Paskevich committed
274
let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
Andrei Paskevich's avatar
Andrei Paskevich committed
275
  | Eapp (aw,al) ->
276
      let ts = find_ts ~loc env impl aw al in
Andrei Paskevich's avatar
Andrei Paskevich committed
277
      let tyl = List.map (ty denv env impl) al in
278
      Loc.try2 ~loc ty_app ts tyl
Andrei Paskevich's avatar
Andrei Paskevich committed
279
  | Edef (dw,al) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
280 281
      let tyl = List.map (ty denv env impl) al in
      defined_ty ~loc denv env impl dw tyl
Andrei Paskevich's avatar
Andrei Paskevich committed
282
  | Evar v ->
Andrei Paskevich's avatar
Andrei Paskevich committed
283
      find_tv ~loc env impl v
Andrei Paskevich's avatar
Andrei Paskevich committed
284 285
  | Elet _ | Eite _ | Eqnt _ | Ebin _
  | Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
Andrei Paskevich's avatar
Andrei Paskevich committed
286

Clément Fumex's avatar
Clément Fumex committed
287
let t_int_const s =
288
  t_const (Number.(ConstInt (int_literal ILitDec ~neg:false s))) ty_int
Clément Fumex's avatar
Clément Fumex committed
289

290
(* unused
291
let t_real_const r = t_const (Number.ConstReal r)
292
*)
293

Andrei Paskevich's avatar
Andrei Paskevich committed
294
let rec term denv env impl { e_loc = loc; e_node = n } = match n with
Andrei Paskevich's avatar
Andrei Paskevich committed
295
  | Eapp (aw,al) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
296
      begin match find_fs ~loc denv env impl aw al with
297 298
        | SFunc (tvl,gl,mvs,fs) -> ls_args denv env impl loc fs tvl gl mvs al
        | SletF (tvl,mvs,vl,e) -> let_args denv env impl loc e tvl mvs vl al
Andrei Paskevich's avatar
Andrei Paskevich committed
299
        | SVar v -> t_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
300 301 302
        | _ -> error ~loc TermExpected
      end
  | Edef (dw,al) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
303
      let tl = List.map (term denv env impl) al in
Andrei Paskevich's avatar
Andrei Paskevich committed
304
      defined_expr ~loc false denv env impl dw tl
Andrei Paskevich's avatar
Andrei Paskevich committed
305
  | Evar v ->
Andrei Paskevich's avatar
Andrei Paskevich committed
306
      find_vs ~loc denv env impl v
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308
  | Edob s ->
      find_dobj ~loc denv env impl s
309
  | Enum (Nint s) -> t_int_const s
Andrei Paskevich's avatar
Andrei Paskevich committed
310
  | Enum (Nreal (i,f,e)) ->
311
      t_const (Number.(ConstReal (real_literal ~radix:10 ~neg:false ~int:i ~frac:(Opt.get_def "0" f) ~exp:e))) ty_real
Andrei Paskevich's avatar
Andrei Paskevich committed
312 313 314 315 316
  | Enum (Nrat (n,d)) ->
      let n = t_int_const n and d = t_int_const d in
      let frac = ns_find_ls denv.th_rat.th_export ["frac"] in
      add_theory env impl denv.th_rat;
      t_app_infer frac [n;d]
Andrei Paskevich's avatar
Andrei Paskevich committed
317 318 319
  | Elet (def,e) ->
      let env,s = let_defn denv env impl def in
      begin match Mstr.find s env with
320
        | SletF ([],_,[],t) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
321
            let id = id_user s def.e_loc in
322
            let vs = create_vsymbol id (Opt.get t.t_ty) in
Andrei Paskevich's avatar
Andrei Paskevich committed
323 324 325 326 327 328
            let env = Mstr.add s (SVar vs) env in
            let t1 = term denv env impl e in
            t_let_close vs t t1
        | _ ->
            term denv env impl e
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
329 330
  | Eite (e1,e2,e3) ->
      (* we can't fix the polarity of the condition here,
331
         hence type quantifiers are forbidden in terms *)
Andrei Paskevich's avatar
Andrei Paskevich committed
332 333 334
      let cn,_ = fmla denv env impl None [] e1 in
      let th = term denv env impl e2 in
      let el = term denv env impl e3 in
Andrei Paskevich's avatar
Andrei Paskevich committed
335 336
      t_if cn th el
  | Eqnt _ | Ebin _ | Enot _ | Eequ _ -> error ~loc TermExpected
Andrei Paskevich's avatar
Andrei Paskevich committed
337 338 339

and fmla denv env impl pol tvl { e_loc = loc; e_node = n } = match n with
  | Eapp (aw,al) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
340
      begin match find_ps ~loc denv env impl aw al with
341 342
        | SPred (tvl,gl,mvs,ps) -> ls_args denv env impl loc ps tvl gl mvs al
        | SletP (tvl,mvs,vl,e) -> let_args denv env impl loc e tvl mvs vl al
Andrei Paskevich's avatar
Andrei Paskevich committed
343
        | _ -> error ~loc FmlaExpected
344
      end, false
Andrei Paskevich's avatar
Andrei Paskevich committed
345
  | Edef (dw,al) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
346
      let tl = List.map (term denv env impl) al in
Andrei Paskevich's avatar
Andrei Paskevich committed
347
      defined_expr ~loc true denv env impl dw tl, false
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349 350
  | Elet (def,e) ->
      let env,s = let_defn denv env impl def in
      begin match Mstr.find s env with
351
        | SletF ([],_,[],t) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
352
            let id = id_user s def.e_loc in
353
            let vs = create_vsymbol id (Opt.get t.t_ty) in
Andrei Paskevich's avatar
Andrei Paskevich committed
354 355 356 357 358 359
            let env = Mstr.add s (SVar vs) env in
            let f,b = fmla denv env impl pol tvl e in
            t_let_close vs t f, b
        | _ ->
            fmla denv env impl pol tvl e
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
360 361 362 363 364
  | Eqnt (quant,vl,e1) ->
      let vlist (env,pol,tvl,vl,b) (s,e) =
        let loc = e.e_loc in
        if e.e_node = Edef (DT DTtype, []) then
          match pol,quant with
365 366
            | None, _ ->
                errorm ~loc "Invalid type quantifier"
Andrei Paskevich's avatar
Andrei Paskevich committed
367 368 369
            | Some true, Qexists  (* goals *)
            | Some false, Qforall (* premises *) ->
                let tv = create_tvsymbol (id_user s loc) in
370
                Mstr.add s (STVar tv) env, pol, tv::tvl, vl, true
Andrei Paskevich's avatar
Andrei Paskevich committed
371 372
            | Some true, Qforall  (* goals *)
            | Some false, Qexists (* premises *) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
373 374
                let _,ln,cn,_ = Loc.get loc in
                let sk = Format.sprintf "_%s_%d_%d" s ln cn in
Clément Fumex's avatar
Clément Fumex committed
375
                let ts = create_tysymbol (id_user sk loc) tvl NoDef in
Andrei Paskevich's avatar
Andrei Paskevich committed
376
                let tv = ty_app ts (List.map ty_var tvl) in
377
                Hstr.add impl sk (SType ts);
378
                Mstr.add s (STSko tv) env, pol, tvl, vl, true
Andrei Paskevich's avatar
Andrei Paskevich committed
379 380 381 382 383 384 385 386 387
        else
          let ty = ty denv env impl e in
          let vs = create_vsymbol (id_user s loc) ty in
          Mstr.add s (SVar vs) env, None, [], vs::vl, b
      in
      let env,pol,tvl,vl,b = List.fold_left vlist (env,pol,tvl,[],false) vl in
      let f1,b1 = fmla denv env impl pol tvl e1 in
      let quant = match quant with
        | Qforall -> Tforall
388
        | Qexists -> Texists in
Andrei Paskevich's avatar
Andrei Paskevich committed
389 390 391 392 393 394 395 396 397 398 399 400 401
      t_quant_close quant (List.rev vl) [] f1, b || b1
  | Eite (e1,e2,e3) ->
      (* here we can treat type quantifiers in 'if' conditions,
         since [if C then T else E == (C => T) /\ (C \/ E)], but
         as for now we won't do it to stay consistent with terms *)
      let cn,_  = fmla denv env impl None [] e1 in
      let th,b1 = fmla denv env impl pol tvl e2 in
      let el,b2 = fmla denv env impl pol tvl e3 in
      t_if cn th el, b1 || b2
  | Ebin (BOequ,e1,e2) ->
      let f1,b1 = fmla denv env impl pol tvl e1 in
      let f2,b2 = fmla denv env impl pol tvl e2 in
      if b1 || b2 then
402 403
        let g1,_ = fmla denv env impl (Opt.map not pol) tvl e1 in
        let g2,_ = fmla denv env impl (Opt.map not pol) tvl e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
404 405 406 407 408 409 410
        t_and (t_implies g1 f2) (t_implies g2 f1), true
      else
        t_iff f1 f2, false
  | Ebin (BOnequ,e1,e2) ->
      let f1,b1 = fmla denv env impl pol tvl e1 in
      let f2,b2 = fmla denv env impl pol tvl e2 in
      if b1 || b2 then
411 412
        let g1,_ = fmla denv env impl (Opt.map not pol) tvl e1 in
        let g2,_ = fmla denv env impl (Opt.map not pol) tvl e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
413 414 415 416
        t_not (t_and (t_implies f1 g2) (t_implies f2 g1)), true
      else
        t_not (t_iff f1 f2), false
  | Ebin (BOimp,e1,e2) ->
417
      let f1,b1 = fmla denv env impl (Opt.map not pol) tvl e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
418 419 420 421
      let f2,b2 = fmla denv env impl pol tvl e2 in
      t_implies f1 f2, b1 || b2
  | Ebin (BOpmi,e1,e2) ->
      let f1,b1 = fmla denv env impl pol tvl e1 in
422
      let f2,b2 = fmla denv env impl (Opt.map not pol) tvl e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
423 424 425 426 427 428 429 430 431 432
      t_implies f2 f1, b1 || b2
  | Ebin (BOand,e1,e2) ->
      let f1,b1 = fmla denv env impl pol tvl e1 in
      let f2,b2 = fmla denv env impl pol tvl e2 in
      t_and f1 f2, b1 || b2
  | Ebin (BOor,e1,e2) ->
      let f1,b1 = fmla denv env impl pol tvl e1 in
      let f2,b2 = fmla denv env impl pol tvl e2 in
      t_or f1 f2, b1 || b2
  | Ebin (BOnand,e1,e2) ->
433 434
      let f1,b1 = fmla denv env impl (Opt.map not pol) tvl e1 in
      let f2,b2 = fmla denv env impl (Opt.map not pol) tvl e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
435 436
      t_not (t_and f1 f2), b1 || b2
  | Ebin (BOnor,e1,e2) ->
437 438
      let f1,b1 = fmla denv env impl (Opt.map not pol) tvl e1 in
      let f2,b2 = fmla denv env impl (Opt.map not pol) tvl e2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
439 440
      t_not (t_or f1 f2), b1 || b2
  | Enot e1 ->
441
      let f1,b1 = fmla denv env impl (Opt.map not pol) tvl e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
442 443 444 445 446 447 448
      t_not f1, b1
  | Eequ (e1,e2) ->
      let t1 = term denv env impl e1 in
      let t2 = term denv env impl e2 in
      t_equ t1 t2, false
  | Evar _ | Edob _ | Enum _ -> error ~loc FmlaExpected

Andrei Paskevich's avatar
Andrei Paskevich committed
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
and let_defn denv env impl { e_node = n ; e_loc = loc } =
  let rec newenv env tvl vl = function
    | [] -> env, List.rev tvl, List.rev vl
    | (s,{ e_node = Edef (DT DTtype, []); e_loc = loc })::al ->
        if vl <> [] then errorm ~loc "Invalid type quantifier";
        let tv = create_tvsymbol (id_user s loc) in
        let env = Mstr.add s (STVar tv) env in
        newenv env (tv::tvl) vl al
    | (s,e)::al ->
        let ty = ty denv env impl e in
        let vs = create_vsymbol (id_user s e.e_loc) ty in
        let env = Mstr.add s (SVar vs) env in
        newenv env tvl (vs::vl) al
  in
  let rec check ss vl al = match vl,al with
    | [],[] -> ()
    | (v,_)::vl, { e_node = Evar u }::al when u = v ->
466
        let ss = Sstr.change (fun b ->
467
          not (b && error ~loc (DuplicateVar v))) v ss in
Andrei Paskevich's avatar
Andrei Paskevich committed
468 469 470 471 472 473
        check ss vl al
    | _,_ -> error ~loc MalformedLet in
  let dig vl d isf e = match d.e_node with
    | Eapp (s,al) ->
        check Sstr.empty vl al;
        let enw,tvl,vl = newenv env [] [] vl in
474 475 476 477
        let fvs s v = ty_freevars s v.vs_ty in
        let tvs = List.fold_left fvs Stv.empty vl in
        let add s v = if Stv.mem v tvs then s else Stv.add v s in
        let mvs = List.fold_left add Stv.empty tvl in
Andrei Paskevich's avatar
Andrei Paskevich committed
478 479
        if isf then
          let f,_ = fmla denv enw impl None [] e in
480
          Mstr.add s (SletP (tvl,mvs,vl,f)) env, s
Andrei Paskevich's avatar
Andrei Paskevich committed
481 482
        else
          let t = term denv enw impl e in
483
          Mstr.add s (SletF (tvl,mvs,vl,t)) env, s
Andrei Paskevich's avatar
Andrei Paskevich committed
484
    | _ -> assert false (* impossible *) in
485 486
  let rec down vl = function
    | Eqnt (Qforall,ul,d) -> down (vl @ ul) d.e_node
Andrei Paskevich's avatar
Andrei Paskevich committed
487 488 489
    | Ebin (BOequ,e1,e2) -> dig vl e1 true e2
    | Eequ (e1,e2) -> dig vl e1 false e2
    | _ -> assert false (* impossible *) in
490
  down [] n
Andrei Paskevich's avatar
Andrei Paskevich committed
491

492
and ls_args denv env impl loc fs tvl gl mvs al =
Andrei Paskevich's avatar
Andrei Paskevich committed
493
  let rec args tvm tvl al = match tvl,al with
494 495 496
    | (tv::tvl),({e_node = Edef (DT DTdummy,[]); e_loc = loc}::al) ->
        if Stv.mem tv mvs then error ~loc InvalidDummy;
        args tvm tvl al
Andrei Paskevich's avatar
Andrei Paskevich committed
497 498 499 500 501
    | (tv::tvl),(a::al) ->
        let ty = ty denv env impl a in
        let tvm = Mtv.add tv ty tvm in
        args tvm tvl al
    | [],al ->
Andrei Paskevich's avatar
Andrei Paskevich committed
502 503
        let ghost v =
          fs_app denv.fs_ghost [] (ty_app denv.ts_ghost [Mtv.find v tvm]) in
504 505
        let tl = List.map ghost gl @ List.map (term denv env impl) al in
        let tvm = List.fold_left2 (ty_check loc) tvm fs.ls_args tl in
506
        let ty = Opt.map (ty_inst tvm) fs.ls_value in
507
        t_app fs tl ty
Andrei Paskevich's avatar
Andrei Paskevich committed
508 509 510 511
    | _ -> error ~loc BadArity
  in
  args Mtv.empty tvl al

512
and let_args denv env impl loc e tvl mvs vl al =
Andrei Paskevich's avatar
Andrei Paskevich committed
513
  let rec args tvm vm tvl vl al = match tvl,vl,al with
514 515 516
    | (tv::tvl),_,({e_node = Edef (DT DTdummy,[]); e_loc = loc}::al) ->
        if Stv.mem tv mvs then error ~loc InvalidDummy;
        args tvm vm tvl vl al
Andrei Paskevich's avatar
Andrei Paskevich committed
517 518 519 520 521 522
    | (tv::tvl),_,(a::al) ->
        let ty = ty denv env impl a in
        let tvm = Mtv.add tv ty tvm in
        args tvm vm tvl vl al
    | _,(v::vl),(a::al) ->
        let t = term denv env impl a in
523
        let tvm = ty_check loc tvm v.vs_ty t in
Andrei Paskevich's avatar
Andrei Paskevich committed
524 525 526 527 528 529 530
        let vm = Mvs.add v t vm in
        args tvm vm tvl vl al
    | [],[],[] ->
        t_ty_subst tvm vm e
    | _ -> error ~loc BadArity
  in
  args Mtv.empty Mvs.empty tvl vl al
Andrei Paskevich's avatar
Andrei Paskevich committed
531

532 533 534 535 536 537 538 539
let typedecl denv env impl loc s (tvl,(el,e)) =
  if e.e_node = Edef (DT DTtype, []) then
    (* type constructor *)
    if tvl <> [] then error ~loc DependentTy else
    let ntv { e_node = n ; e_loc = loc } = match n with
      | Edef (DT DTtype, []) -> create_tvsymbol (id_fresh "a")
      | _ -> error ~loc DependentTy
    in
Andrei Paskevich's avatar
Andrei Paskevich committed
540
    let ss = if s = "int" || s = "real" then "_" ^ s else s in
Clément Fumex's avatar
Clément Fumex committed
541
    let ts = create_tysymbol (id_user ss loc) (List.map ntv el) NoDef in
542
    Hstr.add impl s (SType ts)
543 544 545 546 547 548 549
  else
    (* function/predicate symbol *)
    let ntv (s, { e_node = n ; e_loc = loc }) = match n with
      | Edef (DT DTtype, []) -> create_tvsymbol (id_fresh s)
      | _ -> error ~loc DependentTy
    in
    let tvl = List.map ntv tvl in
550 551 552 553
    let add e v =
      let s = v.tv_name.id_string in
      Mstr.add_new (DuplicateVar s) s (STVar v) e
    in
554 555
    let env = List.fold_left add env tvl in
    let tyl = List.map (ty denv env impl) el in
556 557 558
    let tvs = List.fold_left ty_freevars Stv.empty tyl in
    let add s v = if Stv.mem v tvs then s else Stv.add v s in
    let mvs = List.fold_left add Stv.empty tvl in
Andrei Paskevich's avatar
Andrei Paskevich committed
559
    let ghost v = ty_app denv.ts_ghost [ty_var v] in
560
    if e.e_node = Edef (DT DTprop, []) then
561
      let gvl = List.filter (fun v -> not (Stv.mem v tvs)) tvl in
Andrei Paskevich's avatar
Andrei Paskevich committed
562
      let tyl = List.map ghost gvl @ tyl in
563
      let ls = create_psymbol (id_user s loc) tyl in
Andrei Paskevich's avatar
Andrei Paskevich committed
564
      if gvl <> [] then add_theory env impl denv.th_ghost;
565
      Hstr.add impl s (SPred (tvl,gvl,mvs,ls))
566 567
    else
      let tyv = ty denv env impl e in
568
      let tvs = ty_freevars tvs tyv in
569
      let gvl = List.filter (fun v -> not (Stv.mem v tvs)) tvl in
Andrei Paskevich's avatar
Andrei Paskevich committed
570
      let tyl = List.map ghost gvl @ tyl in
571
      let ls = create_fsymbol (id_user s loc) tyl tyv in
Andrei Paskevich's avatar
Andrei Paskevich committed
572
      if gvl <> [] then add_theory env impl denv.th_ghost;
573
      Hstr.add impl s (SFunc (tvl,gvl,mvs,ls))
574 575

let flush_impl ~strict env uc impl =
Andrei Paskevich's avatar
Andrei Paskevich committed
576 577
  let update_th _ e uc = match e with
    | Suse th ->
578
        let uc = open_scope uc th.th_name.id_string in
Andrei Paskevich's avatar
Andrei Paskevich committed
579
        let uc = use_export uc th in
580
        close_scope uc ~import:false
Andrei Paskevich's avatar
Andrei Paskevich committed
581 582
    | _ -> uc
  in
583 584
  let update s e (env,uc) = match e with
    | SType ts ->
585
        Mstr.add s e env, add_ty_decl uc ts
Andrei Paskevich's avatar
Andrei Paskevich committed
586
    | SFunc (_,_,_,ls) | SPred (_,_,_,ls) ->
587
        Mstr.add s e env, add_param_decl uc ls
588 589 590 591 592
    | STVar tv when strict ->
        errorm ?loc:tv.tv_name.id_loc "Unbound type variable %s" s
    | SVar vs when strict ->
        errorm ?loc:vs.vs_name.id_loc "Unbound variable %s" s
    | STVar _ | SVar _ -> env,uc
Andrei Paskevich's avatar
Andrei Paskevich committed
593
    | Sdobj ls ->
594
        let uc = add_param_decl uc ls in
Andrei Paskevich's avatar
Andrei Paskevich committed
595 596 597 598 599 600 601 602 603 604 605 606
        let t = t_app ls [] ls.ls_value in
        let add _ s f = match s with
          | Sdobj fs -> t_and_simp f (t_neq (t_app fs [] fs.ls_value) t)
          | _ -> f in
        let f = Mstr.fold add env t_true in
        let uc = if t_equal f t_true then uc else
          let id = ls.ls_name.id_string ^ "_def" in
          let pr = create_prsymbol (id_fresh id) in
          add_prop_decl uc Paxiom pr f in
        Mstr.add s e env, uc
    | Suse _ ->
        Mstr.add s e env, uc
607 608 609
    (* none of these is possible in implicit *)
    | SletF _ | SletP _ | STSko _ -> assert false
  in
610 611 612
  let uc = Hstr.fold update_th impl uc in
  let res = Hstr.fold update impl (env,uc) in
  Hstr.clear impl;
613 614
  res

Andrei Paskevich's avatar
Andrei Paskevich committed
615 616 617 618
let typecheck lib path ast =
  (* initial environment *)
  let env  = Mstr.empty in
  let denv = make_denv lib in
619
  let impl = Hstr.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
620 621
  add_theory env impl denv.th_univ;
  (* parsing function *)
622
  let conj = ref [] in
623 624 625 626 627 628 629 630 631 632 633 634 635
  let input (env,uc) = function
    (* type declarations *)
    | Formula (_,_,Type,TypedAtom (s,e),loc) ->
        typedecl denv env impl loc s e;
        flush_impl ~strict:true env uc impl
    | Formula (_,_,Type,_,loc)
    | Formula (_,_,_,TypedAtom _,loc) ->
        errorm ~loc "Invalid type declaration"
    (* logical formulas *)
    | Formula (_,_,_,Sequent _,loc) -> (* TODO *)
        errorm ~loc "Sequents are not supported"
    | Formula (k,s,r,LogicFormula e,loc) ->
        let strict = k <> CNF in
636 637
        let goal = r = Conjecture in
        let f,_ = fmla denv env impl (Some goal) [] e in
638
        let f = if strict then f else
639
          let q = if goal then Texists else Tforall in
640
          let vl = Mvs.keys (t_vars f) in
641 642 643
          t_quant_close q vl [] f in
        let env,uc = flush_impl ~strict env uc impl in
        let pr = create_prsymbol (id_user s loc) in
644 645
        if goal then conj := (pr, f) :: !conj;
        env, if goal then uc else add_prop_decl uc Paxiom pr f
646 647
    (* includes *)
    | Include (_,_,loc) ->
648
        errorm ~loc "Inclusion is not supported"
649 650 651 652
  in
  (* FIXME: localize the identifier *)
  let uc = create_theory ~path (id_fresh "T") in
  let _,uc = List.fold_left input (env,uc) ast in
653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
  (* In presence of conjectures, TPTP requires us to prove
     their conjunction, but no conjectures means |- false.
     This is awkward, and most provers treat conjectures
     disjunctively, as in a sequent. We follow TPTP here. *)
  let pr_false = create_prsymbol (id_fresh "contradiction") in
  let uc = match !conj with
    | g :: gl ->
        let combine (_, f) (pr, g) = pr, t_and g f in
        let pr, goal = List.fold_left combine g gl in
        if Stv.is_empty (t_ty_freevars Stv.empty goal) then
          add_prop_decl uc Pgoal pr goal
        else (* Why3 does not support polymorphic goals *)
          let uc = add_prop_decl uc Paxiom pr (t_not goal) in
          add_prop_decl uc Pgoal pr_false t_false
    | [] -> add_prop_decl uc Pgoal pr_false t_false
  in
669
  Mstr.singleton "T" (close_theory uc)