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

git.iko.soy/Idris-dev

Induction works for all types with eliminators now (some eliminators

still need fixing) including those with indicies.

commit3191f16f6724941522f0526d0ff9ddf54f34b4b0 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSun 5 Jan 2014, 19:41 (13 years ago) parentd7f4e11

3 files changed+18−12

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+1−7 src/Idris/Core/Evaluate.hs+7−1 src/Idris/Core/ProofState.hs+10−4

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

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

209209 = do ES p _ _ <- get

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

211211 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)

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

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

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

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

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

226226 bound_in _ = []

227227

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−

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

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

236230 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,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

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

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

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

1414

1515import Debug.Trace

1616import Control.Monad.State

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

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

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

915915

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

611611 _ -> return []

612612 let (params, indicies) = splitTyArgs param_pos tyargs

613613 let args = getArgTys elimTy

614− let pmargs = take (length tyargs) args

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

614+ let pmargs = take (length params) args

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

616616 let propTy = head args'

617617 let restargs = init $ tail args'

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

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

620620 let scr = last $ tail args'

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

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])))

621+ let indxnames = makeIndexNames indicies

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

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])))

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

624626 mapM_ addConsHole (reverse consargs)

625627 let res' = forget $ res

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

638640 splitTyArgs param_pos tyargs =

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

640642 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

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

642648

643649