Skip to content

Commit

Permalink
Modify rewrite simplify rule
Browse files Browse the repository at this point in the history
  • Loading branch information
@NotBad4U
NotBad4U committed Feb 23, 2024
1 parent 55ef6d6 commit 96640c0
Show file tree
Hide file tree
Showing 7 changed files with 582 additions and 87 deletions.
66 changes: 56 additions & 10 deletions carcara/src/lambdapi/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,13 @@ use self::printer::PrettyPrint;
pub mod output;
pub mod printer;
pub mod proof;
mod simp;
mod tautology;
pub mod term;

use output::*;
use proof::*;
use simp::*;
use tautology::*;
use term::*;

Expand Down Expand Up @@ -107,7 +109,6 @@ macro_rules! make_term {

pub(crate) use make_term;


macro_rules! inline_lambdapi {
($($tokens:tt)+) => {
{
Expand All @@ -123,6 +124,7 @@ macro_rules! inline_lambdapi {
pub(crate) use inline_lambdapi;

macro_rules! tactic {
($steps:ident, symmetry; $($body:tt)*) => { $steps.push(ProofStep::Symmetry) ; tactic![ $steps, $( $body )* ] };
($steps:ident, reflexivity; $($body:tt)*) => { $steps.push(ProofStep::Reflexivity) ; tactic![ $steps, $( $body )* ] };
($steps:ident, apply $i:tt; $($body:tt)+) => {
$steps.push(ProofStep::Apply(Term::from($i), vec![], SubProofs(None)));
Expand Down Expand Up @@ -167,6 +169,24 @@ macro_rules! tactic {
$steps.push(ProofStep::Assume(ids));
tactic![ $steps, $( $body )* ]
};
($steps:ident, try [ $($id:tt)+ ] ; $($body:tt)*) => {
let step = inline_lambdapi![ $( $id )+ ];

$steps.push(ProofStep::Try(Box::new(step)));
tactic![ $steps, $( $body )* ]
};
($steps:ident, rewrite [$($i:tt)+] $( ( $($args:tt) + ) ) * $($body:tt)+) => {
$steps.push(ProofStep::Rewrite(None, $($i)+, vec![ $( make_term![ $( $args )+ ] , )* ]));
tactic![ $steps, $( $body )+ ]
};
($steps:ident, rewrite .$pattern:tt $i:tt $( ( $($args:tt) + ) ) * $($body:tt)+) => {
$steps.push(ProofStep::Rewrite(Some($pattern.to_string()), Term::from($i), vec![ $( make_term![ $( $args )+ ] , )* ]));
tactic![ $steps, $( $body )+ ]
};
($steps:ident, rewrite $i:tt $( ( $($args:tt) + ) ) * $($body:tt)+) => {
$steps.push(ProofStep::Rewrite(None, Term::from($i), vec![ $( make_term![ $( $args )+ ] , )* ]));
tactic![ $steps, $( $body )+ ]
};
($steps:ident, $code:block ; $($body:tt)*) => { $steps.append(&mut $code) ; tactic![ $steps, $( $body )* ] };
($steps:ident, inject($code:expr) ; $($body:tt)*) => { $steps.append(&mut $code) ; tactic![ $steps, $( $body )* ] };
($steps:ident, admit; $($body:tt)*) => { $steps.push(ProofStep::Admit) ; tactic![ $steps, $( $body )* ] };
Expand All @@ -175,7 +195,6 @@ macro_rules! tactic {

pub(crate) use tactic;


macro_rules! lambdapi_wrapper {
(begin $($body:tt)+) => { { let mut steps: Vec<ProofStep> = vec![]; tactic![ steps, $( $body )+ ] ; steps } };
}
Expand Down Expand Up @@ -225,11 +244,14 @@ fn translate_prelude(prelude: ProblemPrelude) -> Vec<Command> {
fn gen_required_module() -> Vec<Command> {
vec![
Command::RequireOpen("Stdlib.Prop".to_string()),
Command::RequireOpen("Stdlib.FOL".to_string()),
Command::RequireOpen("Stdlib.Set".to_string()),
Command::RequireOpen("Stdlib.Eq".to_string()),
Command::RequireOpen("Stdlib.List".to_string()),
Command::RequireOpen("Stdlib.Nat".to_string()),
//Command::RequireOpen("Stdlib.Z".to_string()), FIXME: Intersection between builtin Nat and Z
Command::RequireOpen("lambdapi.Classic".to_string()),
Command::RequireOpen("lambdapi.Alethe".to_string()),
Command::RequireOpen("lambdapi.Simplify".to_string()),
Command::RequireOpen("lambdapi.Rare".to_string()),
]
}

Expand Down Expand Up @@ -869,6 +891,7 @@ fn translate_tautology(
))
})
}

fn translate_commands<'a>(
ctx: &mut Context,
proof_iter: &mut ProofIter<'a>,
Expand Down Expand Up @@ -898,14 +921,37 @@ fn translate_commands<'a>(
)?;
proof_steps.push(proof);
}
ProofCommand::Step(AstProofStep { id, clause, premises: _, rule, .. })
if rule.contains("simp") =>
{
let step =
translate_simplification(&ctx, normalize_name(id).as_str(), clause, rule)?;
ProofCommand::Step(AstProofStep {
id, clause, premises: _, rule, args, ..
}) if rule == "rare_rewrite" => {
let terms: Vec<Term> = clause.into_iter().map(|a| Term::from(a)).collect();

let proof_script = translate_rare_simp(args);

let step = ProofStep::Have(
normalize_name(id),
proof(Term::Alethe(LTerm::Clauses(terms))),
proof_script.0,
);

proof_steps.push(step);
}
ProofCommand::Step(AstProofStep { id, clause, rule, .. }) if rule.contains("simp") => {
let terms: Vec<Term> = clause.into_iter().map(|a| Term::from(a)).collect();

let proof_script = translate_simplify_step(rule);

let step = ProofStep::Have(
normalize_name(id),
proof(Term::Alethe(LTerm::Clauses(terms))),
proof_script.0,
);

proof_steps.push(step);
}
ProofCommand::Step(AstProofStep { id, clause, premises, rule, args, .. }) => {
ProofCommand::Step(AstProofStep {
id, clause, premises, rule, args, ..
}) => {
let step = translate_tautology(
&ctx,
proof_iter,
Expand Down
65 changes: 53 additions & 12 deletions carcara/src/lambdapi/printer.rs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use super::*;
use itertools::concat;
use pretty::RcDoc;


pub const DEFAULT_WIDTH: usize = 120;
pub const DEFAULT_INDENT: isize = 4;

Expand All @@ -11,7 +11,6 @@ const RBRACE: &'static str = "}";
const COMMA: &'static str = ",";
const CLAUSE_NIL: &'static str = "▩";

const CONS: &'static str = "⸬";
const NIL: &'static str = "□";

macro_rules! concat {
Expand Down Expand Up @@ -136,6 +135,7 @@ impl PrettyPrint for BuiltinSort {
fn to_doc(&self) -> RcDoc<()> {
match self {
BuiltinSort::Bool => text("Prop"),
BuiltinSort::Int => text("ℤ"),
}
}
}
Expand All @@ -153,6 +153,7 @@ impl PrettyPrint for Term {
Term::Function(terms) => {
RcDoc::intersperse(terms.iter().map(|term| term.to_doc()), arrow().spaces())
}
Term::Nat(n) => RcDoc::text(format!("{}", n)),
}
}
}
Expand All @@ -174,9 +175,29 @@ impl PrettyPrint for SortedTerm {

impl PrettyPrint for ListLP {
fn to_doc(&self) -> RcDoc<()> {
RcDoc::intersperse(self.0.iter().map(|term| term.to_doc()), text(CONS).spaces())
.append(space().append(text(CONS)).append(space()).append(NIL))
// Take the last element because we will reverse the list latter so: last l = first (rev l)
let (first, elems) = self.0.split_last().expect("distinct should not be empty");

// Generate the root of the vector: (cons _ term1 □)
let first_doc = concat! {
text("cons") // constructor
=> text("_").spaces() // index is inferred by lambdapi
=> first.to_doc().spaces() // element
=> text(NIL)
}
.parens();

// Generate a vector (cons _ term_n ... (cons _ term2 (cons _ term1 □))

elems.into_iter().fold(first_doc, |acc, elem| {
concat! {
text("cons") // constructor
=> text("_").spaces() // index is inferred by lambdapi
=> elem.to_doc().spaces() // element
=> acc // rest of the vector
}
.parens()
})
}
}

Expand All @@ -195,11 +216,11 @@ impl PrettyPrint for LTerm {
classic("∨").spaces(),
)
.parens(),
LTerm::Neg(Some(term)) => classic("¬")
LTerm::Neg(Some(term)) => text("¬")
.append(space())
.append(term.to_doc().parens())
.parens(),
LTerm::Neg(None) => classic("¬"),
LTerm::Neg(None) => text("¬"),
LTerm::Proof(term) => text("π̇").append(space()).append(term.to_doc()),
LTerm::Clauses(terms) => {
if terms.is_empty() {
Expand All @@ -217,13 +238,18 @@ impl PrettyPrint for LTerm {
}
LTerm::Eq(l, r) => l
.to_doc()
.append(space().append(classic("⟺")).append(space()))
.append(text("=").spaces())
.append(r.to_doc())
.parens(),
LTerm::Iff(l, r) => l
.to_doc()
.append(classic("⇔").spaces())
.append(r.to_doc())
.parens(),
LTerm::Implies(l, r) => l
.to_doc()
.parens()
.append(space().append(classic("⟹")).append(space()))
.append(space().append(classic("⇒")).append(space()))
.append(r.to_doc().parens())
.parens(),
LTerm::Exist(bindings, term) => RcDoc::intersperse(
Expand Down Expand Up @@ -263,19 +289,21 @@ impl PrettyPrint for LTerm {
],
space(),
)),
LTerm::Distinct(v) => concat!(
LTerm::Distinct(v) => concat! {
text("distinct")
=> space()
=> text("o").spaces() // FIXME: store the type of vector element
=> RcDoc::text(v.0.len().to_string()).spaces() // size of the vector
=> v.to_doc()
),
}
.parens(),
LTerm::Choice(x, p) => concat!(
text("`ϵ")
=> space()
=> text(x)
=> COMMA
=> space()
=> p.to_doc()
)
),
}
}
}
Expand Down Expand Up @@ -350,6 +378,19 @@ impl PrettyPrint for ProofStep {
)
}))
.append(semicolon()),
ProofStep::Try(t) => text("try").append(space()).append(t.to_doc()),
ProofStep::Rewrite(pattern, h, args) => text("rewrite")
.append(pattern.as_ref().map_or(text(""), |pattern| {
text(".").append(text(pattern.as_str())).spaces()
}))
.append(
h.to_doc()
.append(args.is_empty().then(|| RcDoc::nil()).unwrap_or(space()))
.append(RcDoc::intersperse(args.iter().map(|a| a.to_doc()), space()))
.spaces(),
)
.append(semicolon()),
ProofStep::Symmetry => text("symmetry").append(semicolon()),
}
}
}
Expand Down
16 changes: 14 additions & 2 deletions carcara/src/lambdapi/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ use super::*;

