package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
doc/src/lambdapi.tool/tree_graphviz.ml.html
Source file tree_graphviz.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
(** Representation of trees as graphviz files. {{:https://graphviz.org}Graphviz} is a graph visualization software. This module handles the conversion from {!type:Core.Term.dtree} data structures in the [dot] language that can be interpreted by graphviz. See the chapter [doc/options.md#printing-decision-trees] of the documentation for more information. *) open Lplib open Base open Timed open Core open Term open Tree_type (** Printing hint for conversion to graphviz. *) type dot_term = | DotDefa (* Default case *) | DotAbst of int | DotProd of int | DotCons of TC.t | DotSuccess | DotFailure (** [to_dot ppf sym] prints a dot graphviz representation of the tree of symbol [sym] on [ppf]. Each node of the tree embodies a pattern matrix. The label of a node is the column index in the matrix on which the matching is performed to give birth to the child node. The label on the edge between a node and one of its children represents the term matched to generate the next pattern matrix (the one of the child node). *) let to_dot : Format.formatter -> sym -> unit = fun ppf s -> let output_tree ppf tree = let dotterm : dot_term pp = fun ppf dh -> let var_px = "v" in match dh with | DotAbst(id) -> out ppf "λ%s%d" var_px id | DotProd(id) -> out ppf "Π%s%d" var_px id | DotDefa -> out ppf "*" | DotCons(Symb(_,n,a)) -> out ppf "%s<sub>%d</sub>" n a | DotCons(Vari(i)) -> out ppf "%s%d" var_px i | DotCons(Type) -> out ppf "TYPE" | DotSuccess -> out ppf "✓" | DotFailure -> out ppf "✗" in let tcstr : tree_cond pp = fun ppf cstr -> let ar = Array.pp int " " in match cstr with | CondNL(i, j) -> out ppf "%d ≡ %d" i j | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i in let node_count = ref 0 in (* [write_tree n u v] writes tree [v] obtained from tree number [n] with a switch on [u] ({!constructor:None} if default). *) let rec write_tree father_l swon t = incr node_count; match t with | Leaf(_,(a,_)) -> let _, acte = Bindlib.unmbind a in out ppf "@ %d [label=\"%a\"];" !node_count Print.term acte; out ppf "@ %d -- %d [label=<%a>];" father_l !node_count dotterm swon | Node({swap; children; store; abstraction=abs; default; product}) -> let tag = !node_count in (* Create node *) out ppf "@ %d [label=\"%d\"%s];" tag swap (if store then " shape=\"box\"" else ""); (* Create edge *) out ppf "@ %d -- %d [label=<%a>];" father_l tag dotterm swon; TCMap.iter (fun s e -> write_tree tag (DotCons(s)) e) children; Option.iter (fun (x,t) -> write_tree tag (DotAbst(x)) t) abs; Option.iter (fun (x,t) -> write_tree tag (DotProd(x)) t) product; Option.iter (write_tree tag DotDefa) default | Cond({ ok ; cond ; fail }) -> let tag = !node_count in out ppf "@ %d [label=<%a> shape=\"diamond\"];" tag tcstr cond; out ppf "@ %d -- %d [label=<%a>];" father_l tag dotterm swon; write_tree tag DotSuccess ok; write_tree tag DotFailure fail | Eos(l,r) -> let tag = !node_count in out ppf "@ %d [label=\"\" shape=\"triangle\"];" tag; out ppf "@ %d -- %d [label=<%a>];" father_l tag dotterm swon; write_tree tag DotFailure l; write_tree tag DotSuccess r | Fail -> out ppf "@ %d [label=<!>];" !node_count; out ppf "@ %d -- %d [label=\"!\"];" father_l !node_count in out ppf "graph {@[<v>"; begin match tree with (* First step must be done to avoid drawing a top node. *) | Node{swap; store; children; default; abstraction; product} -> out ppf "@ 0 [label=\"%d\"%s];" swap (if store then " shape=\"box\"" else ""); TCMap.iter (fun sw c -> write_tree 0 (DotCons(sw)) c) children; Option.iter (fun (x,t) -> write_tree 0 (DotAbst(x)) t) abstraction; Option.iter (fun (x,t) -> write_tree 0 (DotProd(x)) t) product; Option.iter (fun t -> write_tree 0 DotDefa t) default | Leaf(_) -> () | _ -> assert false end; out ppf "@.}@\n@?" in output_tree ppf (Lazy.force (snd !(s.sym_dtree)))
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>