From 515ce27a5ebaea3baf7ff621201efa588a83d521 Mon Sep 17 00:00:00 2001 From: eneoli Date: Tue, 6 Aug 2024 22:13:11 +0200 Subject: [PATCH 1/5] added instantiate_parameters_with_context method --- src/kernel/prop.rs | 74 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 74 insertions(+) diff --git a/src/kernel/prop.rs b/src/kernel/prop.rs index ae87a12..c9b23c4 100644 --- a/src/kernel/prop.rs +++ b/src/kernel/prop.rs @@ -1,6 +1,7 @@ use std::fmt::{self, Debug}; use std::vec; +use super::checker::identifier_context::IdentifierContext; use super::{checker::identifier::Identifier, proof_term::Type}; use serde::{Deserialize, Serialize}; use tsify_next::Tsify; @@ -66,6 +67,10 @@ impl PropParameter { } } +pub enum InstatiationError { + UnknownIdentifier(String), +} + #[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Tsify)] #[tsify(into_wasm_abi, from_wasm_abi)] #[serde(tag = "kind", content = "value")] @@ -437,6 +442,75 @@ impl Prop { } } + pub fn instantiate_parameters_with_context( + &mut self, + ctx: &IdentifierContext, + ) -> Result<(), InstatiationError> { + fn _instantiate_with_ctx<'a>( + prop: &'a mut Prop, + ctx: &IdentifierContext, + mut bound_idents: Vec<&'a str>, + ) -> Result<(), InstatiationError> { + match prop { + Prop::True => {} + Prop::False => {} + Prop::And(ref mut fst, ref mut snd) + | Prop::Or(ref mut fst, ref mut snd) + | Prop::Impl(ref mut fst, ref mut snd) => { + _instantiate_with_ctx(fst, ctx, bound_idents.clone())?; + _instantiate_with_ctx(snd, ctx, bound_idents)?; + } + Prop::ForAll { + ref object_ident, + body, + .. + } + | Prop::Exists { + ref object_ident, + body, + .. + } => { + bound_idents.push(object_ident); + + _instantiate_with_ctx(body, ctx, bound_idents)?; + } + Prop::Atom(_, params) => { + for param in params.iter_mut() { + // sanity check + if let PropParameter::Instantiated(identifier) = param { + if ctx.get(identifier).is_none() { + panic!("Instantiated parameter does not exist: {:#?}", identifier); + } + + if let Some(Type::Prop(prop)) = ctx.get(&identifier) { + panic!( + "Parameter is a proposition: {:#?}, {:#?}", + identifier, prop + ); + } + + continue; + } + + let PropParameter::Uninstantiated(name) = param else { + continue; + }; + + let Some((identifier, _)) = ctx.get_by_name(&name) else { + return Err(InstatiationError::UnknownIdentifier(name.clone())); + }; + + *param = PropParameter::Instantiated(identifier.clone()); + } + } + }; + + Ok(()) + } + + _instantiate_with_ctx(self, ctx, vec![]) + } + pub fn alpha_eq(&self, other: &Prop) -> bool { let env = vec![]; From 121eb483b36c7f5c5ddfbf97035070a86a527b35 Mon Sep 17 00:00:00 2001 From: eneoli Date: Tue, 6 Aug 2024 22:13:36 +0200 Subject: [PATCH 2/5] added instantiate_parameters_with_context --- src/kernel/proof_term.rs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/kernel/proof_term.rs b/src/kernel/proof_term.rs index 57f284c..2ccb3ac 100644 --- a/src/kernel/proof_term.rs +++ b/src/kernel/proof_term.rs @@ -1,7 +1,10 @@ use core::fmt; use std::fmt::Display; -use super::prop::Prop; +use super::{ + checker::identifier_context::IdentifierContext, + prop::{InstatiationError, Prop}, +}; use serde::{Deserialize, Serialize}; use tsify_next::Tsify; @@ -49,6 +52,17 @@ impl Type { _ => false, } } + + pub fn instantiate_parameters_with_context( + &mut self, + ctx: &IdentifierContext, + ) -> Result<(), InstatiationError> { + let Type::Prop(prop) = self else { + return Ok(()); + }; + + prop.instantiate_parameters_with_context(ctx) + } } impl From for Prop { From 094c715091654fb4b84f61ce0f2e3483e42d5846 Mon Sep 17 00:00:00 2001 From: eneoli Date: Tue, 6 Aug 2024 22:23:00 +0200 Subject: [PATCH 3/5] instantiate parameters of type annotations --- src/kernel/checker/check.rs | 35 +++++++++++--- src/kernel/checker/synthesize.rs | 79 ++++++++++++-------------------- 2 files changed, 57 insertions(+), 57 deletions(-) diff --git a/src/kernel/checker/check.rs b/src/kernel/checker/check.rs index b91deda..7e2ebe1 100644 --- a/src/kernel/checker/check.rs +++ b/src/kernel/checker/check.rs @@ -3,13 +3,12 @@ use thiserror::Error; use crate::{ kernel::{ - proof::Proof, proof_term::{ Abort, Application, Case, Function, Ident, LetIn, OrLeft, OrRight, Pair, ProjectFst, ProjectSnd, ProofTerm, ProofTermKind, ProofTermVisitor, Type, TypeAscription, }, proof_tree::{ProofTree, ProofTreeConclusion, ProofTreeRule}, - prop::{Prop, PropKind, PropParameter}, + prop::{InstatiationError, Prop, PropKind, PropParameter}, }, util::counter::Counter, }; @@ -314,12 +313,27 @@ impl<'a> ProofTermVisitor> for CheckVisitor<'a> { } }; - // fail if type annotation is not expected type if let Some(unboxed_param_type) = param_type { - if !Type::alpha_eq(unboxed_param_type, &expected_param_type) { + // instantiate uninstantiated params with current context + let mut instantiated_param_type = unboxed_param_type.clone(); + + instantiated_param_type + .instantiate_parameters_with_context(&self.ctx) + .map_err(|err| match err { + InstatiationError::UnknownIdentifier(ident) => { + CheckError::UnknownIdentifier(ident) + } + })?; + + // fail if type annotation is not expected type + if !Type::alpha_eq(&instantiated_param_type, &expected_param_type) { return Err(CheckError::IncompatibleProofTerm { expected_type: self.expected_type.clone(), - proof_term: ProofTerm::Function(function.clone()), + proof_term: Function::create( + function.param_ident.clone(), + Some(instantiated_param_type), + function.body.clone(), + ), }); } } @@ -628,10 +642,17 @@ impl<'a> ProofTermVisitor> for CheckVisitor<'a> { proof_term, } = type_ascription; - if !Type::alpha_eq(&self.expected_type, ascription) { + let mut instantiated_ascription = ascription.clone(); + instantiated_ascription + .instantiate_parameters_with_context(&self.ctx) + .map_err(|err| match err { + InstatiationError::UnknownIdentifier(ident) => CheckError::UnknownIdentifier(ident), + })?; + + if !Type::alpha_eq(&self.expected_type, &instantiated_ascription) { return Err(CheckError::UnexpectedTypeAscription { expected: self.expected_type.clone(), - ascription: ascription.clone(), + ascription: instantiated_ascription.clone(), }); } diff --git a/src/kernel/checker/synthesize.rs b/src/kernel/checker/synthesize.rs index c505112..2ed581a 100644 --- a/src/kernel/checker/synthesize.rs +++ b/src/kernel/checker/synthesize.rs @@ -7,7 +7,7 @@ use crate::kernel::{ ProjectSnd, ProofTerm, ProofTermKind, ProofTermVisitor, Type, TypeAscription, }, proof_tree::{ProofTree, ProofTreeConclusion, ProofTreeRule}, - prop::{Prop, PropKind, PropParameter}, + prop::{InstatiationError, Prop, PropKind, PropParameter}, }; use super::{ @@ -80,32 +80,6 @@ impl<'a> SynthesizeVisitor<'a> { identifier_factory, } } - - fn bind_free_params_to_ctx(&self, _type: &mut Type) -> Result<(), SynthesizeError> { - if let Type::Prop(ref mut prop) = _type { - let free_params = prop.get_free_parameters_mut(); - - for free_param in free_params { - match free_param { - PropParameter::Uninstantiated(name) => { - let (identifier, _) = self - .ctx - .get_by_name(name) - .ok_or(SynthesizeError::UnknownIdentifier(name.clone()))?; - *free_param = PropParameter::Instantiated(identifier.clone()) - } - PropParameter::Instantiated(identifier) => { - // sanity check - if self.ctx.get(identifier).is_none() { - panic!("Instantiated parameter does not exist: {:#?}", identifier); - } - } - } - } - } - - Ok(()) - } } impl<'a> ProofTermVisitor> for SynthesizeVisitor<'a> { @@ -144,9 +118,7 @@ impl<'a> ProofTermVisitor> for Synthe match (&fst_type, &snd_type) { // Exists - (Type::Datatype(_), Type::Prop(_)) => { - Err(SynthesizeError::TypeAnnotationsNeeded) - } + (Type::Datatype(_), Type::Prop(_)) => Err(SynthesizeError::TypeAnnotationsNeeded), // And (Type::Prop(fst_prop), Type::Prop(snd_prop)) => { @@ -175,8 +147,7 @@ impl<'a> ProofTermVisitor> for Synthe ) -> Result<(Type, ProofTree), SynthesizeError> { let ProjectFst(body) = projection; - let (body_type, body_proof_tree) = - synthesize(body, self.ctx, self.identifier_factory)?; + let (body_type, body_proof_tree) = synthesize(body, self.ctx, self.identifier_factory)?; let fst = match body_type { Type::Prop(Prop::And(fst, _)) => fst, @@ -204,8 +175,7 @@ impl<'a> ProofTermVisitor> for Synthe ) -> Result<(Type, ProofTree), SynthesizeError> { let ProjectSnd(body) = projection; - let (body_type, body_proof_tree) = - synthesize(body, self.ctx, self.identifier_factory)?; + let (body_type, body_proof_tree) = synthesize(body, self.ctx, self.identifier_factory)?; let snd = match body_type { Type::Prop(Prop::And(_, snd)) => snd, @@ -243,18 +213,23 @@ impl<'a> ProofTermVisitor> for Synthe None => return Err(SynthesizeError::TypeAnnotationsNeeded), }; - // check that if parameter is Prop, it only has known identifiers as free occurences - let mut binded_param_type = param_type.clone(); - self.bind_free_params_to_ctx(&mut binded_param_type)?; + // check that if parameter is Prop, it only has known identifiers as free occurrences + let mut bound_param_type = param_type.clone(); + bound_param_type + .instantiate_parameters_with_context(&self.ctx) + .map_err(|err| match err { + InstatiationError::UnknownIdentifier(ident) => { + SynthesizeError::UnknownIdentifier(ident) + } + })?; // add param to context let param_identifier = self.identifier_factory.create(param_ident.clone()); let mut body_ctx = self.ctx.clone(); - body_ctx.insert(param_identifier, binded_param_type); - let (body_type, body_proof_tree) = - synthesize(body, &body_ctx, self.identifier_factory)?; + body_ctx.insert(param_identifier, bound_param_type.clone()); + let (body_type, body_proof_tree) = synthesize(body, &body_ctx, self.identifier_factory)?; - match (¶m_type, &body_type) { + match (&bound_param_type, &body_type) { // Forall (Type::Datatype(ident), Type::Prop(body_type)) => { let _type = Prop::ForAll { @@ -454,15 +429,13 @@ impl<'a> ProofTermVisitor> for Synthe let fst_identifier = self.identifier_factory.create(fst_ident.clone()); let mut fst_ctx = self.ctx.clone(); fst_ctx.insert(fst_identifier, Type::Prop(*fst)); - let (fst_type, fst_proof_tree) = - synthesize(fst_term, &fst_ctx, self.identifier_factory)?; + let (fst_type, fst_proof_tree) = synthesize(fst_term, &fst_ctx, self.identifier_factory)?; // snythesize snd arm let snd_identifier = self.identifier_factory.create(snd_ident.clone()); let mut snd_ctx = self.ctx.clone(); snd_ctx.insert(snd_identifier, Type::Prop(*snd)); - let (snd_type, snd_proof_tree) = - synthesize(snd_term, &snd_ctx, self.identifier_factory)?; + let (snd_type, snd_proof_tree) = synthesize(snd_term, &snd_ctx, self.identifier_factory)?; // check for alpha-equivalence if !Type::alpha_eq(&fst_type, &snd_type) { @@ -510,19 +483,25 @@ impl<'a> ProofTermVisitor> for Synthe } = type_ascription; // check that if ascription is Prop, it only has known identifiers as free occurences - let mut binded_ascription = ascription.clone(); - self.bind_free_params_to_ctx(&mut binded_ascription)?; + let mut instantiated_ascription = ascription.clone(); + instantiated_ascription + .instantiate_parameters_with_context(&self.ctx) + .map_err(|err| match err { + InstatiationError::UnknownIdentifier(ident) => { + SynthesizeError::UnknownIdentifier(ident) + } + })?; check_allowing_free_params( proof_term, - &binded_ascription, + &instantiated_ascription, self.ctx, self.identifier_factory, ) - .map(|proof_tree| (ascription.clone(), proof_tree)) + .map(|proof_tree| (instantiated_ascription.clone(), proof_tree)) .map_err(|check_err| SynthesizeError::CheckError(Box::new(check_err))) } - + fn visit_sorry(&mut self) -> Result<(Type, ProofTree), SynthesizeError> { Err(SynthesizeError::NotSynthesizing(ProofTermKind::Sorry)) } From 4da54845bc9516d6908c4c9eea3bb71f195e896c Mon Sep 17 00:00:00 2001 From: eneoli Date: Wed, 7 Aug 2024 12:21:40 +0200 Subject: [PATCH 4/5] fixed typos --- ...l-proof-editor-parameter-binding-selector.tsx | 16 ++++++++-------- src/kernel/checker/tests/mod.rs | 4 ++-- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-binding-selector.tsx b/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-binding-selector.tsx index 11822de..bcc6422 100644 --- a/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-binding-selector.tsx +++ b/frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-binding-selector.tsx @@ -14,7 +14,7 @@ interface RenderPropResult { newIndex: number, } -type RenderProp = (prop: Prop, currentIndex: number, bindedIdentifiers: string[]) => RenderPropResult; +type RenderProp = (prop: Prop, currentIndex: number, boundIdentifiers: string[]) => RenderPropResult; export function VisualProofEditorParameterBindingSelector(props: VisualProofEditorParameterBindingSelectorProps) { @@ -35,7 +35,7 @@ export function VisualProofEditorParameterBindingSelector(props: VisualProofEdit } }, [selectedIndices]); - const renderProp: RenderProp = (prop: Prop, currentIndex: number, bindedIdentifiers: string[]) => { + const renderProp: RenderProp = (prop: Prop, currentIndex: number, boundIdentifiers: string[]) => { const handlePrimitive = useCallback((primitive: string) => { return { @@ -45,8 +45,8 @@ export function VisualProofEditorParameterBindingSelector(props: VisualProofEdit }, [currentIndex]); const handleBinaryConnective = useCallback((connective: string, prop: Prop & { kind: 'And' | 'Or' | 'Impl' }) => { - const fst = renderProp(prop.value[0], currentIndex, [...bindedIdentifiers]); - const snd = renderProp(prop.value[1], fst.newIndex, [...bindedIdentifiers]); + const fst = renderProp(prop.value[0], currentIndex, [...boundIdentifiers]); + const snd = renderProp(prop.value[1], fst.newIndex, [...boundIdentifiers]); const node = ( <> @@ -60,13 +60,13 @@ export function VisualProofEditorParameterBindingSelector(props: VisualProofEdit node, newIndex: snd.newIndex, }; - }, [currentIndex, bindedIdentifiers]); + }, [currentIndex, boundIdentifiers]); const handleQuantifier = useCallback((quantifier: string, prop: Prop & { kind: 'ForAll' | 'Exists' }) => { const body = renderProp( prop.value.body, currentIndex, - [...bindedIdentifiers, prop.value.object_ident], + [...boundIdentifiers, prop.value.object_ident], ); const node = ( @@ -84,7 +84,7 @@ export function VisualProofEditorParameterBindingSelector(props: VisualProofEdit node, newIndex: body.newIndex, }; - }, [currentIndex, bindedIdentifiers]); + }, [currentIndex, boundIdentifiers]); const handleAtom = useCallback((prop: Prop & { kind: 'Atom' }) => { const params = prop.value[1]; @@ -135,7 +135,7 @@ export function VisualProofEditorParameterBindingSelector(props: VisualProofEdit continue; } - if (bindedIdentifiers.includes(paramName)) { + if (boundIdentifiers.includes(paramName)) { paramNodes.push( {paramName} diff --git a/src/kernel/checker/tests/mod.rs b/src/kernel/checker/tests/mod.rs index f8614d1..4427f98 100644 --- a/src/kernel/checker/tests/mod.rs +++ b/src/kernel/checker/tests/mod.rs @@ -572,7 +572,7 @@ mod tests { } #[test] - fn test_allow_binded_params_function_annotations() { + fn test_allow_bound_params_function_annotations() { check_proof_term( " atom A(1); @@ -584,7 +584,7 @@ mod tests { } #[test] - fn test_do_allow_binded_params_type_ascription() { + fn test_do_allow_bound_params_type_ascription() { check_proof_term( " atom A(1); From f5f8c0a843d5a7d51724514020992b72c6c0008f Mon Sep 17 00:00:00 2001 From: eneoli Date: Wed, 7 Aug 2024 12:22:34 +0200 Subject: [PATCH 5/5] added tests for instantiate_parameters_with_context --- src/kernel/prop.rs | 198 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 151 insertions(+), 47 deletions(-) diff --git a/src/kernel/prop.rs b/src/kernel/prop.rs index c9b23c4..2596698 100644 --- a/src/kernel/prop.rs +++ b/src/kernel/prop.rs @@ -67,6 +67,7 @@ impl PropParameter { } } +#[derive(Debug, PartialEq, Eq)] pub enum InstatiationError { UnknownIdentifier(String), } @@ -118,84 +119,81 @@ impl Prop { } pub fn get_free_parameters(&self) -> Vec { - fn _get_free_parameters( - prop: &Prop, - binded_idents: &mut Vec, - ) -> Vec { + fn _get_free_parameters(prop: &Prop, bound_idents: &mut Vec) -> Vec { match prop { Prop::True => vec![], Prop::False => vec![], Prop::And(fst, snd) => { - let fst_idents = _get_free_parameters(fst, &mut binded_idents.clone()); - let snd_idents = _get_free_parameters(snd, binded_idents); + let fst_idents = _get_free_parameters(fst, &mut bound_idents.clone()); + let snd_idents = _get_free_parameters(snd, bound_idents); [fst_idents, snd_idents].concat() } Prop::Or(fst, snd) => { - let fst_idents = _get_free_parameters(fst, &mut binded_idents.clone()); - let snd_idents = _get_free_parameters(snd, binded_idents); + let fst_idents = _get_free_parameters(fst, &mut bound_idents.clone()); + let snd_idents = _get_free_parameters(snd, bound_idents); [fst_idents, snd_idents].concat() } Prop::Impl(fst, snd) => { - let fst_idents = _get_free_parameters(fst, &mut binded_idents.clone()); - let snd_idents = _get_free_parameters(snd, binded_idents); + let fst_idents = _get_free_parameters(fst, &mut bound_idents.clone()); + let snd_idents = _get_free_parameters(snd, bound_idents); [fst_idents, snd_idents].concat() } Prop::Exists { object_ident, body, .. } => { - binded_idents.push(object_ident.to_string()); + bound_idents.push(object_ident.to_string()); - _get_free_parameters(body, binded_idents) + _get_free_parameters(body, bound_idents) } Prop::ForAll { object_ident, body, .. } => { - binded_idents.push(object_ident.to_string()); + bound_idents.push(object_ident.to_string()); - _get_free_parameters(body, binded_idents) + _get_free_parameters(body, bound_idents) } Prop::Atom(_, params) => { let mut free_params = params.clone(); - free_params.retain(|param| !binded_idents.contains(param.name())); + free_params.retain(|param| !bound_idents.contains(param.name())); free_params } } } - let mut binded_idents = Vec::new(); + let mut bound_idents = Vec::new(); - _get_free_parameters(self, &mut binded_idents) + _get_free_parameters(self, &mut bound_idents) } pub fn get_free_parameters_mut(&mut self) -> Vec<&mut PropParameter> { fn _get_free_parameters<'a>( prop: &'a mut Prop, - binded_idents: &mut Vec, + bound_idents: &mut Vec, ) -> Vec<&'a mut PropParameter> { match prop { Prop::True => vec![], Prop::False => vec![], Prop::And(fst, snd) => { - let mut fst_idents = _get_free_parameters(fst, &mut binded_idents.clone()); - let mut snd_idents = _get_free_parameters(snd, binded_idents); + let mut fst_idents = _get_free_parameters(fst, &mut bound_idents.clone()); + let mut snd_idents = _get_free_parameters(snd, bound_idents); fst_idents.append(&mut snd_idents); fst_idents } Prop::Or(fst, snd) => { - let mut fst_idents = _get_free_parameters(fst, &mut binded_idents.clone()); - let mut snd_idents = _get_free_parameters(snd, binded_idents); + let mut fst_idents = _get_free_parameters(fst, &mut bound_idents.clone()); + let mut snd_idents = _get_free_parameters(snd, bound_idents); fst_idents.append(&mut snd_idents); fst_idents } Prop::Impl(fst, snd) => { - let mut fst_idents = _get_free_parameters(fst, &mut binded_idents.clone()); - let mut snd_idents = _get_free_parameters(snd, binded_idents); + let mut fst_idents = _get_free_parameters(fst, &mut bound_idents.clone()); + let mut snd_idents = _get_free_parameters(snd, bound_idents); fst_idents.append(&mut snd_idents); fst_idents @@ -203,29 +201,29 @@ impl Prop { Prop::Exists { object_ident, body, .. } => { - binded_idents.push(object_ident.to_string()); + bound_idents.push(object_ident.to_string()); - _get_free_parameters(body, binded_idents) + _get_free_parameters(body, bound_idents) } Prop::ForAll { object_ident, body, .. } => { - binded_idents.push(object_ident.to_string()); + bound_idents.push(object_ident.to_string()); - _get_free_parameters(body, binded_idents) + _get_free_parameters(body, bound_idents) } Prop::Atom(_, ref mut params) => { let mut free_params = params.iter_mut().collect::>(); - free_params.retain(|param| !binded_idents.contains(param.name())); + free_params.retain(|param| !bound_idents.contains(param.name())); free_params } } } - let mut binded_idents = Vec::new(); + let mut bound_idents = Vec::new(); - _get_free_parameters(self, &mut binded_idents) + _get_free_parameters(self, &mut bound_idents) } // This can only replace with single identifiers, but that should be ok at the current state of the type checker. @@ -288,7 +286,7 @@ impl Prop { identifier: &Identifier, identifier_indices: &Vec, bind_name: &str, - binded_identifiers: &mut Vec<&'a str>, + bound_identifiers: &mut Vec<&'a str>, current_index: &mut usize, ) -> Prop { match prop { @@ -300,7 +298,7 @@ impl Prop { identifier, identifier_indices, bind_name, - &mut binded_identifiers.clone(), + &mut bound_identifiers.clone(), current_index, ) .boxed(), @@ -309,7 +307,7 @@ impl Prop { identifier, identifier_indices, bind_name, - binded_identifiers, + bound_identifiers, current_index, ) .boxed(), @@ -320,7 +318,7 @@ impl Prop { identifier, identifier_indices, bind_name, - &mut binded_identifiers.clone(), + &mut bound_identifiers.clone(), current_index, ) .boxed(), @@ -329,7 +327,7 @@ impl Prop { identifier, identifier_indices, bind_name, - binded_identifiers, + bound_identifiers, current_index, ) .boxed(), @@ -340,7 +338,7 @@ impl Prop { identifier, identifier_indices, bind_name, - &mut binded_identifiers.clone(), + &mut bound_identifiers.clone(), current_index, ) .boxed(), @@ -349,7 +347,7 @@ impl Prop { identifier, identifier_indices, bind_name, - binded_identifiers, + bound_identifiers, current_index, ) .boxed(), @@ -359,7 +357,7 @@ impl Prop { object_type_ident, body, } => { - binded_identifiers.push(object_ident.as_str()); + bound_identifiers.push(object_ident.as_str()); Prop::Exists { object_ident: object_ident.clone(), object_type_ident: object_type_ident.clone(), @@ -368,7 +366,7 @@ impl Prop { identifier, identifier_indices, bind_name, - binded_identifiers, + bound_identifiers, current_index, ) .boxed(), @@ -379,7 +377,7 @@ impl Prop { object_type_ident, body, } => { - binded_identifiers.push(object_ident.as_str()); + bound_identifiers.push(object_ident.as_str()); Prop::ForAll { object_ident: object_ident.clone(), object_type_ident: object_type_ident.clone(), @@ -388,7 +386,7 @@ impl Prop { identifier, identifier_indices, bind_name, - binded_identifiers, + bound_identifiers, current_index, ) .boxed(), @@ -496,6 +494,10 @@ impl Prop { continue; }; + if bound_idents.contains(&name.as_str()) { + continue; + } + let Some((identifier, _)) = ctx.get_by_name(&name) else { return Err(InstatiationError::UnknownIdentifier(name.clone())); }; @@ -593,7 +595,7 @@ impl Prop { return false; } } else { - panic!("Found uninstantiated parameter that is not binded by a quantor. left: {:#?}, right: {:#?}", left, right); + panic!("Found uninstantiated parameter that is not bound by a quantor. left: {:#?}, right: {:#?}", left, right); } } else if l_param != r_param { return false; @@ -648,7 +650,7 @@ impl Debug for Prop { #[cfg(test)] mod tests { - use std::{any::type_name, vec}; + use std::vec; use super::Prop; @@ -657,9 +659,10 @@ mod tests { use chumsky::{Parser, Stream}; use crate::kernel::{ - checker::identifier::Identifier, + checker::{identifier::Identifier, identifier_context::IdentifierContext}, parse::{fol::fol_parser, lexer::lexer}, - prop::{PropParameter, QuantifierKind}, + proof_term::Type, + prop::{InstatiationError, PropParameter, QuantifierKind}, }; fn parse_prop(prop: &str) -> Prop { @@ -1516,7 +1519,7 @@ mod tests { } #[test] - fn test_do_not_bind_already_binded_identifier() { + fn test_do_not_bind_already_bound_identifier() { assert_eq!( parse_prop("\\forall a:t. A(a)").bind_identifier( QuantifierKind::ForAll, @@ -1594,4 +1597,105 @@ mod tests { parse_prop("\\forall x:t. A(x) & B (x)") ) } + + #[test] + fn test_instantiate_with_context_simple() { + let mut prop = Prop::True; + let ctx = IdentifierContext::new(); + + assert_eq!(prop.instantiate_parameters_with_context(&ctx), Ok(())); + } + + #[test] + fn test_instantiate_with_context_atom() { + let mut prop = Prop::Atom( + "A".to_string(), + vec![PropParameter::Uninstantiated("x".to_string())], + ); + + let identifier = Identifier::new("x".to_string(), 42); + let mut ctx = IdentifierContext::new(); + ctx.insert(identifier.clone(), Type::Datatype("t".to_string())); + + assert_eq!(prop.instantiate_parameters_with_context(&ctx), Ok(())); + if let Prop::Atom(_, params) = prop { + assert_eq!(params[0], PropParameter::Instantiated(identifier)); + } else { + panic!("Expected Prop::Atom"); + } + } + + #[test] + fn test_instantiate_with_context_nested() { + let mut prop = Prop::And( + Box::new(Prop::Atom( + "A".to_string(), + vec![PropParameter::Uninstantiated("x".to_string())], + )), + Box::new(Prop::Atom( + "B".to_string(), + vec![PropParameter::Uninstantiated("y".to_string())], + )), + ); + let mut ctx = IdentifierContext::new(); + let fst_ident = Identifier::new("x".to_string(), 1); + let snd_ident = Identifier::new("y".to_string(), 2); + + ctx.insert(fst_ident.clone(), Type::Datatype("t".to_string())); + ctx.insert(snd_ident.clone(), Type::Datatype("list".to_string())); + + assert_eq!(prop.instantiate_parameters_with_context(&ctx), Ok(())); + if let Prop::And(prop1, prop2) = prop { + if let Prop::Atom(_, params1) = *prop1 { + assert_eq!(params1[0], PropParameter::Instantiated(fst_ident)); + } else { + panic!("Expected Prop::Atom"); + } + if let Prop::Atom(_, params2) = *prop2 { + assert_eq!(params2[0], PropParameter::Instantiated(snd_ident)); + } else { + panic!("Expected Prop::Atom"); + } + } else { + panic!("Expected Prop::And with Prop::Atom"); + } + } + + #[test] + fn test_instantiate_with_context_forall() { + let mut prop = Prop::ForAll { + object_ident: "a".to_string(), + object_type_ident: "t".to_string(), + body: Box::new(Prop::Atom( + "A".to_string(), + vec![PropParameter::Uninstantiated("a".to_string())], + )), + }; + let ctx = IdentifierContext::new(); + + assert_eq!(prop.instantiate_parameters_with_context(&ctx), Ok(())); + if let Prop::ForAll { body, .. } = prop { + if let Prop::Atom(_, params) = *body { + assert_eq!(params[0], PropParameter::Uninstantiated("a".to_string())); + } else { + panic!("Expected Prop::Atom"); + } + } else { + panic!("Expected Prop::ForAll"); + } + } + + #[test] + fn test_instantiate_with_context_unknown_identifier() { + let mut prop = Prop::Atom( + "A".to_string(), + vec![PropParameter::Uninstantiated("x".to_string())], + ); + let ctx = IdentifierContext::new(); + + assert_eq!( + prop.instantiate_parameters_with_context(&ctx), + Err(InstatiationError::UnknownIdentifier("x".to_string())) + ); + } }