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

git.iko.soy/Idris-dev

Added %unifyLog construct

For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the trace

commit9c1175445116f4b524ebf70518aedc585ccf8b5b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Jun 2013, 14:56 (13 years ago) parentce7e45b

7 files changed+46−15

compare with master

unifiedsplit

src/Core/Elaborate.hs+4 src/Core/ProofState.hs+15−12 src/Idris/AbsSyntax.hs+7 src/Idris/AbsSyntaxTree.hs+7 src/Idris/ElabTerm.hs+6−1 src/Idris/Parser.hs+5 src/Idris/Prover.hs+2−2

src/Core/Elaborate.hs+4

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

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

9292 return a

9393

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+

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

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

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

src/Core/ProofState.hs+15−12

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

3737 previous :: Maybe ProofState, -- for undo

3838 context :: Context,

3939 plog :: String,

40+ unifylog :: Bool,

4041 done :: Bool

4142 }

4243

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

8182-- Some utilites on proof and tactic states

8283

8384instance Show ProofState where

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

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

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

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

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

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

8789 wkenv = premises g in

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

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

105107 showG ps b = showEnv ps (binderTy b)

106108

107109instance Pretty ProofState where

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

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

109111 if size nm > breakingSize then

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

111113 else

112114 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 _ _ _) =

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

115117 let wkEnv = premises g in

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

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

172174 let dont = dontunify ps

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

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

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

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

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

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

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

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

181− case fails of

177+ traceWhen (unifylog ps)

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

179+ " in " ++ show env ++

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

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

182+-- ++ show (pterm ps)

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

184+ case fails of

182185-- [] -> return u

183186 err ->

184187 do ps <- get

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

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

212215 Nothing [] []

213216 [] []

214− Nothing ctxt "" False

217+ Nothing ctxt "" False False

215218

216219type TState = ProofState -- [TacticAction])

217220type 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

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

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

571571 en (PHidden t) = PHidden (en t)

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

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

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

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

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

883884 = do imps False env ty

884885 imps False (n:env) sc

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

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

886888 imps top env _ = return ()

887889

888890 pibind using [] sc = sc

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

966968 ai env (PHidden tm) = PHidden (ai env tm)

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

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

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

969972 ai env tm = tm

970973

971974 handleErr (Left err) = PElabError err

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

12281231 ms <- match' s s'

12291232 return (mt ++ mty ++ ms)

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

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

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

12311236 match Placeholder _ = return []

12321237 match _ Placeholder = return []

12331238 match (PResolveTC _) _ = return []

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

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

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

12751280 sm xs (PHidden x) = PHidden (sm xs x)

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

12761282 sm xs x = x

12771283

12781284shadow :: Name -> Name -> PTerm -> PTerm

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

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

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

12911297 sm (PHidden x) = PHidden (sm x)

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

12921299 sm x = x

12931300

12941301

src/Idris/AbsSyntaxTree.hs+7

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

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

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

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

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

520521 deriving Eq

521522{-!

522523deriving instance Binary PTerm

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

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

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

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

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

542544 mpt x = x

543545

544546

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

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

10851087 se p (PElabError s) = show s

10861088 se p (PCoerced t) = se p t

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

10871090-- se p x = "Not implemented"

10881091

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

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

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

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

11521155 size (PHidden hidden) = size hidden

1156+ size (PUnifyLog tm) = size tm

11531157 size PType = 1

11541158 size (PConstant const) = 1 + size const

11551159 size Placeholder = 1

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

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

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

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

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

11871192 ni env _ = []

11881193

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

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

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

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

12101215 ni env (PHidden tm) = ni env tm

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

12111217 ni env _ = []

12121218

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

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

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

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

12341240 ni env (PHidden tm) = ni env tm

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

12351242 ni env _ = []

src/Idris/ElabTerm.hs+6−1

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

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

9696 ElabD ()

9797elab ist info pattern tcgen fn tm

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

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

99+ when (loglvl > 5) $ unifyLog True

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

99101 end_unify

100102 when pattern -- convert remaining holes to pattern vars

101103 (do update_term orderPats

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

464466 mkN n = case namespace info of

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

466468 _ -> n

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

470+ elab' ina t

471+ unifyLog False

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

468473

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

src/Idris/Parser.hs+5

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

608608pNoExtExpr syn =

609609 try (pApp syn)

610610 <|> try (pMatchApp syn)

611+ <|> try (pUnifyLog syn)

611612 <|> pRecordType syn

612613 <|> try (pSimpleExpr syn)

613614 <|> pLambda syn

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

883884 (PMatchApp fc f)

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

885886

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

888+ tm <- pSimpleExpr syn

889+ return (PUnifyLog tm)

890+

886891pApp syn = do f <- pSimpleExpr syn

887892 fc <- pfc

888893 args <- many1 (do notEndApp

src/Idris/Prover.hs+2−2

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

7878 fail (pshow i a)

7979

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

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

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

8282 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

8484 let OK ty = goalAtFocus ps

8585 let OK env = envAtFocus ps

8686 putStrLn . render $