Skip to content

Commit

Permalink
coq: Change the record and enum syntax for compatibility with 8.11
Browse files Browse the repository at this point in the history
  • Loading branch information
@cpitclaudel
cpitclaudel committed Jun 4, 2020
1 parent 1bbf1f5 commit f21917b
Show file tree
Hide file tree
Showing 8 changed files with 89 additions and 89 deletions.
16 changes: 8 additions & 8 deletions README.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -349,9 +349,9 @@ The main part of your program is rules. You have access to the following syntax
Call an external function (combinational IP)
``Ob~1~0~1~0``, ``|4`d10|``
Bitset constants (here, the number 10 on 4 bits)
``struct name {| field_n := val_n;… |}``
``struct name { field_n := val_n;… }``
Struct constants
``enum name {| member |}``
``enum name { member }``
Enum constants
``#val``
Lift a Coq value (for example a Coq definition)
Expand All @@ -364,13 +364,13 @@ For example, the following rule decreases the ``ttl`` field of an ICMP packet:
let hdr := unpack(struct_t ipv4_header, read0(input)) in
let valid := Ob~1 in
match get(hdr, protocol) with
| enum proto {| ICMP |} =>
| enum proto { ICMP } =>
let t := get(hdr, ttl) in
if t == |8`d0| then set valid := Ob~0
else set hdr := subst(hdr, ttl, t - |8`d1|)
return default: fail
end;
write0(output, pack(struct response {| valid := valid; value := hdr |}))
write0(output, pack(struct response { valid := valid; value := hdr }))
}}.
This rule fetches the next instruction in our RV32I core:
Expand All @@ -380,16 +380,16 @@ This rule fetches the next instruction in our RV32I core:
Definition fetch := {{
let pc := read1(pc) in
write1(pc, pc + |32`d4|);
toIMem.(MemReq.enq)(struct mem_req {|
toIMem.(MemReq.enq)(struct mem_req {
byte_en := |4`d0|; (* Load *)
addr := pc;
data := |32`d0|
|});
f2d.(fromFetch.enq)(struct fetch_bookkeeping {|
});
f2d.(fromFetch.enq)(struct fetch_bookkeeping {
pc := pc;
ppc := pc + |32`d4|;
epoch := read1(epoch)
|})
})
}}.
Rules are written in an untyped surface language; to typecheck a rule, use ``tc_action R Sigma rule_body``, or use ``tc_rules`` as shown below.
Expand Down
12 changes: 7 additions & 5 deletions coq/Parsing.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,16 +180,16 @@ Declare Custom Entry koika_structs_init.

Notation "f ':=' expr" := (cons (f,expr) nil) (in custom koika_structs_init at level 20, f custom koika_var at level 0, expr custom koika at level 88).
Notation "a ';' b" := (app a b) (in custom koika_structs_init at level 91, a custom koika_structs_init).
Notation "'struct' structtype '{|' fields '|}'" :=
Notation "'struct' structtype '{' fields '}'" :=
(USugar (UStructInit structtype fields)) (in custom koika, structtype constr at level 0, fields custom koika_structs_init at level 92).
Notation "'struct' structtype '{|' '|}'" :=
Notation "'struct' structtype '{' '}'" :=
(USugar (UStructInit structtype [])) (in custom koika, structtype constr at level 0).

Definition mem_req :=
{| struct_name := "mem_req";
struct_fields := cons ("type", bits_t 1) nil |}.

Notation "'enum' enum_type '{|' f '|}'" :=
Notation "'enum' enum_type '{' f '}'" :=
(USugar (UConstEnum enum_type f))
(in custom koika at level 1, enum_type constr at level 1, f custom koika_var at level 1).

Expand Down Expand Up @@ -278,7 +278,8 @@ Module Type Tests.

Definition test_30'' : uaction reg_t :=
{{
struct mem_req {| foo := upu[#(Bits.of_nat 3 0) :+ 2] ; bar := |32`d98| |}
struct mem_req { foo := upu[#(Bits.of_nat 3 0) :+ 2] ;
bar := |32`d98| }
}}.

Definition test_31'' : uaction reg_t :=
Expand All @@ -288,7 +289,8 @@ Module Type Tests.

Definition test_31' : uaction reg_t :=
{{
let a := struct mem_req {| foo := upu[#(Bits.of_nat 3 0) :+ 2] ; bar := |32`d98| |} in
let a := struct mem_req { foo := upu[#(Bits.of_nat 3 0) :+ 2] ;
bar := |32`d98| } in
unpack(struct_t mem_req, pack(a))
}}.
End Tests.
Expand Down
4 changes: 2 additions & 2 deletions coq/Std.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ Section Maybe.

Definition valid {reg_t fn} : UInternalFunction reg_t fn :=
{{ fun valid (x: tau) : struct_t Maybe =>
struct Maybe {| valid := Ob~1; data := x |} }}.
struct Maybe { valid := Ob~1; data := x } }}.

Definition invalid {reg_t fn} : UInternalFunction reg_t fn :=
{{ fun invalid () : struct_t Maybe =>
struct Maybe {| valid := Ob~0 |} }}.
struct Maybe { valid := Ob~0 } }}.
End Maybe.

Notation maybe tau := (struct_t (Maybe tau)).
Expand Down
6 changes: 3 additions & 3 deletions examples/datatypes.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,16 +70,16 @@ Definition _decr_icmp_ttl : uaction _ empty_ext_fn_t :=
let hdr := unpack(struct_t ipv4_header, read0(input)) in
let valid := Ob~1 in
match get(hdr, protocol) with
| enum proto {| ICMP |} =>
| enum proto { ICMP } =>
let t := get(hdr, ttl) in
if t == |8`d0| then
set valid := Ob~0
else
set hdr := subst(hdr, ttl, t - |8`d1|) (* ← same as [put(hdr, ttl, t - 1)] *)
return default: pass
end;
set hdr := subst(hdr, reserved, enum flag {| unset |}); (* reset the [reserved] field, just in case *)
write0(output, pack(struct response {| valid := valid; value := hdr |}))
set hdr := subst(hdr, reserved, enum flag { unset }); (* reset the [reserved] field, just in case *)
write0(output, pack(struct response { valid := valid; value := hdr }))
}}.

Definition _clear_checksum : uaction reg_t empty_ext_fn_t :=
Expand Down
102 changes: 50 additions & 52 deletions examples/rv/RVCore.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,7 @@ Section RV32Helpers.
{{
fun getFields (inst : bits_t 32) : struct_t inst_field =>
let res := struct inst_field
{|
opcode := inst[|5`d0| :+ 7];
{ opcode := inst[|5`d0| :+ 7];
funct3 := inst[|5`d12| :+ 3];
funct7 := inst[|5`d25| :+ 7];
funct5 := inst[|5`d27| :+ 5];
Expand All @@ -76,7 +75,7 @@ Section RV32Helpers.
++ inst[|5`d20|]
++ inst[|5`d21|:+10]
++ |1`d0|);
csr := (inst[|5`d20| :+ 12]) |} in
csr := (inst[|5`d20| :+ 12]) } in
res
}}.

Expand Down Expand Up @@ -169,14 +168,14 @@ Section RV32Helpers.
{{
fun getImmediateType (inst : bits_t 32) : maybe (enum_t imm_type) =>
match (inst[|5`d2|:+5]) with
| #opcode_LOAD[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmI |})
| #opcode_OP_IMM[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmI |})
| #opcode_JALR[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmI |})
| #opcode_AUIPC[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmU |})
| #opcode_LUI[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmU |})
| #opcode_STORE[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmS |})
| #opcode_BRANCH[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmB |})
| #opcode_JAL[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type {| ImmJ |})
| #opcode_LOAD[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmI })
| #opcode_OP_IMM[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmI })
| #opcode_JALR[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmI })
| #opcode_AUIPC[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmU })
| #opcode_LUI[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmU })
| #opcode_STORE[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmS })
| #opcode_BRANCH[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmB })
| #opcode_JAL[|3`d2|:+5] => {valid (enum_t imm_type)}(enum imm_type { ImmJ })
return default: {invalid (enum_t imm_type)}()
end
}}.
Expand Down Expand Up @@ -226,14 +225,14 @@ Section RV32Helpers.
Definition decode_fun : UInternalFunction reg_t empty_ext_fn_t :=
{{ fun decode_fun (arg_inst : bits_t 32) : struct_t decoded_sig
=>
struct decoded_sig {|
struct decoded_sig {
valid_rs1 := usesRS1 (arg_inst);
valid_rs2 := usesRS2 (arg_inst);
valid_rd := usesRD (arg_inst);
legal := isLegalInstruction (arg_inst);
inst := arg_inst;
immediateType := getImmediateType(arg_inst)
|}
}
}}.

Definition getImmediate : UInternalFunction reg_t empty_ext_fn_t :=
Expand All @@ -243,11 +242,11 @@ Section RV32Helpers.
if (get(imm_type_v, valid) == Ob~1) then
let fields := getFields (get(dInst,inst)) in
match (get(imm_type_v, data)) with
| (enum imm_type {| ImmI |}) => get(fields, immI)
| (enum imm_type {| ImmS |}) => get(fields, immS)
| (enum imm_type {| ImmB |}) => get(fields, immB)
| (enum imm_type {| ImmU |}) => get(fields, immU)
| (enum imm_type {| ImmJ |}) => get(fields, immJ)
| (enum imm_type { ImmI }) => get(fields, immI)
| (enum imm_type { ImmS }) => get(fields, immS)
| (enum imm_type { ImmB }) => get(fields, immB)
| (enum imm_type { ImmU }) => get(fields, immU)
| (enum imm_type { ImmJ }) => get(fields, immJ)
return default: |32`d0|
end
else
Expand Down Expand Up @@ -355,8 +354,8 @@ Section RV32Helpers.
set nextPC := (pc + imm_val)
else
set nextPC := incPC);
struct control_result {| taken := taken;
nextPC := nextPC |}
struct control_result { taken := taken;
nextPC := nextPC }
}}.
End RV32Helpers.

Expand Down Expand Up @@ -544,15 +543,15 @@ Module RV32Core (RVP: RVParams) (Multiplier: MultiplierInterface).
Definition fetch : uaction reg_t ext_fn_t :=
{{
let pc := read1(pc) in
let req := struct mem_req {|
let req := struct mem_req {
byte_en := |4`d0|; (* Load *)
addr := pc;
data := |32`d0| |} in
let fetch_bookkeeping := struct fetch_bookkeeping {|
data := |32`d0| } in
let fetch_bookkeeping := struct fetch_bookkeeping {
pc := pc;
ppc := pc + |32`d4|;
epoch := read1(epoch)
|} in
} in
toIMem.(MemReq.enq)(req);
write1(pc, pc + |32`d4|);
f2d.(fromFetch.enq)(fetch_bookkeeping)
Expand Down Expand Up @@ -591,14 +590,14 @@ Module RV32Core (RVP: RVParams) (Multiplier: MultiplierInterface).
scoreboard.(Scoreboard.insert)(sliceReg(rd_idx)));
let rs1 := rf.(Rf.read_1)(sliceReg(rs1_idx)) in
let rs2 := rf.(Rf.read_1)(sliceReg(rs2_idx)) in
let decode_bookkeeping := struct decode_bookkeeping {|
let decode_bookkeeping := struct decode_bookkeeping {
pc := get(fetched_bookkeeping, pc);
ppc := get(fetched_bookkeeping, ppc);
epoch := get(fetched_bookkeeping, epoch);
dInst := decodedInst;
rval1 := rs1;
rval2 := rs2
|} in
} in
d2e.(fromDecode.enq)(decode_bookkeeping))
}}.

