X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=f0626c7724d3056b0e224a3cda39ecdb5c3195b9;hb=23641e7c4b061a2dbc5862d763e8c3602793a94c;hp=80e3effce2e31c0580b3330a3ee09f36c6eeec43;hpb=9680f6df42892b7b586fb2932617fa99703036bf;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 80e3effce..f0626c772 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -39,57 +39,54 @@ 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 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) -> - 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) -> + | 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 - | Hint -> current_size + 4 - | 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))) + | 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) -> + | 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 -> + | Right _ -> current_size + 5 + | Ring _ -> current_size + 4 + | Split _ -> current_size + 5 + | Symmetry _ -> current_size + 8 + | Transitivity (_, term) -> countterm (current_size + 13) term ;; @@ -107,6 +104,7 @@ let string_of_kind = function | `Reduce -> "reduce" | `Simpl -> "simplify" | `Whd -> "whd" + | `Normalize -> "normalize" let dummy_tbl = Hashtbl.create 0 @@ -126,48 +124,26 @@ let rec tactic2box tac = small_tactic2box tac and big_tactic2box = function - LocatedTactic (loc, tac) -> - big_tactic2box tac - | Absurd term -> + | Absurd (_, term) -> Box.V([],[Box.Text([],"absurd"); ast2astBox term]) - | Apply term -> + | Apply (_, term) -> Box.V([],[Box.Text([],"apply"); 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"); + | Assumption _ -> Box.Text([],"assumption") + | Auto _ -> Box.Text([],"auto") + | 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)]) - | 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 -> [] @@ -179,24 +155,21 @@ and big_tactic2box = function (pretty_append [Box.Text([],"elim")] term)@using) - | ElimType term -> + | ElimType (_, term) -> Box.V([],[Box.Text([],"elim type"); Box.indent(ast2astBox term)]) - | Exact term -> + | Exact (_, term) -> Box.V([],[Box.Text([],"exact"); Box.indent(ast2astBox term)]) - | Exists -> Box.Text([],"exists") - | Fold (kind, 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") - | Hint -> Box.Text([],"hint") - | Injection ident -> - Box.V([],[Box.Text([],"transitivity"); - Box.indent (Box.Text([],ident))]) - | Intros (num, idents) -> + | Fourier _ -> Box.Text([],"fourier") + | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) + | Intros (_, num, idents) -> let num = (match num with None -> [] @@ -206,17 +179,16 @@ and big_tactic2box = 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 (ast2astBox term)]) - | Reduce (_, _) -> assert false (* TODO *) - | Reflexivity -> Box.Text([],"reflexivity") - | Replace (t1, t2) -> + | Reflexivity _ -> Box.Text([],"reflexivity") + | Replace (_, t1, t2) -> Box.V([], (pretty_append [Box.Text([],"replace")] @@ -224,13 +196,11 @@ and big_tactic2box = function (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 -> + | 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 (ast2astBox term)]) ;; @@ -238,35 +208,35 @@ and big_tactic2box = function open TacticAst let rec tactical2box = function - | LocatedTactical (loc, tac) -> tactical2box tac - - | Tactic tac -> tactic2box tac + | Tactic (_, tac) -> tactic2box tac +(* | Command cmd -> (* TODO dummy implementation *) Box.Text([], TacticAstPp.pp_tactical (Command cmd)) +*) - | Fail -> Box.Text([],"fail") - | Do (count, tac) -> + | 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) - | 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)])