1 /*-----------------------------------------------------------------------
2 
3 File  : cle_annoterms.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Terms and term sets with annotation lists.
10 
11   Copyright 1998, 1999 by the author.
12   This code is released under the GNU General Public Licence and
13   the GNU Lesser General Public License.
14   See the file COPYING in the main E directory for details..
15   Run "eprover -h" for contact information.
16 
17 Changes
18 
19 <1> Tue Jul 20 17:22:38 MET DST 1999
20     New
21 
22 -----------------------------------------------------------------------*/
23 
24 #ifndef CLE_ANNOTERMS
25 
26 #define CLE_ANNOTERMS
27 
28 #include <cle_annotations.h>
29 #include <cle_clauseenc.h>
30 
31 /*---------------------------------------------------------------------*/
32 /*                    Data type declarations                           */
33 /*---------------------------------------------------------------------*/
34 
35 typedef struct annotermcell
36 {
37    Term_p              term;       /* Usually shared with reference*/
38    Annotation_p        annotation; /* May be one, may be a list */
39 }AnnoTermCell, *AnnoTerm_p;
40 
41 typedef struct annosetcell
42 {
43    TB_p           terms; /* Of real terms */
44    NumTree_p      set;   /* Of AnnoTerms, indexed by term->entry_no */
45    PatternSubst_p subst; /* Usually shared among all terms in set */
46    long           annotation_no;
47 }AnnoSetCell, *AnnoSet_p;
48 
49 
50 /*---------------------------------------------------------------------*/
51 /*                Exported Functions and Variables                     */
52 /*---------------------------------------------------------------------*/
53 
54 #define AnnoTermCellAlloc() (AnnoTermCell*)SizeMalloc(sizeof(AnnoTermCell))
55 #define AnnoTermCellFree(junk)         SizeFree(junk, sizeof(AnnoTermCell))
56 
57 AnnoTerm_p AnnoTermAlloc(Term_p term, Annotation_p annos);
58 AnnoTerm_p AnnoTermAllocNoRef(Term_p term, Annotation_p annos);
59 void       AnnoTermFree(TB_p bank, AnnoTerm_p junk);
60 #define    AnnoTermFreeNoRef(junk) AnnoTermCellFree(junk)
61 AnnoTerm_p AnnoTermParse(Scanner_p in, TB_p bank, long expected);
62 void       AnnoTermPrint(FILE* out, TB_p bank, AnnoTerm_p term, bool
63           fullterms);
64 void       AnnoTermRecToFlatEnc(TB_p bank, AnnoTerm_p term);
65 
66 
67 #define AnnoSetCellAlloc() (AnnoSetCell*)SizeMalloc(sizeof(AnnoSetCell))
68 #define AnnoSetCellFree(junk)         SizeFree(junk, sizeof(AnnoSetCell))
69 
70 AnnoSet_p  AnnoSetAlloc(TB_p bank);
71 void       AnnoSetFree(AnnoSet_p junk);
72 void       AnnoSetFreeNoRef(AnnoSet_p junk);
73 bool       AnnoSetAddTerm(AnnoSet_p set, AnnoTerm_p term);
74 AnnoSet_p  AnnoSetParse(Scanner_p in, TB_p bank, long expected);
75 void       AnnoSetPrint(FILE* out, AnnoSet_p set);
76 bool       AnnoSetComputePatternSubst(PatternSubst_p subst, AnnoSet_p
77                    set);
78 long       AnnoSetRemoveByIdent(AnnoSet_p set, long set_ident);
79 long       AnnoSetRemoveExceptIdentList(AnnoSet_p set, PStack_p
80                set_idents);
81 long       AnnoSetFlatten(AnnoSet_p set, PStack_p set_idents);
82 void       AnnoSetNormalizeFlatAnnos(AnnoSet_p set);
83 
84 long       AnnoSetRecToFlatEnc(TB_p bank, AnnoSet_p set);
85 
86 #endif
87 
88 /*---------------------------------------------------------------------*/
89 /*                        End of File                                  */
90 /*---------------------------------------------------------------------*/
91 
92 
93 
94 
95 
96