Skip to content

Commit

Permalink
added binders: forall; fixed rules: subproof, forall_inst
Browse files Browse the repository at this point in the history
  • Loading branch information
@Mallku2
Mallku2 committed Nov 13, 2024
1 parent 121793a commit 883ed2e
Show file tree
Hide file tree
Showing 4 changed files with 198 additions and 66 deletions.
17 changes: 17 additions & 0 deletions carcara/src/translation/alethe_signature/theory.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,16 +23,25 @@ pub struct AletheTheory {
pub ge: Symbol,

// Rules' names.
// TODO: order this
pub let_rule: Symbol,
pub equiv_pos2: Symbol,
pub bind: Symbol,
pub refl: Symbol,
pub subproof: Symbol,
pub forall_inst: Symbol,

// Context representation and manipulation.
// To bind variables in a context.
pub var: Symbol,

// Binders.
pub let_binder: Symbol,
pub forall_binder: Symbol,
pub exists_binder: Symbol,

// VarList constructors
pub varlist_nil: Symbol,
}

impl AletheTheory {
Expand All @@ -56,12 +65,20 @@ impl AletheTheory {
let_rule: String::from("let_elim"),
refl: String::from("refl"),
equiv_pos2: String::from("equiv_pos2"),
subproof: String::from("subproof"),
forall_inst: String::from("forall_inst"),
bind: String::from("bind"),

// Context representation and manipulation.
var: String::from("@var"),

// Binders.
let_binder: String::from("@let"),
forall_binder: String::from("forall"),
exists_binder: String::from("exists"),

// VarList constructors
varlist_nil: String::from("@varlist.nil"),
}
}

Expand Down
128 changes: 107 additions & 21 deletions carcara/src/translation/eunoia.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,10 +153,11 @@ impl EunoiaTranslator {
rule,
premises,
args,
discharge,
..
}) => {
self.eunoia_proof
.push(self.translate_step(id, clause, rule, premises, args));
.push(self.translate_step(id, clause, rule, premises, args, discharge));
// Keep a reference to the
self.local_steps[self.contexts_opened - 1].push(self.eunoia_proof.len() - 1);
}
Expand All @@ -173,31 +174,43 @@ impl EunoiaTranslator {
AnchorArg::Variable((name, sort)) => {
// TODO: either use borrows or implement
// Copy trait for EunoiaTerms
// Add variables to the current scope.
self.variables_in_scope
.insert(name.clone(), self.translate_term(sort));

ctx_typed_params.push(EunoiaTerm::List(vec![
EunoiaTerm::Id(name.clone()),
self.translate_term(sort),
]));
if !self.variables_in_scope.contains_key(name) {
// Add variables to the current scope.
self.variables_in_scope
.insert(name.clone(), self.translate_term(sort));

ctx_typed_params.push(EunoiaTerm::List(vec![
EunoiaTerm::Id(name.clone()),
self.translate_term(sort),
]));
}
}
AnchorArg::Assign((name, sort), term) => {
// TODO: either use borrows or implement
// Copy trait for EunoiaTerms
// Add variables to the current scope.
self.variables_in_scope
.insert(name.clone(), self.translate_term(sort));
if !self.variables_in_scope.contains_key(name) {
self.variables_in_scope
.insert(name.clone(), self.translate_term(sort));

ctx_typed_params.push(EunoiaTerm::List(vec![
EunoiaTerm::Id(name.clone()),
self.translate_term(sort),
]));
}

// TODO: ugly patch...
let rhs: EunoiaTerm = match term.deref() {
Term::Var(string, _) => EunoiaTerm::Id(string.clone()),

_ => self.translate_term(term),
};

and_params.push(EunoiaTerm::App(
self.alethe_signature.eq.clone(),
vec![EunoiaTerm::Id(name.clone()), self.translate_term(term)],
vec![EunoiaTerm::Id(name.clone()), rhs],
));

ctx_typed_params.push(EunoiaTerm::List(vec![
EunoiaTerm::Id(name.clone()),
self.translate_term(sort),
]));
}
});
// TODO: do not hard-code this string
Expand All @@ -207,7 +220,13 @@ impl EunoiaTranslator {
));

