Code

Issue 130#133

Code

Open

vmurali wants to merge 37 commits intosifive:mastersifive/Kami:masterfrom llee454:issue-130llee454/Kami:issue-130Copy head branch name to clipboard

+1,564-681

Commits

Commits on Apr 29, 2020

• Issue 130: Drafted the Fin type in StdLib/Fin.v and replaced all used functions in the Coq Standard Library Fin.

  llee454

  committed
  a7cc051

  Copy full SHA for a7cc051

Commits on Apr 30, 2020

• Issue 130: Added additional lemmas to StdLib Fin.

  llee454

  committed
  954b064

  Copy full SHA for 954b064

• Issue 130: proved additional lemmas.

  llee454

  committed
  34184a3

  Copy full SHA for 34184a3

• Issue 130: Added additional lemmas.

  llee454

  committed
  a2f5b26

  Copy full SHA for a2f5b26

• Issue 130: Added additional lemma.

  llee454

  committed
  feabe29

  Copy full SHA for feabe29

• Issue 130: [UNSTABLE] ported over a proof from EclecticLib and modified EclecticLib so that it imports the new Fin.

  llee454

  committed
  1a8d4c4

  Copy full SHA for 1a8d4c4

• Issue 130: Ported over all definitions and lemmas in Eclectic lib except listSnoc.

  llee454

  committed
  0ba485f

  Copy full SHA for 0ba485f

• Still working on Vector.v, snocList QED'd.

  tjmach

  committed
  2648304

  Copy full SHA for 2648304

Commits on May 1, 2020

• Finalized Vector, some things required L_R, and were ignored.

  tjmach

  committed
  30acb94

  Copy full SHA for 30acb94

• Issue 130: started porting over Syntax.v to use the new Fin definitions.

  llee454

  committed
  5cb575b

  Copy full SHA for 5cb575b

• Merge branch 'issue-130' of https://github.com/sifive/Kami into issue-130

  llee454

  committed
  ea7d569

  Copy full SHA for ea7d569

• Issue 130: finished another lemma in Syntax.v (1).

  llee454

  committed
  5315a4a

  Copy full SHA for 5315a4a

• Issue 130: finished another lemma in Syntax.v (1).

  llee454

  committed
  0490661

  Copy full SHA for 0490661

• Issue 130: ported Kind_decb_refl.

  llee454

  committed
  2d6eeb0

  Copy full SHA for 2d6eeb0

• Merge branch 'issue-130' of https://github.com/sifive/Kami into issue-130

  tjmach

  committed
  05dc34f

  Copy full SHA for 05dc34f

• Issue 130: ported Kind_decb_eq.

  llee454

  committed
  47dd942

  Copy full SHA for 47dd942

• Issue 130: finished porting Syntax.v

  llee454

  committed
  2009fac

  Copy full SHA for 2009fac

• Issue 130: Ported Properties.v

  llee454

  committed
  dd1d0d6

  Copy full SHA for dd1d0d6

• Issue 130: Ported LibStruct.v

  llee454

  committed
  9c12271

  Copy full SHA for 9c12271

• Issue 130: Ported Tactics and list_to_array_id in Utila.

  llee454

  committed
  0b953a0

  Copy full SHA for 0b953a0

• Issue 130: Ported Compiler.v

  llee454

  committed
  ea2f1eb

  Copy full SHA for ea2f1eb

• Issue 130: Ported Extraction.

  llee454

  committed
  4ba1511

  Copy full SHA for 4ba1511

• Isomorphisms between our Fin/Vec and the Coq Fin/Vec.

  tjmach

  committed
  3fc5489

  Copy full SHA for 3fc5489

• Merge branch 'issue-130' of https://github.com/sifive/Kami into issue-130

  tjmach

  committed
  991e174

  Copy full SHA for 991e174

• Issue 130: Ported CompilerProps.

  llee454

  committed
  9789a58

  Copy full SHA for 9789a58

• Merge branch 'issue-130' of https://github.com/sifive/Kami into issue-130

  llee454

  committed
  33b5e56

  Copy full SHA for 33b5e56

• Issue 130: Ported CompilerSimpleSem.v.

  llee454

  committed
  060dd8b

  Copy full SHA for 060dd8b

Commits on May 3, 2020

• Revied the Fin map2 function so that it will reduce more completely.

  llee454

  committed
  7c196d1

  Copy full SHA for 7c196d1

• Issue 130: Made Fin.eq_dec transparent so that it can reduce.

  llee454

  committed
  b6234bd

  Copy full SHA for b6234bd

• Issue 130: Removed duplicate definitions from CoqSim. Marked an argument implicit in a function in Fin.v.

  llee454

  committed
  e02e8da

  Copy full SHA for e02e8da

• Issue 130: ported Kind_dec_eq2 from CoqSim.

  llee454

  committed
  550309e

  Copy full SHA for 550309e

• Ported HaskellTypes.

  llee454

  committed
  f8e8085

  Copy full SHA for f8e8085

Commits on May 4, 2020

• Issue 130: ported Simulator/CoqSim/Eval.v.

  llee454

  committed
  d9a9d73

  Copy full SHA for d9a9d73

• Issue 130: Finished porting RegisterFile.

  llee454

  committed
  d32df96

  Copy full SHA for d32df96

Commits on May 21, 2020

• Issue 130: Revised fin_dep_destruct to work with the new definition of Fin.

  llee454

  committed
  bc7d184

  Copy full SHA for bc7d184

Commits on Jun 9, 2020

• Removed Fin Haskell constants from Extraction.v. Updated the proofs in VectorFacts.v and removed the Vector_find function whose semantics seemed unnatural. Kept Vector_find_opt. Updated Simulator/C…

  Show description for f1d07d1
  

  Ubuntu

  committed
  f1d07d1

  Copy full SHA for f1d07d1

Commits on Jun 11, 2020

• Fixed the Verilog generator (CompAction and PrettyPrintVerilog.hs) so that they works with the new Fin definition.

  

  Ubuntu

  committed
  1218f82

  Copy full SHA for 1218f82