]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/terms.ml
commitcompleted: some files were missing :(
[helm.git] / matita / 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 | Invertible
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 let is_eq_clause (_,l,_,_) =
50   match l with
51     | Equation _ -> true
52     | Predicate _ -> false
53 ;;
54
55 let vars_of_term t =
56   let rec aux acc = function
57     | Leaf _ -> acc
58     | Var i -> if (List.mem i acc) then acc else i::acc
59     | Node l -> List.fold_left aux acc l
60   in aux [] t
61 ;;
62
63 module OT =
64  struct
65    type t = int 
66    let compare = Pervasives.compare
67  end
68
69 module M : Map.S with type key = int 
70   = Map.Make(OT) 
71
72 type 'a bag = int
73               * (('a unit_clause * bool * int) M.t)
74
75   let add_to_bag (_,lit,vl,proof) (id,bag) =
76     let id = id+1 in
77     let clause = (id, lit, vl, proof) in
78     let bag = M.add id (clause,false,0) bag in
79     (id,bag), clause 
80    ;;
81
82   let replace_in_bag ((id,_,_,_),_,_ as cl) (max_id,bag) =
83     let bag = M.add id cl bag in
84       (max_id,bag)
85   ;;
86
87   let get_from_bag id (_,bag) =
88     M.find id bag
89   ;;
90     
91   let empty_bag = (0,M.empty);;
92
93 module type Blob =
94   sig
95     type t
96     val eq : t -> t -> bool
97     val compare : t -> t -> int
98     val eqP : t
99     val is_eq: t foterm -> (t foterm* t foterm *t foterm) option 
100     val pp : t -> string
101     type input
102     val embed : input -> t foterm
103     val saturate : input -> input -> t foterm * t foterm
104   end
105