open import Interp_ast
open import Interp_utilities
open import Pervasives

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

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))
	| _ -> (i,IOther) end
    | _ -> 
      let i = "Unnamed" in
      match tannot with
	| Just(t,_,_,_) -> (i,(extract_ityp t))
	| _ -> (i,IOther) end
end

let rec extract_from_ast ast = []

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