caledon 3.1.0.0 → 3.2.0.0
raw patch · 15 files changed
+256/−150 lines, 15 files
Files
- Choice.hs +5/−2
- Context.hs +61/−21
- HOU.hs +101/−73
- Main.hs +2/−0
- Options.hs +18/−10
- Substitution.hs +1/−10
- caledon.cabal +1/−1
- examples/#test.ncc# +0/−25
- examples/divergent.ncc +10/−0
- examples/double.ncc +15/−0
- examples/listTest.ncc +11/−0
- examples/tactics.ncc +23/−0
- prelude/booleans.ncc +4/−4
- prelude/list.ncc +2/−2
- prelude/naturals.ncc +2/−2
Choice.hs view
@@ -30,13 +30,16 @@ pure = Success mf <*> ma = mf >>= (<$> ma) +--determine a b = appendErr "" $ (:<|>:) (appendErr "" a) (appendErr "" b)+determine = (:<|>:)+ instance Alternative Choice where empty = Fail ""- (<|>) = (:<|>:)+ (<|>) = determine instance MonadPlus Choice where mzero = Fail ""- mplus = (:<|>:)+ mplus = determine class RunChoice m where runError :: m a -> Either String a
Context.hs view
@@ -62,16 +62,16 @@ addToContext s c (Binding _ _ _ Nothing Nothing) = error $ "context not empty so can't add to tail: "++show c addToContext s c@(Context h ctxt t) elm@(Binding _ nm _ t'@(Just p) Nothing) | t' == t = checkContext (s++"\naddToCtxt J N: "++show elm ++ "\n\tOLD CONTEXT: "++show c) $ Context h (M.insert p t'val $ M.insert nm elm $ ctxt) (Just nm)- where t'val = (lookupWith "looking up p ctxt" p ctxt) { elmNext = Just nm }+ where t'val = (lookupWith (s++" looking up p ctxt") p ctxt) { elmNext = Just nm } addToContext s _ (Binding _ _ _ _ Nothing) = error "can't add this to tail" addToContext s (Context h ctxt t) elm@(Binding _ nm _ Nothing h'@(Just n)) | h' == h = checkContext (s++"\naddToCtxt N J: ") $ Context (Just nm) (M.insert n h'val $ M.insert nm elm $ ctxt) t- where h'val = (lookupWith "looking up n ctxt" n ctxt) { elmPrev = Just nm }+ where h'val = (lookupWith (s++" looking up n ctxt") n ctxt) { elmPrev = Just nm } addToContext s _ (Binding _ _ _ Nothing _) = error "can't add this to head" addToContext s ctxt@Context{ctxtMap = cmap} elm@(Binding _ nm _ (Just p) (Just n)) = checkContext (s++"\naddToCtxt J J: ") $ ctxt { ctxtMap = M.insert n n'val $ M.insert p p'val $ M.insert nm elm $ cmap }- where n'val = (lookupWith "looking up n cmap" n cmap) { elmPrev = Just nm }- p'val = (lookupWith "looking up p cmap" p cmap) { elmNext = Just nm }+ where n'val = (lookupWith (s++" looking up n cmap") n cmap) { elmPrev = Just nm }+ p'val = (lookupWith (s++" looking up p cmap") p cmap) { elmNext = Just nm } removeFromContext :: Name -> Context -> Context removeFromContext nm ctxt@(Context h cmap t) = case M.lookup nm cmap of@@ -90,15 +90,23 @@ p' = M.insert cp $ (lookupWith "looking up a cmap for p'" cp cmap ) { elmNext = Just cn } where isSane bool a = if bool then a else error "This doesn't match intended binding" +addAfter s t quant nm tp ctxt@Context{ctxtMap = cmap} = checkContext "addAfter" $ do+ let top = lookupWith ("looking up "++t++"\n\t in context: "++show cmap++"\n\t"++s) t cmap+ addToContext ("ADD_AFTER: "++s) ctxt $ Binding quant nm tp (Just $ elmName top) (elmNext top)++addBefore s b quant nm tp ctxt@Context{ctxtMap = cmap} = checkContext "addBefore" $ do+ let bot = lookupWith ("looking up "++b++"\n\t in context: "++show cmap++"\n\t"++s) b cmap+ addToContext ("ADD_BEFORE: "++s) ctxt $ Binding quant nm tp (elmPrev bot) (Just $ elmName bot)+ addToHead s quant nm tp ctxt@Context{ctxtMap = cmap} = case M.lookup nm cmap of - Nothing -> addToContext s ctxt $ Binding quant nm tp Nothing (ctxtHead ctxt)+ Nothing -> addToContext ("ATH: "++s) ctxt $ Binding quant nm tp Nothing (ctxtHead ctxt) Just (Binding{ elmQuant = quant', elmType = tp'}) | quant' == quant && tp' == tp && quant == Forall -> - addToContext s ctxt' $ Binding quant nm tp Nothing (ctxtHead ctxt')+ addToContext ("ATH2: "++s) ctxt' $ Binding quant nm tp Nothing (ctxtHead ctxt') where ctxt' = removeFromContext nm ctxt _ -> error $ "Can't add to head, already in context: "++show nm++" : "++show tp++"\n@"++show ctxt addToTail s quant nm tp ctxt@Context{ctxtMap = cmap} = case M.lookup nm cmap of- Nothing -> addToContext s ctxt $ Binding quant nm tp (ctxtTail ctxt) Nothing+ Nothing -> addToContext ("ATT: "++s) ctxt $ Binding quant nm tp (ctxtTail ctxt) Nothing Just (Binding{ elmQuant = quant', elmType = tp'}) | quant' == quant && tp' == tp && quant == Forall -> ctxt _ -> error $ "Can't add to tail, already in context: "++show nm++" : "++show tp++"\n@"++show ctxt @@ -117,8 +125,8 @@ getHead (Context Nothing _ _) = error "no head" -- gets the list of bindings after (below) a given binding-getAfter s bind ctx = tail $ getAfter' s bind ctx -getAfter' s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind+getAfter s bind ctx = tail $ getAfterInclusive s bind ctx +getAfterInclusive s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind where gb ~(Binding quant nm ty _ n) = (quant, (nm,ty)):case n of Nothing -> [] Just n -> gb $ case M.lookup n ctxt of @@ -126,23 +134,23 @@ Just c -> c -- gets the list of bindings before (above) a given binding-getBefore s bind ctx = tail $ getBefore' s bind ctx -getBefore' s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind+getBefore s bind ctx = tail $ getBeforeInclusive s bind ctx +getBeforeInclusive s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind where gb ~(Binding quant nm ty p _) = (quant, (nm,ty)):case p of Nothing -> [] Just p -> gb $ case M.lookup p ctxt of Nothing -> error $ "element "++show p++" not in map \n\twith ctxt: "++show ctx++" \n\t for bind: "++show bind++"\n\t"++s Just c -> c ---checkContext _ c = c-+checkContext _ c = c+{- checkContext _ c@(Context Nothing _ Nothing) = c checkContext s ctx = foldr (\v c -> seq (checkEquals v) c) ctx $ zip st (reverse $ ta)- where st = getBefore' s (getTail ctx) ctx- ta = getAfter' s (getHead ctx) ctx+ where st = getBeforeInclusive s (getTail ctx) ctx+ ta = getAfterInclusive s (getHead ctx) ctx checkEquals (a,b) | (a == b) = () checkEquals (a,b) = error $ s++" \n\tNOT THE SAME" ++show (a,b) ++ " \n\t IN "++show ctx-+-} ------------------------- --- Traversal Monad ---@@ -183,13 +191,32 @@ case ty of Nothing -> Left <$> (\ctxt -> lookupWith ("looking up "++x++"\n\t in context: "++show ctxt++"\n\t"++s) x ctxt) <$> ctxtMap <$> stateCtxt <$> get Just a -> return $ Right a+ +getBindings :: Binding -> Env [(Name,Type)]+getBindings bind = fmap snd <$> getQuantBindings bind +getBindingsInclusive :: Binding -> Env [(Name,Type)]+getBindingsInclusive bind = fmap snd <$> getQuantBindings bind+ -- | This gets all the bindings outside of a given bind and returns them in a list (not including that binding).-getBindings :: Binding -> Env [(Name,Type)]-getBindings bind = do+getQuantBindings :: Binding -> Env [(Quant, (Name,Type))]+getQuantBindings bind = do ctx <- stateCtxt <$> get- return $ snd <$> getBefore "IN: getBindings" bind ctx+ return $ getBefore "IN: getQuantBindings" bind ctx +getQuantBindingsInclusive :: Binding -> Env [(Quant, (Name,Type))]+getQuantBindingsInclusive bind = do+ ctx <- stateCtxt <$> get+ return $ getBeforeInclusive "IN: getQuantBindingsInclusive" bind ctx + + +getBindingsBetween :: Binding -> Binding -> Env [(Name,Type)]+getBindingsBetween top bottom = do+ above <- getBindings top+ target <- getBindings bottom+ let aboveSet = S.insert (elmName top) $ S.fromList $ fst <$> above + return $ filter (\n -> not $ S.member (fst n) aboveSet) target+ getAnExist :: Env (Maybe (Name,Type)) getAnExist = do ctx <- stateCtxt <$> get@@ -197,19 +224,32 @@ last = (elmQuant til, (elmName til, elmType til)) return $ case ctx of Context _ _ Nothing -> Nothing- _ -> snd <$> find (\(q,_) -> q == Exists) (last:getBefore "IN: getBindings" til ctx)+ _ -> snd <$> find (\(q,_) -> q == Exists) (last:getBefore "IN: getAnExist" til ctx) +-- | `getAllBindings` gets all bindings, listed from tightest to loosest+-- ie, ∀a:t∃b:t will return [(∃,(b,t)), (∀,(a,t))] getAllBindings = do ctx <- stateCtxt <$> get case ctx of Context _ _ Nothing -> return []- _ -> (getBindings $ getTail ctx)+ _ -> getQuantBindingsInclusive $ getTail ctx+ getForalls :: Env ContextMap getForalls = do ctx <- ctxtMap <$> stateCtxt <$> get return $ anonymous <$> elmType <$> M.filter (\q -> elmQuant q == Forall) ctx++getForallsAfter :: Binding -> Env (S.Set Name)+getForallsAfter bind = do+ ctx <- stateCtxt <$> get+ return $ S.fromList $ map (fst . snd) $ filter ((== Forall) . fst) $ getAfter "IN: getForalls" bind ctx +getExistsAfter :: Binding -> Env (S.Set Name)+getExistsAfter bind = do+ ctx <- stateCtxt <$> get+ return $ S.fromList $ map (fst . snd) $ filter ((== Exists) . fst) $ getAfter "IN: getExistsAfter" bind ctx + getExists :: Env ContextMap getExists = do ctx <- ctxtMap <$> stateCtxt <$> get
HOU.hs view
@@ -88,14 +88,15 @@ let !sub'' = sub *** sub' modifyCtxt $ subst sub' uniWhile sub'' $! c'- - - vtrace 3 ("CONST: "++show c)- ( uniWith unifyOne + + ctxt <- getAllBindings+ + vtraceShow 2 3 "CONST" c + $ vtraceShow 3 3 "CTXT" (reverse ctxt)+ $ uniWith unifyOne $ uniWith unifySearch $ uniWith unifySearchAtom- $ checkFinished c >> - return (sub, c))+ $ checkFinished c >> return (sub, c) sub <- fst <$> uniWhile mempty cons @@ -165,28 +166,38 @@ return $ Just (mempty, [s `apply` var nm :=: s'], False) (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [], False)- (s@(Spine x yl), s') -> vtrace 4 "-ss-" $ do+ (s@(Spine x yl), s') -> vtraceShow 4 5 "-ss-" cons $ do bind <- getElm ("all: "++show cons) x case bind of- Left bind@Binding{ elmQuant = Exists } -> vtrace 4 "-g?-" $ do- raiseToTop bind (Spine x yl) $ \(a@(Spine x yl),ty) sub ->- case subst sub s' of- b@(Spine x' y'l) -> vtrace 4 "-gs-" $ do+ Left bind@Binding{ elmQuant = Exists, elmType = ty } -> vtraceShow 4 5 "-g?-" cons $ do+ fors <- getForallsAfter bind+ exis <- getExistsAfter bind+ case s' of+ b@(Spine x' y'l) -> vtraceShow 4 5 "-gs-" cons $ do bind' <- getElm ("gvar-blah: "++show cons) x' case bind' of Right ty' -> vtraceShow 1 2 "-gc-" cons $ -- gvar-const--- if allElementsAreVariables yl--- then gvar_const (Spine x yl, ty) (Spine x' y'l, ty') --- else return Nothing- gvar_const (Spine x yl, ty) (Spine x' y'l, ty') - Left Binding{ elmQuant = Forall } | not $ S.member x' $ freeVariables yl -> - throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)+ if allElementsAreVariablesNoPP fors yl+ then gvar_const (Spine x yl, ty) (Spine x' y'l, ty') + else return Nothing+ Left Binding{ elmQuant = Forall } | (not $ elem (var x') yl) && S.member x' fors -> + if allElementsAreVariables fors yl + then throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)+ else return Nothing Left Binding{ elmQuant = Forall } | S.member x $ freeVariables y'l -> - throwTrace 0 $ "CANT: occurs check: "++show (a :=: b)- Left Binding{ elmQuant = Forall, elmType = ty' } -> vtrace 1 "-gui-" $ -- gvar-uvar-inside- gvar_uvar_inside (Spine x yl, ty) (Spine x' y'l, ty')- Left bind@Binding{ elmQuant = Exists, elmType = ty' } -> - if not $ allElementsAreVariables yl && allElementsAreVariables y'l + if allElementsAreVariables fors yl + then throwTrace 0 $ "CANT: occurs check: "++show (a :=: b)+ else return Nothing+ Left Binding{ elmQuant = Forall, elmType = ty' } | S.member x' fors -> vtraceShow 1 5 "-gui-" cons $ -- gvar-uvar-inside+ if allElementsAreVariables fors yl+ then gvar_uvar_inside (Spine x yl, ty) (Spine x' y'l, ty')+ else return Nothing+ Left Binding{ elmQuant = Forall, elmType = ty' } -> vtraceShow 1 5 "-guo-" cons $ + if allElementsAreVariablesNoPP fors yl+ then gvar_uvar_outside (Spine x yl, ty) (Spine x' y'l, ty')+ else return Nothing+ Left bind'@Binding{ elmQuant = Exists, elmType = ty'} -> vtraceShow 4 5 "-gg-" cons $+ if not $ allElementsAreVariables fors yl && allElementsAreVariables fors y'l && S.member x' exis then return Nothing else if x == x' then vtraceShow 1 2 "-ggs-" cons $ -- gvar-gvar-same@@ -194,8 +205,8 @@ else -- gvar-gvar-diff if S.member x $ freeVariables y'l then throwTrace 0 $ "CANT: ggd-occurs check: "++show (a :=: b)- else vtraceShow 1 2 "-ggd-" cons $ gvar_gvar_diff (Spine x yl, ty) (Spine x' y'l, ty') bind- _ -> vtrace 1 "-ggs-" $ return Nothing+ else vtraceShow 1 2 "-ggd-" cons $ gvar_gvar_diff bind (Spine x yl, ty) (Spine x' y'l, ty') bind'+ _ -> vtraceShow 1 5 "-ggs-" cons $ return Nothing _ -> vtrace 4 "-u?-" $ case s' of b@(Spine x' _) | x /= x' -> do bind' <- getElm ("const case: "++show cons) x'@@ -212,16 +223,24 @@ match al (Spine "#tycon#" [Spine _ [_]]:bl) = match al bl match (a:al) (b:bl) = ((a :=: b) :) <$> match al bl match [] [] = return []- match _ _ = throwTrace 0 $ "CANT: different numbers of arguments on constant: "++show cons+ match _ _ = throwTrace 0 $ "CANT: different numbers of arguments: "++show cons cons <- match yl yl' return $ Just (mempty, cons, False) _ -> throwTrace 0 $ "CANT: uvar against a pi WITH CONS "++show cons -allElementsAreVariables :: [Spine] -> Bool-allElementsAreVariables = all $ \c -> case c of- Spine _ [] -> True- _ -> False+allElementsAreVariables :: S.Set Name -> [Spine] -> Bool+allElementsAreVariables fors = partialPerm mempty + where partialPerm s [] = True+ partialPerm s (Spine nm []:l) | S.member nm fors && not (S.member nm s) = + partialPerm (S.insert nm s) l+ partialPerm _ _ = False+ +allElementsAreVariablesNoPP fors = partial+ where partial [] = True+ partial (Spine nm []:l) | S.member nm fors = partial l+ partial _ = False+ typeToListOfTypes (Spine "#forall#" [_, Abs x ty l]) = (x,ty):typeToListOfTypes l typeToListOfTypes (Spine _ _) = []@@ -230,9 +249,10 @@ -- the problem WAS (hopefully) here that the binds were getting -- a different number of substitutions than the constraints were. -- make sure to check that this is right in the future.-raiseToTop bind@Binding{ elmName = x, elmType = ty } sp m = do- - hl <- reverse <$> getBindings bind+raiseToTop top@Binding{ elmNext = Just k} bind@Binding{ elmName = x, elmType = ty } sp m | k == x = + m (sp, ty) mempty+raiseToTop top bind@Binding{ elmName = x, elmType = ty } sp m = do+ hl <- reverse <$> getBindingsBetween top bind x' <- getNewWith "@newx" let newx_args = map (var . fst) hl@@ -248,7 +268,7 @@ modifyCtxt $ subst sub' return $ Just (sub'', cons,b) - modifyCtxt $ addToHead "-rtt-" Exists x' ty' . removeFromContext x+ modifyCtxt $ addAfter "-rtt-" (elmName top) Exists x' ty' . removeFromContext x vtrace 3 ("RAISING: "++x' ++" +@+ "++ show newx_args ++ " ::: "++show ty' ++"\nFROM: "++x ++" ::: "++ show ty ) modifyCtxt $ subst sub@@ -281,19 +301,21 @@ sub = x |-> l - modifyCtxt $ addToHead "-ggs-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!+ modifyCtxt $ addBefore "-ggs-" x Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!+ modifyCtxt $ removeFromContext x return $ Just (sub, [], False) -- var xN :@: xNty]) gvar_gvar_same _ _ = error "gvar-gvar-same is not made for this case" -gvar_gvar_diff (a',aty') (sp, _) bind = raiseToTop bind sp $ \(b'@(Spine x' y'l), bty) subO -> do+gvar_gvar_diff top (a',aty') (sp, _) bind = raiseToTop top bind sp $ \b subO -> do+ let a = (subst subO a', subst subO aty')+ gvar_gvar_diff' a b - let (Spine x yl, aty) = (subst subO a', subst subO aty')-+gvar_gvar_diff' (Spine x yl, aty) ((Spine x' y'l), bty) = do -- now x' comes before x -- but we no longer care since I tested it, and switching them twice reduces to original- n = length yl+ let n = length yl m = length y'l aty <- regenAbsVars aty@@ -314,44 +336,37 @@ xNty = foldr (uncurry forall) (getBase n aty) (map fst perm) - sub = M.fromList [(x ,l), (x',l')]+ sub = (x' |-> l') *** (x |-> l) -- M.fromList [(x , l), (x',l')] - modifyCtxt $ addToHead "-ggd-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!- + modifyCtxt $ addBefore "-ggd-" x Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!+ modifyCtxt $ subst sub . removeFromContext x . removeFromContext x' vtrace 3 ("SUBST: -ggd- "++show sub) $ return $ Just (sub, [] {- var xN :@: xNty] -}, False) gvar_uvar_inside a@(Spine _ yl, _) b@(Spine y _, _) = case elemIndex (var y) $ reverse yl of Nothing -> return Nothing- Just _ -> gvar_uvar_outside a b+ Just _ -> gvar_uvar_possibilities a b gvar_uvar_inside _ _ = error "gvar-uvar-inside is not made for this case"- -gvar_const a@(s@(Spine x yl), _) b@(s'@(Spine y _), bty) = vtrace 3 (show a++" ≐ "++show b) $- case elemIndex (var y) $ yl of - Nothing -> gvar_fixed a b $ var . const y- Just _ -> do- gvar_uvar_outside a b <|> gvar_fixed a b (var . const y) -gvar_const _ _ = error "gvar-const is not made for this case"--gvar_uvar_outside a@(s@(Spine x yl),_) b@(s'@(Spine y _),bty) = do- let ilst = [i | (i,y') <- zip [0..] yl , y' == var y] - i <- F.asum $ return <$> ilst- gvar_fixed a b $ (!! i) +gvar_uvar_outside = gvar_const +gvar_const a@(s@(Spine x yl), _) b@(s'@(Spine y _), bty) = gvar_fixed a b $ var . const y+gvar_const _ _ = error "gvar-const is not made for this case" -gvar_uvar_outside _ _ = error "gvar-uvar-outside is not made for this case"+gvar_uvar_possibilities a@(s@(Spine x yl),_) b@(s'@(Spine y _),bty) = + case elemIndex (var y) yl of+ Just i -> gvar_fixed a b $ (!! i)+ Nothing -> throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (s :=: s')+gvar_uvar_possibilities _ _ = error "gvar-uvar-possibilities is not made for this case" getTyNews (Spine "#forall#" [_, Abs _ _ t]) = Nothing:getTyNews t getTyNews (Spine "#imp_forall#" [_, Abs nm _ t]) = Just nm:getTyNews t getTyNews _ = [] gvar_fixed (a@(Spine x _), aty) (b@(Spine _ y'l), bty) action = do- let m = getTyNews bty -- max (length y'l) (getTyLen bty)+ let m = getTyNews bty cons = a :=: b--- getNewTys "@xm" bty - let getArgs (Spine "#forall#" [ty, Abs ui _ r]) = ((var ui,ui),Left ty):getArgs r getArgs (Spine "#imp_forall#" [ty, Abs ui _ r]) = ((tycon ui $ var ui,ui),Right ty):getArgs r@@ -380,7 +395,8 @@ Left ty -> forall nm ty a Right ty -> imp_forall nm ty a ) e untylr-+ + -- returns the list in the same order as xm substBty sub (Spine "#forall#" [_, Abs vi bi r]) ((x,xi):xmr) = (x,vbuild $ subst sub bi) :substBty (M.insert vi (fst xi) sub) r xmr substBty sub (Spine "#imp_forall#" [_, Abs vi bi r]) ((x,xi):xmr) = (x,vbuild $ subst sub bi)@@ -391,14 +407,14 @@ ++ "\nON "++ show cons sub = x |-> l -- THIS IS THAT STRANGE BUG WHERE WE CAN'T use x in the output substitution!- addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addToHead "-gf-" Exists s t- modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm - modifyCtxt $ subst sub+ addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addAfter "-gf-" x Exists s t+ -- foldr ($) addBeforeX [x1...xN]+ modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm + modifyCtxt $ subst sub . removeFromContext x vtrace 4 ("RES: -gg- "++(show $ subst sub $ a :=: b)) $ vtrace 4 ("FROM: -gg- "++(show $ a :=: b)) $ return $ Just (sub, [ subst sub $ a :=: b -- this ensures that the function resolves to the intended output- - ], False)+ ], False) gvar_fixed _ _ _ = error "gvar-fixed is not made for this case" @@ -502,7 +518,7 @@ res <- Just <$> ls (nm,targ) if sequ then (if not $ null cg then (appendErr "" (F.asum $ reverse cg) <|>) else id) $ - (appendErr "" $ ret res) <|> inter [] l+ (appendErr ""$ ret res) <|> inter [] l else inter (ret res:cg) l @@ -802,7 +818,7 @@ sub = subst $ nm' |-> ascribe val (dontcheck ty) _ -> (l', resp:r, toplst) - (lst',l) <- inferAll (tys, [], topoSortAxioms lst)+ (lst',l) <- inferAll (tys, [], topoSortAxioms True lst) let doubleCheckAll _ [] = return () doubleCheckAll l (p:r) = do@@ -820,22 +836,24 @@ ++ "\nunsound "++nm++" : "++show val doubleCheckAll (S.insert nm l) r - doubleCheckAll (S.union envSet uns) $ topoSortAxioms lst'+ doubleCheckAll (S.union envSet uns) $ topoSortAxioms False lst' return $ snd <$> l --topoSortAxioms :: [FlatPred] -> [FlatPred]-topoSortAxioms axioms = topoSortComp (\p -> (p^.predName,) +topoSortAxioms :: Bool -> [FlatPred] -> [FlatPred]+topoSortAxioms accountPot axioms = showRes $ topoSortComp (\p -> (p^.predName,) + $ showGraph (p^.predName) -- unsound can mean this causes extra cyclical things to occur- $ (if p^.predSound then S.union (getImplieds $ p^.predName) else id)+ $ (if accountPot && p^.predSound then S.union (getImplieds $ p^.predName) else id) $ S.fromList $ concatMap (\nm -> [nm,"#v:"++nm]) $ filter (not . flip elem (map fst consts)) $ S.toList $ freeVariables p ) axioms - where nm2familyLst = catMaybes $ (\p -> (p^.predName,) <$> (p^.predFamily)) <$> axioms+ where showRes a = vtrace 0 ("TOP_RESULT: "++show ((^.predName) <$> a)) a+ showGraph n a = vtrace 1 ("TOP_EDGE: "++n++" -> "++show a) a + nm2familyLst = catMaybes $ (\p -> (p^.predName,) <$> (p^.predFamily)) <$> axioms family2nmsMap = foldr (\(fam,nm) m -> M.insert nm (case M.lookup nm m of Nothing -> S.singleton fam@@ -849,9 +867,19 @@ $ S.toList $ getImpliedFamilies $ p^.predType- )) <$> axioms + )) <$> axioms getImplieds nm = fromMaybe mempty (M.lookup nm family2impliedsMap)++getImpliedFamilies s = S.intersection fs $ gif s+ where fs = freeVariables s+ gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of+ Nothing -> id+ Just f | f == atomName -> id+ Just f -> S.insert f) $ gif ty `S.union` gif a + gif (Spine a l) = mconcat $ gif <$> l+ gif (Abs _ ty l) = S.union (gif ty) (gif l)+ typeCheckAll :: Bool -> [Decl] -> Choice [Decl] typeCheckAll verbose preds = do
Main.hs view
@@ -64,6 +64,8 @@ processFile :: Options -> IO ()+processFile options | options ^. optHelp /= Nothing = case options ^. optHelp of+ Just s -> putStrLn s processFile options = do let fname = options ^. optFile
Options.hs view
@@ -3,6 +3,7 @@ FlexibleContexts #-} module Options where+import Data.List import Data.Maybe import Control.Lens (makeLenses, (.~))@@ -12,13 +13,16 @@ { _optIO_Only :: Bool , _optVerbose :: Int , _optFile :: String- } + , _optHelp :: Maybe String+ }+ $(makeLenses ''Options) defaultOptions = Options { _optIO_Only = False , _optVerbose = 0 , _optFile = ""+ , _optHelp = Nothing } @@ -32,21 +36,25 @@ "a number describing how much debugging information to print" , Option ['f'] ["file", "infile", "input"] (ReqArg (optFile .~) "INFILE")- "the file to interpret and typecheck"+ "a number describing how much debugging information to print"+ , Option ['h'] ["help"]+ (OptArg ((optHelp .~) . Just . fromMaybe helpMsg . fmap getMsg) "OPTION")+ "display this help message" ] helpMessage = "Usage is \"caledon [--io-only] file.ncc\"" -arg_lst = [ ["--io-only", "-i"]- , ["--verbosity", "-V"]- , ["--help", "-h"]- , ["--file", "-f"]- ]- compilerOpts :: [String] -> IO (Options,[String]) compilerOpts argv = case getOpt Permute options argv of (o,n,[] ) -> return (foldl (flip id) defaultOptions o, n)- (_,_,errs) -> ioError $ userError $ concat errs ++ usageInfo header options+ (_,_,errs) -> ioError $ userError $ concat errs ++ helpMsg -header = "Usage: caledon [OPTIONS] file.ncc"+helpMsg = usageInfo header options+getMsg option = usageInfo header $ maybeToList + $ find (\(Option s l _ _) -> elem option $ concat $ + [[['-',i],[i]] | i <- s ] + ++[["--"++i,i] | i <- l ] + ) options+ +header = "Usage: caledon [OPTIONS] file.ncc"
Substitution.hs view
@@ -42,7 +42,7 @@ return $ show n getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String-getNewWith s = {- (++s) <$> -} getNew+getNewWith s = (++s) <$> getNew ---------------------@@ -103,15 +103,6 @@ class Subst a where substFree :: Substitution -> S.Set Name -> a -> a- --getImpliedFamilies s = S.intersection fs $ gif s- where fs = freeVariables s- gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of- Nothing -> id- Just f -> S.insert f) $ gif ty `S.union` gif a - gif (Spine a l) = mconcat $ gif <$> l- gif (Abs _ ty l) = S.union (gif ty) (gif l) subst :: Subst a => Substitution -> a -> a subst s = substFree s $ freeVariables s
caledon.cabal view
@@ -1,6 +1,6 @@ Name: caledon -Version: 3.1.0.0+Version: 3.2.0.0 Description: a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities.
− examples/#test.ncc#
@@ -1,25 +0,0 @@-#include "../prelude/prelude.ncc"--query add0 = add (succ zero) zero (succ zero)--query add1 = succ zero ++ zero == succ zero--query add2 = exists A : natural . add (succ zero) zero A--query add3 = any $ add (succ zero) zero--query findSat1 = succ zero =< succ (succ zero)--query findSat2 = succ zero =< succ (succ zero) /\ zero =< succ (succ zero)--query findSat0 = free A : natural . A =:= zero---defn ismain : prop - as run $ do - , putStr "hey!\n"- , readLine (\A . do - , putStr A- , putStr "\nbye!\n")--query main = ismain
+ examples/divergent.ncc view
@@ -0,0 +1,10 @@+defn unit : prop+ >| u1 = unit++defn divergent : unit -> prop+ | divergentImp = divergent u1 -> divergent S+++defn moop : prop+ | moopimp = moop <- divergent T+query main = moop
+ examples/double.ncc view
@@ -0,0 +1,15 @@+fixity none 5 =:=+defn =:= : char -> char -> prop+ | eq = (B) =:= B++defn char : prop++defn putChar : char -> prop -- builtin+ | putCharImp = [A : char] putChar A++defn main : prop+ | mainImp = main + <- S =:= 'h'+ <- putChar S++query main1 = main
+ examples/listTest.ncc view
@@ -0,0 +1,11 @@+----------------+--- Booleans ---+----------------+defn bool : prop+ | true = bool+ | false = bool++fixity none 0 ==>+defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop+ | thentrue = [F] (true ==> F ) (F (\a1 a2 : A . a1) )+ | thenfalse = [F] (false ==> F) (F (\a1 a2 : B . a2))
+ examples/tactics.ncc view
@@ -0,0 +1,23 @@+#include "../prelude/logic.ncc"++-- just because we can define the theorem +-- doesn't mean we can prove it (we don't have switch?)++defn natural : prop+ as ∀ a : prop . a → (a → a) → a++defn zero : natural+ as λ a : prop . λ z : a . λ s : a → a . z++defn succ : natural → natural+ as λ n : natural . λ a : prop . λ z : a . λ s : a → a . s (n a z s)++defn even : natural → prop+ | even-zero = even zero+ | even-succ = [A : natural] even A -> even (succ (succ A))++defn add : natural → natural → natural+ as λ n₁ n₂ : natural . n₁ natural n₂ succ++defn thm : prop+ as ∀ N . even (add N N)
prelude/booleans.ncc view
@@ -2,8 +2,8 @@ --- Booleans --- ---------------- defn bool : prop- >| true = bool- >| false = bool+ | true = bool+ | false = bool defn if : bool -> bool as \b . b@@ -15,8 +15,8 @@ fixity none 0 ==> defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop- >| thentrue = [F: _ -> A] (true ==> F ) (F (\a1 a2 : A . a1) )- >| thenfalse = [F: _ -> B] (false ==> F) (F (\a1 a2 : B . a2))+ >| thentrue = (true ==> F) (F (\a1 a2 : A . a1) )+ >| thenfalse = (false ==> F) (F (\a1 a2 : B . a2)) defn not : bool -> bool -> prop as \zq . if zq ==> false |:| true
prelude/list.ncc view
@@ -2,8 +2,8 @@ --- Lists --- ------------- defn list : prop -> prop- >| nil = list A- >| cons = A -> list A -> list A+ | nil = list A+ | cons = A -> list A -> list A defn concatList : list A -> list A -> list A -> prop >| concatListNil = concatList {A = T} nil L L
prelude/naturals.ncc view
@@ -3,8 +3,8 @@ --------------------- defn natural : prop- >| zero = natural- >| succ = natural -> natural+ | zero = natural+ | succ = natural -> natural defn add : natural -> natural -> natural -> prop >| add_z = add zero N N