packages feed

idris 0.9.3 → 0.9.3.1

raw patch · 10 files changed

+118/−55 lines, 10 files

Files

idris.cabal view
@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.3+Version:        0.9.3.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady
lib/prelude/fin.idr view
@@ -13,3 +13,7 @@      eq (fS k) (fS k') = eq k k'      eq _ _ = False +wkn : Fin n -> Fin (S n)+wkn fO = fO+wkn (fS k) = fS (wkn k)+
rts/idris_rts.h view
@@ -72,7 +72,7 @@ #define GETPTR(x) (((VAL)(x))->info.ptr)  #define GETFLOAT(x) (((VAL)(x))->info.f) -#define TAG(x) (ISINT(x) ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag : (-1)) )+#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag : (-1)) )  // Integers, floats and operators
rts/libidris_rts.a view

binary file changed (21048 → 21048 bytes)

src/IRTS/CodegenC.hs view
@@ -22,10 +22,11 @@             String -> -- output file name             Bool ->   -- generate executable if True, only .o if False              [FilePath] -> -- include files+            String -> -- extra object files              String -> -- extra compiler flags             DbgLevel ->             IO ()-codegenC defs out exec incs libs dbg+codegenC defs out exec incs objs libs dbg     = do -- print defs          let bc = map toBC defs          let h = concatMap toDecl (map fst bc)@@ -38,7 +39,9 @@          hPutStr tmph cout          hFlush tmph          hClose tmph-         let gcc = "gcc -x c " ++ +         let useclang = False+         let comp = if useclang then "clang" else "gcc"+         let gcc = comp ++ " -I. " ++ objs ++ " -x c " ++                       (if exec then "" else " - c ") ++                      gccDbg dbg ++                      " " ++ tmpn ++@@ -150,7 +153,7 @@  c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ "))" c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"-c_irts FString l x = l ++ "MKSTR(" ++ x ++ ")"+c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")" c_irts FUnit l x = x c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")" c_irts FDouble l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"
src/IRTS/Compiler.hs view
@@ -27,6 +27,9 @@                    used <- mapM (allNames []) tmnames                    defsIn <- mkDecls tm (concat used)                    maindef <- irMain tm+                   objs <- getObjectFiles+                   libs <- getLibs+                   hdrs <- getHdrs                    let defs = defsIn ++ [(MN 0 "runMain", maindef)]                    -- iputStrLn $ showSep "\n" (map show defs)                    let (nexttag, tagged) = addTags 0 (liftAll defs)@@ -36,7 +39,9 @@                    let checked = checkDefs defuns (toAlist defuns)                    case checked of                         OK c -> do -- iputStrLn $ showSep "\n" (map show c)-                                   liftIO $ codegenC c f True [] "" NONE+                                   liftIO $ codegenC c f True hdrs +                                               (concatMap mkObj objs)+                                               (concatMap mkLib libs) NONE                         Error e -> fail $ show e    where checkMVs = do i <- get                       case idris_metavars i \\ primDefs of@@ -45,6 +50,8 @@         inDir d h = do let f = d ++ "/" ++ h                        ex <- doesFileExist f                        if ex then return f else return h+        mkObj f = f ++ " "+        mkLib l = "-l" ++ l ++ " "  irMain :: TT Name -> Idris LDecl irMain tm = do i <- ir tm
src/IRTS/LParser.hs view
@@ -54,7 +54,7 @@             let checked = checkDefs defuns (toAlist defuns) --            print checked             case checked of-                 OK c -> codegenC c "a.out" True ["math.h"] "" TRACE+                 OK c -> codegenC c "a.out" True ["math.h"] "" "" TRACE                  Error e -> fail $ show e   parseFOVM :: FilePath -> IO [(Name, LDecl)]
src/Idris/AbsSyntaxTree.hs view
@@ -114,16 +114,34 @@  -- Commands in the REPL -data Command = Quit   | Help | Eval PTerm | Check PTerm | TotCheck Name-             | Reload | Edit-             | Compile String | Execute | ExecVal PTerm+data Command = Quit+             | Help+             | Eval PTerm+             | Check PTerm+             | TotCheck Name+             | Reload+             | Edit+             | Compile String+             | Execute+             | ExecVal PTerm              | NewCompile String-             | Metavars    | Prove Name | AddProof | RmProof | Proofs | Universes-             | TTShell -             | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name -             | Info Name  | DebugInfo Name+             | Metavars+             | Prove Name+             | AddProof Name+             | RmProof Name+             | ShowProof Name+             | Proofs+             | Universes+             | TTShell+             | LogLvl Int+             | Spec PTerm+             | HNF PTerm+             | Defn Name+             | Info Name+             | DebugInfo Name              | Search PTerm-             | SetOpt Opt | UnsetOpt Opt+             | SetOpt Opt+             | UnsetOpt Opt              | NOP  data Opt = Filename String
src/Idris/REPL.hs view
@@ -81,11 +81,6 @@                                    return (Just inputs)                 Right Edit -> do edit fn orig                                  return (Just inputs)-                Right AddProof -> do idrisCatch (addProof fn orig)-                                                (\e -> iputStrLn (show e))-                                     return (Just inputs)-                Right RmProof -> do rmProof orig-                                    return (Just inputs)                 Right Proofs -> do proofs orig                                    return (Just inputs)                 Right Quit -> do iputStrLn "Bye bye"@@ -94,6 +89,23 @@                                             (\e -> iputStrLn (show e))                                  return (Just inputs) +resolveProof :: Name -> Idris Name+resolveProof n'+  = do i <- get+       ctxt <- getContext+       n <- case lookupNames Nothing n' ctxt of+                 [x] -> return x+                 [] -> return n'+                 ns -> fail $ pshow i (CantResolveAlts (map show ns))+       return n++removeProof :: Name -> Idris ()+removeProof n =+  do i <- get+     let proofs = proof_list i+     let ps = filter ((/= n) . fst) proofs+     put $ i { proof_list = ps }+ edit :: FilePath -> IState -> Idris () edit "" orig = iputStrLn "Nothing to edit" edit f orig@@ -114,38 +126,14 @@                        | Just ed <- lookup "VISUAL" env = ed                        | otherwise = "vi" -addProof :: FilePath -> IState -> Idris ()-addProof "" orig = iputStrLn "Nothing to add to"-addProof f orig-    = do let fb = f ++ "~"-         liftIO $ copyFile f fb -- make a backup in case something goes wrong!-         prog <- liftIO $ readFile fb-         i <- get-         case proof_list i of-            [] -> iputStrLn "No proof to add"-            (n, p) : proofs -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)-                                  liftIO $ writeFile f (unlines prog')-                                  iputStrLn $ "Added proof " ++ show n-                                  put (i { proof_list = proofs })-                                  -- lift $ removeFile fb -- uncomment when less scared :) -rmProof :: IState -> Idris ()-rmProof orig-  = do i <- get-       case proof_list i of-            [] -> iputStrLn "Nothing to remove"-            (n, p) : ps -> do iputStrLn $ "Removed proof " ++ show n-                              let metavars = idris_metavars i-                              put (i { proof_list     = ps-                                     , idris_metavars = n : metavars-                                     })- proofs :: IState -> Idris () proofs orig   = do i <- get-       case proof_list i of-            [] -> iputStrLn "No proofs"-            ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps+       let ps = proof_list i+       case ps of+            [] -> iputStrLn "No proofs available"+            _  -> iputStrLn $ "Proofs:\n\t" ++ (show $ map fst ps)  insertScript :: String -> [String] -> [String] insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]@@ -235,19 +223,60 @@                          ist <- get                          let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm                          iputStrLn (show (delab ist tm'))-process fn (Prove n') ++process fn (RmProof n')+  = do i <- get+       n <- resolveProof n'+       let proofs = proof_list i+       case lookup n proofs of+            Nothing -> iputStrLn "No proof to remove"+            Just _  -> do removeProof n+                          insertMetavar n+                          iputStrLn $ "Removed proof " ++ show n+                          where+                            insertMetavar :: Name -> Idris ()+                            insertMetavar n =+                              do i <- get+                                 let ms = idris_metavars i+                                 put $ i { idris_metavars = n : ms }++process fn (AddProof n')+  = do let fb = fn ++ "~"+       liftIO $ copyFile fn fb -- make a backup in case something goes wrong!+       prog <- liftIO $ readFile fb+       i <- get+       n <- resolveProof n'+       let proofs = proof_list i+       case lookup n proofs of+            Nothing -> iputStrLn "No proof to add"+            Just p  -> do let prog' = insertScript (showProof (lit fn) n p) ls+                          liftIO $ writeFile fn (unlines prog')+                          removeProof n+                          iputStrLn $ "Added proof " ++ show n+                          where ls = (lines prog)++process fn (ShowProof n')+  = do i <- get+       n <- resolveProof n'+       let proofs = proof_list i+       case lookup n proofs of+            Nothing -> iputStrLn "No proof to show"+            Just p  -> iputStrLn $ showProof False n p++process fn (Prove n')      = do ctxt <- getContext           ist <- get           n <- case lookupNames Nothing n' ctxt of                     [x] -> return x                     [] -> return n'-                    ns -> fail $ pshow ist (CantResolveAlts (map show ns)) +                    ns -> fail $ pshow ist (CantResolveAlts (map show ns))           prover (lit fn) n           -- recheck totality           i <- get           totcheck (FC "(input)" 0, n)           mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)           mapM_ checkDeclTotality (idris_totcheck i)+ process fn (HNF t)  = do (tm, ty) <- elabVal toplevel False t                          ctxt <- getContext                          ist <- get@@ -354,9 +383,10 @@     ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),     ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),     ([":p",":prove"], "<name>", "Prove a metavariable"),-    ([":a",":addproof"], "", "Add last proof to source file"),-    ([":rmproof"], "", "Remove last proof from proof stack"),-    ([":proofs"], "", "Show proof stack"),+    ([":a",":addproof"], "<name>", "Add proof to source file"),+    ([":rmproof"], "<name>", "Remove proof from proof stack"),+    ([":showproof"], "<name>", "Show proof"),+    ([":proofs"], "", "Show available proofs"),     ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),     ([":exec",":execute"], "", "Compile to an executable and run"),     ([":?",":h",":help"], "", "Display this help text"),
src/Idris/REPLParser.hs view
@@ -31,8 +31,9 @@    <|> try (do cmd ["m", "metavars"]; eof; return Metavars)    <|> try (do cmd ["proofs"]; eof; return Proofs)    <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))-   <|> try (do cmd ["a", "addproof"]; eof; return AddProof)-   <|> try (do cmd ["rmproof"]; eof; return RmProof)+   <|> try (do cmd ["a", "addproof"]; n <- pName; eof; return (AddProof n))+   <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))+   <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))    <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))    <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))    <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))