diff options
| author | Kathy Gray | 2014-10-01 14:52:00 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-10-01 14:52:00 +0100 |
| commit | ff58bc28111de2935b3e57a6630827a2d0fac202 (patch) | |
| tree | ff7cf60db5f240d60d6ab2fde1e08f5b6bd27b6c /src | |
| parent | b7bf6fc992cc4909b571c600aca3c1807cb62a0e (diff) | |
Fix bug omitting wmem effects
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/instruction_extractor.lem | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 7 |
2 files changed, 6 insertions, 5 deletions
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem index 74e5fd4c..329073f0 100644 --- a/src/lem_interp/instruction_extractor.lem +++ b/src/lem_interp/instruction_extractor.lem @@ -36,7 +36,7 @@ let rec extract_from_decode decoder = | _ -> Skipped end)::(extract_from_decode decoder) end -let rec extract_effects_of_pat id execute = match execute with +let rec extract_effects_of_fcl id execute = match execute with | [] -> [] | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) _) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _))) :: executes -> if i = id @@ -50,7 +50,7 @@ let rec extract_effects instrs execute = | [] -> [] | Skipped::instrs -> Skipped::(extract_effects instrs execute) | (Instr id parms [])::instrs -> - (Instr id parms (extract_effects_of_pat id execute))::(extract_effects instrs execute) + (Instr id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute) end let extract_instructions decode_name execute_name defs = diff --git a/src/type_check.ml b/src/type_check.ml index 5421b1b8..a78a5db1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1166,7 +1166,8 @@ and check_block orig_envs envs imp_param expect_t exps:((tannot exp) list * tann ([E_aux(e',(l,annot))],annot,orig_envs,sc,t,ef) | e::exps -> let (e',t',t_env',sc,ef') = check_exp envs imp_param unit_t e in let (exps',annot',orig_envs,sc',t,ef) = - check_block orig_envs (Env(d_env,Envmap.union_merge (tannot_merge (Expr Parse_ast.Unknown) d_env) t_env t_env')) imp_param expect_t exps in + check_block orig_envs + (Env(d_env,Envmap.union_merge (tannot_merge (Expr Parse_ast.Unknown) d_env) t_env t_env')) imp_param expect_t exps in ((e'::exps'),annot',orig_envs,sc@sc',t,union_effects ef ef') and check_cases envs imp_param check_t expect_t pexps : ((tannot pexp) list * typ * nexp_range list * effect) = @@ -1275,8 +1276,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * | (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,ef_e) -> (es,cs_e,ef_e) | _ -> raise (Reporting_basic.err_unreachable l "Gave check_exp a tuple, didn't get a tuple back")) in - let ef_all = union_effects ef ef_es in - (LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef))), + let ef_all = union_effects ef' ef_es in + (LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef'))), item_t,Envmap.empty,tag,cs_call@cs_es,ef_all) | _ -> let e = match exps with |