1
請按照我上一個問題的示例：Error when convert to Boolean matrix。以Coq格式打印等同類
let entries = [("name", ["string"]); ("label", ["nonNegativeInteger"; "symbol"]);
("symbol", ["name"; "symbol"; "symbol"; "label"]); ("var", ["string"]);
("term", ["var"; "symbol"; "term"]); ("rule", ["term"; "term"]);
("rules", ["rule"]); ("dps", ["rules"]); ("trs", ["rules"]);
("usableRules", ["rules"]);
("number", ["integer"; "integer"; "positiveInteger"]);
("coefficient",["number"; "minusInfinity"; "plusInfinity"; "vector"; "matrix"])
("vector", ["coefficient"]); ("matrix", ["vector"])]
let defined = ["name"; "label"; "symbol"; "var"; "term"; "rule"; "rules";
"dps"; "trs"; "usableRules"; "number"; "coefficient"; "vector"; "matrix"]
let undefined = ["string"; "nonNegativeInteger"; "integer"; "positiveInteger";
"minusInfinity"; "plusInfinity"]
我計算具有以下功能：（詳情請參閱此處：Transitive closure and equivalence classes和Asking about return type, list and set data structure in OCaml）
let rec position x = function
| [] -> raise Not_found
| y :: ys -> if x = y then 0 else 1 + position x ys
let len_undefined = List.length undefined
let num_of_name xsds undefined len_undefined s =
try (position s xsds) + len_undefined;
with Not_found -> position s undefined
let name_of_num xsds undefined len_undefined k =
if k < len_undefined then
List.nth undefined k else
List.nth xsds (k - len_undefined)
let matrix =
let len = List.length defined + len_undefined in
let boolmat = Array.make_matrix len len false in
List.iter (fun (s, strs) ->
let pos1 = num_of_name defined undefined len_undefined s in
List.iter (fun t ->
let pos2 = num_of_name defined undefined len_undefined t in
boolmat.(pos1).(pos2) <- true) strs) entries;
boolmat
let transClosure m =
let n = Array.length m in
for k = 0 to n - 1 do
let mk = m.(k) in
for i = 0 to n - 1 do
let mi = m.(i) in
for j = 0 to n - 1 do
mi.(j) <- max mi.(j) (min mi.(k) mk.(j))
done;
done;
done;
m;;
let eq_class m i =
let column = m.(i)
and set = ref [] in
Array.iteri begin fun j l ->
if j = i || column.(j) && m.(j).(i) then
set := j :: !set else ignore l
end column;
!set;;
let eq_classes m =
let classes = ref [] in
Array.iteri begin fun e _ ->
if not (List.exists (List.mem e) !classes) then
classes := eq_class m e :: !classes
end m;
!classes;;
let cmp_classes m c c' = if c = c' then 0 else
match c, c' with
| i :: _, j :: _ -> if m.(i).(j) then 1 else -1
| _ -> assert false
let sort_eq_classes m = List.sort (cmp_classes m);;
let order_xsds =
let tc_xsds = transClosure matrix in
let eq_xsds = eq_classes tc_xsds in
let sort_eq_xsds = sort_eq_classes tc_xsds eq_xsds in
sort_eq_xsds
let print =
let f elem =
print_int elem ; print_string " "
in List.iter f (List.flatten order_xsds);;
let xsds_of_int =
List.map (List.map (name_of_num defined undefined len_undefined))
let xsds_sort = xsds_of_int order_xsds
let print_string =
let f elem =
print_string elem ; print_string " \n"
in List.iter f (List.flatten xsds_sort);;
我嘗試打印結果看排序等價類：
var name symbol label plusInfinity minusInfinity positiveInteger integer number
matrix vector coefficient nonNegativeInteger string term rule rules usableRules
trs dps
因爲我必須以Coq格式打印，所以我必須將文件輸出組合起來，所以我想按等效類結果的順序打印結果，它看到一個等價類（「標籤」 - 「符號」; 「係數」 - 「基質」 - 「載體」）它應該打印：
編輯：
Inductive label := all the type label depends
with symbol := all the type symbol depends.
例如：
Inductive label :=
| Label : nonNegativeInteger -> symbol -> label
with symbol :=
| Symbol : name -> symbol -> symbol -> label -> symbol.
當一個類型取決於它將打印對我來說，例如：
Definition name := string.
並且當它大於2時依賴性PE，
Inductive numer := all the type number depends.
例如：
Inductive number :=
|Number : integer -> integer -> positiveInteger -> number.
我想類型的undefined類型列表之前應該打印後，將在列表中的排序後的結果打印（和所有類型undefined名單不應該再次打印），例如，結果我希望是這樣的：
Definition string := string.
Definition nonNegative := int.
...
Definition var := string.
Definition name := string.
Inductive label := ...
with symbol := ...
等等
你能幫我嗎？