author | quigley |
Fri, 26 Aug 2005 19:36:07 +0200 | |
changeset 17150 | ce2a1aeb42aa |
parent 16976 | 377962871f5d |
child 17230 | 77e93bf303a5 |
permissions | -rw-r--r-- |
15347 | 1 |
(* Author: Jia Meng, Cambridge University Computer Laboratory |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
2 |
|
15347 | 3 |
ID: $Id$ |
4 |
Copyright 2004 University of Cambridge |
|
5 |
||
6 |
ML data structure for storing/printing FOL clauses and arity clauses. |
|
7 |
Typed equality is treated differently. |
|
8 |
*) |
|
9 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
10 |
(* works for writeoutclasimp on typed *) |
15347 | 11 |
signature RES_CLAUSE = |
12 |
sig |
|
13 |
exception ARCLAUSE of string |
|
14 |
exception CLAUSE of string |
|
15 |
type arityClause |
|
16 |
type classrelClause |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
17 |
val classrelClauses_of : string * string list -> classrelClause list |
15347 | 18 |
type clause |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
19 |
val init : theory -> unit |
15347 | 20 |
val keep_types : bool ref |
21 |
val make_axiom_arity_clause : |
|
22 |
string * (string * string list list) -> arityClause |
|
23 |
val make_axiom_classrelClause : |
|
15531 | 24 |
string * string option -> classrelClause |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
25 |
|
15347 | 26 |
val make_axiom_clause : Term.term -> string * int -> clause |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
27 |
|
15347 | 28 |
val make_conjecture_clause : Term.term -> clause |
29 |
val make_conjecture_clause_thm : Thm.thm -> clause |
|
30 |
val make_hypothesis_clause : Term.term -> clause |
|
31 |
val special_equal : bool ref |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
32 |
val clause_info : clause -> string * string |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
33 |
val typed : unit -> unit |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
34 |
val untyped : unit -> unit |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
35 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
36 |
val dfg_clauses2str : string list -> string |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
37 |
val clause2dfg : clause -> string * string list |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
38 |
val clauses2dfg : clause list -> string -> clause list -> clause list -> |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
39 |
(string * int) list -> (string * int) list -> string list -> string |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
40 |
val tfree_dfg_clause : string -> string |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
41 |
|
15347 | 42 |
val tptp_arity_clause : arityClause -> string |
43 |
val tptp_classrelClause : classrelClause -> string |
|
44 |
val tptp_clause : clause -> string list |
|
45 |
val tptp_clauses2str : string list -> string |
|
15608 | 46 |
val clause2tptp : clause -> string * string list |
47 |
val tfree_clause : string -> string |
|
16953 | 48 |
val schematic_var_prefix : string |
49 |
val fixed_var_prefix : string |
|
50 |
val tvar_prefix : string |
|
51 |
val tfree_prefix : string |
|
52 |
val clause_prefix : string |
|
53 |
val arclause_prefix : string |
|
54 |
val const_prefix : string |
|
55 |
val tconst_prefix : string |
|
56 |
val class_prefix : string |
|
15347 | 57 |
end; |
58 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
59 |
structure ResClause: RES_CLAUSE = |
15347 | 60 |
struct |
61 |
||
62 |
(* Added for typed equality *) |
|
63 |
val special_equal = ref false; (* by default,equality does not carry type information *) |
|
64 |
val eq_typ_wrapper = "typeinfo"; (* default string *) |
|
65 |
||
66 |
||
67 |
val schematic_var_prefix = "V_"; |
|
68 |
val fixed_var_prefix = "v_"; |
|
69 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
70 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
71 |
val tvar_prefix = "Typ_"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
72 |
val tfree_prefix = "typ_"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
73 |
|
15347 | 74 |
|
75 |
val clause_prefix = "cls_"; |
|
76 |
||
77 |
val arclause_prefix = "arcls_" |
|
78 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
79 |
val const_prefix = "const_"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
80 |
val tconst_prefix = "tconst_"; |
15347 | 81 |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
82 |
val class_prefix = "class_"; |
15347 | 83 |
|
84 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
85 |
|
15347 | 86 |
(**** some useful functions ****) |
87 |
||
88 |
val const_trans_table = |
|
89 |
Symtab.make [("op =", "equal"), |
|
90 |
("op <=", "lessequals"), |
|
91 |
("op <", "less"), |
|
92 |
("op &", "and"), |
|
93 |
("op |", "or"), |
|
94 |
("op -->", "implies"), |
|
95 |
("op :", "in"), |
|
96 |
("op Un", "union"), |
|
97 |
("op Int", "inter")]; |
|
98 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
99 |
|
15347 | 100 |
|
15610 | 101 |
(*Escaping of special characters. |
102 |
Alphanumeric characters are left unchanged. |
|
103 |
The character _ goes to __ |
|
104 |
Characters in the range ASCII space to / go to _A to _P, respectively. |
|
105 |
Other printing characters go to _NNN where NNN is the decimal ASCII code.*) |
|
106 |
local |
|
107 |
||
108 |
val A_minus_space = Char.ord #"A" - Char.ord #" "; |
|
109 |
||
15347 | 110 |
fun ascii_of_c c = |
15610 | 111 |
if Char.isAlphaNum c then String.str c |
112 |
else if c = #"_" then "__" |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
113 |
else if c = #"'" then "" |
15610 | 114 |
else if #" " <= c andalso c <= #"/" |
115 |
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) |
|
116 |
else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c)) |
|
117 |
else "" |
|
15347 | 118 |
|
15610 | 119 |
in |
120 |
||
121 |
val ascii_of = String.translate ascii_of_c; |
|
122 |
||
123 |
end; |
|
15347 | 124 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
125 |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
126 |
(*Remove the initial ' character from a type variable, if it is present*) |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
127 |
fun trim_type_var s = |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
128 |
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
129 |
else error ("trim_type: Malformed type variable encountered: " ^ s); |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
130 |
|
16903 | 131 |
fun ascii_of_indexname (v,0) = ascii_of v |
132 |
| ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; |
|
15347 | 133 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
134 |
(* another version of above functions that remove chars that may not be allowed by Vampire *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
135 |
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of v); |
15347 | 136 |
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); |
137 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
138 |
|
16903 | 139 |
(*Type variables contain _H because the character ' translates to that.*) |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
140 |
fun make_schematic_type_var (x,i) = |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
141 |
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
142 |
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
15347 | 143 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
144 |
fun make_fixed_const c = const_prefix ^ (ascii_of c); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
145 |
fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
146 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
147 |
fun make_type_class clas = class_prefix ^ (ascii_of clas); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
148 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
149 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
150 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
151 |
fun lookup_const c = |
16903 | 152 |
case Symtab.lookup (const_trans_table,c) of |
153 |
SOME c' => c' |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
154 |
| NONE => make_fixed_const c; |
15347 | 155 |
|
156 |
||
157 |
||
158 |
(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) |
|
159 |
||
160 |
val keep_types = ref true; (* default is true *) |
|
161 |
fun untyped () = (keep_types := false); |
|
162 |
fun typed () = (keep_types := true); |
|
163 |
||
164 |
||
165 |
datatype kind = Axiom | Hypothesis | Conjecture; |
|
166 |
fun name_of_kind Axiom = "axiom" |
|
167 |
| name_of_kind Hypothesis = "hypothesis" |
|
168 |
| name_of_kind Conjecture = "conjecture"; |
|
169 |
||
170 |
type clause_id = int; |
|
171 |
type axiom_name = string; |
|
172 |
||
173 |
||
174 |
type polarity = bool; |
|
175 |
||
176 |
type indexname = Term.indexname; |
|
177 |
||
178 |
||
179 |
(* "tag" is used for vampire specific syntax *) |
|
180 |
type tag = bool; |
|
181 |
||
182 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
183 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
184 |
fun string_of_indexname (name,index) = name ^ "_" ^ (string_of_int index); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
185 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
186 |
|
16903 | 187 |
val id_ref = ref 0; |
15347 | 188 |
fun generate_id () = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
189 |
let val id = !id_ref |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
190 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
191 |
(id_ref:=id + 1; id) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
192 |
end; |
15347 | 193 |
|
194 |
||
195 |
||
196 |
(**** Isabelle FOL clauses ****) |
|
197 |
||
198 |
(* by default it is false *) |
|
199 |
val tagged = ref false; |
|
200 |
||
201 |
type pred_name = string; |
|
202 |
type sort = Term.sort; |
|
203 |
type fol_type = string; |
|
204 |
||
205 |
||
206 |
datatype type_literal = LTVar of string | LTFree of string; |
|
207 |
||
208 |
||
209 |
datatype folTerm = UVar of string * fol_type| Fun of string * fol_type * folTerm list; |
|
210 |
datatype predicate = Predicate of pred_name * fol_type * folTerm list; |
|
211 |
||
212 |
||
213 |
datatype literal = Literal of polarity * predicate * tag; |
|
214 |
||
215 |
||
216 |
datatype typ_var = FOLTVar of indexname | FOLTFree of string; |
|
217 |
||
218 |
||
219 |
(* ML datatype used to repsent one single clause: disjunction of literals. *) |
|
220 |
datatype clause = |
|
221 |
Clause of {clause_id: clause_id, |
|
222 |
axiom_name: axiom_name, |
|
223 |
kind: kind, |
|
224 |
literals: literal list, |
|
225 |
types_sorts: (typ_var * sort) list, |
|
226 |
tvar_type_literals: type_literal list, |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
227 |
tfree_type_literals: type_literal list , |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
228 |
tvars: string list, |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
229 |
predicates: (string*int) list, |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
230 |
functions: (string*int) list}; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
231 |
|
15347 | 232 |
|
233 |
||
234 |
exception CLAUSE of string; |
|
235 |
||
236 |
||
237 |
||
238 |
(*** make clauses ***) |
|
239 |
||
240 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
241 |
fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals,tvars, predicates, functions) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
242 |
Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, literals = literals, types_sorts = types_sorts,tvar_type_literals = tvar_type_literals,tfree_type_literals = tfree_type_literals,tvars = tvars, predicates = predicates, functions = functions}; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
243 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
244 |
|
15347 | 245 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
246 |
fun type_of (Type (a, [])) = let val t = make_fixed_type_const a |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
247 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
248 |
(t,([],[(t,0)])) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
249 |
end |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
250 |
|
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
251 |
(*Definitions of the current theory--to allow suppressing types.*) |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
252 |
val curr_defs = ref Defs.empty; |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
253 |
|
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
254 |
(*Initialize the type suppression mechanism with the current theory before |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
255 |
producing any clauses!*) |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
256 |
fun init thy = (curr_defs := Theory.defs_of thy); |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
257 |
(*<<<<<<< res_clause.ML |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
258 |
*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
259 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
260 |
(*Types aren't needed if the constant has at most one definition and is monomorphic*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
261 |
(*fun no_types_needed s = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
262 |
(case Defs.fast_overloading_info (!curr_defs) s of |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
263 |
NONE => true |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
264 |
| SOME (T,len,_) => len <= 1 andalso null (typ_tvars T)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
265 |
=======*) |
16976 | 266 |
fun no_types_needed s = Defs.monomorphic (!curr_defs) s; |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
267 |
(*>>>>>>> 1.18*) |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
268 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
269 |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
270 |
(*Flatten a type to a string while accumulating sort constraints on the TFress and |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
271 |
TVars it contains.*) |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
272 |
fun type_of (Type (a, [])) = let val t = make_fixed_type_const a |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
273 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
274 |
(t,([],[(t,0)])) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
275 |
end |
15347 | 276 |
| type_of (Type (a, Ts)) = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
277 |
let val foltyps_ts = map type_of Ts |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
278 |
val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
279 |
val (ts, funcslist) = ListPair.unzip ts_funcs |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
280 |
val ts' = ResLib.flat_noDup ts |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
281 |
val funcs' = (ResLib.flat_noDup funcslist) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
282 |
val t = (make_fixed_type_const a) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
283 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
284 |
((t ^ (ResLib.list_to_string folTyps)),(ts', ((t,(length Ts))::funcs')) ) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
285 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
286 |
| type_of (TFree (a, s)) = let val t = make_fixed_type_const a |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
287 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
288 |
(t, ([((FOLTFree a),s)],[(t,0)]) ) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
289 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
290 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
291 |
| type_of (TVar (v, s)) = let val t =make_schematic_type_var ( v) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
292 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
293 |
(t, ([((FOLTVar v),s)], [(*(t,0)*)])) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
294 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
295 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
296 |
(* added: checkMeta: string -> bool *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
297 |
(* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
298 |
fun checkMeta s = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
299 |
let val chars = explode s |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
300 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
301 |
["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
302 |
end; |
15390 | 303 |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
304 |
fun maybe_type_of c T = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
305 |
if no_types_needed c then ("",([],[])) else type_of T; |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
306 |
|
16903 | 307 |
(* Any variables created via the METAHYPS tactical should be treated as |
308 |
universal vars, although it is represented as "Free(...)" by Isabelle *) |
|
309 |
val isMeta = String.isPrefix "METAHYP1_" |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
310 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
311 |
fun pred_name_type (Const(c,T)) = (let val t = make_fixed_const c |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
312 |
val (typof,(folTyps,funcs)) = type_of T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
313 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
314 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
315 |
(t, (typof,folTyps), (funcs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
316 |
end) |
15390 | 317 |
| pred_name_type (Free(x,T)) = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
318 |
let val is_meta = checkMeta x |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
319 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
320 |
if is_meta then (raise CLAUSE("Predicate Not First Order")) else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
321 |
(let val t = (make_fixed_var x) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
322 |
val (typof,(folTyps, funcs)) = type_of T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
323 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
324 |
(t, (typof,folTyps),funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
325 |
end) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
326 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
327 |
end |
15347 | 328 |
| pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") |
329 |
| pred_name_type _ = raise CLAUSE("Predicate input unexpected"); |
|
330 |
||
15615 | 331 |
|
332 |
(* For type equality *) |
|
333 |
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) |
|
334 |
(* Find type of equality arg *) |
|
335 |
fun eq_arg_type (Type("fun",[T,_])) = |
|
336 |
let val (folT,_) = type_of T; |
|
337 |
in |
|
338 |
folT |
|
339 |
end; |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
340 |
|
15615 | 341 |
|
15347 | 342 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
343 |
(* FIX: retest with lcp's changes *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
344 |
fun fun_name_type (Const(c,T)) args = (let val t = make_fixed_const c |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
345 |
val (typof,(folTyps,funcs)) = maybe_type_of c T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
346 |
val arity = if (!keep_types) then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
347 |
(length args)(*+ 1*) (*(length folTyps) *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
348 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
349 |
(length args)(* -1*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
350 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
351 |
(t, (typof,folTyps), ((t,arity)::funcs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
352 |
end) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
353 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
354 |
| fun_name_type (Free(x,T)) args = (let val t = (make_fixed_var x) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
355 |
val (typof,(folTyps,funcs)) = type_of T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
356 |
val arity = if (!keep_types) then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
357 |
(length args) (*+ 1*) (*(length folTyps)*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
358 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
359 |
(length args) (*-1*)(*(length args) + 1*)(*(length folTyps)*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
360 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
361 |
(t, (typof,folTyps), ((t,0)::funcs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
362 |
end) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
363 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
364 |
| fun_name_type _ args = raise CLAUSE("Function Not First Order"); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
365 |
|
15615 | 366 |
|
15347 | 367 |
fun term_of (Var(ind_nm,T)) = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
368 |
let val (folType,(ts,funcs)) = type_of T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
369 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
370 |
(UVar(make_schematic_var(string_of_indexname ind_nm),folType),(ts, (funcs))) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
371 |
end |
15347 | 372 |
| term_of (Free(x,T)) = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
373 |
let val is_meta = checkMeta x |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
374 |
val (folType,(ts, funcs)) = type_of T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
375 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
376 |
if is_meta then (UVar(make_schematic_var x,folType),(ts, (((make_schematic_var x),0)::funcs))) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
377 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
378 |
(Fun(make_fixed_var x,folType,[]),(ts, (((make_fixed_var x),0)::funcs))) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
379 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
380 |
| term_of (Const(c,T)) = (* impossible to be equality *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
381 |
let val (folType,(ts,funcs)) = type_of T |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
382 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
383 |
(Fun(lookup_const c,folType,[]),(ts, (((lookup_const c),0)::funcs))) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
384 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
385 |
| term_of (app as (t $ a)) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
386 |
let val (f,args) = strip_comb app |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
387 |
fun term_of_aux () = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
388 |
let val (funName,(funType,ts1),funcs) = fun_name_type f args |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
389 |
val (args',ts_funcs) = ListPair.unzip (map term_of args) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
390 |
val (ts2,funcs') = ListPair.unzip ( ts_funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
391 |
val ts3 = ResLib.flat_noDup (ts1::ts2) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
392 |
val funcs'' = ResLib.flat_noDup((funcs::funcs')) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
393 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
394 |
(Fun(funName,funType,args'),(ts3,funcs'')) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
395 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
396 |
fun term_of_eq ((Const ("op =", typ)),args) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
397 |
let val arg_typ = eq_arg_type typ |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
398 |
val (args',ts_funcs) = ListPair.unzip (map term_of args) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
399 |
val (ts,funcs) = ListPair.unzip ( ts_funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
400 |
val equal_name = lookup_const ("op =") |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
401 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
402 |
(Fun(equal_name,arg_typ,args'),(ResLib.flat_noDup ts, (((make_fixed_var equal_name),2):: ResLib.flat_noDup (funcs)))) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
403 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
404 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
405 |
case f of Const ("op =", typ) => term_of_eq (f,args) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
406 |
| Const(_,_) => term_of_aux () |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
407 |
| Free(s,_) => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux () |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
408 |
| _ => raise CLAUSE("Function Not First Order") |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
409 |
end |
15390 | 410 |
| term_of _ = raise CLAUSE("Function Not First Order"); |
411 |
||
15347 | 412 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
413 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
414 |
|
15347 | 415 |
fun pred_of_eq ((Const ("op =", typ)),args) = |
416 |
let val arg_typ = eq_arg_type typ |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
417 |
val (args',ts_funcs) = ListPair.unzip (map term_of args) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
418 |
val (ts,funcs) = ListPair.unzip ( ts_funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
419 |
val equal_name = lookup_const "op =" |
15347 | 420 |
in |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
421 |
(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts,([((make_fixed_var equal_name),2)]:(string*int)list), (ResLib.flat_noDup (funcs))) |
15347 | 422 |
end; |
423 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
424 |
(* CHECK arity for predicate is set to (2*args) to account for type info. Is this right? *) |
15347 | 425 |
(* changed for non-equality predicate *) |
426 |
(* The input "pred" cannot be an equality *) |
|
427 |
fun pred_of_nonEq (pred,args) = |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
428 |
let val (predName,(predType,ts1), pfuncs) = pred_name_type pred |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
429 |
val (args',ts_funcs) = ListPair.unzip (map term_of args) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
430 |
val (ts2,ffuncs) = ListPair.unzip ( ts_funcs) |
15347 | 431 |
val ts3 = ResLib.flat_noDup (ts1::ts2) |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
432 |
val ffuncs' = (ResLib.flat_noDup (ffuncs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
433 |
val newfuncs = distinct (pfuncs@ffuncs') |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
434 |
val pred_arity = (*if ((length ts3) <> 0) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
435 |
then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
436 |
((length args) +(length ts3)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
437 |
else*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
438 |
(* just doing length args if untyped seems to work*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
439 |
(if !keep_types then (length args)+1 else (length args)) |
15347 | 440 |
in |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
441 |
(Predicate(predName,predType,args'),ts3, [(predName, pred_arity)], newfuncs) |
15347 | 442 |
end; |
443 |
||
444 |
||
445 |
(* Changed for typed equality *) |
|
446 |
(* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *) |
|
447 |
fun predicate_of term = |
|
448 |
let val (pred,args) = strip_comb term |
|
449 |
in |
|
450 |
case pred of (Const ("op =", _)) => pred_of_eq (pred,args) |
|
451 |
| _ => pred_of_nonEq (pred,args) |
|
452 |
end; |
|
453 |
||
454 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
455 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
456 |
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
457 |
| literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
458 |
let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
459 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
460 |
literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
461 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
462 |
| literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
463 |
let val (pred,ts', preds', funcs') = predicate_of P |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
464 |
val lits' = Literal(false,pred,false) :: lits |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
465 |
val ts'' = ResLib.no_rep_app ts ts' |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
466 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
467 |
(lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
468 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
469 |
| literals_of_term (P,(lits,ts), preds, funcs) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
470 |
let val (pred,ts', preds', funcs') = predicate_of P |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
471 |
val lits' = Literal(true,pred,false) :: lits |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
472 |
val ts'' = ResLib.no_rep_app ts ts' |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
473 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
474 |
(lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
475 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
476 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
477 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
478 |
fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
479 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
480 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
481 |
(* FIX: not sure what to do with these funcs *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
482 |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
483 |
(*Make literals for sorted type variables*) |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
484 |
fun sorts_on_typs (_, []) = ([]) |
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
485 |
| sorts_on_typs (v, "HOL.type" :: s) = |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
486 |
sorts_on_typs (v,s) (*Ignore sort "type"*) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
487 |
| sorts_on_typs ((FOLTVar(indx)), (s::ss)) = |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
488 |
(LTVar((make_type_class s) ^ |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
489 |
"(" ^ (make_schematic_type_var( indx)) ^ ")") :: |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
490 |
(sorts_on_typs ((FOLTVar(indx)), ss))) |
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
491 |
| sorts_on_typs ((FOLTFree(x)), (s::ss)) = |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
492 |
LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
493 |
(sorts_on_typs ((FOLTFree(x)), ss)); |
15347 | 494 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
495 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
496 |
fun takeUntil ch [] res = (res, []) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
497 |
| takeUntil ch (x::xs) res = if x = ch |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
498 |
then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
499 |
(res, xs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
500 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
501 |
takeUntil ch xs (res@[x]) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
502 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
503 |
fun remove_type str = let val exp = explode str |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
504 |
val (first,rest) = (takeUntil "(" exp []) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
505 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
506 |
implode first |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
507 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
508 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
509 |
fun pred_of_sort (LTVar x) = ((remove_type x),1) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
510 |
| pred_of_sort (LTFree x) = ((remove_type x),1) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
511 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
512 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
513 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
514 |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
515 |
(*Given a list of sorted type variables, return two separate lists. |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
516 |
The first is for TVars, the second for TFrees.*) |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
517 |
fun add_typs_aux [] preds = ([],[], preds) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
518 |
| add_typs_aux ((FOLTVar(indx),s)::tss) preds = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
519 |
let val (vs) = sorts_on_typs (FOLTVar(indx), s) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
520 |
val preds' = (map pred_of_sort vs)@preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
521 |
val (vss,fss, preds'') = add_typs_aux tss preds' |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
522 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
523 |
(ResLib.no_rep_app vs vss, fss, preds'') |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
524 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
525 |
| add_typs_aux ((FOLTFree(x),s)::tss) preds = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
526 |
let val (fs) = sorts_on_typs (FOLTFree(x), s) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
527 |
val preds' = (map pred_of_sort fs)@preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
528 |
val (vss,fss, preds'') = add_typs_aux tss preds' |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
529 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
530 |
(vss, ResLib.no_rep_app fs fss,preds'') |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
531 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
532 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
533 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
534 |
(*fun add_typs_aux [] = ([],[]) |
15347 | 535 |
| add_typs_aux ((FOLTVar(indx),s)::tss) = |
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
536 |
let val vs = sorts_on_typs (FOLTVar(indx), s) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
537 |
val (vss,fss) = add_typs_aux tss |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
538 |
in |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
539 |
(ResLib.no_rep_app vs vss, fss) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
540 |
end |
15347 | 541 |
| add_typs_aux ((FOLTFree(x),s)::tss) = |
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
542 |
let val fs = sorts_on_typs (FOLTFree(x), s) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
543 |
val (vss,fss) = add_typs_aux tss |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
544 |
in |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
545 |
(vss, ResLib.no_rep_app fs fss) |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
546 |
end;*) |
15347 | 547 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
548 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
549 |
fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds |
15347 | 550 |
|
551 |
||
552 |
(** make axiom clauses, hypothesis clauses and conjecture clauses. **) |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
553 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
554 |
local |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
555 |
fun replace_dot "." = "_" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
556 |
| replace_dot "'" = "" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
557 |
| replace_dot c = c; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
558 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
559 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
560 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
561 |
fun proper_ax_name ax_name = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
562 |
let val chars = explode ax_name |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
563 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
564 |
implode (map replace_dot chars) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
565 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
566 |
end; |
15347 | 567 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
568 |
fun get_tvar_strs [] = [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
569 |
| get_tvar_strs ((FOLTVar(indx),s)::tss) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
570 |
let val vstr =(make_schematic_type_var( indx)); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
571 |
val (vstrs) = get_tvar_strs tss |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
572 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
573 |
(distinct( vstr:: vstrs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
574 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
575 |
| get_tvar_strs((FOLTFree(x),s)::tss) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
576 |
let val (vstrs) = get_tvar_strs tss |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
577 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
578 |
(distinct( vstrs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
579 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
580 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
581 |
(* FIX add preds and funcs to add typs aux here *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
582 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
583 |
fun make_axiom_clause_thm thm (name,number)= |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
584 |
let val (lits,types_sorts, preds, funcs) = literals_of_thm thm |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
585 |
val cls_id = number |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
586 |
val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
587 |
val tvars = get_tvar_strs types_sorts |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
588 |
val ax_name = proper_ax_name name |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
589 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
590 |
make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
15347 | 591 |
end; |
592 |
||
593 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
594 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
595 |
fun make_conjecture_clause_thm thm = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
596 |
let val (lits,types_sorts, preds, funcs) = literals_of_thm thm |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
597 |
val cls_id = generate_id() |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
598 |
val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
599 |
val tvars = get_tvar_strs types_sorts |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
600 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
601 |
make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
602 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
603 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
604 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
605 |
fun make_axiom_clause term (name,number)= |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
606 |
let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[]) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
607 |
val cls_id = number |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
608 |
val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
609 |
val tvars = get_tvar_strs types_sorts |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
610 |
val ax_name = proper_ax_name name |
15347 | 611 |
in |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
612 |
make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
15347 | 613 |
end; |
614 |
||
615 |
||
616 |
fun make_hypothesis_clause term = |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
617 |
let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) |
15347 | 618 |
val cls_id = generate_id() |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
619 |
val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
620 |
val tvars = get_tvar_strs types_sorts |
15347 | 621 |
in |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
622 |
make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
15347 | 623 |
end; |
624 |
||
625 |
||
626 |
fun make_conjecture_clause term = |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
627 |
let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) |
15347 | 628 |
val cls_id = generate_id() |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
629 |
val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
630 |
val tvars = get_tvar_strs types_sorts |
15347 | 631 |
in |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
632 |
make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
15347 | 633 |
end; |
634 |
||
635 |
||
636 |
||
637 |
(**** Isabelle arities ****) |
|
638 |
||
639 |
exception ARCLAUSE of string; |
|
640 |
||
641 |
||
642 |
type class = string; |
|
643 |
type tcons = string; |
|
644 |
||
645 |
||
646 |
datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string); |
|
647 |
||
648 |
datatype arityClause = |
|
649 |
ArityClause of {clause_id: clause_id, |
|
650 |
kind: kind, |
|
651 |
conclLit: arLit, |
|
652 |
premLits: arLit list}; |
|
653 |
||
654 |
||
655 |
fun get_TVars 0 = [] |
|
656 |
| get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n-1); |
|
657 |
||
658 |
||
659 |
||
660 |
fun pack_sort(_,[]) = raise ARCLAUSE("Empty Sort Found") |
|
661 |
| pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] |
|
662 |
| pack_sort(tvar, cls::srt) = (make_type_class cls,tvar) :: (pack_sort(tvar, srt)); |
|
663 |
||
664 |
||
665 |
fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); |
|
666 |
fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); |
|
667 |
||
668 |
||
669 |
fun make_arity_clause (clause_id,kind,conclLit,premLits) = |
|
670 |
ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits}; |
|
671 |
||
672 |
||
673 |
fun make_axiom_arity_clause (tcons,(res,args)) = |
|
674 |
let val cls_id = generate_id() |
|
675 |
val nargs = length args |
|
676 |
val tvars = get_TVars nargs |
|
677 |
val conclLit = make_TConsLit(true,(res,tcons,tvars)) |
|
15774 | 678 |
val tvars_srts = ListPair.zip (tvars,args) |
15347 | 679 |
val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) |
680 |
val false_tvars_srts' = ResLib.pair_ins false tvars_srts' |
|
681 |
val premLits = map make_TVarLit false_tvars_srts' |
|
682 |
in |
|
683 |
make_arity_clause (cls_id,Axiom,conclLit,premLits) |
|
684 |
end; |
|
685 |
||
686 |
||
687 |
||
688 |
(**** Isabelle class relations ****) |
|
689 |
||
690 |
||
691 |
datatype classrelClause = |
|
692 |
ClassrelClause of {clause_id: clause_id, |
|
693 |
subclass: class, |
|
15531 | 694 |
superclass: class option}; |
15347 | 695 |
|
696 |
fun make_classrelClause (clause_id,subclass,superclass) = |
|
697 |
ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass}; |
|
698 |
||
699 |
||
700 |
fun make_axiom_classrelClause (subclass,superclass) = |
|
701 |
let val cls_id = generate_id() |
|
702 |
val sub = make_type_class subclass |
|
15531 | 703 |
val sup = case superclass of NONE => NONE |
704 |
| SOME s => SOME (make_type_class s) |
|
15347 | 705 |
in |
706 |
make_classrelClause(cls_id,sub,sup) |
|
707 |
end; |
|
708 |
||
709 |
||
710 |
||
711 |
fun classrelClauses_of_aux (sub,[]) = [] |
|
15531 | 712 |
| classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); |
15347 | 713 |
|
714 |
||
715 |
fun classrelClauses_of (sub,sups) = |
|
15531 | 716 |
case sups of [] => [make_axiom_classrelClause (sub,NONE)] |
15347 | 717 |
| _ => classrelClauses_of_aux (sub, sups); |
718 |
||
719 |
||
720 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
721 |
(***** convert clauses to DFG format *****) |
15347 | 722 |
|
723 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
724 |
fun string_of_clauseID (Clause cls) = clause_prefix ^ (string_of_int (#clause_id cls)); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
725 |
|
15347 | 726 |
|
727 |
fun string_of_kind (Clause cls) = name_of_kind (#kind cls); |
|
728 |
||
729 |
fun string_of_axiomName (Clause cls) = #axiom_name cls; |
|
730 |
||
731 |
(****!!!! Changed for typed equality !!!!****) |
|
732 |
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; |
|
733 |
||
734 |
||
735 |
(****!!!! Changed for typed equality !!!!****) |
|
736 |
(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included. *) |
|
737 |
fun string_of_equality (typ,terms) = |
|
738 |
let val [tstr1,tstr2] = map string_of_term terms |
|
739 |
in |
|
740 |
if ((!keep_types) andalso (!special_equal)) then |
|
741 |
"equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ (wrap_eq_type typ tstr2) ^ ")" |
|
742 |
else |
|
743 |
"equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" |
|
15615 | 744 |
end |
745 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
746 |
|
15615 | 747 |
and |
748 |
string_of_term (UVar(x,_)) = x |
|
749 |
| string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) |
|
750 |
| string_of_term (Fun (name,typ,[])) = name |
|
751 |
| string_of_term (Fun (name,typ,terms)) = |
|
752 |
let val terms' = map string_of_term terms |
|
753 |
in |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
754 |
if !keep_types andalso typ<>"" then name ^ (ResLib.list_to_string (terms' @ [typ])) |
15615 | 755 |
else name ^ (ResLib.list_to_string terms') |
15347 | 756 |
end; |
757 |
||
758 |
||
759 |
||
760 |
(* Changed for typed equality *) |
|
761 |
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
762 |
fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
763 |
| string_of_predicate (Predicate(name,_,[])) = name |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
764 |
| string_of_predicate (Predicate(name,typ,terms)) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
765 |
let val terms_as_strings = map string_of_term terms |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
766 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
767 |
if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
768 |
else name ^ (ResLib.list_to_string terms_as_strings) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
769 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
770 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
771 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
772 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
773 |
(********************************) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
774 |
(* Code for producing DFG files *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
775 |
(********************************) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
776 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
777 |
fun dfg_literal (Literal(pol,pred,tag)) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
778 |
let val pred_string = string_of_predicate pred |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
779 |
val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
780 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
781 |
tagged_pol |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
782 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
783 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
784 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
785 |
(* FIX: what does this mean? *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
786 |
(*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
787 |
| dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
788 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
789 |
fun dfg_of_typeLit (LTVar x) = x |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
790 |
| dfg_of_typeLit (LTFree x) = x ; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
791 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
792 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
793 |
fun strlist [] = "" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
794 |
| strlist (x::[]) = x |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
795 |
| strlist (x::xs) = x ^ "," ^ (strlist xs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
796 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
797 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
798 |
fun gen_dfg_cls (cls_id,ax_name,knd,lits, tvars,vars) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
799 |
let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
800 |
val forall_str = if (vars = []) andalso (tvars = []) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
801 |
then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
802 |
"" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
803 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
804 |
"forall([" ^ (strlist (vars@tvars))^ "]" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
805 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
806 |
if forall_str = "" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
807 |
then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
808 |
"clause( %(" ^ knd ^ ")\n" ^ "or(" ^ lits ^ ") ,\n" ^ cls_id ^ ax_str ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
809 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
810 |
"clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or(" ^ lits ^ ")),\n" ^ cls_id ^ ax_str ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
811 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
812 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
813 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
814 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
815 |
fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars, vars) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
816 |
let val forall_str = if (vars = []) andalso (tvars = []) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
817 |
then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
818 |
"" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
819 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
820 |
"forall([" ^ (strlist (vars@tvars))^"]" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
821 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
822 |
if forall_str = "" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
823 |
then |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
824 |
"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ tfree_lit ^ ") ,\n" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
825 |
else |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
826 |
"clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
827 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
828 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
829 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
830 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
831 |
fun dfg_clause_aux (Clause cls) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
832 |
let val lits = map dfg_literal (#literals cls) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
833 |
val tvar_lits_strs = if (!keep_types) then (map dfg_of_typeLit (#tvar_type_literals cls)) else [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
834 |
val tfree_lits = if (!keep_types) then (map dfg_of_typeLit (#tfree_type_literals cls)) else [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
835 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
836 |
(tvar_lits_strs @ lits,tfree_lits) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
837 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
838 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
839 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
840 |
fun dfg_folterms (Literal(pol,pred,tag)) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
841 |
let val Predicate (predname, foltype, folterms) = pred |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
842 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
843 |
folterms |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
844 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
845 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
846 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
847 |
fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then *)[str] (*else []*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
848 |
| get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
849 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
850 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
851 |
fun is_uvar (UVar(str,typ)) = true |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
852 |
| is_uvar (Fun (str,typ,tlist)) = false; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
853 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
854 |
fun uvar_name (UVar(str,typ)) = str |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
855 |
| uvar_name _ = (raise CLAUSE("Not a variable")); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
856 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
857 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
858 |
fun mergelist [] = [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
859 |
| mergelist (x::xs ) = x@(mergelist xs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
860 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
861 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
862 |
fun dfg_vars (Clause cls) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
863 |
let val lits = (#literals cls) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
864 |
val folterms = mergelist(map dfg_folterms lits) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
865 |
val vars = ResLib.flat_noDup(map get_uvars folterms) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
866 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
867 |
vars |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
868 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
869 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
870 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
871 |
fun dfg_tvars (Clause cls) =(#tvars cls) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
872 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
873 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
874 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
875 |
(* make this return funcs and preds too? *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
876 |
fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
877 |
| string_of_predname (Predicate(name,_,[])) = name |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
878 |
| string_of_predname (Predicate(name,typ,terms)) = name |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
879 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
880 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
881 |
(* make this return funcs and preds too? *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
882 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
883 |
fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
15347 | 884 |
| string_of_predicate (Predicate(name,_,[])) = name |
885 |
| string_of_predicate (Predicate(name,typ,terms)) = |
|
16903 | 886 |
let val terms_as_strings = map string_of_term terms |
887 |
in |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
888 |
if !keep_types andalso typ<>"" |
16903 | 889 |
then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) |
890 |
else name ^ (ResLib.list_to_string terms_as_strings) |
|
891 |
end; |
|
15347 | 892 |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
893 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
894 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
895 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
896 |
fun concat_with sep [] = "" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
897 |
| concat_with sep [x] = "(" ^ x ^ ")" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
898 |
| concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
899 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
900 |
fun concat_with_comma [] = "" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
901 |
| concat_with_comma [x] = x |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
902 |
| concat_with_comma (x::xs) = x ^ ", " ^ (concat_with_comma xs); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
903 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
904 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
905 |
fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred)^" "^ax_name |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
906 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
907 |
fun dfg_clause cls = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
908 |
let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
909 |
val vars = dfg_vars cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
910 |
val tvars = dfg_tvars cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
911 |
val cls_id = string_of_clauseID cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
912 |
val ax_name = string_of_axiomName cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
913 |
val knd = string_of_kind cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
914 |
val lits_str = concat_with_comma lits |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
915 |
val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
916 |
fun typ_clss k [] = [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
917 |
| typ_clss k (tfree :: tfrees) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
918 |
(gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: (typ_clss (k+1) tfrees) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
919 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
920 |
cls_str :: (typ_clss 0 tfree_lits) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
921 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
922 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
923 |
fun clause_info cls = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
924 |
let |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
925 |
val cls_id = string_of_clauseID cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
926 |
val ax_name = string_of_axiomName cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
927 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
928 |
((ax_name^""), cls_id) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
929 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
930 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
931 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
932 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
933 |
fun zip_concat name [] = [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
934 |
| zip_concat name ((str, num)::xs) = (((str^name), num)::(zip_concat name xs)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
935 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
936 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
937 |
(*fun funcs_of_cls (Clause cls) = let val funcs = #functions cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
938 |
val name = #axiom_name cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
939 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
940 |
zip_concat name funcs |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
941 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
942 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
943 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
944 |
fun preds_of_cls (Clause cls) = let val preds = #predicates cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
945 |
; val name = ("foo"^(#axiom_name cls)) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
946 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
947 |
zip_concat name preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
948 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
949 |
*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
950 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
951 |
fun funcs_of_cls (Clause cls) = #functions cls; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
952 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
953 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
954 |
fun preds_of_cls (Clause cls) = #predicates cls; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
955 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
956 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
957 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
958 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
959 |
fun string_of_arity (name, num) = name ^"," ^ (string_of_int num) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
960 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
961 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
962 |
fun string_of_preds preds = "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
963 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
964 |
fun string_of_funcs funcs ="functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
965 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
966 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
967 |
fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
968 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
969 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
970 |
fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
971 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
972 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
973 |
fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
974 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
975 |
fun string_of_descrip () = "list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
976 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
977 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
978 |
fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
979 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
980 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
981 |
fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
982 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
983 |
val delim = "\n"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
984 |
val dfg_clauses2str = ResLib.list2str_sep delim; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
985 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
986 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
987 |
fun clause2dfg cls = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
988 |
let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
989 |
val cls_id = string_of_clauseID cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
990 |
val ax_name = string_of_axiomName cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
991 |
val vars = dfg_vars cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
992 |
val tvars = dfg_tvars cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
993 |
val funcs = funcs_of_cls cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
994 |
val preds = preds_of_cls cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
995 |
val knd = string_of_kind cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
996 |
val lits_str = concat_with_comma lits |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
997 |
val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
998 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
999 |
(cls_str,tfree_lits) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1000 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1001 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1002 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1003 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1004 |
fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1005 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1006 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1007 |
fun gen_dfg_file fname axioms conjectures funcs preds tfrees= |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1008 |
let val (axstrs_tfrees) = (map clause2dfg axioms) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1009 |
val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1010 |
val axstr = ResLib.list2str_sep delim axstrs |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1011 |
val (conjstrs_tfrees) = (map clause2dfg conjectures) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1012 |
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1013 |
val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1014 |
val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1015 |
val funcstr = string_of_funcs funcs |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1016 |
val predstr = string_of_preds preds |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1017 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1018 |
(string_of_start fname) ^ (string_of_descrip ()) ^ (string_of_symbols funcstr predstr ) ^ |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1019 |
(string_of_axioms axstr)^ |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1020 |
(string_of_conjectures conjstr) ^ (string_of_end ()) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1021 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1022 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1023 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1024 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1025 |
fun clauses2dfg [] filename axioms conjectures funcs preds tfrees= |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1026 |
let val funcs' = ((ResLib.flat_noDup(map funcs_of_cls axioms))@funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1027 |
val preds' = ((ResLib.flat_noDup(map preds_of_cls axioms))@preds) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1028 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1029 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1030 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1031 |
gen_dfg_file filename axioms conjectures funcs' preds' tfrees |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1032 |
(*(filename, axioms, conjectures, funcs, preds)*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1033 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1034 |
|clauses2dfg (cls::clss) filename axioms conjectures funcs preds tfrees = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1035 |
let val (lits,tfree_lits) = dfg_clause_aux (cls) (*"lits" includes the typing assumptions (TVars)*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1036 |
val cls_id = string_of_clauseID cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1037 |
val ax_name = string_of_axiomName cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1038 |
val vars = dfg_vars cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1039 |
val tvars = dfg_tvars cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1040 |
val funcs' = distinct((funcs_of_cls cls)@funcs) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1041 |
val preds' = distinct((preds_of_cls cls)@preds) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1042 |
val knd = string_of_kind cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1043 |
val lits_str = concat_with ", " lits |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1044 |
val axioms' = if knd = "axiom" then (cls::axioms) else axioms |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1045 |
val conjectures' = if knd = "conjecture" then (cls::conjectures) else conjectures |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1046 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1047 |
clauses2dfg clss filename axioms' conjectures' funcs' preds' tfrees |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1048 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1049 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1050 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1051 |
fun fileout f str = let val out = TextIO.openOut(f) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1052 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1053 |
ResLib.writeln_strs out (str); TextIO.closeOut out |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1054 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1055 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1056 |
(*val filestr = clauses2dfg newcls "flump" [] [] [] []; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1057 |
*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1058 |
(* fileout "flump.dfg" [filestr];*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1059 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1060 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1061 |
(*FIX: ask Jia what this is for *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1062 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1063 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1064 |
fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1065 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1066 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1067 |
fun string_of_arLit (TConsLit(b,(c,t,args))) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1068 |
let val pol = if b then "++" else "--" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1069 |
val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1070 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1071 |
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1072 |
end |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1073 |
| string_of_arLit (TVarLit(b,(c,str))) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1074 |
let val pol = if b then "++" else "--" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1075 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1076 |
pol ^ c ^ "(" ^ str ^ ")" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1077 |
end; |
15347 | 1078 |
|
1079 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1080 |
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1081 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1082 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1083 |
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1084 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1085 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1086 |
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1087 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1088 |
(*FIX: would this have variables in a forall? *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1089 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1090 |
fun dfg_arity_clause arcls = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1091 |
let val arcls_id = string_of_arClauseID arcls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1092 |
val concl_lit = string_of_conclLit arcls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1093 |
val prems_lits = strings_of_premLits arcls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1094 |
val knd = string_of_arKind arcls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1095 |
val all_lits = concl_lit :: prems_lits |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1096 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1097 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1098 |
"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^ arcls_id ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1099 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1100 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1101 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1102 |
val clrelclause_prefix = "relcls_"; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1103 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1104 |
(* FIX later. Doesn't seem to be used in clasimp *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1105 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1106 |
(*fun tptp_classrelLits sub sup = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1107 |
let val tvar = "(T)" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1108 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1109 |
case sup of NONE => "[++" ^ sub ^ tvar ^ "]" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1110 |
| (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1111 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1112 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1113 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1114 |
fun tptp_classrelClause (ClassrelClause cls) = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1115 |
let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1116 |
val sub = #subclass cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1117 |
val sup = #superclass cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1118 |
val lits = tptp_classrelLits sub sup |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1119 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1120 |
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1121 |
end; |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1122 |
*) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1123 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1124 |
(********************************) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1125 |
(* code to produce TPTP files *) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1126 |
(********************************) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1127 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1128 |
|
15347 | 1129 |
|
1130 |
fun tptp_literal (Literal(pol,pred,tag)) = |
|
1131 |
let val pred_string = string_of_predicate pred |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1132 |
val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---") |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1133 |
else (if pol then "++" else "--") |
15347 | 1134 |
in |
1135 |
tagged_pol ^ pred_string |
|
1136 |
end; |
|
1137 |
||
1138 |
||
1139 |
||
1140 |
fun tptp_of_typeLit (LTVar x) = "--" ^ x |
|
1141 |
| tptp_of_typeLit (LTFree x) = "++" ^ x; |
|
1142 |
||
1143 |
||
1144 |
fun gen_tptp_cls (cls_id,ax_name,knd,lits) = |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1145 |
let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) |
15347 | 1146 |
in |
1147 |
"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." |
|
1148 |
end; |
|
1149 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1150 |
|
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1151 |
fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; |
15347 | 1152 |
|
1153 |
||
1154 |
fun tptp_clause_aux (Clause cls) = |
|
1155 |
let val lits = map tptp_literal (#literals cls) |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1156 |
val tvar_lits_strs = if (!keep_types) then (map tptp_of_typeLit (#tvar_type_literals cls)) else [] |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1157 |
val tfree_lits = if (!keep_types) then (map tptp_of_typeLit (#tfree_type_literals cls)) else [] |
15347 | 1158 |
in |
1159 |
(tvar_lits_strs @ lits,tfree_lits) |
|
1160 |
end; |
|
1161 |
||
15608 | 1162 |
|
15347 | 1163 |
fun tptp_clause cls = |
1164 |
let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
|
1165 |
val cls_id = string_of_clauseID cls |
|
1166 |
val ax_name = string_of_axiomName cls |
|
1167 |
val knd = string_of_kind cls |
|
1168 |
val lits_str = ResLib.list_to_string' lits |
|
1169 |
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] |
|
1170 |
| typ_clss k (tfree :: tfrees) = |
|
1171 |
(gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) |
|
1172 |
in |
|
1173 |
cls_str :: (typ_clss 0 tfree_lits) |
|
1174 |
end; |
|
1175 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1176 |
fun clause_info cls = |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1177 |
let |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1178 |
val cls_id = string_of_clauseID cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1179 |
val ax_name = string_of_axiomName cls |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1180 |
in |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1181 |
((ax_name^""), cls_id) |
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1182 |
end; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
1183 |
|
15347 | 1184 |
|
15608 | 1185 |
fun clause2tptp cls = |
1186 |
let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
|
1187 |
val cls_id = string_of_clauseID cls |
|
1188 |
val ax_name = string_of_axiomName cls |
|
1189 |
val knd = string_of_kind cls |
|
1190 |
val lits_str = ResLib.list_to_string' lits |
|
1191 |
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) |
|
1192 |
in |
|
1193 |
(cls_str,tfree_lits) |
|
1194 |
end; |
|
1195 |
||
1196 |
||
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1197 |
fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; |
15608 | 1198 |
|
15347 | 1199 |
val delim = "\n"; |
1200 |
val tptp_clauses2str = ResLib.list2str_sep delim; |
|
1201 |
||
1202 |
||
1203 |
fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); |
|
1204 |
||
1205 |
||
1206 |
fun string_of_arLit (TConsLit(b,(c,t,args))) = |
|
1207 |
let val pol = if b then "++" else "--" |
|
1208 |
val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) |
|
1209 |
in |
|
1210 |
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" |
|
1211 |
end |
|
1212 |
| string_of_arLit (TVarLit(b,(c,str))) = |
|
1213 |
let val pol = if b then "++" else "--" |
|
1214 |
in |
|
1215 |
pol ^ c ^ "(" ^ str ^ ")" |
|
1216 |
end; |
|
1217 |
||
1218 |
||
1219 |
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); |
|
1220 |
||
1221 |
||
1222 |
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); |
|
1223 |
||
1224 |
||
1225 |
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); |
|
1226 |
||
1227 |
fun tptp_arity_clause arcls = |
|
1228 |
let val arcls_id = string_of_arClauseID arcls |
|
1229 |
val concl_lit = string_of_conclLit arcls |
|
1230 |
val prems_lits = strings_of_premLits arcls |
|
1231 |
val knd = string_of_arKind arcls |
|
1232 |
val all_lits = concl_lit :: prems_lits |
|
1233 |
in |
|
15452 | 1234 |
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")." |
15347 | 1235 |
|
1236 |
end; |
|
1237 |
||
1238 |
||
1239 |
val clrelclause_prefix = "relcls_"; |
|
1240 |
||
1241 |
||
1242 |
fun tptp_classrelLits sub sup = |
|
1243 |
let val tvar = "(T)" |
|
1244 |
in |
|
15531 | 1245 |
case sup of NONE => "[++" ^ sub ^ tvar ^ "]" |
1246 |
| (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" |
|
15347 | 1247 |
end; |
1248 |
||
1249 |
||
1250 |
fun tptp_classrelClause (ClassrelClause cls) = |
|
1251 |
let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) |
|
1252 |
val sub = #subclass cls |
|
1253 |
val sup = #superclass cls |
|
1254 |
val lits = tptp_classrelLits sub sup |
|
1255 |
in |
|
1256 |
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." |
|
1257 |
end; |
|
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
1258 |
|
15347 | 1259 |
end; |