diff options
Diffstat (limited to 'src/lem_interp/instruction_extractor.lem')
| -rw-r--r-- | src/lem_interp/instruction_extractor.lem | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem index 2b37bfb4..11947c17 100644 --- a/src/lem_interp/instruction_extractor.lem +++ b/src/lem_interp/instruction_extractor.lem @@ -52,20 +52,21 @@ open import Interp_ast open import Interp_utilities open import Pervasives -type instr_param_typ = +type instr_param_typ = | IBit | IBitvector of maybe nat | IRange of maybe nat | IEnum of string * nat | IOther -type instruction_form = +type instruction_form = | Instr_form of string * list (string * instr_param_typ) * list base_effect -| Skipped +| Skipped val extract_instructions : string -> defs tannot -> list instruction_form let rec extract_ityp t tag = match (t,tag) with +(* AA: Hack | (T_abbrev _ t,_) -> extract_ityp t tag | (T_id "bit",_) -> IBit | (T_id "bool",_) -> IBit @@ -82,6 +83,7 @@ let rec extract_ityp t tag = match (t,tag) with IEnum i (natFromInteger max) | (T_id i,Tag_enum max) -> IEnum i (natFromInteger max) +*) | _ -> IOther end @@ -101,7 +103,8 @@ end let rec extract_from_decode decoder = match decoder with | [] -> [] - | (FCL_aux (FCL_Funcl _ pat exp) _)::decoder -> + | (FCL_aux (FCL_Funcl _ (Pat_aux pexp _)) _)::decoder -> + let exp = match pexp with Pat_exp _ exp -> exp | Pat_when _ _ exp -> exp end in (match exp with | E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_,_))) -> Instr_form id (List.map extract_parm parms) [] @@ -110,7 +113,7 @@ end 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 -> + | FCL_aux (FCL_Funcl _ (Pat_aux (Pat_exp (P_aux (P_app (Id_aux (Id i) _) _) _) _) _)) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _,_))) :: executes -> if i = id then efs else extract_effects_of_fcl id executes @@ -132,8 +135,11 @@ let rec extract_patt_parm (P_aux p (_,tannot)) = let rec extract_from_execute fcls = match fcls with | [] -> [] - | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) parms) _) _) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls -> - (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls + | FCL_aux (FCL_Funcl _ (Pat_aux (Pat_exp (P_aux (P_app (Id_aux (Id i) _) parms) _) _) _)) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls -> + (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls + | _ :: fcls -> + (* AA: Find out what breaks this *) + extract_from_execute fcls end let rec extract_effects instrs execute = |