-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathxtc.ml
115 lines (73 loc) · 2.51 KB
/
xtc.ml
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
(******************************************************************************
Rainbow, a termination proof certification tool
See the COPYRIGHTS and LICENSE files.
- Frederic Blanqui, 2009-08-28
internal representation of XTC files version 0.4
******************************************************************************)
(* we follow the structure of xtc.xsd:
- a top-level element/group is translated into a type definition
with the same name
- an element/group definition is translated into a type expression
- a choice is translated into a concrete data type T, and
constructor names are prefixed by a prefix of the name of T
- a sequence of non fixed length is translated into a list
- a sequence of fixed length is translated into a tuple
- an element occuring at most once is translated into an option
type except for lists and strings
*)
open Xml;;
type bound =
| BoundUnknown
| BoundPoly
| BoundOn of int;;
type automatonstuff = string;;
type startterm =
| STNone
| STConstructorBased
| STFull
| STAutomaton of automatonstuff;;
type entry = int;;
type var = string;;
type replacementmap = entry list;;
type name = string;;
type typ =
| TypeBasic of string
| TypeArrow of typ * typ;;
type term =
| TermVar of var
| TermFunapp of funapp
| TermLam of var * typ * term
| TermApp of term * term
and funapp = name * term list;;
type arg = term;;
type lhs = term;;
type rhs = term;;
type author = string;;
type date = string;;
type comment = (author * date) * xml list;;
type condition = lhs * rhs;;
type conditions = condition list;;
type rule = lhs * rhs * conditions;;
type originalfilename = string;;
type metainformation = originalfilename list * author * date * comment option;;
type status =
| StatusNone
| StatusNo
| StatusMaybe
| StatusYes of (bound * bound) option;;
type strategy = StratFull | StratInnermost | StratOutermost;;
type conditiontype = CTNone | CTJoin | CTOriented | CTOther;;
type theory = ThyNone | ThyA | ThyC | ThyAC;;
type arity = int;;
type funcsym = name * arity * theory * replacementmap option;;
type varDeclaration = var * typ;;
type funcDeclaration = name * (typ list * typ);;
type signature =
| SignFO of funcsym list
| SignHO of varDeclaration list * funcDeclaration list;;
type relrules = rule list;;
type rules = rule list * relrules;;
type xtc_type = Term | Comp;;
type trs = rules * signature * comment option * conditiontype;;
type problem = xtc_type * trs * strategy * startterm * status
* metainformation option;;