d7f4e11 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Induction now works on types with parameters

commitd7f4e110bf7f81d9f0dc0c0c1e3490899030f547 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSun 5 Jan 2014, 17:29 (13 years ago) parent7e2c212

7 files changed+94−82

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/Evaluate.hs+44−28 src/Idris/Core/ProofState.hs+18−9 src/Idris/Core/TT.hs−15 src/Idris/Core/Typecheck.hs−25 src/Idris/ElabDecls.hs+3 src/Idris/IBC.hs+28−5

src/Idris/AbsSyntaxTree.hs+1

@@ -177,6 +177,7 @@ data IBCWrite = IBCFix FixDecl

177177 | IBCDyLib String

178178 | IBCHeader Codegen String

179179 | IBCAccess Name Accessibility

180+ | IBCMetaInformation Name MetaInformation

180181 | IBCTotal Name Totality

181182 | IBCFlags Name [FnOpt]

182183 | IBCTrans (Term, Term)

src/Idris/Core/Evaluate.hs+44−28

@@ -4,12 +4,12 @@

44module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

55 rt_simplify, simplify, specialise, hnf, convEq, convEq',

66 Def(..), CaseInfo(..), CaseDefs(..),

7− Accessibility(..), Totality(..), PReason(..),

7+ Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9− addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

9+ addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

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

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

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

1313 Value(..), Quote(..), initEval) where

1414

1515import Debug.Trace

@@ -678,12 +678,18 @@ deriving instance Binary Totality

678678deriving instance Binary PReason

679679!-}

680680

681+-- Possible attached meta-information for a definition in context

682+data MetaInformation =

683+ EmptyMI -- ^ No meta-information

684+ | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters

685+ deriving (Eq, Show)

686+

681687-- | Contexts used for global definitions and for proof state. They contain

682688-- universe constraints and existing definitions.

683689data Context = MkContext {

684− uconstraints :: [UConstraint],

685− next_tvar :: Int,

686− definitions :: Ctxt (Def, Accessibility, Totality)

690+ uconstraints :: [UConstraint],

691+ next_tvar :: Int,

692+ definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)

687693 } deriving Show

688694

689695-- | The initial empty context

@@ -691,37 +697,43 @@ initContext = MkContext [] 0 emptyContext

691697

692698-- | Get the definitions from a context

693699ctxtAlist :: Context -> [(Name, Def)]

694−ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

700+ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

695701

696702veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

697703

698704addToCtxt :: Name -> Term -> Type -> Context -> Context

699705addToCtxt n tm ty uctxt

700706 = let ctxt = definitions uctxt

701− ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in

707+ ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in