// Add typed params.
ctx_params.push(EunoiaTerm::List(ctx_typed_params));
if ctx_typed_params.is_empty() {
// Empty VarList
ctx_params.push(EunoiaTerm::Id(self.alethe_signature.varlist_nil.clone()));
} else {
// TODO: shouldn' we build it with @varlist?
ctx_params.push(EunoiaTerm::List(ctx_typed_params));
}

// Concat (and...)
ctx_params.push(EunoiaTerm::App(
Expand Down Expand Up @@ -309,7 +328,37 @@ impl EunoiaTranslator {
],
),

_ => EunoiaTerm::True,
Term::Binder(binder, binding_list, scope) => {
match binder {
Binder::Forall => EunoiaTerm::App(
self.alethe_signature.forall_binder.clone(),
vec![
self.translate_binding_list(binding_list),
self.translate_term(scope),
],
),

Binder::Exists => EunoiaTerm::App(
self.alethe_signature.exists_binder.clone(),
vec![
self.translate_binding_list(binding_list),
self.translate_term(scope),
],
),

// TODO: complete
_ => EunoiaTerm::App(
self.alethe_signature.exists_binder.clone(),
vec![
self.translate_binding_list(binding_list),
self.translate_term(scope),
],
),
}
}

// TODO: complete
Term::ParamOp { .. } => EunoiaTerm::True,
}
}

Expand Down Expand Up @@ -476,6 +525,7 @@ impl EunoiaTranslator {
rule: &str,
premises: &[Rc<ProofNode>],
args: &[ProofArg],
discharge: &[Rc<ProofNode>],
) -> EunoiaCommand {
let command: EunoiaCommand;
let mut alethe_premises: Vec<EunoiaTerm> = Vec::new();
Expand Down Expand Up @@ -570,16 +620,52 @@ impl EunoiaTranslator {
};
}

"equiv_pos2" => {
command = EunoiaCommand::Step {
"bind" => {
// :assumption: ctx
command = EunoiaCommand::StepPop {
name: id.to_owned(),
conclusion_clause: Some(conclusion),
rule: self.alethe_signature.equiv_pos2.clone(),
rule: self.alethe_signature.bind.clone(),
premises: EunoiaList { list: alethe_premises },
arguments: EunoiaList { list: eunoia_arguments },
};
}

"subproof" => {
// TODO: check this
// The command gets the formula proven through
// an "assumption", hence, we use StepPop.
// The discharged assumptions (received through the
// "discharge" formal parameter), will passed to
// our mechanization in Eunoia as :premises
let mut discharged_assumptions: Vec<EunoiaTerm> = Vec::new();

discharge.iter().for_each(|assumption| {
discharged_assumptions
.push(EunoiaTerm::Id(String::from(assumption.deref().id())));
});

// TODO: we are discarding vector premises
command = EunoiaCommand::StepPop {
name: id.to_owned(),
conclusion_clause: Some(conclusion),
rule: self.alethe_signature.subproof.clone(),
premises: EunoiaList { list: discharged_assumptions },
arguments: EunoiaList { list: eunoia_arguments },
};
}

"forall_inst" => {
// TODO: we are discarding vector and premises arguments
command = EunoiaCommand::Step {
name: id.to_owned(),
conclusion_clause: Some(conclusion),
rule: self.alethe_signature.forall_inst.clone(),
premises: EunoiaList { list: Vec::new() },
arguments: EunoiaList { list: Vec::new() },
};
}

_ => {
command = EunoiaCommand::Step {
name: id.to_owned(),
Expand Down
Loading

0 comments on commit 883ed2e

Please sign in to comment.