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

Directly typed parsing #15

Merged
merged 2 commits into from
Nov 13, 2024
Merged

Directly typed parsing #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b651d03
feat(parsing): alternative set syntax
maxkurze1 Nov 13, 2024
72c20a6
feat(parsing): fix get/subst; add explicitly typed variant
maxkurze1 Nov 13, 2024
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
47 changes: 41 additions & 6 deletions coq/TypedParsing.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,9 @@ Export Koika.Primitives.PrimTyped.
Export Coq.Strings.String.
Export Coq.Lists.List.ListNotations.

Export (hints) IdentParsing.TC.
Local Notation id_to_s a := (TC.ident_to_string a : string).

Definition pos_t := unit.
Definition var_t := string.
Definition fn_name_t := string.
Expand Down Expand Up @@ -67,7 +70,7 @@ Notation "'<{' e '}>'" := (e) (e custom koika_t).
* to parse identifiers as strings.
*)
Declare Custom Entry koika_t_var.
Notation "a" := (ident_to_string a) (in custom koika_t_var at level 0, a ident, only parsing).
Notation "a" := (id_to_s a) (in custom koika_t_var at level 0, a ident, only parsing).
Notation "a" := (a) (in custom koika_t_var at level 0, a ident, format "'[' a ']'", only printing).

(* Variable references
Expand Down Expand Up @@ -198,9 +201,14 @@ Notation "'#' s" := (Const (tau := bits_t _) s) (in custom koika_t at level 0, s
* Some of the literal notations also start with an identifier.
* Thus, the same restrictions apply.
*)
Notation "a" := (Var (k := (ident_to_string a)) _) (in custom koika_t at level 0, a constr at level 0, only parsing).
Notation "a" := (Var (k := id_to_s a) _) (in custom koika_t at level 0, a constr at level 0, only parsing).
Notation "a" := (Var a) (in custom koika_t at level 0, a constr at level 0, only printing).

(* Alternative shorter set syntax
* Note: expr is level 89 to stay below ';' *)
Notation "a ':=' b" := (Assign (k := id_to_s a) _ b) (in custom koika_t at level 0, a constr at level 0, b custom koika_t at level 89, only parsing).
Notation "a ':=' b" := (Assign a b) (in custom koika_t at level 0, a constr at level 0, b custom koika_t at level 89, only printing).

Declare Custom Entry koika_t_args.
Notation "'(' x ',' .. ',' y ')'" := (CtxCons (_,_) (x) .. (CtxCons (_,_) (y) CtxEmpty) ..) (in custom koika_t_args, x custom koika_t, y custom koika_t).
Notation "'(' ')'" := (CtxEmpty) (in custom koika_t_args).
Expand Down Expand Up @@ -327,10 +335,19 @@ Notation "'unpack(' t ',' v ')'" := (Unop (Conv t Unpack) v) (in custom

Notation "'extcall' method '(' arg ')'" := (ExternalCall method arg) (in custom koika_t, method constr at level 0).

Notation "'get' '(' v ',' f ')'" := (Unop (Struct1 GetField _ (PrimTypeInference.find_field _ f)) v ) (in custom koika_t, f custom koika_t_var, format "'get' '(' v ',' f ')'").
Notation "'getbits' '(' t ',' v ',' f ')'" := (Unop (Bits1 (GetFieldBits t (PrimTypeInference.find_field t f))) v ) (in custom koika_t, t constr, f custom koika_t_var, format "'getbits' '(' t ',' v ',' f ')'").
Notation "'subst' '(' v ',' f ',' a ')'" := (Binop (Struct2 SubstField _ (PrimTypeInference.find_field _ f)) v a) (in custom koika_t, f custom koika_t_var, format "'subst' '(' v ',' f ',' a ')'").
Notation "'substbits' '(' t ',' v ',' f ',' a ')'" := (Binop (Bits2 (SubstFieldBits t (PrimTypeInference.find_field t f))) v a) (in custom koika_t, t constr, f custom koika_t_var, format "'substbits' '(' t ',' v ',' f ',' a ')'").
Notation "'get' '(' v ',' f ')'" := (Unop (Struct1 GetField _ (struct_idx _ f)) v ) (in custom koika_t, f custom koika_t_var, format "'get' '(' v ',' f ')'").
Notation "'getbits' '(' t ',' v ',' f ')'" := (Unop (Bits1 (GetFieldBits t (struct_idx t f))) v ) (in custom koika_t, t constr, f custom koika_t_var, format "'getbits' '(' t ',' v ',' f ')'").
Notation "'subst' '(' v ',' f ',' a ')'" := (Binop (Struct2 SubstField _ (struct_idx _ f)) v a) (in custom koika_t, f custom koika_t_var, format "'subst' '(' v ',' f ',' a ')'").
Notation "'substbits' '(' t ',' v ',' f ',' a ')'" := (Binop (Bits2 (SubstFieldBits t (struct_idx t f))) v a) (in custom koika_t, t constr, f custom koika_t_var, format "'substbits' '(' t ',' v ',' f ',' a ')'").

Notation "'get@' sig '(' v ',' f ')'" := (Unop (Struct1 GetField sig (struct_idx sig f)) v)
(in custom koika_t, sig constr at level 0, f custom koika_t_var, format "'get@' sig '(' v ',' f ')'").
Notation "'getbits@' sig '(' v ',' f ')'" := (Unop (Bits1 (GetFieldBits sig (struct_idx sig f))) v)
(in custom koika_t, sig constr at level 0, f custom koika_t_var, format "'getbits@' sig '(' v ',' f ')'").
Notation "'subst@' sig '(' v ',' f ',' a ')'" := (Binop (Struct2 SubstField sig (struct_idx sig f)) v a)
(in custom koika_t, sig constr at level 0, f custom koika_t_var, format "'subst@' sig '(' v ',' f ',' a ')'").
Notation "'substbits@' sig '(' v ',' f ',' a ')'" := (Binop (Bits2 (SubstFieldBits sig (struct_idx sig f))) v a)
(in custom koika_t, sig constr at level 0, f custom koika_t_var, format "'substbits@' sig '(' v ',' f ',' a ')'"). (* FIXME parsing.v spacing *)

Notation "'aref' '(' v ',' f ')'" := (Unop (Array1 (GetElement f)) v) (in custom koika_t, f constr, format "'aref' '(' v ',' f ')'").
Notation "'arefbits' '(' t ',' v ',' f ')'" := (Unop (Array1 (GetElementBits t f)) v) (in custom koika_t, t constr, f constr, format "'arefbits' '(' t ',' v ',' f ')'").
Expand Down Expand Up @@ -457,6 +474,7 @@ Module Type Tests2.
Definition test_3' : _action := <{ let yoyo := pass in set yoyo := pass ; pass }>.
Fail Definition test_3'' : _action := <{ set yoyo := pass ; pass; }>.
Fail Definition test_5 : _action := <{ let yoyo := set yoyo := pass in pass; }>.
Definition test_6 : _action := <{ let yoyo := 0b"101" in yoyo := 0b"111"; pass }>.
Inductive test := rData (n:nat).
Definition test_R (r : test) := bits_t 5.
Definition test_9 : _action := <{ read0(data0) }>.
Expand Down Expand Up @@ -603,6 +621,23 @@ Module Type Tests2.
("four" , bits_t 3);
("five" , enum_t numbers_e) ]
|}.

