X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=74a6a749eb245704364bb4b4f34bd3681fd1c87f;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=5d8fae1b6f463961d2610e80199602172ad158c0;hpb=ed3cc138a0066b654db61f28a176c54d35a4ddc3;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 5d8fae1b6..74a6a749e 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -39,55 +39,57 @@ open TacticAst 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 - | Assumption -> current_size + 10 - | Change (t1, t2, where) -> + | 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 *) let size2 = countterm size1 t2 in (match where with None -> size2 | Some ident -> size2 + 3 + String.length ident) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> current_size + 13 - | Cut term -> countterm (current_size + 4) term - | Decompose (ident, principles) -> + | Change_pattern _ -> assert false (* TODO *) + | Contradiction _ -> current_size + 13 + | Cut (_, term) -> countterm (current_size + 4) term + | Decompose (_, ident, principles) -> List.fold_left (fun size s -> size + (String.length s)) (current_size + 11 + String.length ident) principles - | Discriminate ident -> current_size + 12 + (String.length ident) - | Elim (term, using) -> + | Discriminate (_, ident) -> current_size + 12 + (String.length ident) + | Elim (_, term, using) -> let size1 = countterm (current_size + 5) term in (match using with None -> size1 | Some term -> countterm (size1 + 7) term) - | ElimType term -> countterm (current_size + 10) term - | Exact term -> countterm (current_size + 6) term - | Exists -> current_size + 6 - | Fold (kind, term) -> + | ElimType (_, term) -> countterm (current_size + 10) term + | Exact (_, term) -> countterm (current_size + 6) term + | Exists _ -> current_size + 6 + | Fold (_, kind, term) -> countterm (current_size + 5) term - | Fourier -> current_size + 7 - | Injection ident -> current_size + 10 + (String.length ident) - | Intros (num, idents) -> + | Fourier _ -> current_size + 7 + | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) + | Hint _ -> current_size + 4 + | Injection (_, ident) -> current_size + 10 + (String.length ident) + | Intros (_, num, idents) -> List.fold_left (fun size s -> size + (String.length s)) (current_size + 7) idents - | Left -> current_size + 4 - | LetIn (term, ident) -> + | Left _ -> current_size + 4 + | LetIn (_, term, ident) -> countterm (current_size + 5 + String.length ident) term - | Reduce (_, _, _) -> assert false (* TODO *) - | Reflexivity -> current_size + 11 - | Replace (t1, t2) -> + | Reduce _ -> assert false (* TODO *) + | Reflexivity _ -> current_size + 11 + | Replace (_, t1, t2) -> let size1 = countterm (current_size + 14) t1 in (* replace, with *) countterm size1 t2 - | Replace_pattern (_, _) -> assert false (* TODO *) - | Rewrite (_, _, _) -> assert false (* TODO *) - | Right -> current_size + 5 - | Ring -> current_size + 4 - | Split -> current_size + 5 - | Symmetry -> current_size + 8 - | Transitivity term -> + | Replace_pattern _ -> assert false (* TODO *) + | Rewrite _ -> assert false (* TODO *) + | Right _ -> current_size + 5 + | Ring _ -> current_size + 4 + | Split _ -> current_size + 5 + | Symmetry _ -> current_size + 8 + | Transitivity (_, term) -> countterm (current_size + 13) term ;; @@ -98,29 +100,41 @@ let is_big_tac tac = ;; (* 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 - LocatedTactic (loc, tac) -> - big_tactic2box ~attr tac - | Absurd -> Box.Text([],"absurd") - | Apply term -> +and big_tactic2box = function + | Absurd (_, term) -> + Box.V([],[Box.Text([],"absurd"); + ast2astBox term]) + | Apply (_, term) -> Box.V([],[Box.Text([],"apply"); - ast2box ~attr term]) - | Assumption -> Box.Text([],"assumption") - | Change (t1, t2, where) -> + ast2astBox term]) + | Assumption _ -> Box.Text([],"assumption") + | Auto _ -> Box.Text([],"auto") + | Change (_, t1, t2, where) -> let where = (match where with None -> [] @@ -131,18 +145,16 @@ and big_tactic2box ?(attr = []) = function Box.V([], (pretty_append [Box.Text([],"change")] - t1 - [])@ + t1)@ (pretty_append [Box.Text([],"with")] - t2 - [])@where) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> Box.Text([],"contradiction") - | Cut term -> + t2)@where) + | Change_pattern _ -> assert false (* TODO *) + | Contradiction _ -> Box.Text([],"contradiction") + | Cut (_, term) -> Box.V([],[Box.Text([],"cut"); - Box.indent(ast2box term)]) - | Decompose (ident, principles) -> + Box.indent(ast2astBox term)]) + | Decompose (_, ident, principles) -> let principles = List.map (fun x -> Box.Text([],x)) principles in Box.V([],[Box.Text([],"decompose"); @@ -150,40 +162,40 @@ and big_tactic2box ?(attr = []) = function Box.V([],principles); Box.Text([],"]")]); Box.Text([],ident)]) - | Discriminate ident -> + | Discriminate (_, ident) -> Box.V([],[Box.Text([],"discriminate"); Box.Text([],ident)]) - | Elim (term, using) -> + | Elim (_, term, using) -> let using = (match using with None -> [] | Some term -> (pretty_append [Box.Text([],"using")] - term - [])) in + term)) in Box.V([], (pretty_append [Box.Text([],"elim")] - term - [])@using) - | ElimType term -> + term)@using) + | ElimType (_, term) -> Box.V([],[Box.Text([],"elim type"); - Box.indent(ast2box term)]) - | Exact term -> + Box.indent(ast2astBox term)]) + | Exact (_, term) -> Box.V([],[Box.Text([],"exact"); - Box.indent(ast2box term)]) - | Exists -> Box.Text([],"exists") - | Fold (kind, 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)]) - | Fourier -> Box.Text([],"fourier") - | Injection ident -> + Box.indent(ast2astBox term)]) + | Fourier _ -> Box.Text([],"fourier") + | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) + | Hint _ -> Box.Text([],"hint") + | Injection (_, ident) -> Box.V([],[Box.Text([],"transitivity"); Box.indent (Box.Text([],ident))]) - | Intros (num, idents) -> + | Intros (_, num, idents) -> let num = (match num with None -> [] @@ -193,65 +205,67 @@ and big_tactic2box ?(attr = []) = function Box.V([],[Box.Text([],"decompose"); Box.H([],[Box.smallskip; Box.V([],idents)])]) - | Left -> Box.Text([],"left") - | LetIn (term, ident) -> + | Left _ -> Box.Text([],"left") + | LetIn (_, term, ident) -> Box.V([],[Box.H([],[Box.Text([],"let"); Box.smallskip; Box.Text([],ident); Box.smallskip; Box.Text([],"=")]); - Box.indent (ast2box term)]) - | Reduce (_, _, _) -> assert false (* TODO *) - | Reflexivity -> Box.Text([],"reflexivity") - | Replace (t1, t2) -> + 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 - [])) - | Replace_pattern (_, _) -> assert false (* TODO *) - | Rewrite (_, _, _) -> assert false (* TODO *) - | Right -> Box.Text([],"right") - | Ring -> Box.Text([],"ring") - | Split -> Box.Text([],"split") - | Symmetry -> Box.Text([],"symmetry") - | Transitivity term -> + t2)) + | Replace_pattern _ -> assert false (* TODO *) + | Rewrite _ -> assert false (* TODO *) + | Right _ -> Box.Text([],"right") + | Ring _ -> Box.Text([],"ring") + | Split _ -> Box.Text([],"split") + | 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 - | Fail -> Box.Text([],"fail") - | Do (count, tac) -> +let rec tactical2box = function + | 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); Box.indent (tactical2box tac)]) - | IdTac -> Box.Text([],"id") - | Repeat tac -> + | IdTac _ -> Box.Text([],"id") + | Repeat (_, tac) -> Box.V([],[Box.Text([],"repeat"); Box.indent (tactical2box tac)]) - | Seq tacs -> + | Seq (_, tacs) -> Box.V([],tacticals2box tacs) - | Tactic tac -> tactic2box tac - | Then (tac, tacs) -> + | Then (_, tac, tacs) -> Box.V([],[tactical2box tac; Box.H([],[Box.skip; Box.Text([],"["); Box.V([],tacticals2box tacs); Box.Text([],"]");])]) - | Tries tacs -> + | Tries (_, tacs) -> Box.V([],[Box.Text([],"try"); Box.H([],[Box.skip; Box.Text([],"["); Box.V([],tacticals2box tacs); Box.Text([],"]");])]) - | Try tac -> + | Try (_, tac) -> Box.V([],[Box.Text([],"try"); Box.indent (tactical2box tac)])