From da7f6fd7cc9658cfb2423db0d619811b43552976 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 20 Apr 2007 11:30:44 +0000 Subject: [PATCH] Interface of the argument to Continuationals.Make greately simplified. The following functions have been removed: - id_tactic - get_status - get_proof - set_goals --- components/grafite_engine/grafiteEngine.ml | 12 ------------ components/tactics/continuationals.ml | 5 ----- components/tactics/continuationals.mli | 5 ----- components/tactics/tacticals.ml | 7 ------- 4 files changed, 29 deletions(-) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index c93aeb654..f85c13bbb 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -492,23 +492,11 @@ let eval_tactical ~disambiguate_tactic status tac = type tactic = input_status -> output_status - let id_tactic = apply_tactic ("",0,(GrafiteAst.IdTac HExtlib.dummy_floc)) let mk_tactic tac = tac let apply_tactic tac = tac let goals (_, opened, closed) = opened, closed - let set_goals (opened, closed) (status, _, _) = (status, opened, closed) let get_stack (status, _) = GrafiteTypes.get_stack status - let get_status (status, goal) = - match status.GrafiteTypes.proof_status with - | GrafiteTypes.Incomplete_proof incomplete -> incomplete.GrafiteTypes.proof, goal - | _ -> assert false - - let get_proof (status, _, _) = - match status.GrafiteTypes.proof_status with - | GrafiteTypes.Incomplete_proof incomplete -> incomplete.GrafiteTypes.proof - | _ -> assert false - let set_stack stack (status, opened, closed) = GrafiteTypes.set_stack stack status, opened, closed diff --git a/components/tactics/continuationals.ml b/components/tactics/continuationals.ml index 6bb419c03..d90e10019 100644 --- a/components/tactics/continuationals.ml +++ b/components/tactics/continuationals.ml @@ -175,15 +175,10 @@ sig type output_status type tactic - - val id_tactic : tactic val mk_tactic : (input_status -> output_status) -> tactic val apply_tactic : tactic -> input_status -> output_status - val get_status: input_status -> ProofEngineTypes.status - val get_proof: output_status -> ProofEngineTypes.proof val goals : output_status -> goal list * goal list (** opened, closed goals *) - val set_goals: goal list * goal list -> output_status -> output_status val get_stack : input_status -> Stack.t val set_stack : Stack.t -> output_status -> output_status diff --git a/components/tactics/continuationals.mli b/components/tactics/continuationals.mli index f9a17a942..277dfe362 100644 --- a/components/tactics/continuationals.mli +++ b/components/tactics/continuationals.mli @@ -79,15 +79,10 @@ sig type output_status type tactic - - val id_tactic : tactic val mk_tactic : (input_status -> output_status) -> tactic val apply_tactic : tactic -> input_status -> output_status - val get_status: input_status -> ProofEngineTypes.status - val get_proof: output_status -> ProofEngineTypes.proof val goals : output_status -> goal list * goal list (** opened, closed goals *) - val set_goals: goal list * goal list -> output_status -> output_status val get_stack : input_status -> Stack.t val set_stack : Stack.t -> output_status -> output_status diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml index eb3ebc1bb..63b8e12b5 100644 --- a/components/tactics/tacticals.ml +++ b/components/tactics/tacticals.ml @@ -108,8 +108,6 @@ struct type tactic = PET.tactic - let id_tactic = id_tac - (* f is an eval function of a machine; the machine is applied to a fresh stack and the final stack is read back to obtain the result of the tactic *) @@ -130,12 +128,7 @@ struct let opened_goals, closed_goals = goals_diff ~before ~after ~opened in (proof', opened_goals, closed_goals), stack - let get_status (status, _) = status - let get_proof ((proof, _, _), _) = proof - let goals ((_, opened, closed), _) = opened, closed - let set_goals (opened, closed) ((proof, _, _), stack) = - (proof, opened, closed), stack (* Done only at the beginning of the eval of the machine *) let get_stack = snd -- 2.39.2