X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=80e3effce2e31c0580b3330a3ee09f36c6eeec43;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=3c4026f95137deba0ecb6da57323c2cfd5f43770;hpb=9766d606b71ec69594919ca34b067e268afeabf0;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 3c4026f95..80e3effce 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -40,8 +40,9 @@ let rec count_tactic current_size tac = if current_size > maxsize then current_size else match tac with LocatedTactic (_, tac) -> count_tactic current_size tac - | Absurd -> current_size + 6 - | Apply term -> countterm (current_size+6) term + | Absurd term -> countterm (current_size + 6) term + | Apply term -> countterm (current_size + 6) term + | Auto -> current_size + 4 | Assumption -> current_size + 10 | Change (t1, t2, where) -> let size1 = countterm (current_size + 12) t1 in (* change, with *) @@ -68,6 +69,7 @@ let rec count_tactic current_size tac = | Fold (kind, term) -> countterm (current_size + 5) term | Fourier -> current_size + 7 + | Hint -> current_size + 4 | Injection ident -> current_size + 10 + (String.length ident) | Intros (num, idents) -> List.fold_left @@ -76,7 +78,7 @@ let rec count_tactic current_size tac = | Left -> current_size + 4 | LetIn (term, ident) -> countterm (current_size + 5 + String.length ident) term - | Reduce (_, _, _) -> assert false (* TODO *) + | Reduce (_, _) -> assert false (* TODO *) | Reflexivity -> current_size + 11 | Replace (t1, t2) -> let size1 = countterm (current_size + 14) t1 in (* replace, with *) @@ -93,33 +95,47 @@ let rec count_tactic current_size tac = let is_big_tac tac = let n = (count_tactic 0 tac) in - prerr_endline ("Lunghezza: " ^ (string_of_int n)); +(* prerr_endline ("Lunghezza: " ^ (string_of_int n)); *) n > maxsize ;; (* prova *) -let rec small_tactic2box ?(attr = []) tac = +let rec small_tactic2box tac = Box.Text([], TacticAstPp.pp_tactic tac) let string_of_kind = function | `Reduce -> "reduce" - | `Simpl -> "simpl" + | `Simpl -> "simplify" | `Whd -> "whd" -let rec tactic2box ?(attr = []) tac = +let dummy_tbl = Hashtbl.create 0 + +let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl) + +let pretty_append l ast = + if is_big ast then + [Box.H([],l); + Box.H([],[Box.skip; ast2astBox ast])] + else + [Box.H([],l@[Box.smallskip; ast2astBox ast])] + +let rec tactic2box tac = if (is_big_tac tac) then - big_tactic2box ~attr tac + big_tactic2box tac else - small_tactic2box ~attr tac + small_tactic2box tac -and big_tactic2box ?(attr = []) = function +and big_tactic2box = function LocatedTactic (loc, tac) -> - big_tactic2box ~attr tac - | Absurd -> Box.Text([],"absurd") + big_tactic2box tac + | Absurd term -> + Box.V([],[Box.Text([],"absurd"); + ast2astBox term]) | Apply term -> Box.V([],[Box.Text([],"apply"); - ast2box ~attr term]) + ast2astBox term]) | Assumption -> Box.Text([],"assumption") + | Auto -> Box.Text([],"auto") | Change (t1, t2, where) -> let where = (match where with @@ -131,17 +147,15 @@ and big_tactic2box ?(attr = []) = function Box.V([], (pretty_append [Box.Text([],"change")] - t1 - [])@ + t1)@ (pretty_append [Box.Text([],"with")] - t2 - [])@where) + t2)@where) | Change_pattern (_, _, _) -> assert false (* TODO *) | Contradiction -> Box.Text([],"contradiction") | Cut term -> Box.V([],[Box.Text([],"cut"); - Box.indent(ast2box term)]) + Box.indent(ast2astBox term)]) | Decompose (ident, principles) -> let principles = List.map (fun x -> Box.Text([],x)) principles in @@ -160,26 +174,25 @@ and big_tactic2box ?(attr = []) = function | Some term -> (pretty_append [Box.Text([],"using")] - term - [])) in + term)) in Box.V([], (pretty_append [Box.Text([],"elim")] - term - [])@using) + term)@using) | ElimType term -> Box.V([],[Box.Text([],"elim type"); - Box.indent(ast2box term)]) + Box.indent(ast2astBox term)]) | Exact term -> Box.V([],[Box.Text([],"exact"); - Box.indent(ast2box term)]) + Box.indent(ast2astBox term)]) | Exists -> Box.Text([],"exists") | Fold (kind, term) -> Box.V([],[Box.H([],[Box.Text([],"fold"); Box.smallskip; Box.Text([],string_of_kind kind)]); - Box.indent(ast2box term)]) + Box.indent(ast2astBox term)]) | Fourier -> Box.Text([],"fourier") + | Hint -> Box.Text([],"hint") | Injection ident -> Box.V([],[Box.Text([],"transitivity"); Box.indent (Box.Text([],ident))]) @@ -200,19 +213,17 @@ and big_tactic2box ?(attr = []) = function Box.Text([],ident); Box.smallskip; Box.Text([],"=")]); - Box.indent (ast2box term)]) - | Reduce (_, _, _) -> assert false (* TODO *) + Box.indent (ast2astBox term)]) + | Reduce (_, _) -> assert false (* TODO *) | Reflexivity -> Box.Text([],"reflexivity") | Replace (t1, t2) -> Box.V([], (pretty_append [Box.Text([],"replace")] - t1 - [])@ + t1)@ (pretty_append [Box.Text([],"with")] - t2 - [])) + t2)) | Replace_pattern (_, _) -> assert false (* TODO *) | Rewrite (_, _, _) -> assert false (* TODO *) | Right -> Box.Text([],"right") @@ -221,13 +232,18 @@ and big_tactic2box ?(attr = []) = function | Symmetry -> Box.Text([],"symmetry") | Transitivity term -> Box.V([],[Box.Text([],"transitivity"); - Box.indent (ast2box term)]) + Box.indent (ast2astBox term)]) ;; open TacticAst -let rec tactical2box ?(attr = []) = function - LocatedTactical (loc, tac) -> tactical2box tac +let rec tactical2box = function + | LocatedTactical (loc, tac) -> tactical2box tac + + | Tactic tac -> tactic2box tac + | Command cmd -> (* TODO dummy implementation *) + Box.Text([], TacticAstPp.pp_tactical (Command cmd)) + | Fail -> Box.Text([],"fail") | Do (count, tac) -> Box.V([],[Box.Text([],"do " ^ string_of_int count); @@ -238,7 +254,6 @@ let rec tactical2box ?(attr = []) = function Box.indent (tactical2box tac)]) | Seq tacs -> Box.V([],tacticals2box tacs) - | Tactic tac -> tactic2box tac | Then (tac, tacs) -> Box.V([],[tactical2box tac; Box.H([],[Box.skip;