Signatures


(*          UNIVERSAL ALGEGRA          *)
(* Definition of (finite) signatures.  *)
(* Venanzio Capretta, January 1999     *)
(* Coq version 6.2.3                   *)

Require Export Finite_Sets.
Require Export PolyList.
Require Export Lists_Projections.

Section Signatures.

(* n will indicate the number of sorts.  *)
Variable n : nat.

(* Sorts are indicated by elements of the finite set with n elements.  *)
Local Sort := (Finite n).

(* Definition of the types of  functions  n sorts.        *)
(* A function type is represented as a pair of a list of  *)
(* argument sorts, and a result sort.                     *)

Definition Function_type : Set := (list Sort)*Sort.

End Signatures.

(* A signatures is a pair <n,l> where n is the number of sorts  *)
(* and l is a list of function types.                           *)
Record
Signature : Set := signature
  { sorts_num : nat;
    function_types : (list (Function_type sorts_num))
  }.

(* Some tools. *)

Implicit Arguments On.

Section Functions_Tools.

Variable n : nat. (* number of sorts *)

Variable f : (Function_type n).

(* List of arguments of a function type.  *)
Definition
function_type_arguments : (list (Finite n)) :=
(Fst f).

(* Arity of a function type: number of its arguments. *)
Definition
function_type_arity : nat :=
(length function_type_arguments).

(* n-th argument of a function type. *)
Definition
function_type_arg :
  (Finite function_type_arity) -> (Finite n) :=
(Fin_proj function_type_arguments).

(* Result sort of a function type. *)
Definition
function_type_result : (Finite n) :=
(Snd f).

End Functions_Tools.

Section Signatures_Tools.

Variable sigma : Signature.

Local n := (sorts_num sigma).

Local fs := (function_types sigma).

Definition
fun_num := (length fs).

Definition
nth_function := (Fin_proj fs).

Variable i : (Finite fun_num).

Local f := (nth_function i).

Definition
nth_arguments := (function_type_arguments f).
Definition
nth_arity := (function_type_arity f).
Definition
nth_arg := (function_type_arg 2!f).
Definition
nth_result := (function_type_result f).

End Signatures_Tools.

Implicit Arguments Off.

25/02/99, 14:36