#!/usr/bin/env python2
# -*- encoding: utf8 -*-

print "Salut.\n";

# INFO:
#	On va ici implémenter des fonctions de "model checking", c'est-à-dire qui calculent la valeur de vérité d'une formule donnée dans un modèle donné.
#	On va se limiter à la vérification de formules closes (c'est-à-dire sans variable libre).
#	Comme on peut prouver que l'interprétation d'une telle formule ne dépend pas de la fonction d'assignation, on va utiliser des fonctions d'assignations partielles (qui n'associent pas nécessairement de valeurs à toutes les variables).
#	En effet, pour interpréter une formule, on va partir d'une fonction d'assignation vide que l'on va "mettre à jour" lorsque l'on rencontre une quantificateur (voir dans le cours la règle d'interprétation des quantificateurs).

# Pour toute question : timothee.bernard@ens-lyon.org

def checkType(o, t, name):
	if not isinstance(o, t):
		print "type problem: variable", name, "(=", o , ") is not of type", t;

# Model
class Model:
	# domain: set of individuals
	# predDomain: dictionary; predicate to set of tuples of individuals
	def __init__(self, domain, predDomain):
		checkType(domain, set, "domain");
		checkType(predDomain, dict, "predDomain");
		
		self.domain = domain;
		self.predDomain = predDomain;
	
	def __str__(self):
		return "{" + str(self.domain) + "; " + str(self.predDomain) + "}";

# Example: m = Model({1,2,3}, {"P": {(1,1), (2,2), (3,3)}, "Q": {(1,1), (2,3), (3,2)}})


# Assignment function
class Assignment:
	# dico: dictionary; variable to individual
	def __init__(self, dico):
		checkType(dico, dict, "dico");
		
		self.dico = dico;
	
	# Renvoie la fonction d'assignation qui ne différe que par "x -> d"
	# x: variable
	# d: individual
	def assign(self, x, d):
		checkType(x, str, "x"); # On représente les variables par des chaînes de caractères
		checkType(d, int, "d"); # On représente les individus par des entiers
		
		newDico = {x: d};
		newDico.update(self.dico);
		
		return Assignment(newDico);
	
	# Renvoie la liste des valeurs associées aux variables de l ([x1, …, xn] -> [f(x1), …, f(xn)])
	# l: list of variables
	def map(self, l):
		checkType(l, list, "l");
		
		return [self.dico[x] for x in l];

# Logical language
class Formula:
	# Vérifie si la formule est vraie dans le modèle m
	# Utilise une fonction checkAux, définie pour chaque type de formules
	# m: model
	def check(self, m):
		checkType(m, Model, "m");
		
		return self.checkAux(m, Assignment({}));

# Predicate application
class Pred(Formula):
	# pred: predicate
	# args: list of individuals
	def __init__(self, pred, args):
		checkType(pred, str, "pred"); # On représente les prédicats par des chaînes de caractères
		checkType(args, list, "args");
		
		self.pred = pred;
		self.args = args;
	
	# Vérifie si la formule est vrai dans le modèle m pour la fonction d'assignation f
	# m: Model
	# f: Assignment
	def checkAux(self, m, f):
		checkType(m, Model, "m");
		checkType(f, Assignment, "f");
		
		return ((self.pred in m.predDomain) and (tuple(f.map(self.args)) in m.predDomain[self.pred]));
	
	def __str__(self):
		return str(self.pred) + "(" + ','.join([str(x) for x in self.args]) + ")";

# Créer des classes pour la négation ("Neg"), la coordination ("Coord") et la quantification existentielle ("Ex").






# Test
m = Model({1,2,3}, {"P": {(1,1), (2,2), (3,3)}, "Q": {(1,1), (2,3), (3,2)}});
print "Model:", m;
print "";

#p = Pred("P", ["x", "x"]);
#print p.checkAux(m, Assignment({"x": 1})); # True
#print "";

#p = Ex("x", Neg(Pred("P", ["x", "x"])));
#print p;
#print p.check(m); # False
#print "";

#p = Neg(Ex("x", Neg(Pred("P", ["x", "x"]))));
#print p;
#print p.check(m); # True
#print "";

#p = Neg(Ex("x", Ex("y", Coord(Pred("Q", ["x", "y"]), Neg(Pred("Q", ["y", "x"]))))));
#print p;
#print p.check(m); # True
#print "";


# Pour passer en logique modale :
#	– modifier la classe Model ;
#	– créer une classe pour la possibilité modale ;
#	– ajouter un argument à checkAux (pour le monde d'évaluation).