The Coq mailing list

[Coq User <coquser AT googlemail.com>]

Example CODE

Require Import String.
Require Import List.

Section Example.

(*Encoding of the Standard Example MetaModel*)
(*Top*)
CoInductive Top:Set :=
| Build_Top (name:string)
with 
Object:Set :=
| Build_Object (features:list Feature)(super:Top)
with 
Feature:Set :=
| Build_Feature (superfeat:Top)(featOwningObject:Object)
.
(*SpecialObject*)
CoInductive SpecialObject:Set :=

| Build_SpecialObject (info:string)(superObj:Object).


(*Top Functions*)
Definition name:Top -> string:=               
     (fun d:Top =>
         match d with
         | (Build_Top elName) => elName

         end).

(*Object Functions*)
Definition features:Object -> list Feature:=               
     (fun d:Object =>
         match d with
         | (Build_Object feats sup) => feats
         end).

Definition super:Object -> Top:=               
     (fun d:Object =>
         match d with
         | (Build_Object feats sup) => sup
         end).
Coercion super : Object >-> Top. (*Type Coercion*)

(*Feature Functions*)
Definition featOwningObject:Feature -> Object:=               
     (fun d:Feature =>
         match d with
         | (Build_Feature sup p) => p
         end).
Definition superfeat:Feature -> Top:=               

     (fun d:Feature =>
         match d with
         | (Build_Feature sup p) => sup
         end).
Coercion superfeat : Feature >-> Top. (*Type Coercion*)

(*SpecialObject Functions.*)
Definition info:SpecialObject -> string:=               

     (fun d:SpecialObject =>
         match d with
         | (Build_SpecialObject inf sup) => inf
         end).
Definition superObj:SpecialObject -> Object:=               
     (fun d:SpecialObject =>

         match d with
         | (Build_SpecialObject inf sup) => sup
         end).
Coercion superObj : SpecialObject >-> Object.

(*SpecialObject Subtypes*)
Record Singleton:Type := {superSingleton:>SpecialObject}.


(*Instantiaing a SpecialObject is where the error occurs.*)

(*SpecialObject Metamodel Instance*)
CoFixpoint singleton:SpecialObject := 
    Build_Singleton (*Several Levels of Inheritance*)
    (   (*Supertype of Singleton*)

        Build_SpecialObject "someString"
        (
           Build_Object (*Supertype of SpecialObject*)
           (featureOne::featureTwo::nil) (*List of related Example Feature*)
           (

               Build_Top (*Supertype of Object*)
               "singleton" (*Name.*)
           )
       ) 
    )
with
featureOne:Feature :=
    (
        Build_Feature
        (
            (Build_Top (*Supertype of Feature*)
            "featureOne" (*Name.*) 
            )
         
         ) singleton
     ) (*Object that owns the Feature *)
with
featureTwo:Feature := 
    (
        Build_Feature(
          Build_Top (*Supertype of Feature*)

          "featureTwo" (*Name.*)
        )
     ) 
     singleton (*Object that owns the Feature*)
.
End Example.