有条件打印

Question

我在这个问题上明确提出问题。 我有这样一个图：

a <-> b -> e -> f 
|   | 
v   v 
h <------- g 
|   | 
v   v 
u   k 

有依赖关系列表中的描述entries

let entries = [ 
    ("a", ["b"; "h"]); 
    ("b", ["a"; "e"]); 
    ("e", ["f"; "g"]); 
    ("g", ["h"; "k"]); 
    ("h", ["u"]); 
] 

我提取的列表defined和undefined，结果是这样的：

let defined = ["a"; "b"; "e"; "g"; "h"; "u"] 
let undefined = ["f"; "k"] 

经过计算，我得到了一个新的名单与他们的订购：

let ordered = [["u"];["h"]; ["k"]; ["g"]; ["f"]; ["e"]; ["b"; "a"]] 

我想写打印ordered输出在这样的条件下这样的功能：

1）我想有就会在列表中ordered产生一个新的列表功能如果undefined元素出现它会将其删除。我期待一个newordered这样的：

newordered = [["u"]; ["h"]; ["g"]; ["e"]; ["b"; "a"]] 

2）我想打印其取决于这个条件：

当它只是一种依赖，它会打印：

Definition name := type depend. 

当它是一个等价性（一个< - > b）中，将打印：

Inductive name1 := type depend 1 
with name2 := type depend 2. 

WH恩它的类型取决于列表，它会打印：

Inductive name := type depend. 

当看到undefined列表中的类型，当它不依赖型，它将打印：

Definition name := name. 

，并与顺序在newordered列表

输出我期待这样的顺序：

Definition k := k. 
Definition f := f. 
Definition u := u. 
Definition h := u. 
Inductive g := h -> k. 
Inductive e := f -> g. 
Inductive b := a -> e 
with a := b -> h. 

我写这些功能，首先我打印不确定的列表中的所有元素：

let print_undfined = 
List.iter (fun name -> Printf.printf "\nDefinition %s := %s." name name; 
     print_string "\n")undefined 

我有打印权限的功能 - 条目列表的右侧：

let defn_of = 
    List.iter (fun (_, xs) -> 
    List.iter (fun t -> Printf.printf "%s" t) xs) 

我有另一个功能删除在ordered列表中的重复与undefined列表

let rec uniquify = function 
| [] -> [] 
| x::xs -> x :: uniquify (List.filter ((<>) x) xs) 

let new_sort = uniquify (undefined @ List.flatten ordered) 

但这份名单是string list，并将其添加编辑字体中的undefined列表。所以如果我打印我的最后一个功能，它将复制undefined如果我选择先打印undefined中的所有元素。我不想那样。

而我不是我怎么能写出最后的功能与打印我输出我想在最后。

Answer 1

首先，我纠正defn_of功能，通过查找entries返回标签的关系的字符串表示：

let defn_of label = 
    try 
     let (_, xs) = List.find (fun (l, ys) -> l = label) entries in 
     String.concat "->" xs 
    with 
     Not_found -> "" 

其次，你在new_sort返回（这应该是newordered），显然是错误的。你真正想要的是undefined筛选出一个元素发生的历史所有列表：

let newordered = List.filter (function [x] -> List.for_all((<>) x) undefined 
             | _ -> true) ordered 

像往常一样，打印功能是基于Printf模块和String.concat功能。 有两种情况在您的打印任务：

案例1：的所有标签中undefined，使用上面的print_undfined功能。

案例2：newordered任何名单xs，如果xs只有一个元素，这意味着没有等价类存在。如果xs至少有两个元素，等价类应印：

let print_defined_equivalence xs = 
    match xs with 
    | [] ->() 
    | [x] -> Printf.printf "\nInductive %s := %s." x (defn_of x) 
    | _ -> 
     let ys = String.concat "\nwith" 
        (List.map (fun x -> 
        Printf.sprintf "%s := %s" x (defn_of x)) 
         xs) in 
     Printf.printf "\nInductive %s." ys 

作为一个方面说明，我选择来处理空单为newordered元素虽然它没有在您的测试情况下发生。另一件事是entries被遍历多次查找元素，应该更改为Map数据类型，特别是当entries大时。

鉴于我已经明确说明每种情况的条件，您应该能够将这些功能插入到您的程序中。