const WHITE_SPACE: &'static str = " ";


#[derive(Debug, Clone)]
pub struct Proof(pub Vec<ProofStep>);

Expand All @@ -25,6 +24,9 @@ pub enum ProofStep {
Have(String, Term, Vec<ProofStep>), //TODO: change Vec<ProofStep> for Proof
Admit,
Reflexivity,
Try(Box<ProofStep>),
Rewrite(Option<String>, Term, Vec<Term>),
Symmetry,
}

#[derive(Debug, Clone)]
Expand Down Expand Up @@ -93,7 +95,17 @@ impl fmt::Display for ProofStep {
}
ProofStep::Admit => write!(f, "admit;"),
ProofStep::Reflexivity => write!(f, "simplify; reflexivity;"),
ProofStep::Try(t) => write!(f, "try {}", t),
ProofStep::Rewrite(pattern, hyp, args) => {
let pattern = pattern.as_ref().map_or("", |p| p.as_str());
let args = args
.iter()
.map(|i| format!("{}", i))
.collect::<Vec<_>>()
.join(WHITE_SPACE);
write!(f, "rewrite {} ({} {});", pattern, hyp, args)
}
ProofStep::Symmetry => write!(f, "symmetry;"),
}
}
}

Loading

0 comments on commit 96640c0

Please sign in to comment.