diff options
| author | Kathy Gray | 2014-02-07 12:46:56 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-07 12:46:56 +0000 |
| commit | 7eb6dea6255eb0dbddaca6309af4f9fd1755041b (patch) | |
| tree | caeec3011679719b7175bd29e72fd698be851659 /src | |
| parent | 062eadd4238692c2f5b486d0febcf05c7b48ca83 (diff) | |
Correct variable-name bug that was throwing away type checking coercions and type annotations
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.mli | 1 | ||||
| -rw-r--r-- | src/test/test1.sail | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 7 |
3 files changed, 7 insertions, 3 deletions
diff --git a/src/pretty_print.mli b/src/pretty_print.mli index d1ea2479..bf32a805 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -4,6 +4,7 @@ open Format (* Prints on formatter the defs following source syntax *) val pp_defs : Format.formatter -> tannot defs -> unit +val pp_exp : Format.formatter -> exp -> unit (* Prints on formatter the defs as Lem Ast nodes *) val pp_lem_defs : Format.formatter -> tannot defs -> unit diff --git a/src/test/test1.sail b/src/test/test1.sail index c603bb65..da9e43fb 100644 --- a/src/test/test1.sail +++ b/src/test/test1.sail @@ -29,6 +29,8 @@ function clause f ( C (a) ) = C(a) end ast end f +function unit a (bit) b = if b then () else () + function bit sw s = switch s { case 0 -> bitzero } function bit main _ = {ignore(sw(0)); v1[0] } diff --git a/src/type_check.ml b/src/type_check.ml index f394f05e..e58f87b1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -721,8 +721,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) -> let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) pat in let u,cs = type_consistent l d_env t' param_t in - let exp,_,_,constraints,ef = check_exp (Env(d_env,Envmap.union t_env t_env')) ret_t exp in - (FCL_aux((FCL_Funcl(id,pat',exp)),(l,tannot)),constraints'@cs@constraints)) funcls) in + let exp',_,_,constraints,ef = check_exp (Env(d_env,Envmap.union t_env t_env')) ret_t exp in + (*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' in*) + (FCL_aux((FCL_Funcl(id,pat',exp')),(l,tannot)),constraints'@cs@constraints)) funcls) in match (in_env,tannot) with | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),Emp,c',eft') -> let u,constraints,eft = subst params u constraints eft in @@ -736,7 +737,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, Env(d_env,Envmap.insert t_env (id,tannot)) | _ , _-> let t_env = if is_rec then Envmap.insert t_env (id,tannot) else t_env in - let funcles,cs = check t_env in + let funcls,cs = check t_env in let cs' = resolve_constraints cs in let tannot = resolve_params tannot in (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), |