702708 uctxt { definitions = ctxt' }

703709

704710setAccess :: Name -> Accessibility -> Context -> Context

705711setAccess n a uctxt

706712 = let ctxt = definitions uctxt

707− ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in

713+ ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in

708714 uctxt { definitions = ctxt' }

709715

710716setTotal :: Name -> Totality -> Context -> Context

711717setTotal n t uctxt

712718 = let ctxt = definitions uctxt

713− ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in

719+ ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in

720+ uctxt { definitions = ctxt' }

721+

722+setMetaInformation :: Name -> MetaInformation -> Context -> Context

723+setMetaInformation n m uctxt

724+ = let ctxt = definitions uctxt

725+ ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in

714726 uctxt { definitions = ctxt' }

715727

716728addCtxtDef :: Name -> Def -> Context -> Context

717729addCtxtDef n d c = let ctxt = definitions c

718− ctxt' = addDef n (d, Public, Unchecked) $! ctxt in

730+ ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in

719731 c { definitions = ctxt' }

720732

721733addTyDecl :: Name -> NameType -> Type -> Context -> Context

722734addTyDecl n nt ty uctxt

723735 = let ctxt = definitions uctxt

724− ctxt' = addDef n (TyDecl nt ty, Public, Unchecked) ctxt in

736+ ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in

725737 uctxt { definitions = ctxt' }

726738

727739addDatatype :: Datatype Name -> Context -> Context

@@ -729,14 +741,14 @@ addDatatype (Data n tag ty cons) uctxt

729741 = let ctxt = definitions uctxt

730742 ty' = normalise uctxt [] ty

731743 ctxt' = addCons 0 cons (addDef n

732− (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in

744+ (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in

733745 uctxt { definitions = ctxt' }

734746 where

735747 addCons tag [] ctxt = ctxt

736748 addCons tag ((n, ty) : cons) ctxt

737749 = let ty' = normalise uctxt [] ty in

738750 addCons (tag+1) cons (addDef n

739− (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)

751+ (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt)

740752

741753-- FIXME: Too many arguments! Refactor all these Bools.

742754addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

@@ -770,7 +782,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

770782 (args_rt, sc_rt) in

771783 addDef n (CaseOp (ci { case_inlinable = inlc })

772784 ty ps_in ps_tot cdef,

773− access, Unchecked) ctxt in

785+ access, Unchecked, EmptyMI) ctxt in

774786 uctxt { definitions = ctxt' }

775787

776788-- simplify a definition for totality checking

@@ -778,16 +790,16 @@ simplifyCasedef :: Name -> Context -> Context

778790simplifyCasedef n uctxt

779791 = let ctxt = definitions uctxt

780792 ctxt' = case lookupCtxt n ctxt of

781− [(CaseOp ci ty [] ps _, acc, tot)] ->

793+ [(CaseOp ci ty [] ps _, acc, tot, metainf)] ->

782794 ctxt -- nothing to simplify (or already done...)

783− [(CaseOp ci ty ps_in ps cd, acc, tot)] ->

795+ [(CaseOp ci ty ps_in ps cd, acc, tot, metainf)] ->

784796 let ps_in' = map simpl ps_in

785797 pdef = map debind ps_in' in

786798 case simpleCase False True False CompileTime emptyFC pdef of

787799 OK (CaseDef args sc _) ->

788800 addDef n (CaseOp ci

789801 ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

790− acc, tot) ctxt

802+ acc, tot, metainf) ctxt

791803 Error err -> error (show err)

792804 _ -> ctxt in

793805 uctxt { definitions = ctxt' }

@@ -807,10 +819,10 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

807819 Context -> Context

808820addOperator n ty a op uctxt

809821 = let ctxt = definitions uctxt

810− ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in

822+ ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in

811823 uctxt { definitions = ctxt' }

812824

813−tfst (a, _, _) = a

825+tfst (a, _, _, _) = a

814826

815827lookupNames :: Name -> Context -> [Name]

816828lookupNames n ctxt

@@ -856,10 +868,10 @@ lookupP :: Name -> Context -> [Term]

856868lookupP n ctxt

857869 = do def <- lookupCtxt n (definitions ctxt)

858870 p <- case def of

859− (Function ty tm, a, _) -> return (P Ref n ty, a)

860− (TyDecl nt ty, a, _) -> return (P nt n ty, a)

861− (CaseOp _ ty _ _ _, a, _) -> return (P Ref n ty, a)

862− (Operator ty _ _, a, _) -> return (P Ref n ty, a)

871+ (Function ty tm, a, _, _) -> return (P Ref n ty, a)

872+ (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

873+ (CaseOp _ ty _ _ _, a, _, _) -> return (P Ref n ty, a)

874+ (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

863875 case snd p of

864876 Hidden -> []

865877 _ -> return (fst p)

@@ -872,15 +884,19 @@ lookupDefAcc :: Name -> Bool -> Context ->

872884lookupDefAcc n mkpublic ctxt

873885 = map mkp $ lookupCtxt n (definitions ctxt)

874886 -- io_bind a special case for REPL prettiness

875− where mkp (d, a, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))

876− then (d, Public) else (d, a)

887+ where mkp (d, a, _, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))

888+ then (d, Public) else (d, a)

877889

878890lookupTotal :: Name -> Context -> [Totality]

879891lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

880− where mkt (d, a, t) = t

892+ where mkt (d, a, t, m) = t

893+

894+lookupMetaInformation :: Name -> Context -> [MetaInformation]

895+lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

896+ where mkm (d, a, t, m) = m

881897

882898lookupNameTotal :: Name -> Context -> [(Name, Totality)]

883−lookupNameTotal n = map (\(n, (_, _, t)) -> (n, t)) . lookupCtxtName n . definitions

899+lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

884900

885901

886902lookupVal :: Name -> Context -> [Value]

src/Idris/Core/ProofState.hs+18−9

@@ -602,26 +602,32 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

602602 (tmv, tmt) <- lift $ check ctxt env (Var nm)

603603 let tmt' = normalise ctxt env tmt

604604 case unApply tmt' of

605− (P _ tnm _, pms@[]) -> do

605+ (P _ tnm _, tyargs) -> do

606606 case lookupTy (SN (ElimN tnm)) ctxt of

607607 [elimTy] -> do

608+ param_pos <- case lookupMetaInformation tnm ctxt of

609+ [DataMI param_pos] -> return param_pos

610+ m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)

611+ _ -> return []

612+ let (params, indicies) = splitTyArgs param_pos tyargs

608613 let args = getArgTys elimTy

609− let pmargs = take (length pms) args -- TODO: Fill these correctly when having multiple parameters working

610− let args' = drop (length pms) args

614+ let pmargs = take (length tyargs) args

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

611616 let propTy = head args'

612− let consargs = init $ tail args -- TODO: This is incorrect when type has indicies, get indicies and use the correct count

613− let scr = last $ tail 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'

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

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

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

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

617624 mapM_ addConsHole (reverse consargs)

618625 let res' = forget $ res

619626 (scv, sct) <- lift $ check ctxt env res'

620627 let scv' = specialise ctxt env [] scv

621628 return scv'

622− [] -> fail $ "Induction needs an eliminator for " ++ show nm

623− xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show nm

624− (P _ nm _, _) -> fail "Induction not yet supported for types with arguments"

629+ [] -> fail $ "Induction needs an eliminator for " ++ show tnm

630+ xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show tnm

625631 _ -> fail "Unkown type for induction"

626632 where scname = MN 0 "scarg"

627633 makeConsArg (nm, ty) = P Bound nm ty

@@ -629,6 +635,9 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

629635 bindConsArgs [] v = v

630636 addConsHole (nm, ty) =

631637 action (\ps -> ps { holes = nm : holes ps })

638+ splitTyArgs param_pos tyargs =

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

640+ in (map snd params, map snd indicies)

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

633642

634643

src/Idris/Core/TT.hs−15

@@ -515,21 +515,6 @@ raw_unapply t = ua [] t where

515515 ua args (RApp f a) = ua (a:args) f

516516 ua args t = (t, args)

517517

518−data RawFun = RawFun { rtype :: Raw,

519− rval :: Raw

520− }

521− deriving Show

522−

523−data RawDatatype = RDatatype Name Raw [(Name, Raw)]

524− deriving Show

525−

526−data RDef = RFunction RawFun

527− | RConst Raw

528− | RData RawDatatype

529− deriving Show

530−

531−type RProgram = [(Name, RDef)]

532−

533518-- WELL TYPED TERMS ---------------------------------------------------------

534519

535520-- | Universe expressions for universe checking

src/Idris/Core/Typecheck.hs−25

@@ -214,28 +214,3 @@ check' holes ctxt env top = chk env top where

214214 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

215215 discharge n (PVTy t) scv sct

216216 = return (Bind n (PVTy t) scv, sct)

217−

218−

219−checkProgram :: Context -> RProgram -> TC Context

220−checkProgram ctxt [] = return ctxt

221−checkProgram ctxt ((n, RConst t) : xs)

222− = do (t', tt') <- trace (show n) $ check ctxt [] t

223− isType ctxt [] tt'

224− checkProgram (addTyDecl n Ref t' ctxt) xs

225−checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

226− = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

227− (val', valt') <- check ctxt [] val

228− isType ctxt [] tyt'

229− converts ctxt [] ty' valt'

230− checkProgram (addToCtxt n val' ty' ctxt) xs

231−checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)

232− = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

233− isType ctxt [] tyt'

234− -- add the tycon temporarily so we can check constructors

235− let ctxt' = addDatatype (Data n 0 ty' []) ctxt

236− cons' <- mapM (checkCon ctxt') cons

237− checkProgram (addDatatype (Data n 0 ty' cons') ctxt) xs

238− where checkCon ctxt (n, cty) = do (cty', ctyt') <- check ctxt [] cty

239− return (n, cty')

240−

241−

src/Idris/ElabDecls.hs+3

@@ -202,8 +202,11 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

202202 addIBC (IBCData n)

203203 addDocStr n doc

204204 addIBC (IBCDoc n)

205+ let metainf = DataMI params

206+ addIBC (IBCMetaInformation n metainf)

205207 collapseCons n cons

206208 updateContext (addDatatype (Data n ttag cty cons))

209+ updateContext (setMetaInformation n metainf)

207210 mapM_ (checkPositive n) cons

208211 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

209212 else return ()

src/Idris/IBC.hs+28−5

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 48

26+ibcVersion = 49

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -52,7 +52,8 @@ data IBCFile = IBCFile { ver :: Word8,

5252 ibc_transforms :: [(Term, Term)],

5353 ibc_coercions :: [Name],

5454 ibc_lineapps :: [(FilePath, Int, PTerm)],

55− ibc_namehints :: [(Name, Name)]

55+ ibc_namehints :: [(Name, Name)],

56+ ibc_metainformation :: [(Name, MetaInformation)]

5657 }

5758 deriving Show

5859{-!

@@ -60,7 +61,7 @@ deriving instance Binary IBCFile

6061!-}

6162

6263initIBC :: IBCFile

63−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

64+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

6465

6566loadIBC :: FilePath -> Idris ()

6667loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -140,6 +141,7 @@ ibc i (IBCLineApp fp l t) f

140141 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

141142ibc i (IBCNameHint (n, ty)) f

142143 = return f { ibc_namehints = (n, ty) : ibc_namehints f }

144+ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_metainformation f }

143145

144146process :: IBCFile -> FilePath -> Idris ()

145147process i fn

@@ -176,6 +178,7 @@ process i fn

176178 pTrans (ibc_transforms i)

177179 pLineApps (ibc_lineapps i)

178180 pNameHints (ibc_namehints i)

181+ pMetaInformation (ibc_metainformation i)

179182

180183timestampOlder :: FilePath -> FilePath -> IO ()

181184timestampOlder src ibc = do srct <- getModificationTime src

@@ -326,6 +329,12 @@ pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

326329pNameHints :: [(Name, Name)] -> Idris ()

327330pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

328331

332+pMetaInformation :: [(Name, MetaInformation)] -> Idris ()

333+pMetaInformation ds = mapM_ (\ (n, m) ->

334+ do i <- getIState

335+ putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))

336+ ds

337+

329338----- Generated by 'derive'

330339

331340instance Binary SizeChange where

@@ -890,8 +899,20 @@ instance Binary Totality where

890899 3 -> return Productive

891900 _ -> error "Corrupted binary data for Totality"

892901

902+instance Binary MetaInformation where

903+ put x

904+ = case x of

905+ EmptyMI -> do putWord8 0

906+ DataMI x1 -> do putWord8 1

907+ put x1

908+ get = do i <- getWord8

909+ case i of

910+ 0 -> return EmptyMI

911+ 1 -> do x1 <- get

912+ return (DataMI x1)

913+

893914instance Binary IBCFile where

894− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)

915+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29)

895916 = {-# SCC "putIBCFile" #-}

896917 do put x1

897918 put x2

@@ -921,6 +942,7 @@ instance Binary IBCFile where

921942 put x26

922943 put x27

923944 put x28

945+ put x29

924946 get

925947 = do x1 <- get

926948 if x1 == ibcVersion then

@@ -951,7 +973,8 @@ instance Binary IBCFile where

951973 x26 <- get

952974 x27 <- get

953975 x28 <- get

954− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)

976+ x29 <- get

977+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29)

955978 else return (initIBC { ver = x1 })

956979

957980instance Binary DataOpt where