Feature Complete

Finalised the proof output and goals.
The Local Function definition now producces a Function f with the right
domain and range, together with the rules presented in cases.
Then proof goal of this local definition is set to
for all x we have x is element of dom(f) if and only if x is in exactly one of the subdomains.
This suffices as welldefindness check on f, besides the right range.

Further checks that should be implemented are the correct range of the function.
And optional subproof such that the presented goal can be check easily.

2 files changed, 34 insertions, 13 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index 7362c93..b43923c 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -555,30 +555,41 @@ checkProof = \case
             ,Asm (relationNoun (TermVar funVar))]
 
         goals <- gets checkingGoals
-        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union
+        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)]
         tellTasks
 
         assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f)
-        assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians
+        assume (functionSubdomianExpression funVar argVar domVar (NonEmpty.toList definitions)) --behavior on the subdomians
         setGoals goals
         checkProof continue
 
+-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..)))
+--  where the phi_{i} are the subdomain statments
+localFunctionGoal :: NonEmpty (Term,Formula) -> Formula
+localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs
 
--- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!!
-subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula 
-subdomainConjuctionLocalFunction _ defintions = 
-    let stmts = [snd x | x <- NonEmpty.toList defintions]
-    in makeDisjunction stmts 
 
+-- We have our list of expr and forumlas, in this case normaly someone would write
+-- f(x) =  ....cases
+--      & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\)
+--
+-- So therefore we have to check that all free varibels in lhs are free on rhs,
+-- since its an expression all varibals from the lhs has to be free on rhs. 
+--
+-- so we take (exp, frm) -> binding all free in exp 
+-- -> make forall [x, bound vars] x \in \dom(f) & frm => exp
 
-functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
-functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs
-functionSubdomianExpression _ _ [] = []
 
-    
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a d (x:xs) = singleFunctionSubdomianExpression f a d x : functionSubdomianExpression f a d xs
+functionSubdomianExpression _ _ _ [] = []
 
-singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
-singleFunctionSubdomianExpression funVar argVar x = Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` snd x) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` fst x)))
+singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
+singleFunctionSubdomianExpression funVar argVar domVar (expr, frm) = let
+    boundVar = Set.toList (freeVars expr) in
+    let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)
+    in Asm def
+    
 
 
 checkCalc :: Calc -> Checking
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 7046161..e83126d 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -324,6 +324,16 @@ makeDisjunction = \case
     [] -> Bottom
     es -> List.foldl1' Or es
 
+makeIff :: [ExprOf a] -> ExprOf a
+makeIff = \case
+    [] -> Bottom
+    es -> List.foldl1' Iff es
+    
+makeXor :: [ExprOf a] -> ExprOf a
+makeXor = \case
+    [] -> Bottom
+    es -> List.foldl1' Xor es
+
 finiteSet :: NonEmpty (ExprOf a) -> ExprOf a
 finiteSet = foldr cons EmptySet
     where