Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Issue 130 #133

Open
wants to merge 37 commits into
base: master
Choose a base branch
from
Open

Issue 130 #133

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
a7cc051
Issue 130: Drafted the Fin type in StdLib/Fin.v and replaced all used…
llee454 Apr 29, 2020
954b064
Issue 130: Added additional lemmas to StdLib Fin.
llee454 Apr 30, 2020
34184a3
Issue 130: proved additional lemmas.
llee454 Apr 30, 2020
a2f5b26
Issue 130: Added additional lemmas.
llee454 Apr 30, 2020
feabe29
Issue 130: Added additional lemma.
llee454 Apr 30, 2020
1a8d4c4
Issue 130: [UNSTABLE] ported over a proof from EclecticLib and modifi…
llee454 Apr 30, 2020
0ba485f
Issue 130: Ported over all definitions and lemmas in Eclectic lib exc…
llee454 Apr 30, 2020
2648304
Still working on Vector.v, snocList QED'd.
tjmach Apr 30, 2020
30acb94
Finalized Vector, some things required L_R, and were ignored.
tjmach May 1, 2020
5cb575b
Issue 130: started porting over Syntax.v to use the new Fin definitions.
llee454 May 1, 2020
ea7d569
Merge branch 'issue-130' of https://github.com/sifive/Kami into issue…
llee454 May 1, 2020
5315a4a
Issue 130: finished another lemma in Syntax.v (1).
llee454 May 1, 2020
0490661
Issue 130: finished another lemma in Syntax.v (1).
llee454 May 1, 2020
2d6eeb0
Issue 130: ported Kind_decb_refl.
llee454 May 1, 2020
05dc34f
Merge branch 'issue-130' of https://github.com/sifive/Kami into issue…
tjmach May 1, 2020
47dd942
Issue 130: ported Kind_decb_eq.
llee454 May 1, 2020
2009fac
Issue 130: finished porting Syntax.v
llee454 May 1, 2020
dd1d0d6
Issue 130: Ported Properties.v
llee454 May 1, 2020
9c12271
Issue 130: Ported LibStruct.v
llee454 May 1, 2020
0b953a0
Issue 130: Ported Tactics and list_to_array_id in Utila.
llee454 May 1, 2020
ea2f1eb
Issue 130: Ported Compiler.v
llee454 May 1, 2020
4ba1511
Issue 130: Ported Extraction.
llee454 May 1, 2020
3fc5489
Isomorphisms between our Fin/Vec and the Coq Fin/Vec.
tjmach May 1, 2020
991e174
Merge branch 'issue-130' of https://github.com/sifive/Kami into issue…
tjmach May 1, 2020
9789a58
Issue 130: Ported CompilerProps.
llee454 May 1, 2020
33b5e56
Merge branch 'issue-130' of https://github.com/sifive/Kami into issue…
llee454 May 1, 2020
060dd8b
Issue 130: Ported CompilerSimpleSem.v.
llee454 May 1, 2020
7c196d1
Revied the Fin map2 function so that it will reduce more completely.
llee454 May 3, 2020
b6234bd
Issue 130: Made Fin.eq_dec transparent so that it can reduce.
llee454 May 3, 2020
e02e8da
Issue 130: Removed duplicate definitions from CoqSim. Marked an argum…
llee454 May 3, 2020
550309e
Issue 130: ported Kind_dec_eq2 from CoqSim.
llee454 May 3, 2020
f8e8085
Ported HaskellTypes.
llee454 May 3, 2020
d9a9d73
Issue 130: ported Simulator/CoqSim/Eval.v.
llee454 May 4, 2020
d32df96
Issue 130: Finished porting RegisterFile.
llee454 May 4, 2020
bc7d184
Issue 130: Revised fin_dep_destruct to work with the new definition o…
llee454 May 21, 2020
f1d07d1
Removed Fin Haskell constants from Extraction.v. Updated the proofs i…
Jun 9, 2020
1218f82
Fixed the Verilog generator (CompAction and PrettyPrintVerilog.hs) so…
Jun 11, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Compiler/CompAction.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ deriving instance Show T.BitFormat
deriving instance Show T.RegFileReaders
deriving instance Show T.RegFileBase

show_finfun :: Show a => Int -> (CustomExtract.EFin -> a) -> String
show_finfun :: Show a => Int -> (T.Fin -> a) -> String
show_finfun n f = "{ " ++ intercalate " ; " (map (show . f) $ T.getFins n) ++ " }"

