1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
//////////////////////////////////////////////////////////////////////////////
//Copyright 2008
// Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow
//////////////////////////////////////////////////////////////////////////////
// This file is part of Teyjus. //
// //
// Teyjus is free software: you can redistribute it and/or modify //
// it under the terms of the GNU General Public License as published by //
// the Free Software Foundation, either version 3 of the License, or //
// (at your option) any later version. //
// //
// Teyjus is distributed in the hope that it will be useful, //
// but WITHOUT ANY WARRANTY; without even the implied warranty of //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the //
// GNU General Public License for more details. //
// //
// You should have received a copy of the GNU General Public License //
// along with Teyjus. If not, see <http://www.gnu.org/licenses/>. //
//////////////////////////////////////////////////////////////////////////////
/****************************************************************************/
/* File hopu.h. This header file defines the interface components for the */
/* code in hopu.c that implements higher-order pattern unification. */
/* */
/****************************************************************************/
#ifndef HOPU_H
#define HOPU_H
#include "mctypes.h"
#include "dataformats.h"
/* A flag denoting whether new structure is created during the process of */
/* finding substitutions. */
extern Boolean HOPU_copyFlagGlb;
/* Return the dereference of the abstraction body of the given term. */
DF_TermPtr HOPU_lamBody(DF_TermPtr tPtr);
/* Globalize a rigid term and make a variable binding. */
/* If the term pointer to the rigid term is not one referring to a heap */
/* address, its atomic content is then copied into the variable to be bound*/
/* Otherwise, the variable is made a reference to the rigid term. */
void HOPU_globalizeCopyRigid(DF_TermPtr rPtr, DF_TermPtr vPtr);
/* Globalize a flex term. */
/* If the term pointer is one referring to a stack address, (in which case */
/* the flex term must be a free variable itself), the atomic content is */
/* copied onto the current top of heap; the free variable on stack is then */
/* bound to the new heap term, and the binding is trailed if necessary; the */
/* term pointer is updated to the new heap term. */
DF_TermPtr HOPU_globalizeFlex(DF_TermPtr fPtr);
/* Try to find the (partial) structure of the substitution for a flex head */
/* of a LLambda term corresponding to an internal flex term which is not */
/* known to be LLambda in the compiled form of pattern unification. */
DF_TermPtr HOPU_flexNestedSubstC(DF_TermPtr fhPtr, DF_TermPtr args, int nargs,
DF_TermPtr tmPtr, int emblev);
/* Try to find the (partial) binding of the head of a flex term when */
/* unifying it with a rigid term possible under abstractions in the compiled*/
/* form of pattern unification. */
DF_TermPtr HOPU_rigNestedSubstC(DF_TermPtr rhPtr, DF_TermPtr rPtr,
DF_TermPtr args, int rnargs, int emblev);
/* Interpretively pattern unify first the pairs delayed on the PDL, then */
/* those delayed on the live list, if binding occured during the first step */
/* or previous compiled unification process. */
/* Upon successful termination, PDL should be empty and pairs left on the */
/* live list should be those other than LLambda. */
void HOPU_patternUnify();
/* Interpretively pattern unify a pair of terms given as parameters. This is*/
/* the counter part of HOPU_patterUnifyPDL that is invoked from the compiled*/
/* part of unification. In this situation, the procedure has to be applied */
/* to two terms as opposed to pairs delayed on the PDL stack. */
/* */
/* The input term pointers may dereference to register and stack addresses */
/* Care must be taken to avoid making a reference to a register (stack) */
/* address in binding a variable, and in making a disagreement pair. */
void HOPU_patternUnifyPair(DF_TermPtr tPtr1, DF_TermPtr tPtr2);
#endif //HOPU_H
|
