Skip to content

Commit e9117b1

Browse files
HKalbasiHKalbasi
committed
use &str instead of String in tactic args
1 parent 81e6062 commit e9117b1

File tree

13 files changed

+66
-47
lines changed

13 files changed

+66
-47
lines changed

‎docs/tactic.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ pub fn ring(frame: Frame) -> Result<Vec<Frame>> {
5252
تاکتیک بازنویسی:
5353

5454
```rust
55-
pub fn rewrite(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
55+
pub fn rewrite<'a>(mut frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
5656
// ^^^
5757
// ......
5858
frame.goal = if is_reverse {

‎hakim-engine/src/analysis/arith.rs

+4-1
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,10 @@ fn term_ref_to_arith(t: TermRef, arena: ArithArena<'_>) -> &ArithTree<'_> {
134134
),
135135
"minus" => Plus(
136136
term_ref_to_arith(op1.clone(), arena),
137-
term_ref_to_arith(op2.clone(), arena),
137+
arena.alloc(Mult(
138+
arena.alloc(Const((-1).into())),
139+
term_ref_to_arith(op2.clone(), arena),
140+
)),
138141
),
139142
"mult" => Mult(
140143
term_ref_to_arith(op1.clone(), arena),

‎hakim-engine/src/interactive.rs

+17-10
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ pub struct Session {
5050
}
5151

5252
fn smart_split(text: &str) -> Vec<String> {
53+
let c = text.split(" ");
5354
let mut r = vec![];
5455
let mut s = "".to_string();
5556
let mut d = 0;
@@ -256,25 +257,31 @@ impl Frame {
256257
Ok(())
257258
}
258259

259-
pub fn deny_dependency(&self, name: String) -> tactic::Result<()> {
260+
pub fn deny_dependency(&self, name: &str) -> tactic::Result<()> {
260261
for (_, hyp) in &self.hyps {
261262
if predict_axiom(hyp, &|x| x == name) {
262-
return Err(tactic::Error::ContextDependOnHyp(name, hyp.clone()));
263+
return Err(tactic::Error::ContextDependOnHyp(
264+
name.to_string(),
265+
hyp.clone(),
266+
));
263267
}
264268
}
265269
if predict_axiom(&self.goal, &|x| x == name) {
266-
return Err(tactic::Error::ContextDependOnHyp(name, self.goal.clone()));
270+
return Err(tactic::Error::ContextDependOnHyp(
271+
name.to_string(),
272+
self.goal.clone(),
273+
));
267274
}
268275
Ok(())
269276
}
270277

271-
pub fn remove_hyp_with_name(&mut self, name: String) -> tactic::Result<TermRef> {
272-
self.deny_dependency(name.clone())?;
273-
if let Some(hyp) = self.hyps.remove(&name) {
274-
self.engine.remove_name_unchecked(&name);
278+
pub fn remove_hyp_with_name(&mut self, name: &str) -> tactic::Result<TermRef> {
279+
self.deny_dependency(name)?;
280+
if let Some(hyp) = self.hyps.remove(name) {
281+
self.engine.remove_name_unchecked(name);
275282
return Ok(hyp);
276283
}
277-
Err(tactic::Error::UnknownHyp(name))
284+
Err(tactic::Error::UnknownHyp(name.to_string()))
278285
}
279286

280287
pub fn suggest_on_goal_dblclk(&self) -> Option<Suggestion> {
@@ -295,10 +302,10 @@ impl Frame {
295302

296303
pub fn run_tactic(&self, line: &str) -> Result<Vec<Self>, tactic::Error> {
297304
let parts = smart_split(line);
298-
let mut parts = parts.into_iter();
305+
let mut parts = parts.iter().map(|x| x.as_str());
299306
let name = parts.next().ok_or(tactic::Error::EmptyTactic)?;
300307
let frame = self.clone();
301-
match name.as_str() {
308+
match name {
302309
"intros" => intros(frame, parts),
303310
"rewrite" => rewrite(frame, parts),
304311
"replace" => replace(frame, parts),

‎hakim-engine/src/interactive/natural.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ impl From<Session> for NaturalProof {
9191
if cur.hyps.contains_key(hn) {
9292
continue;
9393
}
94-
if next.deny_dependency(hn.clone()).is_ok() {
94+
if next.deny_dependency(&hn).is_ok() {
9595
continue;
9696
}
9797
let ty = next.engine.pretty_print(next.hyps.get(hn).unwrap());
@@ -102,7 +102,7 @@ impl From<Session> for NaturalProof {
102102
if cur.hyps.contains_key(hn) {
103103
continue;
104104
}
105-
if next.deny_dependency(hn.clone()).is_err() {
105+
if next.deny_dependency(&hn).is_err() {
106106
continue;
107107
}
108108
let ty = next.engine.pretty_print(next.hyps.get(hn).unwrap());

‎hakim-engine/src/interactive/tactic.rs

+11-11
Original file line numberDiff line numberDiff line change
@@ -69,33 +69,33 @@ use Error::*;
6969

7070
use self::apply::FindInstance;
7171

72-
pub(crate) fn next_arg(
73-
args: &mut impl Iterator<Item = String>,
72+
pub(crate) fn next_arg<'a>(
73+
args: &mut impl Iterator<Item = &'a str>,
7474
tactic_name: &'static str,
75-
) -> Result<String> {
75+
) -> Result<&'a str> {
7676
let arg = args.next().ok_or(BadArgCount {
7777
tactic_name: tactic_name.to_string(),
7878
})?;
7979
Ok(arg)
8080
}
8181

82-
pub(crate) fn next_arg_constant(
83-
args: &mut impl Iterator<Item = String>,
82+
pub(crate) fn next_arg_constant<'a>(
83+
args: &mut impl Iterator<Item = &'a str>,
8484
tactic_name: &'static str,
8585
expected: &'static str,
8686
) -> Result<()> {
8787
let v = next_arg(args, tactic_name)?;
8888
if v != expected {
8989
return Err(BadArg {
90-
arg: v,
90+
arg: v.to_string(),
9191
tactic_name: tactic_name.to_string(),
9292
});
9393
}
9494
Ok(())
9595
}
9696

97-
pub(crate) fn deny_arg(
98-
mut args: impl Iterator<Item = String>,
97+
pub(crate) fn deny_arg<'a>(
98+
mut args: impl Iterator<Item = &'a str>,
9999
tactic_name: &'static str,
100100
) -> Result<()> {
101101
if args.next().is_some() {
@@ -106,10 +106,10 @@ pub(crate) fn deny_arg(
106106
Ok(())
107107
}
108108

109-
pub(crate) fn get_one_arg(
110-
mut args: impl Iterator<Item = String>,
109+
pub(crate) fn get_one_arg<'a>(
110+
mut args: impl Iterator<Item = &'a str>,
111111
tactic_name: &'static str,
112-
) -> Result<String> {
112+
) -> Result<&'a str> {
113113
let arg1 = next_arg(&mut args, tactic_name)?;
114114
deny_arg(args, tactic_name)?;
115115
Ok(arg1)

‎hakim-engine/src/interactive/tactic/apply.rs

+8-5
Original file line numberDiff line numberDiff line change
@@ -110,9 +110,9 @@ fn find_args_in_apply_hyp(
110110
None
111111
}
112112

113-
fn apply_for_hyp(mut frame: Frame, exp: &str, name: String) -> Result<Vec<Frame>> {
113+
fn apply_for_hyp(mut frame: Frame, exp: &str, name: &str) -> Result<Vec<Frame>> {
114114
let (term, ic) = frame.engine.parse_text_with_wild(exp)?;
115-
let prev_hyp = frame.remove_hyp_with_name(name.clone())?;
115+
let prev_hyp = frame.remove_hyp_with_name(name)?;
116116
let op = term_ref!(axiom name, prev_hyp);
117117
let ty = match find_args_in_apply_hyp(term, op, ic, &name) {
118118
Some(x) => x,
@@ -158,21 +158,24 @@ fn apply_for_goal(frame: Frame, exp: &str) -> Result<Vec<Frame>> {
158158
Ok(v)
159159
}
160160

161-
pub(crate) fn apply(frame: Frame, mut args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
161+
pub(crate) fn apply<'a>(
162+
frame: Frame,
163+
mut args: impl Iterator<Item = &'a str>,
164+
) -> Result<Vec<Frame>> {
162165
let exp = &next_arg(&mut args, "apply")?;
163166
if let Some(in_kw) = args.next() {
164167
if in_kw != "in" {
165168
return Err(BadArg {
166169
tactic_name: "apply".to_string(),
167-
arg: in_kw,
170+
arg: in_kw.to_string(),
168171
});
169172
}
170173
if let Some(hyp) = args.next() {
171174
apply_for_hyp(frame, exp, hyp)
172175
} else {
173176
Err(BadArg {
174177
tactic_name: "apply".to_string(),
175-
arg: in_kw,
178+
arg: in_kw.to_string(),
176179
})
177180
}
178181
} else {

‎hakim-engine/src/interactive/tactic/auto_set.rs

+2-5
Original file line numberDiff line numberDiff line change
@@ -383,17 +383,14 @@ fn negator(x: EnsembleStatement) -> EnsembleStatement {
383383

384384
fn pre_process_frame(frame: Frame) -> Frame {
385385
let mut intros_flag = false;
386-
let frame = match apply(frame.clone(), vec!["included_fold".to_string()].into_iter()) {
386+
let frame = match apply(frame.clone(), vec!["included_fold"].into_iter()) {
387387
Ok(x) if x.len() == 1 => {
388388
intros_flag = true;
389389
x.into_iter().next().unwrap()
390390
}
391391
_ => frame,
392392
};
393-
let frame = match apply(
394-
frame.clone(),
395-
vec!["set_equality_forall".to_string()].into_iter(),
396-
) {
393+
let frame = match apply(frame.clone(), vec!["set_equality_forall"].into_iter()) {
397394
Ok(x) if x.len() == 1 => {
398395
intros_flag = true;
399396
x.into_iter().next().unwrap()

‎hakim-engine/src/interactive/tactic/chain.rs

+7-4
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
use super::{next_arg, next_arg_constant, Result};
22
use crate::interactive::Frame;
33

4-
fn eat_paren(mut x: &str) -> String {
4+
fn eat_paren(mut x: &str) -> &str {
55
if let Some(a) = x.strip_prefix('(') {
66
if let Some(a) = a.strip_suffix(')') {
77
x = a;
88
}
99
}
10-
x.to_string()
10+
x
1111
}
1212

13-
pub(crate) fn chain(frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
13+
pub(crate) fn chain<'a>(frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
1414
let mut frames = vec![frame];
1515
for arg in args {
1616
let arg = eat_paren(&arg);
@@ -25,7 +25,10 @@ pub(crate) fn chain(frame: Frame, args: impl Iterator<Item = String>) -> Result<
2525
Ok(frames)
2626
}
2727

28-
pub(crate) fn destruct(frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
28+
pub(crate) fn destruct<'a>(
29+
frame: Frame,
30+
args: impl Iterator<Item = &'a str>,
31+
) -> Result<Vec<Frame>> {
2932
let args = &mut args.peekable();
3033
let tactic_name = "destruct";
3134
let hyp = next_arg(args, tactic_name)?;

‎hakim-engine/src/interactive/tactic/hyps.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use crate::{
44
interactive::Frame,
55
};
66

7-
pub fn add_hyp(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
7+
pub fn add_hyp<'a>(mut frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
88
let exp = get_one_arg(args, "add_hyp")?;
99
let term = frame.engine.parse_text(&exp)?;
1010
let ty = type_of(term.clone())?;
@@ -17,7 +17,7 @@ pub fn add_hyp(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<V
1717
Ok(vec![frame, frame2])
1818
}
1919

20-
pub fn remove_hyp(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
20+
pub fn remove_hyp<'a>(mut frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
2121
let exp = get_one_arg(args, "remove_hyp")?;
2222
frame.remove_hyp_with_name(exp)?;
2323
Ok(vec![frame])

‎hakim-engine/src/interactive/tactic/intros.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ pub fn intros_one(frame: &mut Frame, name: &str) -> Result<()> {
2222
}
2323
}
2424

25-
pub fn intros(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
25+
pub fn intros<'a>(mut frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
2626
let mut args = args.peekable();
2727
if args.peek().is_none() {
2828
while let Term::Forall(Abstraction {

‎hakim-engine/src/interactive/tactic/rewrite.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -74,9 +74,9 @@ pub fn get_eq_params(term: &Term) -> Option<[TermRef; 3]> {
7474
None
7575
}
7676

77-
pub fn rewrite(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
77+
pub fn rewrite<'a>(mut frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
7878
let mut args = args.peekable();
79-
let is_reverse = args.peek() == Some(&"<-".to_string());
79+
let is_reverse = args.peek() == Some(&"<-");
8080
if is_reverse {
8181
args.next();
8282
}
@@ -92,13 +92,13 @@ pub fn rewrite(mut frame: Frame, args: impl Iterator<Item = String>) -> Result<V
9292
Ok(vec![frame])
9393
}
9494

95-
pub fn replace(frame: Frame, args: impl Iterator<Item = String>) -> Result<Vec<Frame>> {
95+
pub fn replace<'a>(frame: Frame, args: impl Iterator<Item = &'a str>) -> Result<Vec<Frame>> {
9696
let mut args = args.peekable();
9797
let mut which = None;
9898
if let Some(x) = args.peek() {
9999
if &x[..1] == "#" {
100100
let n: isize = x[1..].parse().map_err(|_| BadArg {
101-
arg: args.next().unwrap(),
101+
arg: x.to_string(),
102102
tactic_name: "replace".to_string(),
103103
})?;
104104
which = Some(n);

‎hakim-engine/src/interactive/tactic/ring.rs

+1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ pub fn ring(frame: Frame) -> Result<Vec<Frame>> {
55
let goal = frame.goal;
66
let [op1, op2, _] = get_eq_params(&goal).ok_or(BadGoal("ring only work on equality"))?;
77
let d = Poly::from_subtract(op1, op2);
8+
dbg!(&d);
89
if d.is_zero() {
910
Ok(vec![])
1011
} else {

‎hakim-engine/src/parser/pretty_print.rs

+6-1
Original file line numberDiff line numberDiff line change
@@ -223,5 +223,10 @@ fn term_pretty_print_inner(
223223

224224
pub fn term_pretty_print(term: &Term, contain_name: impl Fn(&str) -> bool) -> String {
225225
let r = term_pretty_print_inner(term, &mut (vec![], contain_name), (200, 200));
226-
format!("\u{2068}{}\u{2069}", r)
226+
#[cfg(not(test))]
227+
{
228+
format!("\u{2068}{}\u{2069}", r)
229+
}
230+
#[cfg(test)]
231+
r
227232
}

0 commit comments

Comments
 (0)