9c11754 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added %unifyLog construct

9c11754Edwin Brady13 years ago

src/Core/Elaborate.hs+4

compare with master

unifiedsplit

@@ -91,6 +91,10 @@ getAux :: Elab' aux aux

91getAux = do ES (ps, a) _ _ <- get

92 return a

94+unifyLog :: Bool -> Elab' aux ()

95+unifyLog log = do ES (ps, a) l p <- get

96+ put (ES (ps { unifylog = log }, a) l p)

97+

94processTactic' t = do ES (p, a) logs prev <- get

98processTactic' t = do ES (p, a) logs prev <- get

95 (p', log) <- lift $ processTactic t p

99 (p', log) <- lift $ processTactic t p

96 put (ES (p', a) (logs ++ log) prev)

100 put (ES (p', a) (logs ++ log) prev)

src/Core/ProofState.hs+15−12

@@ -37,6 +37,7 @@ data ProofState = PS { thname :: Name,

37 previous :: Maybe ProofState, -- for undo

38 context :: Context,

39 plog :: String,

40+ unifylog :: Bool,

40 done :: Bool

41 done :: Bool

41 }

42 }

@@ -81,8 +82,9 @@ data Tactic = Attack

81-- Some utilites on proof and tactic states

82-- Some utilites on proof and tactic states

83instance Show ProofState where

84instance Show ProofState where

84− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

85+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _)

86+ = show nm ++ ": no more goals"

85− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _)

87+ show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _)

86 = let OK g = goal (Just h) tm

88 = let OK g = goal (Just h) tm

87 wkenv = premises g in

89 wkenv = premises g in

88 "Other goals: " ++ show hs ++ "\n" ++

90 "Other goals: " ++ show hs ++ "\n" ++

@@ -105,12 +107,12 @@ instance Show ProofState where

105 showG ps b = showEnv ps (binderTy b)

107 showG ps b = showEnv ps (binderTy b)

106

108

107instance Pretty ProofState where

109instance Pretty ProofState where

108− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _) =

110+ pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

109 if size nm > breakingSize then

111 if size nm > breakingSize then

110 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

112 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

111 else

113 else

112 pretty nm <> colon <+> text " no more goals."

114 pretty nm <> colon <+> text " no more goals."

113− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _) =

115+ pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =

114 let OK g = goal (Just h) tm in

116 let OK g = goal (Just h) tm in

115 let wkEnv = premises g in

117 let wkEnv = premises g in

116 text "Other goals" <+> colon <+> pretty hs $$

118 text "Other goals" <+> colon <+> pretty hs $$

@@ -172,13 +174,14 @@ unify' ctxt env topx topy =

172 let dont = dontunify ps

174 let dont = dontunify ps

173 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $

175 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $

174 lift $ unify ctxt env topx topy dont (holes ps)

176 lift $ unify ctxt env topx topy dont (holes ps)

177+ traceWhen (unifylog ps)

175−-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

178+ ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

176−-- " in " ++ show env ++

179+ " in " ++ show env ++

177−-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

180+ "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

178−-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

181+ ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

179−-- -- ++ show (pterm ps)

182+-- ++ show (pterm ps)

180−-- ++ "\n----------") $

183+ ++ "\n----------") $

181− case fails of

184+ case fails of

182-- [] -> return u

185-- [] -> return u

183 err ->

186 err ->

184 do ps <- get

187 do ps <- get

@@ -211,7 +214,7 @@ newProof n ctxt ty = let h = holeName 0

211 (P Bound h ty')) ty [] (h, []) []

214 (P Bound h ty')) ty [] (h, []) []

212 Nothing [] []

215 Nothing [] []

213 [] []

216 [] []

214− Nothing ctxt "" False

217+ Nothing ctxt "" False False

215

218

216type TState = ProofState -- [TacticAction])

219type TState = ProofState -- [TacticAction])

217type RunTactic = Context -> Env -> Term -> StateT TState TC Term

220type RunTactic = Context -> Env -> Term -> StateT TState TC Term

src/Idris/AbsSyntax.hs+7

@@ -569,6 +569,7 @@ expandParams dec ps ns infs tm = en tm

569 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

570 en (PAlternative a as) = PAlternative a (map en as)

571 en (PHidden t) = PHidden (en t)

572+ en (PUnifyLog t) = PUnifyLog (en t)

572 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

573 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

573 en (PProof ts) = PProof (map (fmap en) ts)

574 en (PProof ts) = PProof (map (fmap en) ts)

574 en (PTactics ts) = PTactics (map (fmap en) ts)

