/* Pour comprendre cette partie je pense qu'il est indispensable de lire la documentation http://url.bobu.eu/3rH. Le mathématicien pourrait penser qu'il s'agit là d'informatique, mais les types Lazi rejoignent la notion de structure en mathématique. On pourra par exemple voir un groupe (au sens mathématique) comme un type et produire des théorèmes sur les groupes en utilisant les types Lazi. Bien que la notion de type défini ici soit proche des mathématiques nous utilisons le vocabulaire informatique car il est plus développée en matière d'organisation, ce dont nous avons besoin à la base. Les types définis ici sont souvent paramétrables, par exemple le type "pairT" nécessite les paramètres des types des deux éléments de la paire. On pourrait définir des fonctions prenant en argument ces paramètres et retournant le type. Si on faisait ainsi on se priverait de la possibilité de modifier par la suite une partie de ces paramètres. Prenons un exemple: si un type est en paramètre, il peut être construit à partir d'autres données (comme par exemple un dictionnaire de types), et on peut vouloir par la suite modifier une de ces données. Pour réaliser simplement cette fonctionalité, les paramètres des types ne seront simplement par fournis! Il suffirat d'utiliser l'union d'objets pour les fournir. Ainsi on peut voir une des définitions suivantes de types comme une base à laquelle, pour l'utiliser, on doit ajouter des entrées. */ /// Utilitaires // Est-ce que i est une instance de o $Def isInstance = $F i,o → o .o'domain i $Operator ∈t infix 20 isInstance // Est-ce que i n'est pas une instance de o $Def isNotInstance = $F i,o → ¬b i ∈t o $Operator ∉t infix 20 isNotInstance /// /// Types structurels /// // Ce sont des types utilisés comme structure d'autres types. /// nothingT /* Type de domaine vide. Comme il n'y a aucune instance la fonction "equal" et "object" ne peuvent être appelées sur des instances. */ $Def nothingT = $O[ domain = constF 0b ] /// anythingT /* Type "tout". Toutes les instances sont égales et ont pour objet 1b. */ $Def anythingT = $O[ domain = constF 1b, equal = $F i,j → 1b, object = 1b ] /// /// Types conteneurs /// /* Ce sont des types servant à contenir des éléments quelconques (comme le type des paires, des listes etc). Leurs objets possèdent en plus les fonctions : map et fold. L'ordre du fold n'est pas garantie. Nous utiliseront le terme "uniform" et son abréviation "uni" pour indiquer que les éléments du conteneur sont de même type. */ /// Le type "dynpairT" /* Type ``pair'' dynamique, dans le sens où le type du deuxième élément dépend du premier élément. Paramètres: - t1 : le type du premier élément, - t2f : fonction qui prend en argument la première valeur de la paire et retourne le type du second élément. */ $Def dynPairT = $O($O[t1,t2f])[ domain = $F i@$T[x1,x2] → isPair i ∧b x1 ∈t t1 ∧b x2 ∈t t2f x1 , equal = $F $T[x1,x2],$T[y1,y2] → (t1 .o'equal) x1 y1 ∧b (t2f x1 .o'equal) x2 y2 , object = $F $T[x1,x2] → $T[t1 .o'object x1 , t2f x1 .o'object x2 ] , map = $F $T[x1,x2],f → $T[ f t1 x1 , f (t2f x1) x2 ] , fold = $F $T[x1,x2],f,r → f (t2f x1) (f t1 r x1) x2 ] /// Le type "pairT" /* Type ``pair'',t1 et t2 sont les types des éléments de gauche et droite. Paramètres: - t1: type du premier élément. - t2: type du deuxième élément. */ $Def pairT = dynPairT ∪o $O($O[t2])[ t2f = constF t2 ] /// Le type "uniPairT" /* Type ``pair'' où les deux éléments ont le type t. */ $Def uniPairT = pairT ∪o $O($O[t])[t1=t,t2=t] /// Le type "uniListT" /* Type d'une liste dont les éléments sont de type t. */ $Def uniListT = $O($O[t])[ domain = $F i → isList i ∧b ∀lr x/i; x ∈t t , // On utilise un fold sans utiliser accumulateur, nous sommes juste interessé à savoir s'il y a une erreur. equal = $F i,j → listEqual (t .o'equal) i j , object = $F i → listMap (t .o'object) i , map = $F i,f → listMap f i , fold = $F i,f,r → fwListFold f r i ] /// liste non vide /* toNonEmptyListTF transforme un type de liste en un type similaire ajoutant la condition que la liste ne doit pas être vide. */ $Def toNonEmptyListTF = modObj 'domain $F f → $F i → f i ∧b notEmptyList i /// Le type "uniSetT" /* Comme uniListT mais voit l'instance comme un ensemble : cela change l'égalité. */ $Def uniSetT = uniListT ∪o $O($O[t])[ equal = $F i,j → listSetEqual (t .o'equal) i j ] /// Le type "uniChoosedListT" /* Type d'une liste dont les éléments sont de type t et vérifiant une propriété p. */ $Def uniChoosedListT = $O($O[t,p])[ domain = $F i → isList i ∧b ∀lr x/i; x ∈t t ∧b p x ] /// Le type "dynListT" /* Type d'une liste dont les éléments sont de type dynamique: le type du premier élément est donné, le type d'un élément suivant est calculé en fonction du type et de la valeur de l'élément précédent. Les paramètres sont : - la fonction de calcul du type de l'élément suivant, elle a pour arguments: - le type de l'élément actuel - la valeur de l'élément actuel - le type du premier élément Remarque : ∅l est une instance. */ $Def dynListT = $O($O[next,t])[ domain = $F i → isList i ∧b isThing \ fwListFoldMaybe ( $F t2,x → if(x ∈t t2; just \ next t2 x; nothing) ) t i , equal = $F i,j → isThing \ fw2listFoldMaybe ($F t2,ix,jx → if(t2 .o'equal ix jx ; just \ next t2 ix ; nothing)) t i j , // On calcul la liste d'objets correspondante. object = $F i → listFoldMap ($F t2,x →t2 .o'object x) next t i , // f prend en premier argument le type de l'élément à mapper. map = $F i,f → listFoldMap f next t i , // f prend en premier argument le type de l'élément. // On utilise un accumulateur double (par une paire) : $T[type de l'élément suivant, accumulateur]. fold = $F i,f,r → pairSecond \ fwListFold ($F $T[t2,r2],x → $T[next t2 x,f t r2 x]) $T[t,r] i ] /// dynDictT // Il arrive que le type d'une entrée d'un dictionnaire dépende de la valeur de l'instance d'une autre entrée. Il nous faut alors un type de dictionnaire où le dictionnaire des types puisse utiliser certaines valeurs de l'instance. Pour réaliser cela le paramètre de dynDictT est une fonction prenant en argument une chose (qui est sensée être une instance) et retourne le dictionnaire des types. Remarquons que pour que l'utilisation de dynDictT ait un sens il faut qu'une entrée du dictionnaire des types ne dépende pas des entrées suivantes ou d'elle-même dans l'instance. /* Type des dictionnaires dynamiques. Le paramètre est : -dtf: fonction prenant en argument une chose sensée être une instance et retournant le dictionnaire des types. */ $Def dynDictT = $O($O[dtf])[ domain = $F i → isDict i ∧b wordListEqual ( dictEntries (dtf i) , dictEntries i ) ∧b listAnd \ dictValues \ dict2Map isInstance i \ dtf i , equal = $F i,j → listAnd \ dictValues \ dict2Map apply ( dict2Map ( $F t → t .o'equal ) (dtf i) i ) j , object = $F i → dict2Map ( $F t,v → t .o'object v ) (dtf i) i , // Notons que f a pour premier argument le type de la valeur. map = $F i,f → dict2Map ( $F t,v → f t v ) (dtf i) i , // Notons que f a pour premier argument le type de la valeur. fold = $F i,f,r → fwListFold ($F r2,$T[k,v] → f ((dtf i) .o k) r2 v) r i ] /// dictT /* Version statique de dynDictT où les types ne dépendent pas de l'instance. Le paramètre est : - dt: le dictionnaire des types. */ $Def dictT = dynDictT ∪o $O($O[dt])[ dtf = constF dt ] /// uniDictT // Le type ``uniDictT t'' est le type d'un dictionnaire où toutes les valeurs on le même type t. /* Type des dictionnaires, t est le type des valeurs. */ $Def uniDictT = $O($O[t])[ domain = $F i → isDict i ∧b // les valeurs doivent avoir le type demandé ∀l x/dictValues i; x ∈t t , equal = $F i,j → wordListEqual ( dictEntries i , dictEntries j ) ∧b listAnd ( dictValues \ dict2Map (t .o'equal) i j ) , object = $F i → dictMap (t .o'object) i , map = $F i,f → dictMap f i , fold = $F i,f,r → fwListFold ($F r2,$T[k,v] → f r2 v) r i ] /// uniDictFixT /* Le type ``uniDictFixT kl t'' est comme un uniDictT mais où les clés sont fixées par la liste kl. */ $Def uniDictFixT = uniDictT ∪o $O($O[kl,t])[ domain = $F i → i ∈t (uniDictT ∪od $D[ t = t ]) ∧b wordListEqual (dictEntries i) kl ] /// /// Autres types /// /// wordT /* Le type "mot". */ $Def wordT = $O[ domain = isWord , equal = wordEqual , object = $F i -> i ] /// wordChoosedT /* Le type "mot" où les mots sont sélectionnés par "filter". */ $Def wordChoosedT = wordT ∪o $O($O[filter])[ domain = $F w → isWord w ∧b filter w ] /// wordExtT /* Le type "mot" où les mots sont sélectionnés par une définition par extension : la liste wordList. */ $Def wordExtT = wordChoosedT ∪o $O($O[wordList])[ filter = listHasWord wordList ] /// unionT /* unionT est une union de types. unionT prend en paramètre le dictionnaire "types" des types dont on fait l'union. Le nom associé à chaque type permet de les différencier dans la construction des instances. Les types composants le type union sont appelés les "types composants". Une instance de unionT est la paire (nom, instance du type de ce nom). L'objet est l'objet du type sous ce nom. Paramètre: -types: le dictionnaire des types. */ $Def unionT = $O($O[types])[ domain = $F p@$T[name,i] → isPair p ∧b isWord name ∧b isDictEntry name types ∧b i ∈t getType name , equal = $F $T[name1,i1],$T[name2,i2] → wordEqual name1 name2 ∧b getType name1 .o'equal i1 i2 , object = $F $T[name,i] → getType name .o'object i , // Retourne le type à partir de son nom. getType = $F typeName → types .d typeName , // Ajoute un type constituant "t" de nom "n" et nécessitant le paramètre de nom "un" du type union. // Remarque: this2 représente le nouveau unionT puisque l'on transforme un objet "o" en dictionnaire par "o o" et que this2 est ce "o". Quand à "this", il ne contient pas le type ajouté. addConstituent = $F n,t,un → objDynMod this 'types $F this2 → addToDict n \ objAdd t un this2 , // Appelle une fonction "funcName" du type constituant. Fonctionne seulement si l'instance est le premier argument de la fonction à appeler. callPureVirtual = $F funcName → $F $T[typeName,j] → getType typeName .o funcName j , // Appelle une fonction "funcName" du type constituant, si le type n'existe pas, on retourne f sur l'instance. Fonctionne seulement si l'instance est le premier argument de la fonction à appeler et de la fonction par défaut. callVirtual = $F funcName,f → $F i@$T[typeName,j] → maybeMap( objApplyMaybe (getType typeName) funcName, applyArg j, f i ) , // Appelle une fonction de mapping "funcName" qui retourne une instance du type constituant, retourne cette instance transformée en instance du type union. Par défaut retourne l'instance en argument. // La fonction m est la fonction à mapper sur l'instance, elle est passée en argument à la fonction "map" spécialisée qui prend en argument une instance (du type constituant), m et retourne une instance du type constituant. // Généralement m prend en argument le type union, une instance du type constituant et retourne instance du type constituant. callMap = $F funcName,i@$T[typeName,j],m → // map est la valeur de l'entrée "funcName", c'est la fonction de mapping à appeler. maybeMap(objApplyMaybe (getType typeName) funcName, $F map → $T[typeName,map j m], i) ] // Remarque: l'instance est l'unique argument considéré par callVirtual et callPureVirtual, cela n'empêche pas d'avoir d'autres arguments par la suite puisqu'une fonction peut retourner. /* Teste si le type d'une instance d'union a un certain nom. */ $Def hasTypeName = $F name,i → wordEqual name \ pairFirst i /* Teste si le type d'une instance d'union a un certain nom parmi une liste. */ $Def hasTypeNameAmong = $F wl,i → listHasWord wl \ pairFirst i /* Construit le type de l'union à partir du nom du type constituant et d'une de ses instances. */ $Def liftInstance = pair