diff options
Diffstat (limited to 'source/Checking/Core.hs')
| -rw-r--r-- | source/Checking/Core.hs | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index 4b7478f..f8466af 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -58,6 +58,7 @@ module Checking.Core , closeScopedExists , openScopedForall , openScopedImplication + , openScopedAssumption , closeScopedCore , instantiateCanonical , mapCanonicalGlobals @@ -1058,6 +1059,52 @@ openScopedImplication openScopedImplication _scoped = Nothing +-- | Open a checked proof assumption against the current goal. Besides a +-- direct implication antecedent, the source language historically permits +-- either immediate side of one binary conjunction antecedent to be assumed +-- first. The other side remains the next implication antecedent. This is a +-- deliberately shallow structural rule: it neither flattens conjunctions nor +-- treats disjunction as an eliminable assumption. +openScopedAssumption + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +openScopedAssumption supplied goal = do + (antecedent, conclusion) <- openScopedImplication goal + if supplied == antecedent + then pure (antecedent, conclusion) + else do + (left, right) <- splitScopedConjunction antecedent + if supplied == left + then do + remaining <- implyScopedCore right conclusion + pure (left, remaining) + else if supplied == right + then do + remaining <- implyScopedCore left conclusion + pure (right, remaining) + else Nothing + +splitScopedConjunction + :: ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +splitScopedConjunction + (ScopedCheckedCore context TyProp + (CImp (CImp left (CImp right CFalsum)) CFalsum)) = + Just + ( ScopedCheckedCore context TyProp left + , ScopedCheckedCore context TyProp right + ) +splitScopedConjunction _scoped = + Nothing + closeScopedCore :: ScopedCheckedCore global -> Maybe (FrozenCheckedCore global) |