Skip to content

Commit

Permalink
removed checking function application rule
Browse files Browse the repository at this point in the history
  • Loading branch information
@eneoli
eneoli committed Oct 4, 2024
1 parent 9aee6f9 commit 0a8899f
Show file tree
Hide file tree
Showing 3 changed files with 84 additions and 84 deletions.
64 changes: 32 additions & 32 deletions src/kernel/checker/check.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -409,38 +409,38 @@ impl<'a> ProofTermVisitor<Result<TypeCheckerResult, CheckError>> for CheckVisito
span,
} = application;

let (expected_return_prop, conclusion) = match self.expected_type {
Type::Prop(ref prop) => (prop, ProofTreeConclusion::PropIsTrue(prop.clone())),
Type::Datatype(_) => return Err(CheckError::CannotReturnDatatype(span.clone())),
};

// synthesize applicant
let applicant_synthesize_result = synthesize(applicant, self.ctx, self.identifier_factory);

// use ⊃ E<= rule
if let Ok((Type::Prop(applicant_prop), applicant_result)) = applicant_synthesize_result {
// check function
let expected_function_type = Type::Prop(Prop::Impl(
applicant_prop.boxed(),
expected_return_prop.boxed(),
));

let function_result = check_allowing_free_params(
function,
&expected_function_type,
self.ctx,
self.identifier_factory,
)?;

return Ok(TypeCheckerResult {
goals: vec![function_result.goals, applicant_result.goals].concat(),
proof_tree: ProofTree {
premisses: vec![function_result.proof_tree, applicant_result.proof_tree],
rule: ProofTreeRule::ImplElim,
conclusion,
},
});
}
// let (expected_return_prop, conclusion) = match self.expected_type {
// Type::Prop(ref prop) => (prop, ProofTreeConclusion::PropIsTrue(prop.clone())),
// Type::Datatype(_) => return Err(CheckError::CannotReturnDatatype(span.clone())),
// };

// // synthesize applicant
// let applicant_synthesize_result = synthesize(applicant, self.ctx, self.identifier_factory);

// // use ⊃ E<= rule
// if let Ok((Type::Prop(applicant_prop), applicant_result)) = applicant_synthesize_result {
// // check function
// let expected_function_type = Type::Prop(Prop::Impl(
// applicant_prop.boxed(),
// expected_return_prop.boxed(),
// ));

// let function_result = check_allowing_free_params(
// function,
// &expected_function_type,
// self.ctx,
// self.identifier_factory,
// )?;

// return Ok(TypeCheckerResult {
// goals: vec![function_result.goals, applicant_result.goals].concat(),
// proof_tree: ProofTree {
// premisses: vec![function_result.proof_tree, applicant_result.proof_tree],
// rule: ProofTreeRule::ImplElim,
// conclusion,
// },
// });
// }

// use =>
// <= rule
Expand Down
42 changes: 21 additions & 21 deletions src/kernel/checker/tests/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -512,23 +512,23 @@ mod tests {
);
}

#[test]
fn test_composition_of_identities_annotated_right() {
check_proof_term(
"
atom A;
(fn u => fn w: A => (snd u) ((fst u) w)) ((fn x: A => x), (fn y: A => y))
",
"A -> A",
);
}
// #[test]
// fn test_composition_of_identities_annotated_right() {
// check_proof_term(
// "
// atom A;
// (fn u => fn w: A => (snd u) ((fst u) w)) ((fn x: A => x), (fn y: A => y))
// ",
// "A -> A",
// );
// }

#[test]
fn test_non_minimal_identity_proof() {
check_proof_term("
atom A;
fn u => (fn w => w) u
fn u => (fn w: A => w) u
", "A -> A");
}

Expand Down Expand Up @@ -752,14 +752,14 @@ mod tests {
);
}

#[test]
fn test_sorry_in_application_as_function() {
check_proof_term(
"
atom A;
sorry ()
",
"A",
);
}
// #[test]
// fn test_sorry_in_application_as_function() {
// check_proof_term(
// "
// atom A;
// sorry ()
// ",
// "A",
// );
// }
}
62 changes: 31 additions & 31 deletions src/kernel/proof_tree.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -242,57 +242,57 @@ impl ProofTreeExporter {
panic!("Not enough premisses given.");
};

let old_atoms = self.atoms.clone();
let old_datatypes = self.datatypes.clone();
// let old_atoms = self.atoms.clone();
// let old_datatypes = self.datatypes.clone();

let fst_reasoning_mode = Self::expected_premisse_mode(rule, reasoning_mode, 0);
let snd_reasoning_mode = Self::expected_premisse_mode(rule, reasoning_mode, 1);
// let fst_reasoning_mode = Self::expected_premisse_mode(rule, reasoning_mode, 0);
// let snd_reasoning_mode = Self::expected_premisse_mode(rule, reasoning_mode, 1);

let fst_proof_term_checking =
self.do_export_as_proof_term(fst, &fst_reasoning_mode);
let snd_proof_term_checking =
self.do_export_as_proof_term(snd, &snd_reasoning_mode);
// let fst_proof_term_checking =
// self.do_export_as_proof_term(fst, &fst_reasoning_mode);
// let snd_proof_term_checking =
// self.do_export_as_proof_term(snd, &snd_reasoning_mode);

let proof_term_checking = Application::create(
fst_proof_term_checking.boxed(),
snd_proof_term_checking.boxed(),
None,
);
// let proof_term_checking = Application::create(
// fst_proof_term_checking.boxed(),
// snd_proof_term_checking.boxed(),
// None,
// );

let annotation_count = fst_proof_term_checking.annotation_count()
+ snd_proof_term_checking.annotation_count();
// let annotation_count = fst_proof_term_checking.annotation_count()
// + snd_proof_term_checking.annotation_count();

if *reasoning_mode == ReasoningMode::Synthesize || annotation_count == 0 {
return proof_term_checking;
}
// if *reasoning_mode == ReasoningMode::Synthesize || annotation_count == 0 {
// return proof_term_checking;
// }

// use =>
// <= rule

let checking_atoms = self.atoms.clone();
let checking_datatypes = self.datatypes.clone();
// let checking_atoms = self.atoms.clone();
// let checking_datatypes = self.datatypes.clone();

self.atoms = old_atoms;
self.datatypes = old_datatypes;
// self.atoms = old_atoms;
// self.datatypes = old_datatypes;

let fst_proof_term_synth =
self.do_export_as_proof_term(fst, &ReasoningMode::Synthesize);
let snd_proof_term_synth = self.do_export_as_proof_term(snd, &ReasoningMode::Check);

let proof_term_synth = Application::create(
Application::create(
fst_proof_term_synth.boxed(),
snd_proof_term_synth.boxed(),
None,
);
)

if proof_term_checking.annotation_count() <= proof_term_synth.annotation_count() {
self.atoms = checking_atoms;
self.datatypes = checking_datatypes;
// if proof_term_checking.annotation_count() <= proof_term_synth.annotation_count() {
// self.atoms = checking_atoms;
// self.datatypes = checking_datatypes;

proof_term_checking
} else {
proof_term_synth
}
// proof_term_checking
// } else {
// proof_term_synth
// }
}
ProofTreeRule::OrIntroFst | ProofTreeRule::OrIntroSnd => {
let expected_reasoning_mode = Self::expected_conclusion_mode(rule);
Expand Down

0 comments on commit 0a8899f

Please sign in to comment.