575 en (PTactics ts) = PTactics (map (fmap en) ts)

@@ -883,6 +884,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

883 = do imps False env ty

884 = do imps False env ty

884 imps False (n:env) sc

885 imps False (n:env) sc

885 imps top env (PHidden tm) = imps False env tm

886 imps top env (PHidden tm) = imps False env tm

887+ imps top env (PUnifyLog tm) = imps False env tm

886 imps top env _ = return ()

888 imps top env _ = return ()

887

889

888 pibind using [] sc = sc

890 pibind using [] sc = sc

@@ -966,6 +968,7 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

966 ai env (PHidden tm) = PHidden (ai env tm)

968 ai env (PHidden tm) = PHidden (ai env tm)

967 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

969 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

968 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

970 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

971+ ai env (PUnifyLog tm) = PUnifyLog (ai env tm)

969 ai env tm = tm

972 ai env tm = tm

970

973

971 handleErr (Left err) = PElabError err

974 handleErr (Left err) = PElabError err

@@ -1228,6 +1231,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1228 ms <- match' s s'

1231 ms <- match' s s'

1229 return (mt ++ mty ++ ms)

1232 return (mt ++ mty ++ ms)

1230 match (PHidden x) (PHidden y) = match' x y

1233 match (PHidden x) (PHidden y) = match' x y

1234+ match (PUnifyLog x) y = match' x y

1235+ match x (PUnifyLog y) = match' x y

1231 match Placeholder _ = return []

1236 match Placeholder _ = return []

1232 match _ Placeholder = return []

1237 match _ Placeholder = return []

1233 match (PResolveTC _) _ = return []

1238 match (PResolveTC _) _ = return []

@@ -1273,6 +1278,7 @@ substMatchShadow n shs tm t = sm shs t where

1273 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

1278 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

1274 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

1279 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

1275 sm xs (PHidden x) = PHidden (sm xs x)

1280 sm xs (PHidden x) = PHidden (sm xs x)

1281+ sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

1276 sm xs x = x

1282 sm xs x = x

1277

1283

1278shadow :: Name -> Name -> PTerm -> PTerm

1284shadow :: Name -> Name -> PTerm -> PTerm

@@ -1289,6 +1295,7 @@ shadow n n' t = sm t where

1289 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1295 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1290 sm (PAlternative a as) = PAlternative a (map sm as)

1296 sm (PAlternative a as) = PAlternative a (map sm as)

1291 sm (PHidden x) = PHidden (sm x)

1297 sm (PHidden x) = PHidden (sm x)

1298+ sm (PUnifyLog x) = PUnifyLog (sm x)

1292 sm x = x

1299 sm x = x

1293

1300

1294

1301

src/Idris/AbsSyntaxTree.hs+7

@@ -517,6 +517,7 @@ data PTerm = PQuote Raw

517 | PElabError Err -- ^ Error to report on elaboration

518 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

519 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

520+ | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

520 deriving Eq

521 deriving Eq

521{-!

522{-!

522deriving instance Binary PTerm

523deriving instance Binary PTerm

@@ -539,6 +540,7 @@ mapPT f t = f (mpt t) where

539 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

540 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

540 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

541 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

541 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

542 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)

543+ mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)

542 mpt x = x

544 mpt x = x

543

545

544

546

@@ -1084,6 +1086,7 @@ showImp impl tm = se 10 tm where

1084 se p (PDoBlock _) = "do block show not implemented"

1086 se p (PDoBlock _) = "do block show not implemented"

1085 se p (PElabError s) = show s

1087 se p (PElabError s) = show s

1086 se p (PCoerced t) = se p t

1088 se p (PCoerced t) = se p t

1089+ se p (PUnifyLog t) = "%unifyLog " ++ se p t

1087-- se p x = "Not implemented"

1090-- se p x = "Not implemented"

1088

1091

1089 slist' p (PApp _ (PRef _ nil) _)

1092 slist' p (PApp _ (PRef _ nil) _)

@@ -1150,6 +1153,7 @@ instance Sized PTerm where

1150 size (PDPair fs left ty right) = 1 + size left + size ty + size right

1153 size (PDPair fs left ty right) = 1 + size left + size ty + size right

1151 size (PAlternative a alts) = 1 + size alts

1154 size (PAlternative a alts) = 1 + size alts

1152 size (PHidden hidden) = size hidden

1155 size (PHidden hidden) = size hidden

1156+ size (PUnifyLog tm) = size tm

1153 size PType = 1

1157 size PType = 1

