X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=d2df977fa68dfd72c5c9484c7a1e8bd6fbb90f8a;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=5afb38ca8a1c00f485137e251963710f423bafb0;hpb=e0fc20211c796fd90db43b9caece8f9aa1c75390;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 5afb38ca8..d2df977fa 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -39,57 +39,56 @@ 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) -> + | 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 - | 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 (_, 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 ;; @@ -105,8 +104,9 @@ let rec small_tactic2box tac = let string_of_kind = function | `Reduce -> "reduce" - | `Simpl -> "simpl" + | `Simpl -> "simplify" | `Whd -> "whd" + | `Normalize -> "normalize" let dummy_tbl = Hashtbl.create 0 @@ -126,17 +126,15 @@ 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) -> + | Assumption _ -> Box.Text([],"assumption") + | Auto _ -> Box.Text([],"auto") + | Change (_, t1, t2, where) -> let where = (match where with None -> [] @@ -151,12 +149,12 @@ and big_tactic2box = function (pretty_append [Box.Text([],"with")] t2)@where) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> Box.Text([],"contradiction") - | Cut term -> + | Change_pattern _ -> assert false (* TODO *) + | Contradiction _ -> Box.Text([],"contradiction") + | Cut (_, term) -> Box.V([],[Box.Text([],"cut"); Box.indent(ast2astBox term)]) - | Decompose (ident, principles) -> + | Decompose (_, ident, principles) -> let principles = List.map (fun x -> Box.Text([],x)) principles in Box.V([],[Box.Text([],"decompose"); @@ -164,10 +162,10 @@ and big_tactic2box = 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 -> [] @@ -179,24 +177,24 @@ 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 -> + | Fourier _ -> Box.Text([],"fourier") + | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) + | Injection (_, ident) -> Box.V([],[Box.Text([],"transitivity"); Box.indent (Box.Text([],ident))]) - | Intros (num, idents) -> + | Intros (_, num, idents) -> let num = (match num with None -> [] @@ -206,17 +204,17 @@ 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) -> + | Reduce _ -> assert false (* TODO *) + | Reflexivity _ -> Box.Text([],"reflexivity") + | Replace (_, t1, t2) -> Box.V([], (pretty_append [Box.Text([],"replace")] @@ -224,13 +222,13 @@ 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 -> + | 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 (ast2astBox term)]) ;; @@ -238,35 +236,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)])