Merge pull request #22 from eneoli/type-annotations-with-params

Type annotations with params

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(
                         <span title={'This parameter is bound by a quantifier.'}>
                             {paramName}

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<Result<ProofTree, CheckError>> 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<Result<ProofTree, CheckError>> 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(),
             });
         }
 

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<Result<(Type, ProofTree), SynthesizeError>> for SynthesizeVisitor<'a> {
@@ -144,9 +118,7 @@ impl<'a> ProofTermVisitor<Result<(Type, ProofTree), SynthesizeError>> 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<Result<(Type, ProofTree), SynthesizeError>> 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<Result<(Type, ProofTree), SynthesizeError>> 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<Result<(Type, ProofTree), SynthesizeError>> 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 (&param_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<Result<(Type, ProofTree), SynthesizeError>> 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<Result<(Type, ProofTree), SynthesizeError>> 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))
     }

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);

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<Type> for Prop {