diff options
| -rw-r--r-- | src/translation/HTLgen.v | 5 | ||||
| -rw-r--r-- | src/verilog/Value.v | 9 |
2 files changed, 5 insertions, 9 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index dc82fb1..e637d6f 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -572,8 +572,7 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true. -(* +Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => @@ -582,7 +581,7 @@ Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true. | _ => false end | _ => false - end. *) + end. Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p diff --git a/src/verilog/Value.v b/src/verilog/Value.v index becc44c..52a87e3 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -372,7 +372,7 @@ Lemma boolToValue_ValueToBool : valueToBool (boolToValue 32 b) = b. Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. -Lemma ZToValue_valueToNat : +(*Lemma ZToValue_valueToNat : forall x sz, sz > 0 -> (x < 2^(Z.of_nat sz))%Z -> @@ -384,8 +384,5 @@ Proof. unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) - Search Pos.to_nat. - (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *) - Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n). - econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat. -Admitted. + Search "inj" positive nat. +*) |