The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

 Here is a simpler representation of contexts.

Hope this helps,

Pierre





Quoting Pierre Casteran 
<pierre.casteran AT labri.fr>:

> Hi,
>
>  There are two precisions that should be made :
>   I assume a) that the "x" points out to a position where seqDiag is expected
>            b) there is exactly one occurrence of "x".
>
> With these assumptions, one can define a type called "context" in the
> attached file.
>
> But the best is to have a look at Gérard Huet's proposition for writing
> contexts : the zipper data structure.
>
> http://en.wikipedia.org/wiki/Zipper_%28data_structure%29
>
> The best,
>
> Pierre
>
>
> Quoting 
> ldou AT cs.ecnu.edu.cn:
>
> > hi,guys,
> >    i'm using Coq to formalize the Sequence Diagram. The following   
> > inductive type of sequence diagram has been defined:
> > Inductive seqDiag:Set :=
> > |DE: event ->seqDiag
> > |DStrict:seqDiag->seqDiag->seqDiag
> > |DPar: seqDiag->seqDiag->seqDiag
> > |DSeq: seqDiag -> seqDiag ->seqDiag.
> >   Then i want to define "context" in Coq. According to our concept,  
> >  a context is a sequence diagram with one of its fragment replaced  
> > by  a special symbol x, just like term rewriting. how should i  
> > define  "context"? any suggestions are appreciated.
> >
> >
> > ----------------
> > ===========================================================
> > Best regards!
> >
> > 窦亮
> > 华东师范大学计算机科学技术系
> > (Department of Computer Science, East China Normal University)
> >
> > E-mail:ldou AT cs.ecnu.edu.cn
> >
> > ===========================================================

Parameter event : Type.

Inductive seqDiag:Type :=
|DE: event ->seqDiag
|DStrict:seqDiag->seqDiag->seqDiag
|DPar: seqDiag->seqDiag->seqDiag
|DSeq: seqDiag -> seqDiag ->seqDiag.


(* type of seqDiags with exactly one hole (where a seqDiag is expected) *)

Inductive context : Type := 
Root : context |
 CStrictL : seqDiag -> context  -> context|
 CStrictR : seqDiag -> context  -> context |
CParL : seqDiag -> context  -> context |
 CParR : seqDiag -> context  -> context |
CSeqL : seqDiag -> context  -> context |
CSeqR : seqDiag -> context  -> context .

(* replacing the hole with d *)

Fixpoint fill (d:seqDiag) (gamma:context) :seqDiag :=
match gamma with
 Root => d |
 CStrictL d2 gamma   => fill ( DStrict d d2) gamma  |
 CStrictR  d1 gamma => fill (DStrict d1 d)  gamma  |
CParL d2 gamma =>  fill  (DPar d d2) gamma |
 CParR  d1 gamma => fill (DPar d1 d) gamma |
CSeqL d2 gamma =>  fill  (DSeq d d2) gamma |
 CSeqR  d1 gamma => fill (DSeq d1 d) gamma 
end.


Require Import List.
Open Scope list_scope.


(* building a context from a seqDiag and a path 
  1 for left son, 2 for right son *)

(* I should use the monad notations :-) *)

Fixpoint diag2context_aux (d:seqDiag)(p:list nat)(g:context) : option context 
:=
 match d,p with 
 | d,nil => Some g
 |  DE e, _ => None
 | DStrict d1 d2, (1::p')  => diag2context_aux d1 p' (CStrictL  d2 g)
 | DStrict d1 d2, (2::p')  => diag2context_aux d2 p' (CStrictR  d1 g)
 | DPar d1 d2, (1::p')  => diag2context_aux d1 p' (CParL  d2 g)
 | DPar d1 d2, (2::p')  => diag2context_aux d2 p' (CParR  d1 g)
 | DSeq d1 d2, (1::p')  => diag2context_aux d1 p' (CSeqL  d2 g)
 | DSeq d1 d2, (2::p')  => diag2context_aux d2 p' (CStrictR  d1 g)
 | _,_ => None
end.

Definition  diag2context d path := diag2context_aux d path Root.      

 
(* Example *)

Parameters e1 e2 e3 e4 e5: event.

Definition d : seqDiag := DStrict (DE e1) 
                         (DStrict (DStrict (DE e1) (DE e2))
                                  (DStrict (DE e3) (DE e4))).

Definition og := diag2context d (2::1::2::nil).

Compute og.

Compute (match og with Some g => Some (fill (DE e5) g) | _ => None end).


Definition og' := diag2context d (2::2::nil).

Compute (match og' with Some g => Some (fill (DE e5) g) | _ => None end).