Skip to content

Commit

Permalink
Fix up GenQuery.
Browse files Browse the repository at this point in the history
  • Loading branch information
@Chobbes
Chobbes committed Mar 18, 2024
1 parent a172bad commit 3218f1a
Show file tree
Hide file tree
Showing 2 changed files with 137 additions and 95 deletions.
9 changes: 9 additions & 0 deletions src/coq/QC/ECS.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1180,17 +1180,26 @@ Definition query {world a m} `{Monad m} (f : world FieldOf -> option a) : QueryT
| Some x => ret x
end.

Definition queryl {world a m} `{Monad m} (l : Lens' (world FieldOf) (Component FieldOf Field a)) : QueryT world m a
:= query (view l).

Definition withq {world a m} `{Monad m} (f : world FieldOf -> option a) : QueryT world m unit
:= query f;;
ret tt.

Definition withl {world a m} `{Monad m} (l : Lens' (world FieldOf) (Component FieldOf Field a)) : QueryT world m unit
:= withq (view l).

Definition without {world a m} `{MonadZero m} `{Monad m} (f : world FieldOf -> option a) : QueryT world m unit
:= e <- @mkQueryT world m _ (asks snd);;
match f e with
| None => ret tt
| Some x => mzero
end.

Definition withoutl {world a m} `{MonadZero m} `{Monad m} (l : Lens' (world FieldOf) (Component FieldOf Field a)) : QueryT world m unit
:= without (view l).

(* I want to be able to use `IS.t` and `IM.Raw.t unit` and maybe `list Z` and `list Ent` as targets... What do I need from an EntTarget? *)
Class ToEnt T :=
{ toEnt : T -> Ent
Expand Down
223 changes: 128 additions & 95 deletions src/coq/QC/GenAST.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1015,10 +1015,26 @@ Section TypGenerators.
(* | _ => false *)
(* end) ctx. *)

Definition gen_IntMapRaw_key_filter {a} (m : IM.Raw.t a) (filter : Z -> GenLLVM bool) : GenLLVM (option Z)
Definition GenQuery' m := QueryT Metadata m.
Definition runGenQuery {m A E}
`{TE : ToEnt E}
`{Monad m}
`{MS: MetadataStore m Metadata (SystemState GenState m)}
`{MT: MonadT (SystemT GenState m) m}
(q : GenQuery' m A) (k : E) : SystemT GenState m (option A):=
let e := toEnt k in
meta <- getEntity e;;
lift (unQueryT q e meta).
Definition GenQuery := GenQuery' G.

Definition runGenQueryLLVM {A E} `{TE : ToEnt E}
(q : GenQuery A) (k : E) : GenLLVM (option A):=
lift (runGenQuery q k).

Definition gen_IntMapRaw_key_filter {a b} (m : IM.Raw.t a) (filter : GenQuery b) : GenLLVM (option Z)
:= '(g, _) <- (IM.Raw.fold
(fun key _ (grest : GenLLVM (option Z * N)) =>
cnd <- filter key;;
cnd <- is_some <$> runGenQueryLLVM filter key;;
'(gacc, k) <- grest;;
swap <- lift (fmap (N.eqb 0) (choose (0%N, k)));;
let k' := if cnd then (k+1)%N else k in
Expand All @@ -1029,37 +1045,27 @@ Section TypGenerators.
ret (gacc, k'))
m (ret (@None Z, 0%N)));;
ret g.

Definition gen_IntMapRaw_key {a} (m : IM.Raw.t a) : GenLLVM (option Z)
:= gen_IntMapRaw_key_filter m (ret tt).

Definition gen_IntMapRaw_ent {a} (m : IM.Raw.t a) : GenLLVM (option Ent)
:= fmap (fmap mkEnt) (gen_IntMapRaw_key m).

Definition gen_IntMapRaw_key {a} (m : IM.Raw.t a) : GenLLVM Z
:= fst (IM.Raw.fold
(fun key _ '(gacc, k) =>
let gen' :=
swap <- lift (fmap (N.eqb 0) (choose (0%N, k)));;
if swap
then (* swap *)
ret key
else (* No swap *)
gacc
in (gen', (k+1)%N))
m (failGen "gen_IntMapRaw_key", 0%N)).

Definition gen_IntMapRaw_ent {a} (m : IM.Raw.t a) : GenLLVM Ent
:= fmap mkEnt (gen_IntMapRaw_key m).

Definition gen_IntMapRaw_ent_filter {a} (m : IM.Raw.t a) (filter : Z -> GenLLVM bool) : GenLLVM (option Ent)
Definition gen_IntMapRaw_ent_filter {a b} (m : IM.Raw.t a) (filter : GenQuery b) : GenLLVM (option Ent)
:= fmap (fmap mkEnt) (gen_IntMapRaw_key_filter m filter).


Definition gen_sized_type_alias : GenLLVM ident
Definition gen_sized_type_alias : GenLLVM (option ident)
:= es <- use (gen_context' .@ is_sized_type_alias');;
var <- gen_IntMapRaw_ent es;;
mident <- use (gen_context' .@ entl var .@ name');;
match mident with
| Some id => ret id
| None => failGen "gen_sized_type_alias, couldn't find entity... Shouldn't happen"
end.
match var with
| Some var =>
id <- use (gen_context' .@ entl var .@ name');;
ret id
| None => ret None
end.

Definition gen_entity_with {a} (focus : Lens' (SystemState GenState G) (IM.Raw.t a)): GenLLVM Ent
Definition gen_entity_with {a} (focus : Lens' (SystemState GenState G) (IM.Raw.t a)): GenLLVM (option Ent)
:= es <- use focus;;
gen_IntMapRaw_ent es.

Expand All @@ -1070,9 +1076,9 @@ Section TypGenerators.
| None => ret false
end.

Definition gen_entity_with_filter {a}
Definition gen_entity_with_filter {a b}
(focus : Lens' (SystemState GenState G) (IM.Raw.t a))
(filter : Z -> GenLLVM bool)
(filter : GenQuery b)
: GenLLVM (option Ent)
:= es <- use focus;;
gen_IntMapRaw_ent_filter es filter.
Expand All @@ -1094,11 +1100,15 @@ Section TypGenerators.
(* Generate a type that matches one of the type aliases *)
Definition gen_sized_type_of_alias {a} (focus : Lens' (SystemState GenState G) (IM.Raw.t a)) : GenLLVM typ
:= var <- gen_entity_with focus;;
get_type_from_alias var.
match var with
| Some var =>
get_type_from_alias var
| None => failGen "gen_sized_type_of_alias, couldn't find entity... Shouldn't happen"
end.

Definition gen_sized_type_of_alias_filter {a}
Definition gen_sized_type_of_alias_filter {a b}
(focus : Lens' (SystemState GenState G) (IM.Raw.t a))
(filter : Z -> GenLLVM bool)
(filter : GenQuery b)
: GenLLVM (option typ)
:= var <- gen_entity_with_filter focus filter;;
match var with
Expand All @@ -1107,14 +1117,9 @@ Section TypGenerators.
end.

(* Generate a type that matches one of the variables *)
Definition gen_sized_type_of_variable {a} (focus : Lens' (SystemState GenState G) (IM.Raw.t a)) : GenLLVM typ
:= var <- gen_entity_with focus;;
get_type_of_variable var.

(* Generate a type that matches one of the variables *)
Definition gen_sized_type_of_variable_filter {a}
Definition gen_type_of_variable_filter {a b}
(focus : Lens' (SystemState GenState G) (IM.Raw.t a))
(filter : Z -> GenLLVM bool)
(filter : GenQuery b)
: GenLLVM (option typ)
:= var <- gen_entity_with_filter focus filter;;
match var with
Expand All @@ -1124,12 +1129,13 @@ Section TypGenerators.

(* Not sized in the QuickChick sense, sized in the LLVM sense. *)
Definition gen_sized_typ_0 : GenLLVM typ :=
sized_aliases <- use (gen_context' .@ is_sized_type_alias');;
oid <- gen_sized_type_alias;;
let ident_gen :=
(* Don't want to fail if there are no identifiers *)
if (IM.Raw.is_empty sized_aliases)%nat
then []
else [TYPE_Identified <$> gen_sized_type_alias] in
match oid with
| None => []
| Some id => [ret (TYPE_Identified id)]
end
in
oneOf_LLVM
(ident_gen ++
(map ret
Expand Down Expand Up @@ -1161,80 +1167,107 @@ Section TypGenerators.
(* Definition gen_ident_from_ctx (ctx : var_context) : GenLLVM ident *)
(* := fmap fst (elems_LLVM ctx). *)

Definition gen_type_matching_alias_focus {a} (focus : Lens' (SystemState GenState G) (IM.Raw.t a)) : GenLLVM (N * (unit -> GenLLVM typ))
Definition def_option_GenLLVM {a} (def : GenLLVM a) (gopt : GenLLVM (option a)) : GenLLVM a
:= o <- gopt;;
match o with
| Some a => ret a
| None => def
end.

Definition gen_type_matching_alias_focus {a b}
(focus : Lens' (SystemState GenState G) (IM.Raw.t a)) (filter : GenQuery b)
: GenLLVM (N * (unit -> GenLLVM typ))
:= focused <- use focus;;
ret (N.min (N.of_nat (IM.Raw.cardinal focused)) 10, (fun _ => gen_sized_type_of_alias focus)).
let sz := IM.Raw.cardinal focused in
ret (N.min (N.of_nat sz) 10,
(fun _ => def_option_GenLLVM (failGen "gen_type_matching_alias_focus: shouldn't happen!") (gen_sized_type_of_alias_filter focus filter))).

Definition gen_type_matching_variable_focus {a} (focus : Lens' (SystemState GenState G) (IM.Raw.t a)) : GenLLVM (N * (unit -> GenLLVM typ))
Definition gen_type_matching_variable_focus {a b}
(focus : Lens' (SystemState GenState G) (IM.Raw.t a)) (filter : GenQuery b)
: GenLLVM (N * (unit -> GenLLVM typ))
:= focused <- use focus;;
ret (N.min (N.of_nat (IM.Raw.cardinal focused)) 10, (fun _ => gen_sized_type_of_variable focus)).
let sz := IM.Raw.cardinal focused in
ret (N.min (N.of_nat sz) 10,
(fun _ => def_option_GenLLVM (failGen "gen_type_matching_variable_focus: shouldn't happen!") (gen_type_of_variable_filter focus filter))).

Definition gen_type_matching_alias : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_alias_focus (gen_context' .@ is_sized_type_alias').
Definition gen_type_matching_alias {b} (filter : GenQuery b) : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_alias_focus (gen_context' .@ is_sized_type_alias') filter.

Definition gen_type_matching_local : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_variable_focus (gen_context' .@ is_local').
Definition gen_type_matching_local {b} (filter : GenQuery b) : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_variable_focus (gen_context' .@ is_local') filter.

Definition gen_type_matching_global : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_variable_focus (gen_context' .@ is_global').
Definition gen_type_matching_global {b} (filter : GenQuery b) : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_variable_focus (gen_context' .@ is_global') filter.

Definition gen_type_matching_locals_and_globals : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_variable_focus (gen_context' .@ variable_type').
Definition gen_type_matching_locals_and_globals {b} (filter : GenQuery b) : GenLLVM (N * (unit -> GenLLVM typ))
:= gen_type_matching_variable_focus (gen_context' .@ variable_type') filter.

Program Fixpoint gen_sized_typ_size' (from_context : GenLLVM (N * (unit -> GenLLVM typ))) (sz : nat) {measure sz} : GenLLVM typ :=
match sz with
| O => gen_sized_typ_0
| (S sz') =>
fc <- from_context;;
freq_LLVM_thunked_N
([fc] ++
[(1%N, (fun _ => gen_sized_typ_0))
; (1%N, (fun _ => ret TYPE_Pointer <*> gen_sized_typ_size' from_context sz'))
(* TODO: Might want to restrict the size to something reasonable *)
; (1%N, (fun _ => ret TYPE_Array <*> lift_GenLLVM genN <*> gen_sized_typ_size' from_context sz'))
; (1%N, (fun _ => ret TYPE_Vector <*> (n <- lift_GenLLVM genN;; ret (n + 1)%N) <*> gen_sized_typ_size' from_context 0))
(* TODO: I don't think functions are sized types? *)
(* ; let n := Nat.div sz 2 in *)
(* ret TYPE_Function <*> gen_sized_typ_size n <*> listOf_LLVM (gen_sized_typ_size n) *)
; (1%N, (fun _ => ret TYPE_Struct <*> nonemptyListOf_LLVM (gen_sized_typ_size' from_context sz')))
; (1%N, (fun _ => ret TYPE_Packed_struct <*> nonemptyListOf_LLVM (gen_sized_typ_size' from_context sz')))
])
[ fc
; (1%N, (fun _ => gen_sized_typ_0))
; (1%N, (fun _ => ret TYPE_Pointer <*> gen_sized_typ_size' from_context sz'))
(* TODO: Might want to restrict the size to something reasonable *)
; (1%N, (fun _ => ret TYPE_Array <*> lift_GenLLVM genN <*> gen_sized_typ_size' from_context sz'))
; (1%N, (fun _ => ret TYPE_Vector <*> (n <- lift_GenLLVM genN;; ret (n + 1)%N) <*> gen_sized_typ_size' from_context 0))
(* TODO: I don't think functions are sized types? *)
(* ; let n := Nat.div sz 2 in *)
(* ret TYPE_Function <*> gen_sized_typ_size n <*> listOf_LLVM (gen_sized_typ_size n) *)
; (1%N, (fun _ => ret TYPE_Struct <*> nonemptyListOf_LLVM (gen_sized_typ_size' from_context sz')))
; (1%N, (fun _ => ret TYPE_Packed_struct <*> nonemptyListOf_LLVM (gen_sized_typ_size' from_context sz')))
]
end.

Definition gen_sized_typ_size := gen_sized_typ_size' gen_type_matching_alias.
Definition gen_sized_typ_size := gen_sized_typ_size' (gen_type_matching_alias (withl is_sized')).

Definition gen_sized_typ' (from_context : GenLLVM (N * (unit -> GenLLVM typ))) : GenLLVM typ
:= sized_LLVM (fun sz => gen_sized_typ_size' from_context sz).

Definition gen_sized_typ : GenLLVM typ
:= gen_sized_typ' gen_type_matching_alias.

(* Want to be able to use gen_sized_typ' to do this...
But I did not notice this wants only sized types from the contexts.
Need to be able to filter focused entities to only the ones with the sized type tags... Should be doable.
*)
Definition gen_sized_typ_ptrin_fctx : GenLLVM typ
:= gen_sized_typ_size'
ctx <- get_ctx;;
aliases <- get_typ_ctx;;
let typs_in_ctx := filter_sized_typs aliases ctx in
sized_LLVM (fun sz => gen_sized_typ_size_ptrinctx sz typs_in_ctx).

Definition gen_sized_typ_ptrin_gctx : GenLLVM typ
:=
gctx <- get_global_ctx;;
aliases <- get_typ_ctx;;
let typs_in_ctx := filter_sized_typs aliases gctx in
sized_LLVM (fun sz => gen_sized_typ_size_ptrinctx sz typs_in_ctx).
:= sized_LLVM (fun sz => gen_sized_typ_size sz).

(* (* Want to be able to use gen_sized_typ' to do this... *)
(* But I did not notice this wants only sized types from the contexts. *)
(* Need to be able to filter focused entities to only the ones with the sized type tags... Should be doable. *)
(* *) *)
(* Definition gen_sized_typ_ptrin_fctx : GenLLVM typ *)
(* := gen_typ_size' ( *)
(* ctx <- get_ctx;; *)
(* aliases <- get_typ_ctx;; *)
(* let typs_in_ctx := filter_sized_typs aliases ctx in *)
(* sized_LLVM (fun sz => gen_sized_typ_size_ptrinctx sz typs_in_ctx). *)

(* gen_sized_typ_ptrin_fctx seems to grab a *)

(* Definition gen_sized_typ_ptrin_gctx : GenLLVM typ *)
(* := *)
(* gctx <- get_global_ctx;; *)
(* aliases <- get_typ_ctx;; *)
(* let typs_in_ctx := filter_sized_typs aliases gctx in *)
(* sized_LLVM (fun sz => gen_sized_typ_size_ptrinctx sz typs_in_ctx). *)

Definition gen_type_alias_ident : GenLLVM (option ident)
:= es <- use (gen_context' .@ type_alias');;
var <- gen_IntMapRaw_ent es;;
match var with
| Some var =>
id <- use (gen_context' .@ entl var .@ name');;
ret id
| None => ret None
end.

(* Generate a type of size 0 *)
Definition gen_typ_0 : GenLLVM typ :=
aliases <- get_typ_ctx;;
let identified :=
match aliases with
| [] => []
| _ => [(ret TYPE_Identified <*> gen_ident_from_ctx aliases)]
end
oid <- gen_sized_type_alias;;
let ident_gen :=
match oid with
| None => []
| Some id => [ret (TYPE_Identified id)]
end
in
oneOf_LLVM
((* identified ++ *)
Expand Down

0 comments on commit 3218f1a

Please sign in to comment.