The Coq mailing list

[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 := 
 Hole |
 CStrictL : context -> seqDiag -> context |
 CStrictR : seqDiag -> context  -> context |
CParL : context -> seqDiag -> context |
 CParR : seqDiag -> context  -> context |
CSeqL : context -> seqDiag -> context |
 CSeqR : seqDiag -> context  -> context .

(* replacing the hole with d *)

Fixpoint fill (d:seqDiag) (gamma:context) :seqDiag :=
match gamma with
 Hole => d |
 CStrictL gamma  d' => DStrict (fill  d gamma) d' |
 CStrictR  d' gamma => DStrict d' (fill d gamma)  |
CParL gamma  d' => DPar (fill  d gamma) d' |
 CParR  d' gamma => DPar d' (fill d gamma) |
CSeqL gamma  d'  => DSeq (fill  d gamma) d' |
 CSeqR d' gamma => DSeq d' (fill 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 (d:seqDiag)(p:list nat) : option context :=
 match d,p with 
 | d,nil => Some Hole
 |  DE e, _ => None
 | DStrict d1 d2, (1::p')  => match diag2context d1 p' with
                                Some g => Some (CStrictL g d2) | _ => None end
 | DStrict d1 d2, (2::p')  => match diag2context d2 p' with
                                Some g => Some (CStrictR d1 g) | _ => None end
 | DPar d1 d2, (1::p')  => match diag2context d1 p' with
                                Some g => Some (CParL g d2) | _ => None end
 | DPar d1 d2, (2::p')  => match diag2context d2 p' with
                                Some g => Some (CParR d1 g) | _ => None end
 | DSeq d1 d2, (1::p')  => match diag2context d1 p' with
                                Some g => Some (CSeqL g d2) | _ => None end
 | DSeq d1 d2, (2::p')  => match diag2context d2 p' with
                                Some g => Some (CSeqR d1 g) | _ => None end
 | _, _ => None
end.
        
(* Example *)

Parameters e1 e2 e3 e4 e5: event.

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

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

Compute og.

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