Commit d09182e1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: more typing

parent 13012033
......@@ -290,6 +290,8 @@ expr:
triple:
| LOGIC expr LOGIC
{ lexpr $1, $2, lexpr $3 }
| expr
{ lexpr_true (), $1, lexpr_true () }
;
simple_expr:
......
......@@ -82,8 +82,7 @@ and expr_desc =
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
(* TODO: raise, try, any, post?,
ghost *)
(* TODO: raise, try, any, post?, ghost *)
and triple = lexpr * expr * lexpr
......
......@@ -62,7 +62,7 @@ and dexpr_desc =
| DEapply of dexpr * dexpr
| DEfun of dbinder list * dtriple
| DElet of string * dexpr * dexpr
| DEletrec of (string * dbinder list * dvariant option * dtriple) * dexpr
| DEletrec of (string * dbinder list * dvariant option * dtriple) list * dexpr
| DEsequence of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
......@@ -114,6 +114,8 @@ and expr_desc =
| Eapply of expr * expr
| Efun of binder list * triple
| Elet of Term.vsymbol * expr * expr
| Eletrec of
(Term.vsymbol * Term.vsymbol list * variant option * triple) list * expr
| Esequence of expr * expr
| Eif of expr * expr * expr
......
......@@ -151,13 +151,11 @@ and expr_desc env loc = function
| Pgm_ptree.Eapply (e1, e2) ->
let e1 = dexpr env e1 in
let e2 = dexpr env e2 in
begin match e1.dexpr_type with
| Tyapp (ts, [ty2; ty]) when Ty.ts_equal ts (ts_arrow env.uc) ->
expected_type e2 ty2;
DEapply (e1, e2), ty
| _ ->
errorm ~loc:e1.dexpr_loc "this expression is not a function"
end
let ty2 = create_type_var loc and ty = create_type_var loc in
if not (Denv.unify e1.dexpr_type (Tyapp (ts_arrow env.uc, [ty2; ty]))) then
errorm ~loc:e1.dexpr_loc "this expression is not a function";
expected_type e2 ty2;
DEapply (e1, e2), ty
| Pgm_ptree.Efun (bl, t) ->
let env, bl = map_fold_left dbinder env bl in
let (_,e,_) as t = dtriple env t in
......@@ -170,8 +168,10 @@ and expr_desc env loc = function
let env = { env with denv = Typing.add_var x ty1 env.denv } in
let e2 = dexpr env e2 in
DElet (x, e1, e2), e2.dexpr_type
| Pgm_ptree.Eletrec _ (*(id, bl, v, p, e, q)*) ->
assert false (*TODO*)
| Pgm_ptree.Eletrec (dl, e1) ->
let env, dl = dletrec env dl in
let e1 = dexpr env e1 in
DEletrec (dl, e1), e1.dexpr_type
| Pgm_ptree.Esequence (e1, e2) ->
let e1 = dexpr env e1 in
......@@ -220,6 +220,28 @@ and expr_desc env loc = function
expected_type e1 ty;
e1.dexpr_desc, ty
and dletrec env dl =
(* add all functions into environment *)
let add_one env (id,_,_,_) =
let ty = create_type_var id.id_loc in
{ env with denv = Typing.add_var id.id ty env.denv }
in
let env = List.fold_left add_one env dl in
(* then type-check all of them and unify *)
let type_one (id, bl, v, t) =
let tyres = Typing.find_var id.id env.denv in
let env, bl = map_fold_left dbinder env bl in
let (_,e,_) as t = dtriple env t in
let tyl = List.map (fun (x,_) -> Typing.find_var x env.denv) bl in
let ty = dcurrying env.uc tyl e.dexpr_type in
if not (Denv.unify ty tyres) then
errorm ~loc:id.id_loc
"this expression has type %a, but is expected to have type %a"
print_dty ty print_dty tyres;
(id.id, bl, v, t)
in
env, List.map type_one dl
and dtriple env (p, e, q) =
let p = env.denv, p in
let e = dexpr env e in
......
......@@ -4,7 +4,13 @@ use import list.List
logic c : int
}
let p = c
let test (n:int) =
let rec is_even (x:int) =
{x>=0}
if x=0 then True else if x=1 then False else is_even (x-2)
{true}
in
is_even n
(*
let rec mem (x:int) (l:int list) =
......
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