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

Jump to bottom

Graph query semantic formalization #2

Open
wants to merge 24 commits into
base: master
Choose a base branch
from
Open

Graph query semantic formalization #2

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
c3f6fc2
initial commit
HeyLey Apr 22, 2017
79b9d79
Update README.md
HeyLey Apr 22, 2017
a4c1df1
Some about language
HeyLey Apr 23, 2017
fa63083
Merge remote-tracking branch 'origin/master'
HeyLey Apr 23, 2017
e5c8d40
Some about language
HeyLey Apr 23, 2017
9097701
Lemma start
HeyLey Apr 24, 2017
c2b712a
add simple lemma T0
HeyLey Apr 29, 2017
a118017
add proof for lemma 2.1
HeyLey Apr 29, 2017
46dd514
Add graph library
fedorovr May 8, 2017
2a6367c
Add CCFPQ definition
fedorovr May 8, 2017
ea46320
Add different semantics of CCFPQ evaluation
fedorovr May 8, 2017
5c037bb
Rename constructor and remove unused variables
fedorovr May 9, 2017
6f60e84
Avoid apostrophes in names
fedorovr May 9, 2017
b3159e8
Add graph construction examples
fedorovr May 9, 2017
3bc3bd5
Add cfg construction examples
fedorovr May 9, 2017
c5f149f
Add ccfpq construction examples
fedorovr May 9, 2017
bf0a7c3
Fix definition of CCFPQ_result with relational semantics
fedorovr May 10, 2017
ab0533c
Add definition of CFG in CNF
fedorovr May 17, 2017
095f85f
Remove paths from Graph lib
fedorovr May 17, 2017
0010f32
Use CFG in CNF in definition of CCFPQ
fedorovr May 17, 2017
46e6efd
Add parse tree and 3 semantics of evaluation of CCFPQ; plus theorems …
fedorovr May 17, 2017
969e9a2
Update examples according new defenitions
fedorovr May 20, 2017
3fcc087
Make names more understandable
fedorovr May 22, 2017
6dc9545
Use Graph record instead of (Vertices, Arcs) pair
fedorovr May 23, 2017
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
16 changes: 10 additions & 6 deletions CCFPQ/CCFPQ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
Require Import Definitions.
Require Import CF_Definitions.
Require Import Graph.
Require Import List.
Import ListNotations.

Unset Implicit Arguments.
Set Strict Implicit.

Expand Down Expand Up @@ -31,10 +34,10 @@ Section CCFPQ.

Inductive CCFPQ_Builder : V_set -> Nat_set -> list var_EitherVertexNat_pair -> Type :=
| Empty_query : CCFPQ_Builder V_empty Nat_empty []
| Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair)
| Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Дайте, пожалуйста, нормальные имена всем сущьностям. Читать код с V_Set и прочим очень тяжело.

(x : Vertex),
CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder (V_union v (V_single x)) n var_evnp_l
| Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair)
| Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair)
(bv : nat),
CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v (Nat_union n (Nat_single bv)) var_evnp_l
| Add_conj_vertex_vertex : forall v n var_evnp_l nt (x1 x2 : Vertex),
Expand Down Expand Up @@ -99,15 +102,16 @@ Section CCFPQ.
| (nt, _)::tl => nt::get_nonterminals tl
end.

Fixpoint get_all_vars (G : grammar) : list var :=
Fixpoint get_all_vars (G : Grammar) : list var :=
match G with
| [] => []
| R A u::Gr => A::(get_all_vars Gr)
| (Rv A v1 v2)::Gr => A::(get_all_vars Gr)
| x::Gr => get_all_vars Gr
end.

Record CCFPQ_on_grammar : Type := {
ccfpq : CCFPQ;
gr : grammar;
gr : Grammar;

nonterminals_in_grammar : forall (nt : var),
In nt (get_nonterminals (var_evnp_l ccfpq)) -> In nt (get_all_vars gr)
Expand Down
Loading