Expand Down Expand Up @@ -671,8 +670,8 @@ Module RV32Core (RVP: RVParams) (Multiplier: MultiplierInterface).
set data := rs2_val << shift_amount;
set addr := addr[|5`d2| :+ 30 ] ++ |2`d0|;
set isUnsigned := funct3[|2`d2|];
toDMem.(MemReq.enq)(struct mem_req {|
byte_en := byte_en; addr := addr; data := data |})
toDMem.(MemReq.enq)(struct mem_req {
byte_en := byte_en; addr := addr; data := data })
else if (isControlInst(dInst)) then
set data := (pc + |32`d4|) (* For jump and link *)
else if (isMultiplyInst(dInst)) then
Expand All @@ -686,13 +685,13 @@ Module RV32Core (RVP: RVParams) (Multiplier: MultiplierInterface).
write0(pc, nextPc)
else
pass;
let execute_bookkeeping := struct execute_bookkeeping {|
let execute_bookkeeping := struct execute_bookkeeping {
isUnsigned := isUnsigned;
size := size;
offset := offset;
newrd := data;
dInst := get(decoded_bookkeeping, dInst)
|} in
} in
e2w.(fromExecute.enq)(execute_bookkeeping))
else
pass
Expand Down Expand Up @@ -738,10 +737,10 @@ Module RV32Core (RVP: RVParams) (Multiplier: MultiplierInterface).
Definition memoryBus (m: memory) : UInternalFunction reg_t ext_fn_t :=
{{ fun memoryBus (get_ready: bits_t 1) (put_valid: bits_t 1) (put_request: struct_t mem_req) : struct_t mem_output =>
`match m with
| imem => {{ extcall (ext_mem m) (struct mem_input {|
| imem => {{ extcall (ext_mem m) (struct mem_input {
get_ready := get_ready;
put_valid := put_valid;
put_request := put_request |}) }}
put_request := put_request }) }}
| dmem => {{ let addr := get(put_request, addr) in
let byte_en := get(put_request, byte_en) in
let is_write := byte_en == Ob~1~1~1~1 in
Expand All @@ -758,42 +757,41 @@ Module RV32Core (RVP: RVParams) (Multiplier: MultiplierInterface).
if is_uart_write then
let char := get(put_request, data)[|5`d0| :+ 8] in
let may_run := get_ready && put_valid && is_uart_write in
let ready := extcall ext_uart_write (struct (Maybe (bits_t 8)) {|
valid := may_run; data := char |}) in
struct mem_output {| get_valid := may_run && ready;
put_ready := may_run && ready;
get_response := struct mem_resp {|
let ready := extcall ext_uart_write (struct (Maybe (bits_t 8)) {
valid := may_run; data := char }) in
struct mem_output { get_valid := may_run && ready;
put_ready := may_run && ready;
get_response := struct mem_resp {
byte_en := byte_en; addr := addr;
data := |32`d0| |} |}
data := |32`d0| } }

else if is_uart_read then
let may_run := get_ready && put_valid && is_uart_read in
let opt_char := extcall ext_uart_read (may_run) in
let ready := get(opt_char, valid) in
struct mem_output {| get_valid := may_run && ready;
put_ready := may_run && ready;
get_response := struct mem_resp {|
struct mem_output { get_valid := may_run && ready;
put_ready := may_run && ready;
get_response := struct mem_resp {
byte_en := byte_en; addr := addr;
data := zeroExtend(get(opt_char, data), 32) |} |}
data := zeroExtend(get(opt_char, data), 32) } }

else if is_led then
let on := get(put_request, data)[|5`d0|] in
let may_run := get_ready && put_valid && is_led_write in
let current := extcall ext_led (struct (Maybe (bits_t 1)) {|
valid := may_run; data := on |}) in
let current := extcall ext_led (struct (Maybe (bits_t 1)) {
valid := may_run; data := on }) in
let ready := Ob~1 in
struct mem_output {| get_valid := may_run && ready;
put_ready := may_run && ready;
get_response := struct mem_resp {|
byte_en := byte_en; addr := addr;
data := zeroExtend(current, 32) |} |}
struct mem_output { get_valid := may_run && ready;
put_ready := may_run && ready;
get_response := struct mem_resp {
byte_en := byte_en; addr := addr;
data := zeroExtend(current, 32) } }

else
extcall (ext_mem m) (struct mem_input {|
extcall (ext_mem m) (struct mem_input {
get_ready := get_ready && is_mem;
put_valid := put_valid && is_mem;
put_request := put_request |})
}}
put_request := put_request }) }}
end` }}.

Definition mem (m: memory) : uaction reg_t ext_fn_t :=
Expand Down
16 changes: 8 additions & 8 deletions examples/uart.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,11 +53,11 @@ Module UART.

Definition _read_input : uaction reg_t ext_fn_t :=
{{
let ready := read1(state) == enum tx_state {| idle |} in
let ready := read1(state) == enum tx_state { idle } in
let opt_byte := extcall ext_read_byte(ready) in
(when ready && get(opt_byte, valid) do
write1(in_byte, get(opt_byte, data));
write1(state, enum tx_state {| start |}))
write1(state, enum tx_state { start }))
}}.

Definition _transmit : uaction reg_t ext_fn_t :=
Expand All @@ -66,21 +66,21 @@ Module UART.
let state := read0(state) in
(if read0(delay) == |CLOCK_DELAY_BITS`d0| then
match state with
| enum tx_state {| start |} =>
| enum tx_state { start } =>
(set bit := Ob~0;
set state := enum tx_state {| tx |})
| enum tx_state {| tx |} =>
set state := enum tx_state { tx })
| enum tx_state { tx } =>
let bits := read0(in_byte) in
let offset := read0(in_byte_offset) in
let last_char := offset == Ob~1~1~1 in
set bit := bits[Ob~0~0~0];
write0(in_byte, bits >> Ob~1);
write0(in_byte_offset, offset + Ob~0~0~1);
(when last_char do
set state := enum tx_state {| finish |})
| enum tx_state {| finish |} =>
set state := enum tx_state { finish })
| enum tx_state { finish } =>
(set bit := Ob~1;
set state := enum tx_state {| idle |})
set state := enum tx_state { idle })
return default: pass
end;
write0(delay, #CLOCK_DELAY)
Expand Down
Loading

0 comments on commit f21917b

Please sign in to comment.