module Definition
imports String int
abstract syntax

Input = Input(ctx: Context, cl: ConstraintList, t: Term, ty: Type)

// comment

Type = Atom(name: String)
     | Composed(dom: TypeList, codom: Type)

TypeList = TyList(Type*)

Term = Var(name: /* comment */ String)
     | Fun(name: String, args: TermList)

TermList = TeList(Term*)

Constraint = Subtype(type1: String, type2: String)

ConstraintList = CList(Constraint*)

Jugement = SigOf(name: String, sig: Type)

Mapping = TypeOf(term: Term, sig: Type)
   
Context = Context(Jugement*)

Statement = Statement1(name: String, path: PathTree, ctx: Context, consequence1: Mapping)
          | Statement2(name: String, path: PathTree, ctx: Context, consequence2: Constraint)

Tree = SList(Statement*)

Label = Label(num: int)

PathTree = PTree(Label*)

Paths = Paths(PathTree*)