Definition test_get : action' R Sigma (sig := [("a", struct_t numbers_s)]) := <{
get(a, one)
}>.

Definition test_get2 : action' R Sigma (sig := [("a", struct_t numbers_s)]) := <{
get@numbers_s(a, one)
}>.

Definition test_subst : action' R Sigma (sig := [("a", struct_t numbers_s)]) := <{
subst(a, one, 0b"111")
}>.

Definition test_subst2 : action' R Sigma (sig := [("a", struct_t numbers_s)]) := <{
subst@numbers_s(a, one, 0b"111")
}>.

Definition struct_test_1 : _action := <{ struct numbers_s::{ } }>.
Definition struct_test_3 : _action := <{ struct numbers_s::{ one := 0b"010" } }>.
Definition struct_test_7 : _action := <{ struct numbers_s::{ one := 0b"111"; two := 0b"101"; } }>. (* trailing comma *)
Expand Down
10 changes: 10 additions & 0 deletions coq/TypedSyntaxMacros.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,8 @@ Section TypedSyntaxMacros.
field_subst_constr : {idx : struct_index sig & field_type sig idx}.
Hint Mode FieldSubstConstr + + + + : typeclass_instances.

Class StructIdx sig (f : string) := struct_idx : struct_index sig.

Section Switch.
Notation action := (action R Sigma).

Expand Down Expand Up @@ -275,6 +277,14 @@ Arguments field_subst {pos_t var_t fn_name_t reg_t ext_fn_t} {R Sigma}
Arguments field_subst_constr {T} {sig} field val {FieldSubstConstr}.
Arguments lift_fn_of {A A' B} {fA fA'} lift_fn lift_comm : assert.


#[export] Instance struct_idx_hd {f t sig nm}:
StructIdx {| struct_name := nm; struct_fields := (f,t) :: sig |} f := thisone.
#[export] Instance struct_idx_tl {f f' t sig nm}
{si : StructIdx {| struct_name := nm; struct_fields := sig |} f}:
StructIdx {| struct_name := nm; struct_fields := (f',t) :: sig |} f := anotherone si.
Arguments struct_idx sig f {StructIdx} : assert.

(* Notation lift_intfun lR lSigma fn :=
(lift_intfun' (lift lR lSigma) fn). *)

Expand Down
Loading