From 448583e76767da575c9d90f54266d434c86282ed Mon Sep 17 00:00:00 2001 From: mark <> Date: Thu, 23 Feb 2012 11:00:45 +0000 Subject: Capability for exporting .dot files added. --- hol-light/TacticRecording/ex.dot | 13 ++ hol-light/TacticRecording/examples1.ml | 7 +- hol-light/TacticRecording/examples3.ml | 65 +++++++++- hol-light/TacticRecording/examples3_LEMMA1.dot | 24 ++++ hol-light/TacticRecording/gvexport.ml | 44 +++++++ hol-light/TacticRecording/hiproofs.ml | 173 +++++++++++++++++++++---- hol-light/TacticRecording/lib.ml | 7 + hol-light/TacticRecording/main.ml | 7 +- hol-light/TacticRecording/mlexport.ml | 75 +---------- hol-light/TacticRecording/printutils.ml | 61 +++++++++ 10 files changed, 375 insertions(+), 101 deletions(-) create mode 100644 hol-light/TacticRecording/ex.dot create mode 100644 hol-light/TacticRecording/examples3_LEMMA1.dot create mode 100644 hol-light/TacticRecording/gvexport.ml create mode 100644 hol-light/TacticRecording/printutils.ml diff --git a/hol-light/TacticRecording/ex.dot b/hol-light/TacticRecording/ex.dot new file mode 100644 index 00000000..fbe961bd --- /dev/null +++ b/hol-light/TacticRecording/ex.dot @@ -0,0 +1,13 @@ +digraph G { + subgraph cluster0 { + label = "process #1" + a0->a1->a2->a3 + } + subgraph cluster1 { + label = "process #2" + b0->b1->b2->b3 + } + b3->23 + b2->a3 + a3->23 +} \ No newline at end of file diff --git a/hol-light/TacticRecording/examples1.ml b/hol-light/TacticRecording/examples1.ml index b587c18f..fd0b446c 100644 --- a/hol-light/TacticRecording/examples1.ml +++ b/hol-light/TacticRecording/examples1.ml @@ -45,10 +45,11 @@ let th = top_thm ();; #use"TacticRecording/mlexport.ml";; -print_executed_proof ();; -print_flat_proof ();; +print_executed_proof true;; +print_flat_proof true;; print_thenl_proof ();; -print_optimal_proof ();; +print_packaged_proof ();; +print_gv_proof ();; g `(y:A) = z ==> (x:A) = x /\ y = y /\ z = z`;; e (STRIP_TAC);; diff --git a/hol-light/TacticRecording/examples3.ml b/hol-light/TacticRecording/examples3.ml index d0e181e2..62a2ef70 100644 --- a/hol-light/TacticRecording/examples3.ml +++ b/hol-light/TacticRecording/examples3.ml @@ -42,9 +42,14 @@ let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;; top_thm ();; print_executed_proof true;; -print_flat_proof false;; +print_flat_proof true;; print_packaged_proof ();; print_thenl_proof ();; +print_gv_proof ();; + +let gtr = !the_goal_tree;; +let h = gtree_to_hiproof gtr;; +let h' = (trivsimp_hiproof o dethen_hiproof) h;; g `!x n. x pow (n + 1) - (&n + &1) * x + &n = (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`;; @@ -82,6 +87,7 @@ let LEMMA_2 = theorem_wrap "LEMMA_2" LEMMA_2;; print_executed_proof true;; print_flat_proof true;; print_packaged_proof ();; +print_gv_proof ();; g `!n x. &0 <= x ==> &0 <= x pow (n + 1) - (&n + &1) * x + &n`;; @@ -123,11 +129,68 @@ print_executed_proof true;; print_flat_proof true;; print_thenl_proof ();; print_packaged_proof ();; +print_gv_proof ();; g `!n x. 1 <= n /\ (!i. 1 <= i /\ i <= n + 1 ==> &0 <= x i) ==> x(n + 1) * (sum(1..n) x / &n) pow n <= (sum(1..n+1) x / (&n + &1)) pow (n + 1)`;; +print_flat_proof true;; +e (STRIP_TAC);; +e (STRIP_TAC);; +e (STRIP_TAC);; +e (ABBREV_TAC `a = sum (1..n + 1) x / (&n + &1)`);; +e (ABBREV_TAC `b = sum (1..n) x / &n`);; +e (SUBGOAL_THEN `x (n + 1) = (&n + &1) * a - &n * b` SUBST1_TAC);; +(* *** Subgoal 1 *** *) +e (EXPAND_TAC "a");; +e (EXPAND_TAC "b");; +e (ASM_SIMP_TAC [REAL_DIV_LMUL; REAL_OF_NUM_EQ; LE_1; REAL_ARITH `~(&n + &1 = &0)`]);; +e (SIMP_TAC [SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; SUM_SING_NUMSEG]);; +e (REAL_ARITH_TAC);; +(* *** Subgoal 2 *** *) +e (SUBGOAL_THEN `&0 <= a /\ &0 <= b` STRIP_ASSUME_TAC);; +(* *** Subgoal 2.1 *** *) +e (EXPAND_TAC "a");; +e (EXPAND_TAC "b");; +e (CONJ_TAC);; +(* *** Subgoal 2.1.1 *** *) +e (MATCH_MP_TAC REAL_LE_DIV);; +e (CONJ_TAC);; +(* *** Subgoal 2.1.1.1 *** *) +e (MATCH_MP_TAC SUM_POS_LE_NUMSEG);; +e (ASM_SIMP_TAC [ARITH_RULE `p <= n ==> p <= n + 1`]);; +(* *** Subgoal 2.1.1.2 *** *) +e (REAL_ARITH_TAC);; +(* *** Subgoal 2.1.2 *** *) +e (MATCH_MP_TAC REAL_LE_DIV);; +e (CONJ_TAC);; +(* *** Subgoal 2.1.2.1 *** *) +e (MATCH_MP_TAC SUM_POS_LE_NUMSEG);; +e (ASM_SIMP_TAC [ARITH_RULE `p <= n ==> p <= n + 1`]);; +(* *** Subgoal 2.1.2.2 *** *) +e (REAL_ARITH_TAC);; +(* *** Subgoal 2.2 *** *) +e (ASM_CASES_TAC `b = &0`);; +(* *** Subgoal 2.2.1 *** *) +e (ASM_SIMP_TAC [REAL_POW_ZERO;LE_1;REAL_MUL_RZERO;REAL_POW_LE]);; +(* *** Subgoal 2.2.2 *** *) +e (ASM_SIMP_TAC [REAL_POW_ZERO;LE_1;REAL_MUL_RZERO;REAL_POW_LE]);; +e (MP_TAC (ISPECL [`n`;`a / b`] LEMMA_2));; +e (ASM_SIMP_TAC [REAL_LE_DIV]);; +e (REWRITE_TAC [REAL_ARITH `&0 <= x - a + b <=> a - b <= x`; REAL_POW_DIV]);; +e (SUBGOAL_THEN `&0 < b` ASSUME_TAC);; +(* *** Subgoal 2.2.2.1 *** *) +e (ASM_REAL_ARITH_TAC);; +(* *** Subgoal 2.2.2.2 *** *) +e (ASM_SIMP_TAC [REAL_LE_RDIV_EQ;REAL_POW_LT]);; +e (MATCH_MP_TAC EQ_IMP);; +e (AP_THM_TAC);; +e (AP_TERM_TAC);; +e (REWRITE_TAC [REAL_POW_ADD]);; +e (UNDISCH_TAC `~(b = &0)`);; +e (CONV_TAC REAL_FIELD);; + (* AGM *) let AGM = prove diff --git a/hol-light/TacticRecording/examples3_LEMMA1.dot b/hol-light/TacticRecording/examples3_LEMMA1.dot new file mode 100644 index 00000000..69bc7c4a --- /dev/null +++ b/hol-light/TacticRecording/examples3_LEMMA1.dot @@ -0,0 +1,24 @@ +digraph G { + subgraph cluster0 { + label = "induction"; + 517->518; + 517->519; + } + subgraph cluster1 { + label = "base case"; + 528->528 + } + subgraph cluster2 { + label = "step case"; + 537->538; + 538->540; + 540->542; + 542->544; + 544->546; + 546->548; + } + 512->513; + 513->517; + 518->528; + 519->537; +} \ No newline at end of file diff --git a/hol-light/TacticRecording/gvexport.ml b/hol-light/TacticRecording/gvexport.ml new file mode 100644 index 00000000..050ef997 --- /dev/null +++ b/hol-light/TacticRecording/gvexport.ml @@ -0,0 +1,44 @@ +(* ========================================================================== *) +(* GRAPHVIZ EXPORT (HOL LIGHT) *) +(* - Exporting recorded tactics into a Dot file for GraphViz *) +(* *) +(* By Mark Adams *) +(* Copyright (c) Univeristy of Edinburgh, 2012 *) +(* ========================================================================== *) + + +let cluster_count = ref 0;; + +let rec print_gv_graphelem d ge = + match ge with + Box (l,ges) + -> let () = (cluster_count := !cluster_count + 1) in + (print_indent d; print_string "subgraph cluster"; + print_int !cluster_count; print_string " "; print_string "{\n"; + print_indent (d+2); print_string "label = "; print_label l; + print_string ";\n"; + do_list (print_gv_graphelem (d+2)) ges; + print_indent d; print_string "}\n") + | Line (id1,id2) + -> (print_indent d; print_goalid id1; print_string " -> "; + print_goalid id2; print_string ";\n") + | Single id + -> (print_indent d; print_goalid id; print_string ";\n");; + +let print_gv_graph ges = + let () = (cluster_count := 0) in + (print_string "digraph G {\n"; + do_list (print_gv_graphelem 2) ges; + print_string "}\n");; + +let print_hiproof_gv_graph h = + let h' = (trivsimp_hiproof o rightgroup_hiproof o + trivsimp_hiproof o dethen_hiproof) h in + let ges = hiproof_graph h' in + print_gv_graph ges;; + +let print_gtree_gv_proof gtr = + let h = gtree_to_hiproof gtr in + print_hiproof_gv_graph h;; + +let print_gv_proof () = print_gtree_gv_proof !the_goal_tree;; diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml index 41941cde..4adee607 100644 --- a/hol-light/TacticRecording/hiproofs.ml +++ b/hol-light/TacticRecording/hiproofs.ml @@ -27,9 +27,9 @@ (* indicates a tactic that completes its goal. *) type hiproof = - Hactive (* Active subgoal *) - | Hatomic of (finfo * int) (* Atomic tactic + arity *) - | Hidentity (* Null, for wiring *) + Hactive of goalid (* Active subgoal *) + | Hatomic of (goalid * int) (* Atomic tactic + arity *) + | Hidentity of goalid (* Null, for wiring *) | Hlabelled of (label * hiproof) (* Box *) | Hsequence of (hiproof * hiproof) (* Serial application *) | Htensor of hiproof list (* Parallel application *) @@ -47,19 +47,21 @@ let dest_hsequence h = let is_hsequence h = can dest_hsequence h;; -let dest_atomic_hiproof h = +let is_hidentity h = match h with Hidentity _ -> true | _ -> false;; + +let hiproof_id h = match h with - Hatomic (info,n) -> (info,n) - | _ -> failwith "dest_atomic_hiproof: Not an atomic hiproof";; + Hactive id | Hatomic (id,_) | Hidentity id -> id + | _ -> failwith "hiproof_id: Not a unit hiproof";; (* Arity *) let rec hiproof_arity h = match h with - Hactive -> 1 + Hactive _ -> 1 | Hatomic (_,n) -> n - | Hidentity -> 1 + | Hidentity _ -> 1 | Hlabelled (_,h0) -> hiproof_arity h0 | Hsequence (h1,h2) -> hiproof_arity h2 | Htensor hs -> sum (map hiproof_arity hs) @@ -74,6 +76,29 @@ type hitrace = +(* ** TRANSLATION OF GOAL TREE TO HIPROOF ** *) + + +let rec gtree_to_hiproof gtr = + let id = gtree_id gtr in + let (_,gtrm) = gtr in + match !gtrm with + Gactive + -> Hactive id + | Gexit _ + -> Hidentity id + | Gexecuted (gstp,gtrs) + -> let h1 = + match gstp with + Gatom _ | Gbox (_,_,true) + -> Hatomic (id, length gtrs) + | Gbox (l,gtr,false) + -> Hlabelled (l, gtree_to_hiproof gtr) in + let h2 = Htensor (map gtree_to_hiproof gtrs) in + Hsequence (h1,h2);; + + + (* ** REFACTORING OPERATIONS ** *) @@ -118,22 +143,27 @@ let collapse_tensor h hs = let trivsimp_hiproof h = let trivsimp h = match h with - Hatomic ((Some"ALL_TAC",[]), _) -> Hidentity - | Hsequence (h1, Hempty) -> h1 - | Hsequence (h1, Hidentity) -> h1 - | Hsequence (Hidentity, h2) -> h2 - | Htensor [] -> Hempty - | Htensor [h0] -> h0 - | Htensor hs0 -> if (forall (fun h0 -> h0 = Hidentity) hs0) - then Hidentity - else Htensor (foldr collapse_tensor hs0 []) - | _ -> h in + Hatomic (id,_) when (gtree_tactic (get_gtree id) = (Some "ALL_TAC",[])) + -> Hidentity id + | Hsequence (h1, Hempty) -> h1 + | Hsequence (h1, Hidentity _) -> h1 + | Hsequence (h1, Htensor hs2) -> if (forall is_hidentity hs2) + then h1 + else h + | Hsequence (Hidentity _, h2) -> h2 + | Hsequence (Htensor hs1, h2) -> if (forall is_hidentity hs1) + then h2 + else h + | Htensor [] -> Hempty + | Htensor [h0] -> h0 + | Htensor hs0 -> Htensor (foldr collapse_tensor hs0 []) + | _ -> h in refactor_hiproof true trivsimp h;; (* Matching up lists of hiproofs *) -let rec matchup_hiproofs hs1 hs2 = +let rec matchup_hiproofs0 hs1 hs2 = match hs1 with [] -> [] | h1::hs01 @@ -144,11 +174,16 @@ let rec matchup_hiproofs hs1 hs2 = then failwith "matchup_hiproofs: unknown arity" else failwith "matchup_hiproofs: Internal error - \ inconsistent arities" in - Hsequence (h1, Htensor hs2a) :: (matchup_hiproofs hs01 hs2b);; + (h1,hs2a) :: (matchup_hiproofs0 hs01 hs2b);; + +let matchup_hiproofs hs1 hs2 = + let hhs = matchup_hiproofs0 hs1 hs2 in + map (fun (h1,hs2) -> Hsequence (h1, Htensor hs2)) hhs;; (* Separating out lists of hiproofs *) +(* let separate_hiproofs0 h (hs01,hs02) = match h with Hsequence (h1,h2) @@ -158,6 +193,7 @@ let separate_hiproofs0 h (hs01,hs02) = (h::hs01, h2::hs02);; let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);; +*) (* Delabelling *) @@ -176,6 +212,14 @@ let delabel_hiproof h = | _ -> h in refactor_hiproof true delabel h;; +let dethen_hiproof h = + let dethen h = + match h with + Hlabelled (Tactical (Some ("THEN" | "THENL"),_), h0) + -> h0 + | _ -> h in + refactor_hiproof true dethen h;; + (* Right-grouping *) @@ -189,6 +233,8 @@ let rightgroup_hiproof h = -> Hsequence (h1, Htensor (matchup_hiproofs hs2 hs3)) | Hsequence (Hsequence (h1, Htensor hs2), h3) -> Hsequence (h1, Htensor (matchup_hiproofs hs2 [h3])) + | Hsequence (Hsequence (h1,h2), h3) + -> Hsequence (h1, Hsequence (h2,h3)) | _ -> h in refactor_hiproof true rightgroup h;; @@ -234,21 +280,94 @@ let thenise_hiproof h = +(* ** HIPROOF GRAPH ** *) + + +(* Graph element datatype *) + +type graph_elem = + Box of (label * graph_elem list) + | Line of (goalid * goalid) + | Single of goalid;; + +let is_box ge = + match ge with Box _ -> true | _ -> false;; + +let mk_line id1 id2 = Line (id1,id2);; + + +(* Utils *) + +let rec hiproof_ins h = + match h with + Hactive id -> [id] + | Hatomic (id,n) -> [id] + | Hidentity id -> [-1] + | Hlabelled (l,h0) -> hiproof_ins h0 + | Hsequence (h1,h2) -> hiproof_ins h1 + | Htensor hs -> flat (map hiproof_ins hs) + | Hempty -> [];; + +let rec hiproof_outs (h:hiproof) : goalid list = + match h with + Hactive id -> [id] + | Hatomic (id,n) -> copy n id + | Hidentity id -> [id] + | Hlabelled (l,h0) -> hiproof_outs h0 + | Hsequence (h1, Htensor hs2) + -> let nhs2 = enumerate hs2 in + let ids1 = hiproof_outs h1 in + let foo (n2,h2) = + if (is_hidentity h2) then [el (n2-1) ids1] + else hiproof_outs h2 in + flat (map foo nhs2) + | Hsequence (h1,h2) -> hiproof_outs h2 + | Htensor hs -> flat (map hiproof_outs hs) + | Hempty -> [];; + + +(* Graph production *) + +let rec hiproof_graph0 h = + match h with + Hactive _ -> [] + | Hatomic _ -> [] + | Hidentity _ -> [] + | Hlabelled (l,Hatomic (id,_)) + -> [Box (l, [Single id])] + | Hlabelled (l,h0) + -> [Box (l, hiproof_graph0 h0)] + | Hsequence (h1,h2) + -> let idids = zip (hiproof_outs h1) (hiproof_ins h2) in + let idids' = filter (fun (_,id2) -> (id2 > 0)) idids in + (hiproof_graph0 h1) @ + (map (fun idid -> Line idid) idids') @ + (hiproof_graph0 h2) + | Htensor hs -> flat (map hiproof_graph0 hs) + | Hempty -> [];; + +let hiproof_graph h = + let ges = hiproof_graph0 h in + let (ges1,ges2) = partition is_box ges in + ges1 @ ges2;; + + + (* ** OTHER OPERATIONS ** *) (* Tactic trace *) -(* Gives a trace of the basic tactics used in the proof, ignoring how they *) -(* were combined by tacticals. *) +(* Gives a linear trace of the basic tactics used in the proof, ignoring how *) +(* they were combined by tacticals. *) let rec hiproof_tactic_trace0 h = match h with - Hactive + Hactive _ -> [active_info] - | Hatomic (info, _) - -> [info] - | Hidentity + | Hatomic (id, _) + -> [gtree_tactic (get_gtree id)] + | Hidentity _ -> [] | Hlabelled (_,h0) -> hiproof_tactic_trace0 h0 @@ -264,7 +383,7 @@ let hiproof_tactic_trace h = (hiproof_tactic_trace0 o delabel_hiproof) h;; (* Block trace *) -(* Gives a trace of the hiproofs used in the proof, stopping at boxes. *) +(* Gives a linear trace of the hiproofs used in the proof, stopping at boxes. *) let rec hiproof_block_trace0 ns0 h = match h with diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml index ae66892e..b1309f84 100644 --- a/hol-light/TacticRecording/lib.ml +++ b/hol-light/TacticRecording/lib.ml @@ -4,6 +4,13 @@ let rec copy n x = else [];; +let rec enumerate0 n xs = + match xs with + [] -> [] + | x::xs0 -> (n,x)::enumerate0 (n+1) xs0;; +let enumerate xs = enumerate0 1 xs;; + + (* foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b *) let rec foldr f xs a = diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml index 44c01951..bfdc1488 100644 --- a/hol-light/TacticRecording/main.ml +++ b/hol-light/TacticRecording/main.ml @@ -15,9 +15,14 @@ #use "TacticRecording/prooftree.ml";; -(* Hiproofs, refactoring and export *) +(* Hiproofs & refactoring *) #use "TacticRecording/hiproofs.ml";; + +(* Export *) + +#use "TacticRecording/printutils.ml";; +#use "TacticRecording/gvexport.ml";; #use "TacticRecording/mlexport.ml";; (* Overwriting the existing HOL Light objects *) diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml index d790deee..429cb770 100644 --- a/hol-light/TacticRecording/mlexport.ml +++ b/hol-light/TacticRecording/mlexport.ml @@ -8,74 +8,11 @@ (* Routines for exporting an ML tactic proof script from the recorded tactic *) -(* proof tree. *) +(* proof tree, via a hiproof representation. *) -(* Translation to hiproof *) - -let rec gtree_to_hiproof gtr = - let (_,gtrm) = gtr in - match !gtrm with - Gactive - -> Hactive - | Gexit id - -> Hidentity - | Gexecuted (gstp,gtrs) - -> let h1 = - match gstp with - Gatom info | Gbox (Tactical info, _, true) - -> Hatomic (info, length gtrs) - | Gbox (l,gtr,false) - -> Hlabelled (l, gtree_to_hiproof gtr) in - let h2 = Htensor (map gtree_to_hiproof gtrs) in - Hsequence (h1,h2);; - - - -(* ** PRINT UTILITIES ** *) - - -(* Basics *) - -let print_string_if b x = if b then print_string x;; - -let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");; - -let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");; - -let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");; - - -(* Printer for 'finfo' *) - -let rec print_farg x0 br arg = - match arg with - Fint n -> print_int n - | Fstring x -> print_fstring x - | Fterm tm -> print_fterm tm - | Ftype ty -> print_ftype ty - | Fthm prf -> print_finfo "" br prf - | Fpair (arg1,arg2) - -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in - (print_string_if br "("; - print_farg x0 false arg1; - print_string sep; - print_farg x0 false arg2; - print_string_if br ")") - | Flist args - -> let sep = if (forall is_atomic_farg args) then ";" else "; " in - (print_string "["; - print_seplist (print_farg x0 false) sep args; - print_string "]") - | Ffn f - -> (print_finfo x0 br f) - -and print_finfo x0 br ((x_,args):finfo) = - (print_string_if (br & not (is_empty args)) "("; - print_option x0 x_; - do_list (fun arg -> print_string " "; print_farg x0 true arg) args; - print_string_if (br & not (is_empty args)) ")");; +(* ** UTILS ** *) (* Printer for tactic 'finfo' *) @@ -116,11 +53,11 @@ let print_hitrace_line_with fl pr htr = let print_hiproof0 pr br h = match h with - Hactive + Hactive _ -> print_string "..." - | Hatomic (info,_) - -> print_tactic br info - | Hidentity + | Hatomic (id,_) + -> print_tactic br (gtree_tactic (get_gtree id)) + | Hidentity _ -> print_string "ALL_TAC" | Hlabelled (_,h0) -> pr br h0 diff --git a/hol-light/TacticRecording/printutils.ml b/hol-light/TacticRecording/printutils.ml new file mode 100644 index 00000000..9131e18d --- /dev/null +++ b/hol-light/TacticRecording/printutils.ml @@ -0,0 +1,61 @@ +(* ========================================================================== *) +(* PRINTER UTILITIES (HOL LIGHT) *) +(* - Various basic utilities used in writing the exporters *) +(* *) +(* By Mark Adams *) +(* Copyright (c) Univeristy of Edinburgh, 2012 *) +(* ========================================================================== *) + + +(* Basics *) + +let print_string_if b x = if b then print_string x;; + +let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");; + +let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");; + +let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");; + +let print_goalid id = print_int id;; + +let print_indent d = print_string (String.make d ' ');; + + +(* Printer for 'finfo' *) + +let rec print_farg x0 br arg = + match arg with + Fint n -> print_int n + | Fstring x -> print_fstring x + | Fterm tm -> print_fterm tm + | Ftype ty -> print_ftype ty + | Fthm prf -> print_finfo "" br prf + | Fpair (arg1,arg2) + -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in + (print_string_if br "("; + print_farg x0 false arg1; + print_string sep; + print_farg x0 false arg2; + print_string_if br ")") + | Flist args + -> let sep = if (forall is_atomic_farg args) then ";" else "; " in + (print_string "["; + print_seplist (print_farg x0 false) sep args; + print_string "]") + | Ffn f + -> (print_finfo x0 br f) + +and print_finfo x0 br ((x_,args):finfo) = + (print_string_if (br & not (is_empty args)) "("; + print_option x0 x_; + do_list (fun arg -> print_string " "; print_farg x0 true arg) args; + print_string_if (br & not (is_empty args)) ")");; + + +(* Printer for labels *) + +let print_label l = + match l with + Tactical (Some x, _) | Label x -> print_fstring x + | Tactical (None, _) -> print_fstring "";; -- cgit v1.2.3