programs: new type-checker still in progress

parent 11fb9f0a
......@@ -208,7 +208,7 @@ PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_parser.output src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
pgm_types pgm_typing pgm_itree pgm_wp pgm_main
pgm_types pgm_typing pgm_wp pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......@@ -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 $@' &&) \
......
......@@ -68,7 +68,8 @@ val type_term : denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val type_fmla : denv -> vsymbol Mstr.t -> Ptree.lexpr -> fmla
val dty : denv -> Ptree.pty -> Denv.dty
val dterm : denv -> Ptree.lexpr -> Denv.dterm
val dfmla : denv -> Ptree.lexpr -> Denv.dfmla
val dpat : denv -> Ptree.pattern -> denv * Denv.dpattern
val dpat_list :
denv -> Denv.dty list -> Ptree.pattern list -> denv * Denv.dpattern list
......
......@@ -64,17 +64,16 @@ type dloop_annotation = {
}
type dexpr = {
dexpr_desc : dexpr_desc;
dexpr_denv : Typing.denv;
dexpr_type : Denv.dty;
dexpr_type_v: dtype_v;
dexpr_loc : loc;
dexpr_desc : dexpr_desc;
dexpr_denv : Typing.denv;
dexpr_type : Denv.dty;
dexpr_loc : loc;
}
and dexpr_desc =
| DEconstant of constant
| DElocal of string
| DEglobal of Term.lsymbol
| DElocal of string * dtype_v
| DEglobal of Term.lsymbol * dtype_v
| DElogic of Term.lsymbol
| DEapply of dexpr * dexpr
| DEfun of dbinder list * dtriple
......@@ -131,8 +130,8 @@ type iexpr = {
and iexpr_desc =
| IElogic of Term.term
| IElocal of Term.vsymbol
| IEglobal of Term.lsymbol
| IElocal of Term.vsymbol * type_v
| IEglobal of Term.lsymbol * type_v
| IEapply of iexpr * Term.vsymbol
| IEapply_ref of iexpr * reference
| IEfun of binder list * itriple
......
......@@ -160,7 +160,11 @@ let add_global id tyv env =
let s = create_lsymbol id tyl (Some ty) in
s, { env with globals = Mstr.add s.ls_name.id_string (s, tyv) env.globals }
let add_decl d env = { env with uc = add_decl env.uc d }
let add_decl d env =
{ env with uc = Typing.with_tuples add_decl env.uc d }
let add_pdecl e d env =
{ env with uc = Typing.add_decl e Mnm.empty env.uc d }
let add_exception id ty env =
let tyl = match ty with None -> [] | Some ty -> [ty] in
......
......@@ -55,6 +55,7 @@ val empty_env : theory_uc -> env
val add_global : preid -> type_v -> env -> lsymbol * env
val add_decl : decl -> env -> env
val add_pdecl : Env.env -> Ptree.decl -> env -> env
val add_exception : preid -> ty option -> env -> lsymbol * env
......
This diff is collapsed.
......@@ -33,3 +33,4 @@ val report : Format.formatter -> error -> unit
val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
val reference_of_term : Term.term -> Pgm_effect.reference
......@@ -372,7 +372,6 @@ let add_wp_decl l f env =
let decl env = function
| Pgm_ttree.Dlet (ls, e) ->
let e = expr env e in
if !debug then
eprintf "@[--effect %a-----@\n %a@]@\n----------------@."
Pretty.print_ls ls print_type_v e.expr_type_v;
......@@ -380,20 +379,16 @@ let decl env = function
if !debug then
eprintf "wp = %a@\n----------------@." Pretty.print_fmla f;
let env = add_wp_decl ls f env in
let env = add_global ls e.expr_type_v env in
env
| Pgm_ttree.Dletrec dl ->
let add_one env (ls, def) =
let def = recfun env def in
let f = wp_recfun env ls def in
let env = add_wp_decl ls f env in
let v = assert false (*TODO*) in
let env = add_global ls v env in
let _v = assert false (*TODO*) in
env
in
List.fold_left add_one env dl
| Pgm_ttree.Dparam (ls, v) ->
let env = add_global ls v env in
| Pgm_ttree.Dparam (_ls, _v) ->
env
let file uc dl =
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment