Skip to content

Latest commit

 

History

History
85 lines (73 loc) · 3.58 KB

TODO.org

File metadata and controls

85 lines (73 loc) · 3.58 KB

Notes 2019-10-10

TODO schedule meetings in Nov.

Notes 2019-10-03

The graph shows that PDecl + PTerm (+ friends) are the first AST TTDecl + Type + Term (+ friends) are the elaborated AST

RDeclInstructions finns i file 1 file 2

Patrik är borta 2019-10-25 till 2019-11-04.

Notes 2019-06-27

  • diskuterar halvtidsrapportens frågor
  • söker buggar i sts och ita (lovand ingångar funna)
  • Patrik kan bygga koden [yeah!] - lägg in i README hur man bygger “from git checkout”
  • Plan: skicka brev till NAD CC: patrik angående ny tidplan

++ skicka halvtidsrapport til Patrik senast 27:e juli ++ Patrik läser och kommenterar senast 1:a aug. ++ skicka till NAD 3:e Aug

Notes 2019-05-23

Priolista

Priortering: uttrycksspråket

hur kan lämpliga Idris-funktioner fylla på med exempelvis dolda arg.?

Here, I have some leads. It should be doable, but the problem can be how to connect the two representations to each other.

Structure build system.

Pull in Idris and Agda as submodules to track updates and patches. Create executables for printing parse trees and statistics.

statistikverktyg

This should be easy once I have all the sources in one repo. Ongoing

“Explicit” hidden arguments

hur kan man enkelt “komma runt” nedanstående begränsningar? Kan Agda ge hjälp?

Skriva på half-time report.

Planera half-time presentation.

Kolla om det är möjligt att få mer info från Idris, om argument osv. Genom att köra fler steg i compilation-pipeline

Kolla om det är möjligt att köra Agdas type-checker för att få info om var `ita` klarar och inte klarar.

Notes

IdrisLibs/SequentialDecisionProblems/CoreTheory.lidr

Senare: datatyper med parametrar och index – how frequent?

Senare: not even declared hidden arguments – how frequent?

IdrisLibs/SequentialDecisionProblems/examples/Example1.lidr (and friends)

Agda: id : {A : Set} -> A -> A id {A} x = x

Time plan

(from the planning report + later additions)

2019-04-18; WR; Planning report.

2019-04-26; A; Book supervision meetings

2019-04-29; TW; First runnable implementation of STLC.

2019-05-05; TW; First runnable Dependent types example. (without hidden arg.)

2019-05-10; CE; Industry and career advancement seminar

2019-06-01; TW; Decide verification method.

2019-05-19; WR; Incorporate planning report suggestions into half-time report

2019-06-10; WR; Half-time presentation.

2019-06-19; WR; Content complete draft of half-time report.

2019-06-22; WR; Final draft of half-time report to supervisor.

2019-06-30; WR; Half-time report done.

2019-10-??; TW; Implementation of Implicit arguments done.

2019-10-??; WR; Content complete draft of Background in Final report.

2019-10-22; TW; Final implementation version.

2019-10-29; TW; Final verification.

2019-10-29; WR; Content complete draft of Final report.

2019-10-??; CE; Opposition.

2019-10-??; CE; Writing seminar I

2019-10-??; CE; Writing seminar II

2019-10-06; WR; Complete draft of Final report to supervisor

2019-10-20; WR; Final report.

2019-10-??; CE; Presentation.

Time plan notation

From the planning report

  • TW = 6.1 Technical work
  • WR = 6.2 Writing
  • CE = 6.3 Compulsory events