metoo et lambda expressions

Revoir le cours de Spec1 sur B

Application à metoo

Ex. 1
Vous avez entré
union-a-b(a1, b1);
Tapez
union-a-b;
metoo répond
lambda(a1, b1). '(metoo set union a1 b1)'.

Ex2
Tapez
union_a_b();
metoo attendait un ensemble (c'est le type des opérandes de l'opérateur union), mais il a trouvé False. En effet, les arguments non trouvés étant remplacés par False, metoo essaie quand même d'évaluer la lambda expression. Dans ce cas, l'échec est patent.

Ex 3
essai(ens, dom, ran) == ens overwr {dom -> ran};
construit un ensemble de maplets (de couples)

Tapez
essai({}, d1, r1);
metoo renvoie une image du maplet créé
{d1 -> r1};
Tapez
essai({d1 -> r1}, d2, r2);
metoo renvoie
{d1 -> r1, d2 -> r2};
Tapez maintenant
essai({d1 -> r1});
Il manquait deux arguments, mais metoo a quand même évalué la fonction et on observe :
'd1-> r1, false -> false};
Tapez maintenant
union_a_b(1, 2);
metoo repond encore que les types des opérandes sont erronés, car on trouve des integers au lieu d'ensembles

Voyons les fonctions prédéfinies de metoo telles que :

inv_

Tapons
inv_cte;
metoo répond
TRUE;
On constate qu'alors que nous avons oublié de définir cet invariant, metoo le considère comme vrai. Normal. Un invariant est une contrainte. TRUE c'est le moins contraignant !

mk_

Tapons
mk_cpte;

metoo répond

lambda(arg-2, arg-1). '(metoo-construct-rec (quote cpte) (quote (comp1 comp2)) (list arg-2 arg-1) inv_cpte)';

Ainsi vous voyez que :
mk_cpte est une lambda expression :

• qui a deux arguments, les champs définis
• qui évalue inv_cpte
• et qui rend une liste enregistrant les constructions faites, pour les stocker en mémoire.

Tapons
mk_cpte();
metoo répond
mk_cpte(false, false).