Require Iteration.
Require Floats.
Require RTLgen.
Require Coloring.
Require Allocation.
Require Main.

(* Standard lib *)
Extract Inductive unit => "unit" [ "()" ].
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].

(* Float *)
Extract Inlined Constant Floats.float => "float".
Extract Constant Floats.Float.zero   => "0.".
Extract Constant Floats.Float.one   => "1.".
Extract Constant Floats.Float.neg => "( ~-. )".
Extract Constant Floats.Float.abs => "abs_float".
Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat".
Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat".
Extract Constant Floats.Float.floatofint => "Floataux.floatofint".
Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu".
Extract Constant Floats.Float.add => "( +. )".
Extract Constant Floats.Float.sub => "( -. )".
Extract Constant Floats.Float.mul => "( *. )".
Extract Constant Floats.Float.div => "( /. )".
Extract Constant Floats.Float.cmp => "Floataux.cmp".
Extract Constant Floats.Float.eq_dec => "fun (x: float) (y: float) -> x = y".

(* Iteration *)
Extract Constant Iteration.dependent_description' =>
  "fun x -> assert false".

Extract Constant Iteration.GenIter.iterate =>
  "let rec iter f a =
     match f a with Coq_inl b -> Some b | Coq_inr a' -> iter f a'
   in iter".


(* RTLgen *)
Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch".
Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".

(* RTLtyping *)
Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_environment".

(* Coloring *)
Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".

(* PPC *)
Extract Constant PPC.low_half_signed => "fun _ -> assert false".
Extract Constant PPC.high_half_signed => "fun _ -> assert false".
Extract Constant PPC.low_half_unsigned => "fun _ -> assert false".
Extract Constant PPC.high_half_unsigned => "fun _ -> assert false".

(* Suppression of stupidly big equality functions *)
Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y".
Extract Constant Locations.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y".
Extract Constant PPC.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
Extract Constant PPC.freg_eq => "fun (x: freg) (y: freg) -> x = y".
Extract Constant PPC.preg_eq => "fun (x: preg) (y: preg) -> x = y".

(* Go! *)
Recursive Extraction Library Main.