diff options
| author | Peter Sewell | 2014-10-30 16:24:38 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-10-30 16:24:38 +0000 |
| commit | 21738f049b1365c8436780449f9fbfdce1e9324d (patch) | |
| tree | a5fc9f57db9d873fccac21b1cd839aeef1fc4bfc /src/lem_interp/interp_inter_imp.lem | |
| parent | f77c8772511be123bf3178ac486bc622d3bab008 (diff) | |
| parent | aead63946e85ccd9468f8315abc319be965e1030 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/l2
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index bfca32d3..7b96aef5 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -336,13 +336,14 @@ let rec find_reg_name reg = function | [] -> Nothing | (reg_name,v)::registers -> match (reg,reg_name) with - | (Reg i, Reg n) -> if i = n then v else find_reg_name reg registers + | (Reg i, Reg n) -> if i = n then (Just v) else find_reg_name reg registers | (Reg_slice i (p1,p2), Reg_slice n (p3,p4)) -> - if i=n && p1=p3 && p2 = p4 then v else find_reg_name reg registers + if i=n && p1=p3 && p2 = p4 then (Just v) else find_reg_name reg registers | (Reg_field i f _,Reg_field n fn _) -> - if i=n && f = fn then v else find_reg_name reg registers + if i=n && f = fn then (Just v) else find_reg_name reg registers | (Reg_f_slice i f _ (p1,p2), Reg_f_slice n fn _ (p3,p4)) -> - if i=n && f=fn && p1=p3 && p2=p3 then v else find_reg_name reg registers + if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers + | _ -> find_reg_name reg registers end end let rec ie_loop mode register_values i_state = |