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