Extensible records - #1

Open

ebresafegaga wants to merge 61 commits into

mainfrom

gaga/extensible-records

Commits on Jul 22, 2025

parse `FRecord` keyword
ebresafegaga
committed
8770ce5

Commits on Jul 24, 2025

Step 1: Parsing
ebresafegaga
committed
e6d61eb
Connect everything to fix build
ebresafegaga
committed
f3344d6
Stage 2: add the linkage element
ebresafegaga
committed
7c17bbd
first stab at an implementation of `add_record`
ebresafegaga
committed
44131b8
update tests
ebresafegaga
committed
cc1c227
Add a sketch of the compilation strategy
ebresafegaga
committed
e98d7fb
sketch of systemf prime case study
ebresafegaga
committed
5931173
Add FDefault
ebresafegaga
committed
352f779
Add marker
ebresafegaga
committed
adf5886
WIP
ebresafegaga
committed
3736565
WIP
ebresafegaga
committed
87f16ac

Commits on Jul 25, 2025

more compiler code
ebresafegaga
committed
bcf2d3f

Commits on Jul 27, 2025

Record constructor
ebresafegaga
committed
f885935
Resolve the types properly
ebresafegaga
committed
76456b2
eliminators for records
ebresafegaga
committed
963c7b7
Implementation of records
ebresafegaga
committed
de6e288
Compiling the constructor implementation
ebresafegaga
committed
9850638
linkage concatenation and provenance
ebresafegaga
committed
7a12b2b

Commits on Jul 28, 2025

Definition mapping
ebresafegaga
committed
8358cb7
syntax for default values
ebresafegaga
committed
34658dd
Ask a question about default values and use the syntax
ebresafegaga
committed
674d67a

Commits on Jul 29, 2025

parsing defaults
ebresafegaga
committed
24c3457
naive vernac inductive linkage concatenation to include records
ebresafegaga
committed
95eb6aa
WIP: step 1 and 2 of extend record
ebresafegaga
committed
0a51778
fix parsing
ebresafegaga
committed
05b4113
fun comment
ebresafegaga
committed
696cc49
fill in the implementation of extend_record
ebresafegaga
committed
52259e7
Compose things nicely
ebresafegaga
committed
a5b87bb
Inherit dependencies
ebresafegaga
committed
9f228d1
Implement inheritance
ebresafegaga
committed
800b8bc
WIP
ebresafegaga
committed
88a8dce

Commits on Jul 30, 2025

First take at resolving record literal
ebresafegaga
committed
1e50175
resolve arbitrarily deeply nested record literals
ebresafegaga
committed
f4dccbf
Add some examples and ideas
ebresafegaga
committed
95fbebd
Add TODOs
ebresafegaga
committed
e441500
WIP
ebresafegaga
committed
7abf2be

Commits on Jul 31, 2025

Resolution for record projection
ebresafegaga
committed
86a3243
fresh names for record constructors
ebresafegaga
committed
addbeca
proper prefixing
ebresafegaga
committed
d840fbb
Do actual deep resolution
ebresafegaga
committed
d4c0d99
comment about the definition mapping for records
ebresafegaga
committed
6308da3

Commits on Aug 5, 2025

Add RecordComputationalAxiom
ebresafegaga
committed
bb5b3ff

Commits on Aug 6, 2025

Add construct_one_field_comp_axiom
ebresafegaga
committed
cb40d37
Actually use the RecordCompAxiom
ebresafegaga
committed
1ad4569
impl record comp behaviour just like regular comp behaviour
ebresafegaga
committed
e9f5ff1
Use comp behaviour to prove a simple theorem
ebresafegaga
committed
a4babdf
WIP
ebresafegaga
committed
4634cb7
WIP 2
ebresafegaga
committed
433e9af

Commits on Aug 7, 2025

Commits on Aug 8, 2025

Implement for fsimpl in */ fsimpl in H
ebresafegaga
committed
71ea483
Update test file
ebresafegaga
committed
f9145b4

Commits on Aug 10, 2025

use reachable fields to resolve record constructor
ebresafegaga
committed
c44b43a
Synthesize contexts correctly for RecordConstrAxioms
ebresafegaga
committed
731f4f5
Update tests
ebresafegaga
committed
6e0b402

Commits on Aug 11, 2025

Add a more complex test
ebresafegaga
committed
8416484
More tests
ebresafegaga
committed
061c01b
Use the pinned context API
ebresafegaga
committed
f5980b8