1 files changed, 46 insertions, 20 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 5cf1115b..f78e2d29 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -4,27 +4,32 @@ open import Pervasives
 
 type instr_parm_typ = 
 | IBit
-| IBitvector of maybe integer
-| IRange of maybe integer
+| IBitvector of maybe nat
+| IRange of maybe nat
+| IEnum of string * nat
 | IOther
 
 type instruction_form = 
 |  Instr_form of string * list (string * instr_parm_typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs tannot -> list instruction_form
+val extract_instructions : string -> defs tannot -> list instruction_form
 
-let extract_ityp t = match t with
-  | T_id "bit" -> IBit
-  | T_id "bool" -> IBit
-  | T_app "vector" (T_args [_; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]) ->
-    IBitvector (Just len)
-  | T_app "vector" (T_args [_;_;_;T_arg_typ (T_id "bit")]) -> IBitvector Nothing
-  | T_app "atom" (T_args [T_arg_nexp (Ne_const num)]) ->
-    IRange (Just num)
-  | T_app "atom" _ -> IRange Nothing
-  | T_app "range" (T_args [_;T_arg_nexp (Ne_const max)]) -> IRange (Just max)
-  | T_app "range" _ -> IRange Nothing
+let rec extract_ityp t tag = match (t,tag) with
+  | (T_abbrev _ t,_) -> extract_ityp t tag
+  | (T_id "bit",_) -> IBit
+  | (T_id "bool",_) -> IBit
+  | (T_app "vector" (T_args [_; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_) ->
+    IBitvector (Just (natFromInteger len))
+  | (T_app "vector" (T_args [_;_;_;T_arg_typ (T_id "bit")]),_) -> IBitvector Nothing
+  | (T_app "atom" (T_args [T_arg_nexp (Ne_const num)]),_) ->
+    IRange (Just (natFromInteger num))
+  | (T_app "atom" _,_) -> IRange Nothing
+  | (T_app "range" (T_args [_;T_arg_nexp (Ne_const max)]),_) -> 
+    IRange (Just (natFromInteger max))
+  | (T_app "range" _,_) -> IRange Nothing
+  | (T_app i (T_args []),Tag_enum max) ->
+    IEnum i (natFromInteger max)
   | _ -> IOther
 end 
 
@@ -32,17 +37,15 @@ let extract_parm (E_aux e (_,tannot)) =
   match e with
     | E_id (Id_aux (Id i) _) ->
       match tannot with
-	| Just(t,_,_,_) -> (i,(extract_ityp t))
+	| Just(t,tag,_,_) -> (i,(extract_ityp t tag))
 	| _ -> (i,IOther) end
     | _ -> 
       let i = "Unnamed" in
       match tannot with
-	| Just(t,_,_,_) -> (i,(extract_ityp t))
+	| Just(t,tag,_,_) -> (i,(extract_ityp t tag))
 	| _ -> (i,IOther) end
 end
 
-let rec extract_from_ast ast = []
-
 let rec extract_from_decode decoder = 
   match decoder with
     | [] -> []
@@ -62,6 +65,25 @@ let rec extract_effects_of_fcl id execute = match execute with
   | _::executes -> extract_effects_of_fcl id executes
 end
 
+let rec extract_patt_parm (P_aux p (_,tannot)) = 
+  let t = match tannot with
+    | Just(t,tag,_,_) -> extract_ityp t tag
+    | _ -> IOther end in
+  match p with
+    | P_lit lit -> ("",t)
+    | P_wild -> ("Unnamed",t)
+    | P_as _ (Id_aux (Id id) _) -> (id,t)
+    | P_typ typ p -> extract_patt_parm p
+    | P_id (Id_aux (Id id) _) -> (id,t)
+    | P_app (Id_aux (Id id) _) [] -> (id,t)
+    | _ -> ("",t) end
+
+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
+end
+
 let rec extract_effects instrs execute = 
   match instrs with
     | [] -> []
@@ -70,10 +92,14 @@ let rec extract_effects instrs execute =
       (Instr_form id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
 end
 
-let extract_instructions decode_name execute_name defs = 
+let extract_instructions_old decode_name execute_name defs = 
   let (Just decoder) = find_function defs (Id_aux (Id decode_name) Unknown) in
   let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
   let instr_no_effects = extract_from_decode decoder in
   let instructions = extract_effects instr_no_effects executer in
   instructions
-  
+
+let extract_instructions execute_name defs =
+  let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
+  let instructions = extract_from_execute executer in
+  instructions