X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=ba14fd0d635372a4480f3e9e7daa4af681e14ecf;hb=a3acd934eba07f24937e59c3c7a41db82d901025;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..ba14fd0d6 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -39,55 +39,49 @@ 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) -> - 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) -> - 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) -> + | Absurd (_, term) -> countterm (current_size + 6) term + | Apply (_, term) -> countterm (current_size + 6) term + | Auto _ -> current_size + 4 + | Assumption _ -> current_size + 10 + | Compare (_, term) -> countterm (current_size + 7) term + | Constructor (_, n) -> current_size + 12 + | Contradiction _ -> current_size + 13 + | Cut (_, ident, term) -> + let id_size = + match ident with + None -> 0 + | Some id -> String.length id + 4 + in + countterm (current_size + 4 + id_size) term + | DecideEquality _ -> current_size + 15 + | Decompose (_, term) -> + countterm (current_size + 11) term + | Discriminate (_, term) -> countterm (current_size + 12) term + | 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) -> - countterm (current_size + 5) term - | Fourier -> current_size + 7 - | Injection ident -> current_size + 10 + (String.length ident) - | Intros (num, idents) -> + | ElimType (_, term) -> countterm (current_size + 10) term + | Exact (_, term) -> countterm (current_size + 6) term + | Exists _ -> current_size + 6 + | Fourier _ -> current_size + 7 + | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) + | Injection (_, term) -> + countterm (current_size + 10) term + | 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) -> - 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 -> + | Reflexivity _ -> current_size + 11 + | Right _ -> current_size + 5 + | Ring _ -> current_size + 4 + | Split _ -> current_size + 5 + | Symmetry _ -> current_size + 8 + | Transitivity (_, term) -> countterm (current_size + 13) term ;; @@ -98,92 +92,74 @@ 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" + | `Normalize -> "normalize" + +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 ?(attr = []) tac = +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) -> - let where = - (match where with - None -> [] - | Some ident -> - [Box.Text([],"in"); - Box.smallskip; - Box.Text([],ident)]) in - Box.V([], - (pretty_append - [Box.Text([],"change")] - t1 - [])@ - (pretty_append - [Box.Text([],"with")] - 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) -> - let principles = - List.map (fun x -> Box.Text([],x)) principles in + ast2astBox term]) + | Assumption _ -> Box.Text([],"assumption") + | Auto _ -> Box.Text([],"auto") + | Compare (_, term) -> + Box.V([],[Box.Text([],"compare"); + Box.indent(ast2astBox term)]) + | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n) + | Contradiction _ -> Box.Text([],"contradiction") + | DecideEquality _ -> Box.Text([],"decide equality") + | Decompose (_, term) -> Box.V([],[Box.Text([],"decompose"); - Box.H([],[Box.Text([],"["); - Box.V([],principles); - Box.Text([],"]")]); - Box.Text([],ident)]) - | Discriminate ident -> - Box.V([],[Box.Text([],"discriminate"); - Box.Text([],ident)]) - | Elim (term, using) -> + Box.indent(ast2astBox term)]) + | Discriminate (_, term) -> + Box.V([],pretty_append [Box.Text([],"discriminate")] term) + | 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.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.V([],[Box.Text([],"transitivity"); - Box.indent (Box.Text([],ident))]) - | Intros (num, idents) -> + Box.indent(ast2astBox term)]) + | Exists _ -> Box.Text([],"exists") + | Fourier _ -> Box.Text([],"fourier") + | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) + | Intros (_, num, idents) -> let num = (match num with None -> [] @@ -193,65 +169,49 @@ 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.V([], - (pretty_append - [Box.Text([],"replace")] - 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 -> + Box.indent (ast2astBox term)]) + | Reflexivity _ -> Box.Text([],"reflexivity") + | 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 + | Do (_, count, tac) -> Box.V([],[Box.Text([],"do " ^ string_of_int count); Box.indent (tactical2box tac)]) - | IdTac -> Box.Text([],"id") - | Repeat tac -> + | 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)])