X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=ba14fd0d635372a4480f3e9e7daa4af681e14ecf;hb=a3acd934eba07f24937e59c3c7a41db82d901025;hp=35a27ff24785fa17640b023ebc5d374efd95a076;hpb=1416af941615fa434b71c0adda461d5bcac65f89;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 35a27ff24..ba14fd0d6 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -43,20 +43,20 @@ let rec count_tactic current_size tac = | 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 *) *) + | Compare (_, term) -> countterm (current_size + 7) term + | Constructor (_, n) -> current_size + 12 | 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) + | 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 @@ -65,12 +65,10 @@ let rec count_tactic current_size tac = | 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 - | Generalize (_,term,pattern) -> assert false (* TODO *) | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) - | Injection (_, ident) -> current_size + 10 + (String.length ident) + | Injection (_, term) -> + countterm (current_size + 10) term | Intros (_, num, idents) -> List.fold_left (fun size s -> size + (String.length s)) @@ -78,14 +76,7 @@ let rec count_tactic current_size tac = | Left _ -> current_size + 4 | LetIn (_, term, ident) -> countterm (current_size + 5 + String.length ident) term -(* | Reduce _ *) - | 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 @@ -136,37 +127,17 @@ and big_tactic2box = function ast2astBox term]) | Assumption _ -> Box.Text([],"assumption") | Auto _ -> Box.Text([],"auto") - | 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"); + | Compare (_, term) -> + Box.V([],[Box.Text([],"compare"); Box.indent(ast2astBox term)]) - | Decompose (_, ident, principles) -> - let principles = - List.map (fun x -> Box.Text([],x)) principles in + | 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)]) + Box.indent(ast2astBox term)]) + | Discriminate (_, term) -> + Box.V([],pretty_append [Box.Text([],"discriminate")] term) | Elim (_, term, using) -> let using = (match using with @@ -186,17 +157,8 @@ and big_tactic2box = function Box.V([],[Box.Text([],"exact"); 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(ast2astBox term)]) | Fourier _ -> Box.Text([],"fourier") - | Generalize _ -> assert false (* TODO *) | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) - | Injection (_, ident) -> - Box.V([],[Box.Text([],"transitivity"); - Box.indent (Box.Text([],ident))]) | Intros (_, num, idents) -> let num = (match num with @@ -215,19 +177,7 @@ and big_tactic2box = function Box.smallskip; Box.Text([],"=")]); Box.indent (ast2astBox term)]) -(* | Reduce _ *) - | 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") @@ -241,16 +191,9 @@ open TacticAst 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) -> Box.V([],[Box.Text([],"repeat"); Box.indent (tactical2box tac)])