Commit eaee6284 authored by Heiko Becker's avatar Heiko Becker

Fix Coq types to make extraction work again...

parent a473371d
......@@ -57,8 +57,8 @@ Proof.
destruct e5.
+ apply Ndec.Pcompare_Peqb in e8.
congruence.
+ apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl in H; congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in H; congruence.
Qed.
Lemma usedVars_toREval_toRExp_compat e:
......@@ -104,8 +104,8 @@ Proof.
destruct e3.
+ apply Ndec.Pcompare_Peqb in e6.
congruence.
+ apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl in H; congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in H; congruence.
- intros valid1; destruct valid1 as [validsub1 validr1].
specialize (IHc Heq validsub1).
split; auto.
......@@ -229,8 +229,8 @@ Proof.
destruct e5.
+ apply Ndec.Pcompare_Peqb in e8.
congruence.
+ apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl in *; congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in *; congruence.
Qed.
Definition updateExpMapIncr e new_af noise (emap: expressionsAffine) intv incr :=
......@@ -2146,7 +2146,7 @@ Proof.
* rewrite FloverMapFacts.P.F.add_neq_o in Hsome; auto.
apply checked_expressions_flover_map_add_compat; auto.
apply visitedSubexpr; eauto.
Unshelve. all:exact 0%nat.
Unshelve. all:exact 0%N.
Qed.
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
......
......@@ -13,7 +13,7 @@ Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t nat):=
(P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t N):=
let tMap := (typeMap defVars e (FloverMap.empty mType) fBits) in
if (typeCheck e defVars tMap fBits)
then
......
......@@ -49,7 +49,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> (expr R -> option nat) -> R -> mType -> Prop :=
Inductive bstep : cmd R -> env -> (nat -> option mType) -> (expr R -> option N) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars fBits:
eval_expr E defVars fBits e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) fBits res m' ->
......
......@@ -167,7 +167,7 @@ Open Scope R_scope.
Inductive eval_expr (E:env)
(Gamma: nat -> option mType)
(fBits:expr R -> option nat)
(fBits:expr R -> option N)
:(expr R) -> R -> mType -> Prop :=
| Var_load m x v:
Gamma x = Some m ->
......
......@@ -23,13 +23,13 @@ Proof.
now apply Qeq_eqR.
- apply Ndec.Pcompare_Peqb in e6.
apply Pos.eqb_eq in e6; subst.
apply Nat.compare_eq in Heq; subst; auto.
apply N.compare_eq in Heq; subst; auto.
- simpl in e3.
apply andb_false_iff in e3.
apply Ndec.Pcompare_Peqb in e6.
apply Pos.eqb_eq in e6; subst.
apply Nat.compare_eq in Heq; subst; auto.
rewrite Nat.eqb_refl, Pos.eqb_refl in e3.
apply N.compare_eq in Heq; subst; auto.
rewrite N.eqb_refl, Pos.eqb_refl in e3.
destruct e3; congruence.
- unfold unopEq in e5.
destruct u1, u2; congruence.
......@@ -37,14 +37,14 @@ Proof.
apply andb_false_iff in e5.
apply Ndec.Pcompare_Peqb in e8.
rewrite Pos.eqb_eq in e8; subst.
apply Nat.compare_eq in Heq; subst.
apply N.compare_eq in Heq; subst.
destruct e5; congruence.
- simpl in e5.
apply andb_false_iff in e5.
apply Ndec.Pcompare_Peqb in e8.
rewrite Pos.eqb_eq in e8.
apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl, Pos.eqb_refl in *.
apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl, Pos.eqb_refl in *.
destruct e5; congruence.
Qed.
......@@ -132,8 +132,8 @@ Proof.
auto.
Qed.
Definition toRBMap (bMap:FloverMap.t nat) : expr R -> option nat :=
let elements := FloverMap.elements (elt:=nat) bMap in
Definition toRBMap (bMap:FloverMap.t N) : expr R -> option N :=
let elements := FloverMap.elements (elt:=N) bMap in
fun (e:expr R) =>
olet p := find (fun p => match R_orderedExps.compare e (toRExp (fst p)) with
| Eq => true |_ => false end) elements in
......@@ -176,11 +176,11 @@ Proof.
apply findA_find in find_Q as [key [find_Q k_eq]].
unfold FloverMapFacts.P.F.eqb in k_eq.
cut (find
(fun p : expr Q * nat =>
(fun p : expr Q * N =>
match R_orderedExps.compare (toRExp e) (toRExp (fst p)) with
| Eq => true
| _ => false
end) (FloverMap.elements (elt:=nat) bMap) = Some (key, b)).
end) (FloverMap.elements (elt:=N) bMap) = Some (key, b)).
- intros find_R. rewrite find_R. auto.
- eapply find_swap with (f1 := fun p => match Q_orderedExps.exprCompare e (fst p) with
|Eq => true |_ => false end).
......
......@@ -19,7 +19,7 @@ From Flover
the base field.
**)
Inductive mType: Type := REAL | M16 | M32 | M64
| F (w:positive) (f:nat). (*| M128 | M256*)
| F (w:positive) (f:N). (*| M128 | M256*)
Definition isFixedPoint m :Prop :=
match m with
......@@ -56,7 +56,7 @@ Definition mTypeToR (m:mType) :R :=
| M16 => 1 / 2^11
| M32 => 1/ 2^24
| M64 => 1/ 2^53
| F w f => 1/ 2^f
| F w f => 1/ 2^(N.to_nat f)
(*
(* the epsilons below match what is used internally in Daisy,
although these value do not match the IEEE standard *)
......@@ -70,7 +70,7 @@ Definition mTypeToQ (m:mType) :Q :=
| M16 => (Qpower (2#1) (Zneg 11))
| M32 => (Qpower (2#1) (Zneg 24))
| M64 => (Qpower (2#1) (Zneg 53))
| F w f => Qpower (2#1) (- Z.of_nat f)
| F w f => Qpower (2#1) (- Z.of_N f)
(*
(* the epsilons below match what is used internally in Daisy,
although these value do not match the IEEE standard *)
......@@ -103,13 +103,13 @@ Lemma mTypeToQ_mTypeToR m :
Q2R (mTypeToQ m) = mTypeToR m.
Proof.
destruct m; cbn; try auto using Q2R0_is_0; try (unfold Q2R; simpl; lra).
pose proof (Qpower_opp (2#1) (Z.of_nat f)) as Qpower_eq.
pose proof (Qpower_opp (2#1) (Z.of_N f)) as Qpower_eq.
apply Qeq_eqR in Qpower_eq.
rewrite Qpower_eq.
rewrite Q2R_inv.
- unfold Rdiv. rewrite Rmult_1_l.
f_equal.
destruct (Z.of_nat f) eqn:z_nat; try (destruct f; cbn in z_nat; congruence).
destruct (Z.of_N f) eqn:z_nat; try (destruct f; cbn in z_nat; congruence).
+ cbn. destruct f; simpl in *; try congruence.
lra.
+ unfold Qpower.
......@@ -117,7 +117,8 @@ Proof.
unfold Q2R; simpl.
rewrite Zpower_pos_powerRZ.
rewrite pow_powerRZ.
rewrite <- z_nat.
rewrite N_nat_Z.
rewrite z_nat.
assert (IZR (Z.pos (1 ^ p)) = 1%R) as pow_1.
{ unfold IZR.
f_equal.
......@@ -128,7 +129,7 @@ Proof.
destruct f; simpl in *; try lra.
rewrite Qpower_decomp in *.
unfold Qeq in *; simpl in *.
pose proof (Zpow_facts.Zpower_pos_pos 2 (Pos.of_succ_nat f)) as Zpower_pos.
pose proof (Zpow_facts.Zpower_pos_pos 2 p) as Zpower_pos.
assert (0 <2)%Z as pos2 by (omega).
specialize (Zpower_pos pos2).
rewrite Z.mul_1_r in *.
......@@ -199,7 +200,7 @@ Definition mTypeEq (m1:mType) (m2:mType) :=
| M16, M16 => true
| M32, M32 => true
| M64, M64 => true
| F w1 f1, F w2 f2 => (w1 =? w2)%positive && (f1 =? f2)%nat
| F w1 f1, F w2 f2 => (w1 =? w2)%positive && (f1 =? f2)%N
(* | M128, M128 => true *)
(* | M256, M256 => true *)
| _, _ => false
......@@ -209,7 +210,7 @@ Lemma mTypeEq_refl (m:mType):
mTypeEq m m = true.
Proof.
intros. destruct m; try auto; simpl.
rewrite Pos.eqb_refl, Nat.eqb_refl; auto.
rewrite Pos.eqb_refl, N.eqb_refl; auto.
Qed.
Lemma mTypeEq_compat_eq(m1:mType) (m2:mType):
......@@ -221,7 +222,7 @@ Proof.
try congruence; try auto;
try simpl in eq_case; try inversion eq_case.
- andb_to_prop eq_case. f_equal; auto using Peqb_true_eq.
rewrite <- Nat.eqb_eq; auto.
rewrite <- N.eqb_eq; auto.
- inversion m2_case. apply mTypeEq_refl.
Qed.
......@@ -233,8 +234,8 @@ Proof.
congruence.
- case_eq m1; intros; case_eq m2; intros; subst; simpl; try congruence.
destruct (w =? w0)%positive eqn:?; try auto.
destruct (f =? f0)%nat eqn:?; try auto.
rewrite Pos.eqb_eq, Nat.eqb_eq in *; subst. congruence.
destruct (f =? f0)%N eqn:?; try auto.
rewrite Pos.eqb_eq, N.eqb_eq in *; subst. congruence.
Qed.
Ltac type_conv :=
......@@ -250,7 +251,7 @@ Proof.
intros.
destruct m1, m2; simpl; auto.
rewrite Pos.eqb_sym; f_equal.
apply Nat.eqb_sym.
apply N.eqb_sym.
Qed.
(**
......@@ -336,7 +337,7 @@ Qed.
in which evaluation has to be performed, e.g. addition of 32 and 64 bit floats
has to happen in 64 bits
**)
Definition join (m1:mType) (m2:mType) (fracBits:nat) :option mType:=
Definition join (m1:mType) (m2:mType) (fracBits:N) :option mType:=
match m1, m2 with
| F w1 f1, F w2 f2 =>
if (w2 <=? w1)%positive
......@@ -347,7 +348,7 @@ Definition join (m1:mType) (m2:mType) (fracBits:nat) :option mType:=
| _ , _ => if (morePrecise m1 m2) then Some m1 else Some m2
end.
Definition join3 (m1:mType) (m2:mType) (m3:mType) (fBits:nat):=
Definition join3 (m1:mType) (m2:mType) (m3:mType) (fBits:N):=
olet msub := (join m2 m3 fBits) in
join m1 msub fBits.
......@@ -383,7 +384,7 @@ Qed.
(* destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. *)
(* Qed. *)
Definition maxExponent (m:mType) :nat :=
Definition maxExponent (m:mType) :N :=
match m with
| REAL => 1
| M16 => 15
......@@ -392,7 +393,7 @@ Definition maxExponent (m:mType) :nat :=
| F w f => f
end.
Definition minExponentPos (m:mType) :nat :=
Definition minExponentPos (m:mType) :N :=
match m with
| REAL => 1
| M16 => 14
......@@ -413,15 +414,15 @@ Fixed-Points:
**)
Definition maxValue (m:mType) :=
match m with
|F w f => (((Z.pow_pos 2 (w -1))-1)#1) * Qinv ((Z.pow 2 (Z.of_nat (maxExponent m)))#1)
|_ => (Z.pow 2 (Z.of_nat (maxExponent m))) # 1
|F w f => (((Z.pow_pos 2 (w -1))-1)#1) * Qinv ((Z.pow 2 (Z.of_N (maxExponent m)))#1)
|_ => (Z.pow 2 (Z.of_N (maxExponent m))) # 1
end.
(* Similarly: minimum values: we return 0 for fixed-point numbers here to make no fixed-point number be a denormal number ever*)
Definition minValue_pos (m:mType) :=
match m with
|F w f => 0
| _ => Qinv ((Z.pow 2 (Z.of_nat (minExponentPos m))) # 1)
| _ => Qinv ((Z.pow 2 (Z.of_N (minExponentPos m))) # 1)
end.
(* (** Goldberg - Handbook of Floating-Point Arithmetic: (p.183) *)
......
......@@ -252,7 +252,7 @@ Proof.
inversion env1; inversion env2; subst.
destruct b; simpl in *.
* split;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%N); eauto; try congruence;
try rewrite Rabs_R0; cbn; lra|].
pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
......@@ -265,7 +265,7 @@ Proof.
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb. lra.
* split;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%N); eauto; try congruence;
try rewrite Rabs_R0; cbn; lra|].
pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
......@@ -279,7 +279,7 @@ Proof.
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb; lra.
* split;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%N); eauto; try congruence;
try rewrite Rabs_R0; cbn; lra|].
pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
......@@ -295,7 +295,7 @@ Proof.
canonize_hyps.
apply le_neq_bool_to_lt_prop in L.
split;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
[eapply Binop_dist' with (delta := 0%R) (fBit:=0%N); eauto; try congruence;
try rewrite Rabs_R0; cbn; try lra|].
(* No division by zero proof *)
{ hnf; intros.
......@@ -339,7 +339,7 @@ Proof.
exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
inversion env1; inversion env2; inversion env3; subst.
split; [auto | ].
* eapply Fma_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence; cbn;
* eapply Fma_dist' with (delta := 0%R) (fBit:=0%N); eauto; try congruence; cbn;
try rewrite Rabs_R0; lra.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
......
This diff is collapsed.
......@@ -43,7 +43,7 @@ From Flover
(* end. *)
Fixpoint typeMap (Gamma:nat -> option mType) (e:expr Q) (tMap:FloverMap.t mType)
(fBits:FloverMap.t nat)
(fBits:FloverMap.t N)
: FloverMap.t mType :=
if (FloverMap.mem e tMap)
then tMap
......@@ -148,7 +148,7 @@ Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) tMap fBits :=
end.
Fixpoint typeCheck (e:expr Q) (Gamma:nat -> option mType)
(tMap: FloverMap.t mType) (fBits:FloverMap.t nat) : bool :=
(tMap: FloverMap.t mType) (fBits:FloverMap.t N) : bool :=
match e with
| Var _ v =>
match FloverMap.find e tMap, Gamma v with
......@@ -278,7 +278,7 @@ Proof.
assert (fBit = n) by congruence.
subst; auto.
+ rewrite <- isFixedPoint_isFixedPointB_false in *.
rewrite join_float with (f2:=0%nat) in H9; try auto.
rewrite join_float with (f2:=0%N) in H9; try auto.
Flover_compute; type_conv; auto.
- destruct (FloverMap.find (elt:=mType) (Fma e1 e2 e3) exprTypes) eqn:?;
try congruence.
......@@ -317,7 +317,7 @@ Proof.
destruct m4_fixed as [? [? ?]]; subst.
destruct m1; cbn in *; congruence.
+ rewrite <- isFixedPoint_isFixedPointB_false in *.
rewrite join_float with (f2:=0%nat) in H9; try auto.
rewrite join_float with (f2:=0%N) in H9; try auto.
destruct (isFixedPointB m1) eqn:?; simpl in typechecks.
* destruct m1; simpl in *; try congruence.
assert (forall w f, join m2 m3 0 = Some (F w f) -> False).
......@@ -329,7 +329,7 @@ Proof.
* rewrite <- isFixedPoint_isFixedPointB_false in *; try auto.
Flover_compute; type_conv; auto.
rewrite <- Heqo0. rewrite <- H9.
setoid_rewrite join_float with (f2 := 0%nat) at 2; try auto; try congruence.
setoid_rewrite join_float with (f2 := 0%N) at 2; try auto; try congruence.
hnf; intros isFP.
destruct m2, m3; cbn in *; inversion Heqo1; subst; cbn in isFP; try congruence.
contradiction.
......@@ -354,7 +354,7 @@ Proof.
simpl in subexpr_ok; Flover_compute.
exists n; auto.
- rewrite <- isFixedPoint_isFixedPointB_false in *.
exists 0%nat.
exists 0%N.
intros; contradiction.
Qed.
......@@ -380,7 +380,7 @@ Proof.
- rewrite <- isFixedPoint_isFixedPointB_false in *.
simpl in *. Flover_compute.
type_conv. exists m0; rewrite <- Heqo0.
rewrite join_float with (f2:=0%nat); auto.
rewrite join_float with (f2:=0%N); auto.
Qed.
Lemma typingFixedPoint_fma_defined e1 e2 e3 m1 m2 m3 Gamma exprTypes fBits:
......@@ -427,7 +427,7 @@ Proof.
destruct m, m1; cbn in *; congruence. }
rewrite m1_fixed in *.
simpl in *; Flover_compute.
exists 0%nat.
exists 0%N.
intros; contradiction.
Qed.
......@@ -477,7 +477,7 @@ Proof.
simpl in *; Flover_compute.
unfold join3 in *.
exists m0. rewrite <- Heqo; unfold join3.
erewrite join_float with (f1:=fBit) (f2:=0%nat); eauto.
erewrite join_float with (f1:=fBit) (f2:=0%N); eauto.
destruct (join m2 m3 0) eqn:?; try auto.
assert (isFixedPointB m4 = false).
{ destruct m2, m3; cbn in *; inversion Heqo0; simpl; try congruence.
......
native:
ocamlc -c big.ml
ocamlc -c CoqChecker.ml
ocamlc -c CoqChecker.mli
ocamlc -c CoqChecker.ml
ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
all: native
......@@ -15,7 +15,7 @@ Inductive Token:Type :=
| DTYPE:mType -> Token
| DFIXED
| DVAR
| DCONST: nat -> Token
| DCONST: N -> Token
| DNEG
| DPLUS
| DSUB
......@@ -30,11 +30,11 @@ Open Scope string_scope.
Definition getChar (input:string):=
match input with
|String c s => c
| _ => ascii_of_nat 0
| _ => ascii_of_N 0
end.
Definition getConst (c:ascii) :=
((nat_of_ascii c) - 48)%nat.
((N_of_ascii c) - 48)%N.
Definition suffix (s:string) :=
match s with
......@@ -43,16 +43,16 @@ match s with
end.
Definition isDigit (c:ascii) :=
(48 <=? (nat_of_ascii c)) && (nat_of_ascii c <=? 57).
(48 <=? (N_of_ascii c))%N && (N_of_ascii c <=? 57)%N.
Definition isAlpha (c:ascii) :bool :=
(65 <=? nat_of_ascii c) && (nat_of_ascii c <=? 90) ||
(97 <=? nat_of_ascii c) && (nat_of_ascii c <=? 122).
(65 <=? N_of_ascii c)%N && (N_of_ascii c <=? 90)%N ||
(97 <=? N_of_ascii c)%N && (N_of_ascii c <=? 122)%N.
Definition isAlphaNum (c :ascii) :bool :=
isDigit c || isAlpha c.
Fixpoint lexConst (input:string) (akk:nat) :=
Fixpoint lexConst (input:string) (akk:N) :=
match input with
|String c input' =>
if (isDigit c)
......@@ -106,7 +106,7 @@ match fuel with
|DCONST 32 :: ts' => DTYPE M32 :: ts'
|DCONST 64 :: ts' => DTYPE M64 :: ts'
|DFIXED :: DCONST w :: DCONST f :: ts' =>
DTYPE (F (Pos.of_nat w) f) :: ts'
DTYPE (F ((N.succ_pos w)-1) f) :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => []
......@@ -137,11 +137,11 @@ Fixpoint str_join s1 s2 :=
| "" => s2
end.
Fixpoint str_of_num (n:nat) (m:nat):=
Fixpoint str_of_num (n:N) (m:nat):=
match m with
|S m' =>
if n <? 10 then String (ascii_of_nat (n + 48)) ""
else str_join (str_of_num (n/10) m') (String (ascii_of_nat ((n mod 10) + 48)) "")
if (n <? 10)%N then String (ascii_of_N (n + 48)%N) ""
else str_join (str_of_num (n/10) m') (String (ascii_of_N ((n mod 10) + 48)) "")
|_ => ""
end .
......@@ -160,7 +160,7 @@ Definition pp_token (token:Token) :=
| DABS => "ABS"
| DCOND => "?"
| DVAR => "Var"
| DCONST num => str_of_num num num
| DCONST num => str_of_num num (N.to_nat num)
| DGAMMA => "Gamma"
| DTYPE m => str_join "MTYPE " (type_to_string m)
| DFIXED => ""
......@@ -188,10 +188,10 @@ Fixpoint parseExp (tokList:list Token) (fuel:nat):option (expr Q * list Token) :
match tokList with
| DCONST n :: DFRAC :: DCONST m :: DTYPE t :: tokRest =>
match m with
| 0%nat => None
|S p => Some (Const t (Z.of_nat n # (Pos.of_nat p)), tokRest)
| 0%N => None
| Npos p => Some (Const t (Z.of_N n # p), tokRest)
end
| DVAR :: DCONST n :: tokRest => Some (Var Q n, tokRest)
| DVAR :: DCONST n :: tokRest => Some (Var Q (N.to_nat n), tokRest)
| DNEG :: tokRest =>
match (parseExp tokRest fuel') with
| Some (Const m c, tokRest) => Some (Const m (- c), tokRest)
......@@ -266,7 +266,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* Parse it *)
match (parseLet letBodyRest fuel') with
(* And construct a result from it *)
| Some (letCmd, arbRest) => Some (Let m n e letCmd, arbRest)
| Some (letCmd, arbRest) => Some (Let m (N.to_nat n) e letCmd, arbRest)
| _ => None
end
(* But if we have a return *)
......@@ -274,7 +274,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* parse only this *)
match (parseRet retBodyRest fuel) with
(* and construct the result *)
| Some (retCmd, arbRest) => Some (Let m n e retCmd, arbRest)
| Some (retCmd, arbRest) => Some (Let m (N.to_nat n) e retCmd, arbRest)
| _ => None
end
| _ => None (* fail if there is no continuation for the let *)
......@@ -290,13 +290,13 @@ Definition parseFrac (input:list Token) :option (Q * list Token) :=
match input with
| DNEG :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
match m with
|0%nat => None
|S p => Some ((- Z.of_nat n # Pos.of_nat p),tokRest)
|0%N => None
|Npos p => Some ((- Z.of_N n # p),tokRest)
end
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
match m with
|0%nat => None
|S p => Some ((Z.of_nat n # Pos.of_nat p),tokRest)
|0%N => None
|Npos p => Some ((Z.of_N n # p),tokRest)
end
| _ => None
end.
......@@ -329,8 +329,8 @@ Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list T
match parseIV fracRest with
| Some (iv, precondRest) =>
match parsePrecondRec precondRest fuel' with
| Some (P, tokRest) => Some (updPre n iv P, tokRest)
| None => Some (updPre n iv defaultPre, precondRest)
| Some (P, tokRest) => Some (updPre (N.to_nat n) iv P, tokRest)
| None => Some (updPre (N.to_nat n) iv defaultPre, precondRest)
end
| _ => None
end
......@@ -393,7 +393,7 @@ Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * lis
match input with
| DVAR :: DCONST n :: DTYPE m :: inputRest =>
match parseGammaRec inputRest with
| Some (Gamma, rest) => Some (updDefVars n m Gamma, rest)
| Some (Gamma, rest) => Some (updDefVars (N.to_nat n) m Gamma, rest)
| None => None
end
| _ => Some (defaultGamma, input)
......@@ -504,11 +504,11 @@ Fixpoint check_rec (input:list Token) (num_fun:nat) fuel:=
| S n' =>
match dParse input fuel with
| Some ((dCmd, P, A, Gamma), []) =>
if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty nat)
if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty N)
then "True\n"
else "False\n"
| Some ((dCmd, P, A, Gamma), residual) =>
if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty nat)
if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty N)
then check_rec residual n' fuel
else "False\n"
| None => "parse failure\n"
......@@ -524,7 +524,7 @@ Fixpoint str_length s :=
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
match n with
|S n' => CertificateCheckerCmd f A P Gamma (FloverMap.empty nat) && (check f P A Gamma n')
|S n' => CertificateCheckerCmd f A P Gamma (FloverMap.empty N) && (check f P A Gamma n')
|_ => true
end.
......@@ -549,6 +549,6 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
Definition runChecker (input:string) :=
let tokList := lex input (str_length input) in
match tokList with
| DCONST n :: DCONST m :: tokRest => check_all m n tokRest (List.length tokList * 100)
| DCONST n :: DCONST m :: tokRest => check_all (N.to_nat m) (N.to_nat n) tokRest (List.length tokList * 100)
| _ => "failure no num of functions"
end.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment