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 }.