open import Interp_ast
open import Interp_utilities
open import Pervasives

type instr_parm_typ = 
| IBit
| IBitvector of maybe integer
| 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

let extract_parm (E_aux e (_,tannot)) =
  match e with
    | E_id (Id_aux (Id i) _) ->
      match tannot with
	| Just(T_id "bit",_,_,_) -> (i,IBit)
	| Just(T_id "bool",_,_,_) -> (i,IBit)
	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
	  (i,IBitvector (Just len))
	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
	  (i,IBitvector Nothing)
	| _ -> (i,IOther) end
    | _ -> 
      let i = "Unnamed" in
      match tannot with
	| Just(T_id "bit",_,_,_) -> (i,IBit)
	| Just(T_id "bool",_,_,_) -> (i,IBit)
	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
	  (i,IBitvector (Just len))
	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
	  (i,IBitvector Nothing)
	| _ -> (i,IOther) end
end

let rec extract_from_decode decoder = 
  match decoder with
    | [] -> []
    | (FCL_aux (FCL_Funcl _ pat exp) _)::decoder ->
      (match exp with
	| E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_))) ->
	  Instr_form id (List.map extract_parm parms) []
	| _ -> Skipped end)::(extract_from_decode decoder)
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 ->
    if i = id 
    then efs
    else extract_effects_of_fcl id executes
  | _::executes -> extract_effects_of_fcl id executes
end

let rec extract_effects instrs execute = 
  match instrs with
    | [] -> []
    | Skipped::instrs -> Skipped::(extract_effects instrs execute)
    | (Instr_form id parms [])::instrs -> 
      (Instr_form id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
end

let extract_instructions 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