Commit 196c64b5 authored by Heiko Becker's avatar Heiko Becker

Enable unverified extraction of binary in Coq

parent a7677a70
......@@ -28,7 +28,10 @@ hol4/*/*.ui
hol4/*/*.uo
hol4/*/.*
hol4/heap
hol4/output/heap
hol4/*/heap
hol4/output/*.sml
hol4/binary/cake_checker
hol4/binary/checker.S
daisy
rawdata/*
.ensime*
......
type bool =
| True
| False
(** val negb : bool -> bool **)
let negb = function
| True -> False
| False -> True
type nat =
| O
| S of nat
type 'a option =
| Some of 'a
| None
type ('a, 'b) prod =
| Pair of 'a * 'b
(** val fst : ('a1, 'a2) prod -> 'a1 **)
let fst = function
| Pair (x, _) -> x
(** val snd : ('a1, 'a2) prod -> 'a2 **)
let snd = function
| Pair (_, y) -> y
type 'a list =
| Nil
| Cons of 'a * 'a list
(** val length : 'a1 list -> nat **)
let rec length = function
| Nil -> O
| Cons (_, l') -> S (length l')
type comparison =
| Eq
| Lt
| Gt
(** val compOpp : comparison -> comparison **)
let compOpp = function
| Eq -> Eq
| Lt -> Gt
| Gt -> Lt
type compareSpecT =
| CompEqT
| CompLtT
| CompGtT
(** val compareSpec2Type : comparison -> compareSpecT **)
let compareSpec2Type = function
| Eq -> CompEqT
| Lt -> CompLtT
| Gt -> CompGtT
type 'a compSpecT = compareSpecT
(** val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT **)
let compSpec2Type _ _ c =
compareSpec2Type c
type sumbool =
| Left
| Right
type positive =
| XI of positive
| XO of positive
| XH
type z =
| Z0
| Zpos of positive
| Zneg of positive
(** val flip : ('a1 -> 'a2 -> 'a3) -> 'a2 -> 'a1 -> 'a3 **)
let flip f x y =
f y x
module type OrderedType =
sig
type t
val compare : t -> t -> comparison
val eq_dec : t -> t -> sumbool
end
module type OrderedType' =
sig
type t
val compare : t -> t -> comparison
val eq_dec : t -> t -> sumbool
end
module OT_to_Full =
functor (O:OrderedType') ->
struct
type t = O.t
(** val compare : t -> t -> comparison **)
let compare =
O.compare
(** val eq_dec : t -> t -> sumbool **)
let eq_dec =
O.eq_dec
end
module OT_to_OrderTac =
functor (OT:OrderedType) ->
struct
module OTF = OT_to_Full(OT)
module TO =
struct
type t = OTF.t
(** val compare : t -> t -> comparison **)
let compare =
OTF.compare
(** val eq_dec : t -> t -> sumbool **)
let eq_dec =
OTF.eq_dec
end
end
module OrderedTypeFacts =
functor (O:OrderedType') ->
struct
module OrderTac = OT_to_OrderTac(O)
(** val eq_dec : O.t -> O.t -> sumbool **)
let eq_dec =
O.eq_dec
(** val lt_dec : O.t -> O.t -> sumbool **)
let lt_dec x y =
let c = compSpec2Type x y (O.compare x y) in
(match c with
| CompLtT -> Left
| _ -> Right)
(** val eqb : O.t -> O.t -> bool **)
let eqb x y =
match eq_dec x y with
| Left -> True
| Right -> False
end
(** val gmax : ('a1 -> 'a1 -> comparison) -> 'a1 -> 'a1 -> 'a1 **)
let gmax cmp x y =
match cmp x y with
| Lt -> y
| _ -> x
(** val gmin : ('a1 -> 'a1 -> comparison) -> 'a1 -> 'a1 -> 'a1 **)
let gmin cmp x y =
match cmp x y with
| Gt -> y
| _ -> x
module Nat =
struct
(** val compare : nat -> nat -> comparison **)
let rec compare n m =
match n with
| O ->
(match m with
| O -> Eq
| S _ -> Lt)
| S n' ->
(match m with
| O -> Gt
| S m' -> compare n' m')
(** val eq_dec : nat -> nat -> sumbool **)
let rec eq_dec n m =
match n with
| O ->
(match m with
| O -> Left
| S _ -> Right)
| S n0 ->
(match m with
| O -> Right
| S m0 -> eq_dec n0 m0)
end
module Pos =
struct
(** val succ : positive -> positive **)
let rec succ = function
| XI p -> XO (succ p)
| XO p -> XI p
| XH -> XO XH
(** val add : positive -> positive -> positive **)
let rec add x y =
match x with
| XI p ->
(match y with
| XI q0 -> XO (add_carry p q0)
| XO q0 -> XI (add p q0)
| XH -> XO (succ p))
| XO p ->
(match y with
| XI q0 -> XI (add p q0)
| XO q0 -> XO (add p q0)
| XH -> XI p)
| XH ->
(match y with
| XI q0 -> XO (succ q0)
| XO q0 -> XI q0
| XH -> XO XH)
(** val add_carry : positive -> positive -> positive **)
and add_carry x y =
match x with
| XI p ->
(match y with
| XI q0 -> XI (add_carry p q0)
| XO q0 -> XO (add_carry p q0)
| XH -> XI (succ p))
| XO p ->
(match y with
| XI q0 -> XO (add_carry p q0)
| XO q0 -> XI (add p q0)
| XH -> XO (succ p))
| XH ->
(match y with
| XI q0 -> XI (succ q0)
| XO q0 -> XO (succ q0)
| XH -> XI XH)
(** val pred_double : positive -> positive **)
let rec pred_double = function
| XI p -> XI (XO p)
| XO p -> XI (pred_double p)
| XH -> XH
(** val mul : positive -> positive -> positive **)
let rec mul x y =
match x with
| XI p -> add y (XO (mul p y))
| XO p -> XO (mul p y)
| XH -> y
(** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
let rec iter f x = function
| XI n' -> f (iter f (iter f x n') n')
| XO n' -> iter f (iter f x n') n'
| XH -> f x
(** val pow : positive -> positive -> positive **)
let pow x =
iter (mul x) XH
(** val compare_cont : comparison -> positive -> positive -> comparison **)
let rec compare_cont r x y =
match x with
| XI p ->
(match y with
| XI q0 -> compare_cont r p q0
| XO q0 -> compare_cont Gt p q0
| XH -> Gt)
| XO p ->
(match y with
| XI q0 -> compare_cont Lt p q0
| XO q0 -> compare_cont r p q0
| XH -> Gt)
| XH ->
(match y with
| XH -> r
| _ -> Lt)
(** val compare : positive -> positive -> comparison **)
let compare =
compare_cont Eq
end
module Z =
struct
(** val double : z -> z **)
let double = function
| Z0 -> Z0
| Zpos p -> Zpos (XO p)
| Zneg p -> Zneg (XO p)
(** val succ_double : z -> z **)
let succ_double = function
| Z0 -> Zpos XH
| Zpos p -> Zpos (XI p)
| Zneg p -> Zneg (Pos.pred_double p)
(** val pred_double : z -> z **)
let pred_double = function
| Z0 -> Zneg XH
| Zpos p -> Zpos (Pos.pred_double p)
| Zneg p -> Zneg (XI p)
(** val pos_sub : positive -> positive -> z **)
let rec pos_sub x y =
match x with
| XI p ->
(match y with
| XI q0 -> double (pos_sub p q0)
| XO q0 -> succ_double (pos_sub p q0)
| XH -> Zpos (XO p))
| XO p ->
(match y with
| XI q0 -> pred_double (pos_sub p q0)
| XO q0 -> double (pos_sub p q0)
| XH -> Zpos (Pos.pred_double p))
| XH ->
(match y with
| XI q0 -> Zneg (XO q0)
| XO q0 -> Zneg (Pos.pred_double q0)
| XH -> Z0)
(** val add : z -> z -> z **)
let add x y =
match x with
| Z0 -> y
| Zpos x' ->
(match y with
| Z0 -> x
| Zpos y' -> Zpos (Pos.add x' y')
| Zneg y' -> pos_sub x' y')
| Zneg x' ->
(match y with
| Z0 -> x
| Zpos y' -> pos_sub y' x'
| Zneg y' -> Zneg (Pos.add x' y'))
(** val opp : z -> z **)
let opp = function
| Z0 -> Z0
| Zpos x0 -> Zneg x0
| Zneg x0 -> Zpos x0
(** val mul : z -> z -> z **)
let mul x y =
match x with
| Z0 -> Z0
| Zpos x' ->
(match y with
| Z0 -> Z0
| Zpos y' -> Zpos (Pos.mul x' y')
| Zneg y' -> Zneg (Pos.mul x' y'))
| Zneg x' ->
(match y with
| Z0 -> Z0
| Zpos y' -> Zneg (Pos.mul x' y')
| Zneg y' -> Zpos (Pos.mul x' y'))
(** val compare : z -> z -> comparison **)
let compare x y =
match x with
| Z0 ->
(match y with
| Z0 -> Eq
| Zpos _ -> Lt
| Zneg _ -> Gt)
| Zpos x' ->
(match y with
| Zpos y' -> Pos.compare x' y'
| _ -> Gt)
| Zneg x' ->
(match y with
| Zneg y' -> compOpp (Pos.compare x' y')
| _ -> Lt)
(** val leb : z -> z -> bool **)
let leb x y =
match compare x y with
| Gt -> False
| _ -> True
(** val abs : z -> z **)
let abs = function
| Zneg p -> Zpos p
| x -> x
end
(** val zeq_bool : z -> z -> bool **)
let zeq_bool x y =
match Z.compare x y with
| Eq -> True
| _ -> False
(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)
let rec fold_left f l a0 =
match l with
| Nil -> a0
| Cons (b, t0) -> fold_left f t0 (f a0 b)
type q = { qnum : z; qden : positive }
(** val qnum : q -> z **)
let qnum x = x.qnum
(** val qden : q -> positive **)
let qden x = x.qden
(** val qcompare : q -> q -> comparison **)
let qcompare p q0 =
Z.compare (Z.mul p.qnum (Zpos q0.qden)) (Z.mul q0.qnum (Zpos p.qden))
(** val qeq_bool : q -> q -> bool **)
let qeq_bool x y =
zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
(** val qle_bool : q -> q -> bool **)
let qle_bool x y =
Z.leb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
(** val qplus : q -> q -> q **)
let qplus x y =
{ qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)));
qden = (Pos.mul x.qden y.qden) }
(** val qmult : q -> q -> q **)
let qmult x y =
{ qnum = (Z.mul x.qnum y.qnum); qden = (Pos.mul x.qden y.qden) }
(** val qopp : q -> q **)
let qopp x =
{ qnum = (Z.opp x.qnum); qden = x.qden }
(** val qminus : q -> q -> q **)
let qminus x y =
qplus x (qopp y)
(** val qinv : q -> q **)
let qinv x =
match x.qnum with
| Z0 -> { qnum = Z0; qden = XH }
| Zpos p -> { qnum = (Zpos x.qden); qden = p }
| Zneg p -> { qnum = (Zneg x.qden); qden = p }
(** val qdiv : q -> q -> q **)
let qdiv x y =
qmult x (qinv y)
(** val qmax : q -> q -> q **)
let qmax =
gmax qcompare
(** val qmin : q -> q -> q **)
let qmin =
gmin qcompare
(** val qabs : q -> q **)
let qabs x =
let { qnum = n; qden = d } = x in { qnum = (Z.abs n); qden = d }
type intv = (q, q) prod
type error = q
(** val mkIntv : q -> q -> (q, q) prod **)
let mkIntv ivlo0 ivhi0 =
Pair (ivlo0, ivhi0)
(** val ivlo : intv -> q **)
let ivlo intv0 =
fst intv0
(** val ivhi : intv -> q **)
let ivhi intv0 =
snd intv0
type precond = nat -> intv
module MakeListOrdering =
functor (O:OrderedType) ->
struct
module MO = OrderedTypeFacts(O)
end
module OrderedTypeLists =
functor (O:OrderedType) ->
struct
end
module MakeRaw =
functor (X:OrderedType) ->
struct
module MX = OrderedTypeFacts(X)
module ML = OrderedTypeLists(X)
type elt = X.t
type t = elt list
(** val empty : t **)
let empty =
Nil
(** val is_empty : t -> bool **)
let is_empty = function
| Nil -> True
| Cons (_, _) -> False
(** val mem : X.t -> X.t list -> bool **)
let rec mem x = function
| Nil -> False
| Cons (y, l) ->
(match X.compare x y with
| Eq -> True
| Lt -> False
| Gt -> mem x l)
(** val add : X.t -> X.t list -> X.t list **)
let rec add x s = match s with
| Nil -> Cons (x, Nil)
| Cons (y, l) ->
(match X.compare x y with
| Eq -> s
| Lt -> Cons (x, s)
| Gt -> Cons (y, (add x l)))
(** val singleton : elt -> elt list **)
let singleton x =
Cons (x, Nil)
(** val remove : X.t -> X.t list -> t **)
let rec remove x s = match s with
| Nil -> Nil
| Cons (y, l) ->
(match X.compare x y with
| Eq -> l
| Lt -> s
| Gt -> Cons (y, (remove x l)))
(** val union : t -> t -> t **)
let rec union s = match s with
| Nil -> (fun s' -> s')
| Cons (x, l) ->
let rec union_aux s' = match s' with
| Nil -> s
| Cons (x', l') ->
(match X.compare x x' with
| Eq -> Cons (x, (union l l'))
| Lt -> Cons (x, (union l s'))
| Gt -> Cons (x', (union_aux l')))
in union_aux
(** val inter : t -> t -> t **)
let rec inter = function
| Nil -> (fun _ -> Nil)
| Cons (x, l) ->
let rec inter_aux s' = match s' with
| Nil -> Nil
| Cons (x', l') ->
(match X.compare x x' with
| Eq -> Cons (x, (inter l l'))
| Lt -> inter l s'
| Gt -> inter_aux l')
in inter_aux
(** val diff : t -> t -> t **)
let rec diff s = match s with
| Nil -> (fun _ -> Nil)
| Cons (x, l) ->
let rec diff_aux s' = match s' with
| Nil -> s
| Cons (x', l') ->
(match X.compare x x' with
| Eq -> diff l l'
| Lt -> Cons (x, (diff l s'))
| Gt -> diff_aux l')
in diff_aux
(** val equal : t -> t -> bool **)
let rec equal s s' =
match s with
| Nil ->
(match s' with
| Nil -> True
| Cons (_, _) -> False)
| Cons (x, l) ->
(match s' with
| Nil -> False
| Cons (x', l') ->
(match X.compare x x' with
| Eq -> equal l l'
| _ -> False))
(** val subset : X.t list -> X.t list -> bool **)
let rec subset s s' =
match s with
| Nil -> True
| Cons (x, l) ->