module Terme: sig .. end
Fichier .mli (interface) non existante
Le type des termes
type ('a, 'b) t =
| |
Var of 'b |
| |
Operation of 'a * ('a, 'b) t list |
Termes sur un signature 'a
et une ensemble de variables 'b
Itérateurs sur les termes
val iter_term1 : ('a -> 'b) ->
('c -> 'd -> 'b) -> ('d -> 'b -> 'd) -> 'd -> ('c, 'a) t -> 'b
Itérateur sur les termes, première version.
On utilise List.map pour les calculs recursifs sur les fils.
On utilise List.fold_left, recursif terminal.
val iter_term2 : ('a -> 'b) ->
('c -> 'd -> 'b) -> ('d -> 'b -> 'd) -> 'd -> ('c, 'a) t -> 'b
Itérateur sur les termes, deuxième version.
On n'utilise pas List.map.
On utilise seulement List.fold_left.
val iter_term : ('a -> 'b) ->
('c -> 'd -> 'b) -> ('d -> 'b -> 'd) -> 'd -> ('c, 'a) t -> 'b
Itérateur sur les termes, version finale.
Il s'agit de iter_yerm2.
Opérations sur les termes
val vars : ('a, 'b) t -> 'b list
Calcul des variables dans un terme.
val occurs : 'a -> ('b, 'a) t -> bool
Est ce que une variable occurre un terme?.
Le type des substitutions
type ('a, 'b) s = ('b * ('a, 'b) t) list
Type des substitutions.
Une substitution est une liste de couple.
Chaque couple est formée par une variable de type 'b, et
d'un terme de type ('a,'b) t.
Opérations sur les substitutions (et les termes)
val apply_subst : ('a, 'b) s -> ('a, 'b) t -> ('a, 'b) t
Appliquer une substitition s à un terme t.
val compsubst1 : ('a, 'b) s ->
('b * ('a, 'b) t) list -> ('b * ('a, 'b) t) list
Calcul de la composition de deux substitutions.
Il s'agit de s2 o s1 :
d'abord on applilque s1 et puis on applique s2.
val compsubst2 : ('a, 'b) s ->
('b * ('a, 'b) t) list -> ('b * ('a, 'b) t) list
Calcul de la composition de deux substitution, deuxième version.
On se sert du fait que List.assoc cherche la premiere
occurrence dans une liste.
val compsubst : ('a, 'b) s -> ('a, 'b) s -> ('a, 'b) s
Calcul de la composition de deux substitution, version finale.
Filtrage
Filtrage, traitement des erreurs faible
exception Match_exc1
val add_subst1 : ('a, 'b) s -> 'b * ('a, 'b) t -> ('a, 'b) s
val matching1 : ('a, 'b) t * ('a, 'b) t -> ('a, 'b) s
Filtrage, première version
val matching2 : ('a, 'b) t * ('a, 'b) t -> ('a, 'b) s
Filtrage, deuxième version.
On intercepte les exception lévées par List.combine
Filtrage, traitement des erreurs amelioré
exception Match_exc of string
val add_subst2 : ('a, string) s -> string * ('a, string) t -> ('a, string) s
val matching3 : (string, string) t * (string, string) t ->
(string, string) s
Filtrage, version avec traitment d'erreurs.
val matching : (string, string) t * (string, string) t ->
(string, string) s
Filtrage, version finale.
Unification
val unify : (('a, 'b) t * ('a, 'b) t) list -> ('a, 'b) s
Unification