]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/projdat/database.ma
update in delayed_updating
[helm.git] / matita / matita / projdat / database.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "projdat/nth_proj.ma".
16
17 (* Definizione della funzione di proiezione n-esima su valori *)
18 let rec selection (l:DeqList DeqNat) s (t:DeqList s) ≝ 
19   match l with
20   [ nil ⇒ []
21   | cons a b ⇒ match (nth_opt ? a t ) with
22             [None ⇒  selection b s t
23             |Some w ⇒ w::(selection b s t)]
24   ].
25
26
27 (* Data una lista di associazioni ID-Valori ed una lista di id, restituisce una
28    tupla *)
29 definition ValueMap_tuple : ∀a. ∀b:(DeqList DeqNat). tuple (getSchema ( selection b ? (a))).
30 #a #b %
31   [@( ( selection b ? ( a)))
32   | //
33   ]
34 qed.
35
36
37 (* NOTA: tutte le mappe debbono essere riconvertite in liste, dove gli elementi
38   si ottengono non per id k *)
39
40 (* Definizione di un campo della tabella *)
41 record table_record (schema: DeqList DeqType) (Tvaluemap: DeqList DeqCoer) (id:ℕ) : Type[0] ≝ {
42   
43   (* Lista di id dei valori *)
44   Rids   : DeqList DeqNat;
45   
46   (* Preservazione dello schema *)
47   Rprop  : (getSchema (selection  Rids ? Tvaluemap)) = schema;
48   Rtuple : tuple schema;
49   RLen   : length ? Rids = length ? schema;
50   
51   (* Corrispondenza tra <chiavi,valoritupla>∈Tvaluemap *)
52   Rvalprop: getSchema (selection Rids ? (Sig_fst ? ? Rtuple)) =schema           (*All ? 
53            (λp. nth_opt ? (fst ?? p) (Tvaluemap)=Some ? (snd ?? p))
54            (compose DeqNat DeqCoer (DeqProd DeqNat DeqCoer) (λx,y. 〈x,y〉) ) *)          
55
56 }.
57
58 (* Definizione di una tabella, contraddistinta da una particolare mappa di 
59    associazione di tipi-etichette *)
60 record table (Tlabelmap: DeqList DeqType) (Tvaluemap: DeqList DeqCoer) : Type[0] ≝ {
61   Tid    : ℕ;                                   (* ID della tabella *)
62   Tschema: DeqList DeqType;                     (* Schema della tabella *)
63   Tids   : DeqList DeqNat;                      (* Elenco di identificativi dei tipi *)
64   cLen   : (length ? Tschema)=(length ? Tids);  (* Le liste hanno stessa lunghezza *)
65   
66   (* Impongo che le coppie di Tschema-Tids appartengano alla mappa di etichette *)
67   cAss   : All ? 
68             (λp. nth_opt ? (fst ?? p) (getSchema Tvaluemap)=Some ? (snd ?? p) )
69             (compose DeqNat DeqType (DeqProd DeqNat DeqType) (λx,y. 〈x,y〉) Tids Tschema)
70            ;
71    (* Le tuple devono avere lo stesso schema*)
72   Ttuples: list (table_record Tschema Tvaluemap Tid);
73   
74   
75   
76   (* Ed in particolare il loro schema *)
77   Preserv1: (Tschema=selection Tids DeqType Tlabelmap)
78   
79   
80                  
81 }.
82
83
84 (* Un database può essere visto come una lista di tabelle descritte come
85    sopra *)
86 record database (Tlabelmap: DeqList DeqType) ( Dvaluemap: DeqList DeqCoer) : Type[0] ≝ {
87   DB : list (table Tlabelmap Dvaluemap);
88   
89   (* Ogni tabella del DB deve avere  ID unico *)          
90   DTabUnique : uniqueb ? (map ? DeqNat (λx. Tid ?? x) DB)=true;
91   
92   (* Per poter riuscire a garantire la unicità delle assoc....*)
93   DBTables:  All ? (λp. length ? (Ttuples ?? p) > O) DB
94                                                 
95 }.