instance Show T.FullFormat where
Expand Down Expand Up @@ -66,10 +66,10 @@ instance Show (T.Expr ty) where
show (T.BinBitBool n m o e1 e2) = "BinBitBool " ++ show n ++ " " ++ show m ++ " " ++ show o ++ " " ++ show e1 ++ " " ++ show e2
show (T.ITE fk e1 e2 e3) = "ITE " ++ show fk ++ " " ++ show e1 ++ " " ++ show e2 ++ " " ++ show e3
show (T.Eq k e1 e2) = "Eq " ++ show k ++ " " ++ show e1 ++ " " ++ show e2
show (T.ReadStruct n fk fs e i) = "ReadStruct " ++ show n ++ " " ++ show_finfun n fk ++ " " ++ show_finfun n fs ++ " " ++ show e ++ " " ++ show i
show (T.ReadStruct n fk fs e i) = "ReadStruct " ++ show n ++ " " ++ show_finfun n fk ++ " " ++ show_finfun n fs ++ " " ++ show e ++ " " ++ show (T.to_nat n i)
show (T.BuildStruct n fk fs fe) = "BuildStruct " ++ show n ++ " " ++ show_finfun n fk ++ " " ++ show_finfun n fs ++ " " ++ show_finfun n fe
show (T.ReadArray n m k e1 e2) = "ReadArray " ++ show n ++ " " ++ show m ++ " " ++ show e1 ++ " " ++ show e2
show (T.ReadArrayConst n k e i) = "ReadArrayConst " ++ show n ++ " " ++ show k ++ " " ++ show e ++ " " ++ show i
show (T.ReadArrayConst n k e i) = "ReadArrayConst " ++ show n ++ " " ++ show k ++ " " ++ show e ++ " " ++ show (T.to_nat n i)
show (T.BuildArray n k f) = "BuildArray " ++ show n ++ " " ++ show k ++ " " ++ show_finfun n f

deriving instance Show T.SyncRead
Expand Down
15 changes: 8 additions & 7 deletions Compiler/Compiler.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
Require Import Kami.StateMonad Kami.Syntax Kami.Properties Kami.PProperties Kami.PPlusProperties Kami.Notations Kami.Lib.EclecticLib.
Require Import Kami.StdLib.Fin.
Import Word.Notations.

Require Import ZArith.
Expand Down Expand Up @@ -277,7 +278,7 @@ Section Compile.
Proof.
split; intros.
- unfold SyncRead_eqb in H.
repeat (apply andb_prop in H; dest; rewrite String.eqb_eq in *).
repeat (apply andb_prop in H; dest; rewrite String.eqb_eq in * ).
destruct r, r'; simpl in *; subst; auto.
- rewrite H.
unfold SyncRead_eqb; repeat rewrite eqb_refl; auto.
Expand Down Expand Up @@ -595,7 +596,7 @@ Section Semantics.
(HIn : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regVal)) updatedRegs)
cont calls val contArray
(HContArray : contArray =
BuildArray (fun i : Fin.t num =>
BuildArray (fun i : Fin num =>
ReadArray
(Var type _ regVal)
(CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
Expand Down Expand Up @@ -663,7 +664,7 @@ Section Semantics.
(HRegVal : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regV)) updatedRegs)
(HWriteMap : WfRegMapExpr
(UpdRegMap readRegName pred
(BuildArray (fun i : Fin.t num =>
(BuildArray (fun i : Fin num =>
ReadArray
(Var type _ regV)
(CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
Expand All @@ -682,7 +683,7 @@ Section Semantics.
(HRegVal2 : In (dataArray, existT _ (SyntaxKind (Array idxNum Data)) regVal) updatedRegs)
(contArray : Expr type (SyntaxKind (Array num Data)))
(HContArray : contArray =
BuildArray (fun i : Fin.t num =>
BuildArray (fun i : Fin num =>
ReadArray
(Var type _ regVal)
(CABit Add (Var type (SyntaxKind _) idx ::
Expand Down Expand Up @@ -816,7 +817,7 @@ Section EActionT_Semantics.
(cont : type (Array num Data) -> EActionT type retK)
(contArray : Expr type (SyntaxKind (Array num Data)))
(HContArray : contArray =
BuildArray (fun i : Fin.t num =>
BuildArray (fun i : Fin num =>
ReadArray
(Var type _ regV)
(CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
Expand Down Expand Up @@ -878,7 +879,7 @@ Section EActionT_Semantics.
(HANewUml : anewUml =
(UmUpd (readRegName, existT _ _
(evalExpr
(BuildArray (fun i : Fin.t num =>
(BuildArray (fun i : Fin num =>
ReadArray
(Var type _ regV)
(CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
Expand All @@ -893,7 +894,7 @@ Section EActionT_Semantics.
(HRegVal2 : In (dataArray, existT _ (SyntaxKind (Array idxNum Data)) regVal) o)
(contArray : Expr type (SyntaxKind (Array num Data)))
(HContArray : contArray =
BuildArray (fun i : Fin.t num =>
BuildArray (fun i : Fin num =>
ReadArray
(Var type _ regVal)
(CABit Add (Var type (SyntaxKind _) idx ::
Expand Down
Loading