programs: complete rewrite of the type-checker in progress (in particular,...

programs: complete rewrite of the type-checker in progress (in particular, types dterm and dfmla have been moved to Denv, together with some functions); make does not compile whyml anymore; make bench will stop at the first program test; with my apologies if I messed up somewhere...
parent b255b8e8
......@@ -221,8 +221,8 @@ $(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
# build targets
byte: bin/whyml.byte
opt: bin/whyml.opt
# byte: bin/whyml.byte
# opt: bin/whyml.opt
bin/whyml.opt: src/why.cmxa $(PGMCMX) src/main.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
......@@ -504,7 +504,8 @@ clean::
.PHONY: bench test
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
# bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
bench:: bin/why.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
sh bench/bench \
"bin/why.@OCAMLBEST@" \
"bin/whyml.@OCAMLBEST@"
......
......@@ -112,10 +112,147 @@ let rec ty_of_dty = function
| Tyvar { type_val = None; user = false; type_var_loc = loc } ->
error ?loc (AnyMessage "undefined type variable")
| Tyvar { tvsymbol = tv } ->
Ty.ty_var tv
ty_var tv
| Tyapp (s, tl) ->
Ty.ty_app s (List.map ty_of_dty tl)
ty_app s (List.map ty_of_dty tl)
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
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 ->
let v = create_vsymbol (id_fresh x) ty in
Mstr.add x v env, pat_var v
| Papp (s, pl) ->
let env, pl = map_fold_left pattern env pl in
env, pat_app s pl ty
| Pas (p, x) ->
let v = create_vsymbol (id_fresh x) ty in
let env, p = pattern (Mstr.add x v env) p in
env, pat_as p v
type uquant = string list * dty
type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node =
| Tvar of string
| Tconst of constant
| Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm
| Tlet of dterm * string * dterm
| Tmatch of dterm list * (dpattern list * dterm) list
| Tnamed of string * dterm
| Teps of string * dty * dfmla
and dfmla =
| Fapp of lsymbol * dterm list
| Fquant of quant * uquant list * dtrigger list list * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
| Ftrue
| Ffalse
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * string * dfmla
| Fmatch of dterm list * (dpattern list * dfmla) list
| Fnamed of string * dfmla
| Fvar of fmla
and dtrigger =
| TRterm of dterm
| TRfmla of dfmla
let rec term env t = match t.dt_node with
| Tvar x ->
assert (Mstr.mem x env);
t_var (Mstr.find x env)
| Tconst c ->
t_const c (ty_of_dty t.dt_ty)
| Tapp (s, tl) ->
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| Tif (f, t1, t2) ->
t_if (fmla env f) (term env t1) (term env t2)
| 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
let env = Mstr.add x v env in
let e2 = term env e2 in
t_let v e1 e2
| Tmatch (tl, bl) ->
let branch (pl,e) =
let env, pl = map_fold_left pattern env pl in
(pl, term env e)
in
let bl = List.map branch bl in
let ty = (snd (List.hd bl)).t_ty in
t_case (List.map (term env) tl) bl ty
| Tnamed (x, e1) ->
let e1 = term env e1 in
t_label_add x e1
| Teps (x, ty, e1) ->
let ty = ty_of_dty ty in
let v = create_vsymbol (id_fresh x) ty in
let env = Mstr.add x v env in
let e1 = fmla env e1 in
t_eps v e1
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)
| Fquant (q, uqu, trl, f1) ->
(* TODO: shouldn't we localize this ident? *)
let uquant env (xl,ty) =
let ty = ty_of_dty ty in
map_fold_left
(fun env x ->
let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
env xl
in
let env, vl = map_fold_left uquant env uqu in
let trigger = function
| TRterm t -> Term (term env t)
| TRfmla f -> Fmla (fmla env f)
in
let trl = List.map (List.map trigger) trl in
f_quant q (List.concat vl) trl (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, x, f2) ->
let ty = ty_of_dty e1.dt_ty in
let e1 = term env e1 in
let v = create_vsymbol (id_fresh x) ty in
let env = Mstr.add x v env in
let f2 = fmla env f2 in
f_let v e1 f2
| Fmatch (tl, bl) ->
let branch (pl,e) =
let env, pl = map_fold_left pattern env pl in
(pl, fmla env e)
in
f_case (List.map (term env) tl) (List.map branch bl)
| Fnamed (x, f1) ->
let f1 = fmla env f1 in
f_label_add x f1
| Fvar f ->
f
(* Specialize *)
......@@ -127,15 +264,96 @@ let find_type_var ~loc env tv =
Htv.add env tv v;
v
let rec specialize ~loc env t = match t.ty_node with
let rec specialize_ty ~loc env t = match t.ty_node with
| Ty.Tyvar tv ->
Tyvar (find_type_var ~loc env tv)
| Ty.Tyapp (s, tl) ->
Tyapp (s, List.map (specialize ~loc env) tl)
Tyapp (s, List.map (specialize_ty ~loc env) tl)
let specialize_lsymbol ~loc s =
let tl = s.ls_args in
let t = s.ls_value in
let env = Htv.create 17 in
List.map (specialize ~loc env) tl, option_map (specialize ~loc env) t
List.map (specialize_ty ~loc env) tl, option_map (specialize_ty ~loc env) t
let rec specialize_pattern ~loc htv p =
{ dp_node = specialize_pattern_node ~loc htv p.pat_node;
dp_ty = specialize_ty ~loc htv p.pat_ty; }
and specialize_pattern_node ~loc htv = function
| Term.Pwild ->
Pwild
| Term.Pvar v ->
Pvar v.vs_name.id_string
| Term.Papp (s, pl) ->
Papp (s, List.map (specialize_pattern ~loc htv) pl)
| Term.Pas (p, v) ->
Pas (specialize_pattern ~loc htv p, v.vs_name.id_string)
let rec specialize_term ~loc htv t =
{ dt_node = specialize_term_node ~loc htv t.t_node;
dt_ty = specialize_ty ~loc htv t.t_ty; }
and specialize_term_node ~loc htv = function
| Term.Tbvar _ ->
assert false
| Term.Tvar v ->
Tvar v.vs_name.id_string (* TODO: correct? is capture possible? *)
| Term.Tconst c ->
Tconst c
| Term.Tapp (ls, tl) ->
Tapp (ls, List.map (specialize_term ~loc htv) tl)
| Term.Tif (f, t1, t2) ->
Tif (specialize_fmla ~loc htv f,
specialize_term ~loc htv t1, specialize_term ~loc htv t2)
| Term.Tlet (t1, t2) ->
let v, t2 = t_open_bound t2 in
Tlet (specialize_term ~loc htv t1,
v.vs_name.id_string, specialize_term ~loc htv t2)
| Term.Tcase (tl, bl) ->
let branch b =
let pl, t = t_open_branch b in
List.map (specialize_pattern ~loc htv) pl, specialize_term ~loc htv t
in
Tmatch (List.map (specialize_term ~loc htv) tl, List.map branch bl)
| Term.Teps fb ->
let v, f = f_open_bound fb in
Teps (v.vs_name.id_string, specialize_ty ~loc htv v.vs_ty,
specialize_fmla ~loc htv f)
(* TODO: labels are lost *)
and specialize_fmla ~loc htv f = match f.f_node with
| Term.Fapp (ls, tl) ->
Fapp (ls, List.map (specialize_term ~loc htv) tl)
| Term.Fquant (q, fq) ->
let vl, tl, f = f_open_quant fq in
let uquant v = [v.vs_name.id_string], specialize_ty ~loc htv v.vs_ty in
let tl = List.map (List.map (specialize_trigger ~loc htv)) tl in
Fquant (q, List.map uquant vl, tl, specialize_fmla ~loc htv f)
| Term.Fbinop (b, f1, f2) ->
Fbinop (b, specialize_fmla ~loc htv f1, specialize_fmla ~loc htv f2)
| Term.Fnot f1 ->
Fnot (specialize_fmla ~loc htv f1)
| Term.Ftrue ->
Ftrue
| Term.Ffalse ->
Ffalse
| Term.Fif (f1, f2, f3) ->
Fif (specialize_fmla ~loc htv f1,
specialize_fmla ~loc htv f2, specialize_fmla ~loc htv f3)
| Term.Flet (t1, f2b) ->
let v, f2 = f_open_bound f2b in
Flet (specialize_term ~loc htv t1,
v.vs_name.id_string, specialize_fmla ~loc htv f2)
| Term.Fcase (tl, fbl) ->
let branch b =
let pl, f = f_open_branch b in
List.map (specialize_pattern ~loc htv) pl, specialize_fmla ~loc htv f
in
Fmatch (List.map (specialize_term ~loc htv) tl, List.map branch fbl)
and specialize_trigger ~loc htv = function
| Term.Term t -> TRterm (specialize_term ~loc htv t)
| Term.Fmla f -> TRfmla (specialize_fmla ~loc htv f)
......@@ -26,23 +26,74 @@ open Theory
type type_var
val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var
type dty =
| Tyvar of type_var
| Tyapp of tysymbol * dty list
val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var
val unify : dty -> dty -> bool
val print_dty : Format.formatter -> dty -> unit
val ty_of_dty : dty -> ty
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
val pattern : vsymbol Mstr.t -> dpattern -> vsymbol Mstr.t * pattern
type uquant = string list * dty
type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node =
| Tvar of string
| Tconst of constant
| Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm
| Tlet of dterm * string * dterm
| Tmatch of dterm list * (dpattern list * dterm) list
| Tnamed of string * dterm
| Teps of string * dty * dfmla
and dfmla =
| Fapp of lsymbol * dterm list
| Fquant of quant * uquant list * dtrigger list list * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
| Ftrue
| Ffalse
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * string * dfmla
| Fmatch of dterm list * (dpattern list * dfmla) list
| Fnamed of string * dfmla
| Fvar of fmla
and dtrigger =
| TRterm of dterm
| TRfmla of dfmla
val term : vsymbol Mstr.t -> dterm -> term
val fmla : vsymbol Mstr.t -> dfmla -> fmla
(** Specialization *)
val specialize_ty : loc:Ptree.loc -> type_var Htv.t -> ty -> dty
val specialize_lsymbol :
loc:Ptree.loc -> lsymbol -> dty list * dty option
val specialize_term : loc:Ptree.loc -> type_var Htv.t -> term -> dterm
val specialize_fmla : loc:Ptree.loc -> type_var Htv.t -> fmla -> dfmla
(** Error reporting *)
......
......@@ -277,45 +277,6 @@ let split_qualid = function
(** Typing terms and formulas *)
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
type uquant = string list * dty
type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node =
| Tvar of string
| Tconst of constant
| Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm
| Tlet of dterm * string * dterm
| Tmatch of dterm list * (dpattern list * dterm) list
| Tnamed of string * dterm
| Teps of string * dty * dfmla
and dfmla =
| Fapp of lsymbol * dterm list
| Fquant of quant * uquant list * dtrigger list list * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
| Ftrue
| Ffalse
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * string * dfmla
| Fmatch of dterm list * (dpattern list * dfmla) list
| Fnamed of string * dfmla
| Fvar of fmla
and dtrigger =
| TRterm of dterm
| TRfmla of dfmla
let binop = function
| PPand -> Fand
| PPor -> For
......@@ -582,104 +543,6 @@ and dtype_args s loc env el tl =
in
check_arg (el, tl)
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 ->
let v = create_vsymbol (id_fresh x) ty in
Mstr.add x v env, pat_var v
| Papp (s, pl) ->
let env, pl = map_fold_left pattern env pl in
env, pat_app s pl ty
| Pas (p, x) ->
let v = create_vsymbol (id_fresh x) ty in
let env, p = pattern (Mstr.add x v env) p in
env, pat_as p v
let rec term env t = match t.dt_node with
| Tvar x ->
assert (Mstr.mem x env);
t_var (Mstr.find x env)
| Tconst c ->
t_const c (ty_of_dty t.dt_ty)
| Tapp (s, tl) ->
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| Tif (f, t1, t2) ->
t_if (fmla env f) (term env t1) (term env t2)
| 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
let env = Mstr.add x v env in
let e2 = term env e2 in
t_let v e1 e2
| Tmatch (tl, bl) ->
let branch (pl,e) =
let env, pl = map_fold_left pattern env pl in
(pl, term env e)
in
let bl = List.map branch bl in
let ty = (snd (List.hd bl)).t_ty in
t_case (List.map (term env) tl) bl ty
| Tnamed (x, e1) ->
let e1 = term env e1 in
t_label_add x e1
| Teps (x, ty, e1) ->
let ty = ty_of_dty ty in
let v = create_vsymbol (id_fresh x) ty in
let env = Mstr.add x v env in
let e1 = fmla env e1 in
t_eps v e1
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)
| Fquant (q, uqu, trl, f1) ->
(* TODO: shouldn't we localize this ident? *)
let uquant env (xl,ty) =
let ty = ty_of_dty ty in
map_fold_left
(fun env x ->
let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
env xl
in
let env, vl = map_fold_left uquant env uqu in
let trigger = function
| TRterm t -> Term (term env t)
| TRfmla f -> Fmla (fmla env f)
in
let trl = List.map (List.map trigger) trl in
f_quant q (List.concat vl) trl (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, x, f2) ->
let ty = ty_of_dty e1.dt_ty in
let e1 = term env e1 in
let v = create_vsymbol (id_fresh x) ty in
let env = Mstr.add x v env in
let f2 = fmla env f2 in
f_let v e1 f2
| Fmatch (tl, bl) ->
let branch (pl,e) =
let env, pl = map_fold_left pattern env pl in
(pl, fmla env e)
in
f_case (List.map (term env) tl) (List.map branch bl)
| Fnamed (x, f1) ->
let f1 = fmla env f1 in
f_label_add x f1
| Fvar f ->
f
(** Typing declarations, that is building environments. *)
open Ptree
......
......@@ -40,7 +40,10 @@ exception Error of error
val report : Format.formatter -> error -> unit
(** export for program typing *)
(******************************************************************************)
(** The following is exported for program typing (src/programs/pgm_typing.ml) *)
(******************************************************************************)
val specialize_fsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
......@@ -66,13 +69,9 @@ val type_fmla : denv -> vsymbol Mstr.t -> Ptree.lexpr -> fmla
val dty : denv -> Ptree.pty -> Denv.dty
type dpattern
val dpat : denv -> Ptree.pattern -> denv * dpattern
val dpat : denv -> Ptree.pattern -> denv * Denv.dpattern
val dpat_list :
denv -> Denv.dty list -> Ptree.pattern list -> denv * dpattern list
val pattern : vsymbol Mstr.t -> dpattern -> vsymbol Mstr.t * pattern
denv -> Denv.dty list -> Ptree.pattern list -> denv * Denv.dpattern list
val qloc : Ptree.qualid -> Loc.position
......
......@@ -27,7 +27,6 @@ open Term
open Decl
open Theory
open Pgm_ttree
open Pgm_itree
open Pgm_typing
module E = Pgm_effect
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Why
(* intermediate trees for weakest preconditions *)
type loc = Loc.position
type assertion_kind = Pgm_ptree.assertion_kind
type lazy_op = Pgm_ptree.lazy_op
type variant = Pgm_ttree.variant
type reference = Pgm_ttree.reference
type effect = Pgm_effect.t
type pre = Pgm_ttree.pre
type post = Pgm_ttree.post
type type_v = Pgm_ttree.type_v
type type_c = Pgm_ttree.type_c
type binder = Pgm_ttree.binder
type loop_annotation = Pgm_ttree.loop_annotation
type label = Pgm_ttree.label
type expr = {
expr_desc : expr_desc;
expr_type : Ty.ty;
expr_type_v: type_v;
expr_effect: Pgm_effect.t;
expr_loc : loc;
}
and expr_desc =
| Elogic of Term.term
| Elocal of Term.vsymbol
| Eglobal of Term.lsymbol
| Efun of binder list * triple
| Elet of Term.vsymbol * expr * expr
| Eletrec of recfun list * expr
| Esequence of expr * expr
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Ematch of expr list * (Term.pattern list * expr) list
| Eskip
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
| Elabel of label * expr
| Eany of type_c
and recfun = Term.vsymbol * binder list * variant option * triple
and triple = pre * expr * post
type decl =
| Dlet of Term.lsymbol * expr
| Dletrec of (Term.lsymbol * recfun) list
| Dparam of Term.lsymbol * type_v
type file = decl list
......@@ -27,6 +27,7 @@ type assertion_kind = Pgm_ptree.assertion_kind
type lazy_op = Pgm_ptree.lazy_op
(*****************************************************************************)
(* phase 1: destructive typing *)
type dreference =
......@@ -39,11 +40,9 @@ type deffect = {
de_raises : Term.lsymbol list;
}
type dlexpr = Typing.denv * Ptree.lexpr
type dpre = Denv.dfmla
type dpre = dlexpr
type dpost = dlexpr * (Term.lsymbol * dlexpr) list
type dpost = Denv.dfmla * (Term.lsymbol * Denv.dfmla) list
type dtype_v =
| DTpure of Denv.dty
......@@ -57,18 +56,19 @@ and dtype_c =
and dbinder = string * dtype_v
type dvariant = Ptree.lexpr * Term.lsymbol
type dvariant = Denv.dterm * Term.lsymbol
type dloop_annotation = {
dloop_invariant : Ptree.lexpr option;
dloop_invariant : Denv.dfmla option;
dloop_variant : dvariant option;
}
type dexpr = {
dexpr_desc : dexpr_desc;
dexpr_denv : Typing.denv;
dexpr_type : Denv.dty;
dexpr_loc : loc;
dexpr_desc : dexpr_desc;
dexpr_denv : Typing.denv;
dexpr_type : Denv.dty;