]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/terms.ml
....
[helm.git] / helm / software / components / ng_paramodulation / terms.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 type 'a foterm = 
15   | Leaf of 'a
16   | Var of int
17   | Node of ('a foterm) list
18
19 type 'a substitution = (int * 'a foterm) list
20
21 type comparison = Lt | Eq | Gt | Incomparable
22
23 type rule = Superposition | Demodulation
24 type direction = Left2Right | Right2Left | Nodir
25 type position = int list
26
27 type 'a proof =
28   | Exact of 'a foterm
29   | Step of rule * int * int * direction * position * 'a substitution
30          (* rule, eq1, eq2, direction of eq2, position, substitution *)
31
32 type 'a literal = 
33  | Equation of    'a foterm  (* lhs *)
34                 * 'a foterm  (* rhs *)
35                 * 'a foterm  (* type *)
36                 * comparison (* orientation *)
37  | Predicate of   'a foterm 
38
39 type varlist = int list
40
41 type 'a unit_clause =
42    int        (* ID *)
43  * 'a literal
44  * varlist       (* variable list *)
45  * 'a proof      (* proof *)
46
47 type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
48
49
50 module OT =
51  struct
52    type t = int 
53    let compare = Pervasives.compare
54  end
55
56 module M : Map.S with type key = int 
57   = Map.Make(OT) 
58
59 type 'a bag = ('a unit_clause * bool) M.t
60
61 module type Blob =
62   sig
63     type t
64     val eq : t -> t -> bool
65     val compare : t -> t -> int
66     val eqP : t
67     val pp : t -> string
68     type input
69     val embed : input -> t foterm
70     val saturate : input -> input -> t foterm * t foterm
71   end
72