3191f16 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Induction works for all types with eliminators now (some eliminators

3191f16Ahmad Salim Al-Sibahi13 years ago

src/Idris/Core/Elaborate.hs+1−7

compare with master

unifiedsplit

@@ -209,7 +209,7 @@ unique_hole' reusable n

209 = do ES p _ _ <- get

210 let bs = bound_in (pterm (fst p)) ++

211 bound_in (ptype (fst p))

212− n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p)

212+ n' <- return $ uniqueNameCtxt (context (fst p)) n (holes (fst p)

213 ++ bs ++ dontunify (fst p) ++ usedns (fst p))

214 ES (p, a) s u <- get

215 -- Hmm: Do we need this level of uniqueness?

@@ -225,12 +225,6 @@ unique_hole' reusable n

225 bound_in (App f a) = bound_in f ++ bound_in a

226 bound_in _ = []

227

228−uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name

229−uniqueNameCtxt ctxt n hs

230− | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

231− | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

232− | otherwise = return n

233−

234elog :: String -> Elab' aux ()

228elog :: String -> Elab' aux ()

235elog str = do ES p logs prev <- get

229elog str = do ES p logs prev <- get

236 put (ES p (logs ++ str ++ "\n") prev)

230 put (ES p (logs ++ str ++ "\n") prev)

src/Idris/Core/Evaluate.hs+7−1

@@ -10,7 +10,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

12 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

13− Value(..), Quote(..), initEval) where

13+ Value(..), Quote(..), initEval, uniqueNameCtxt) where

15import Debug.Trace

16import Control.Monad.State

@@ -913,3 +913,9 @@ lookupTyEnv n env = li n 0 env where

913 | n == x = Just (i, binderTy b)

914 | otherwise = li n (i+1) xs

915

916+-- | Create a unique name given context and other existing names

917+uniqueNameCtxt :: Context -> Name -> [Name] -> Name

918+uniqueNameCtxt ctxt n hs

919+ | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

920+ | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

921+ | otherwise = n

src/Idris/Core/ProofState.hs+10−4

@@ -611,15 +611,17 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

611 _ -> return []

612 let (params, indicies) = splitTyArgs param_pos tyargs

613 let args = getArgTys elimTy

614− let pmargs = take (length tyargs) args

614+ let pmargs = take (length params) args

615− let args' = drop (length tyargs) args

615+ let args' = drop (length params) args

616 let propTy = head args'

617 let restargs = init $ tail args'

618 let consargs = take (length restargs - length indicies) $ restargs

619 let indxargs = drop (length restargs - length indicies) $ restargs

620 let scr = last $ tail args'

621− let prop = Bind nm (Lam tmt') t -- TODO: Make this work for types with indicies

621+ let indxnames = makeIndexNames indicies

622+ prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t

622− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0))) (params ++ [prop] ++ map makeConsArg consargs ++ [tmv])))

623+ let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))

624+ (params ++ [prop] ++ map makeConsArg consargs ++ indicies ++ [tmv])))

623 action (\ps -> ps {holes = holes ps \\ [x]})

625 action (\ps -> ps {holes = holes ps \\ [x]})

624 mapM_ addConsHole (reverse consargs)

626 mapM_ addConsHole (reverse consargs)

625 let res' = forget $ res

627 let res' = forget $ res

@@ -638,6 +640,10 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

638 splitTyArgs param_pos tyargs =

640 splitTyArgs param_pos tyargs =

639 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs

641 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs

640 in (map snd params, map snd indicies)

642 in (map snd params, map snd indicies)

643+ makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (MN 0 "idx") nms):nms) []

644+ replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

645+ let var = P Bound idnm idxt

646+ return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

641induction tm ctxt env _ = do fail "Can't do induction here"

647induction tm ctxt env _ = do fail "Can't do induction here"

642

648

643

649