1154 size (PConstant const) = 1 + size const

1158 size (PConstant const) = 1 + size const

1155 size Placeholder = 1

1159 size Placeholder = 1

@@ -1184,6 +1188,7 @@ allNamesIn tm = nub $ ni [] tm

1184 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1188 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1185 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1189 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1186 ni env (PAlternative a ls) = concatMap (ni env) ls

1190 ni env (PAlternative a ls) = concatMap (ni env) ls

1191+ ni env (PUnifyLog tm) = ni env tm

1187 ni env _ = []

1192 ni env _ = []

1188

1193

1189-- Return names which are free in the given term.

1194-- Return names which are free in the given term.

@@ -1208,6 +1213,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1208 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1213 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1209 ni env (PAlternative a as) = concatMap (ni env) as

1214 ni env (PAlternative a as) = concatMap (ni env) as

1210 ni env (PHidden tm) = ni env tm

1215 ni env (PHidden tm) = ni env tm

1216+ ni env (PUnifyLog tm) = ni env tm

1211 ni env _ = []

1217 ni env _ = []

1212

1218

1213-- Return which of the given names are used in the given term.

1219-- Return which of the given names are used in the given term.

@@ -1232,4 +1238,5 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1232 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1238 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1233 ni env (PAlternative a as) = concatMap (ni env) as

1239 ni env (PAlternative a as) = concatMap (ni env) as

1234 ni env (PHidden tm) = ni env tm

1240 ni env (PHidden tm) = ni env tm

1241+ ni env (PUnifyLog tm) = ni env tm

1235 ni env _ = []

1242 ni env _ = []

src/Idris/ElabTerm.hs+6−1

@@ -95,7 +95,9 @@ buildTC ist info pattern tcgen fn tm

95elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

96 ElabD ()

97elab ist info pattern tcgen fn tm

98+ = do let loglvl = opt_logLevel (idris_options ist)

99+ when (loglvl > 5) $ unifyLog True

98− = do elabE (False, False) tm -- (in argument, guarded)

100+ elabE (False, False) tm -- (in argument, guarded)

99 end_unify

101 end_unify

100 when pattern -- convert remaining holes to pattern vars

102 when pattern -- convert remaining holes to pattern vars

101 (do update_term orderPats

103 (do update_term orderPats

@@ -464,6 +466,9 @@ elab ist info pattern tcgen fn tm

464 mkN n = case namespace info of

466 mkN n = case namespace info of

465 Just xs@(_:_) -> NS n xs

467 Just xs@(_:_) -> NS n xs

466 _ -> n

468 _ -> n

469+ elab' ina (PUnifyLog t) = do unifyLog True

470+ elab' ina t

471+ unifyLog False

467 elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

472 elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

468

473

469 caseBlock :: FC -> Name -> [(Name, Binder Term)] ->

474 caseBlock :: FC -> Name -> [(Name, Binder Term)] ->

src/Idris/Parser.hs+5

@@ -608,6 +608,7 @@ pSimpleExtExpr syn = do i <- getState

608pNoExtExpr syn =

609 try (pApp syn)

610 <|> try (pMatchApp syn)

611+ <|> try (pUnifyLog syn)

611 <|> pRecordType syn

612 <|> pRecordType syn

612 <|> try (pSimpleExpr syn)

613 <|> try (pSimpleExpr syn)

613 <|> pLambda syn

614 <|> pLambda syn

@@ -883,6 +884,10 @@ pMatchApp syn = do ty <- pSimpleExpr syn

883 (PMatchApp fc f)

884 (PMatchApp fc f)

884 (PRef fc (MN 0 "match")))

885 (PRef fc (MN 0 "match")))

885

886

887+pUnifyLog syn = do lchar '%'; reserved "unifyLog";

888+ tm <- pSimpleExpr syn

889+ return (PUnifyLog tm)

890+

886pApp syn = do f <- pSimpleExpr syn

891pApp syn = do f <- pSimpleExpr syn

887 fc <- pfc

892 fc <- pfc

888 args <- many1 (do notEndApp

893 args <- many1 (do notEndApp

src/Idris/Prover.hs+2−2

@@ -78,9 +78,9 @@ elabStep st e = do case runStateT e st of

78 fail (pshow i a)

80dumpState :: IState -> ProofState -> IO ()

81−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) =

81+dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

82 putStrLn . render $ pretty nm <> colon <+> text "No more goals."

83−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _) = do

83+dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

84 let OK ty = goalAtFocus ps

85 let OK env = envAtFocus ps

86 putStrLn . render $