Permalink
Browse files

Some preparing for writing out files as raw TT, other tweaks

darcs-hash:20060519221833-974a0-f1d775cb448092491b93d96bb2ca3b104849b41b.gz
  • Loading branch information...
1 parent 4a53940 commit 5c7172d2d2765dabb87593f3520da0e3560e334b eb committed May 19, 2006
Showing with 44 additions and 19 deletions.
  1. +4 −2 Ivor/Datatype.lhs
  2. +1 −1 Ivor/MakeData.lhs
  3. +1 −1 Ivor/Nobby.lhs
  4. +1 −2 Ivor/Primitives.lhs
  5. +4 −2 Ivor/Shell.lhs
  6. +18 −1 Ivor/State.lhs
  7. +1 −1 Ivor/TT.lhs
  8. +6 −0 TODO
  9. +4 −6 docs/HCAR.tex
  10. +3 −2 ivor.cabal
  11. +1 −1 release/Release.lhs
View
6 Ivor/Datatype.lhs
@@ -21,6 +21,7 @@ Elaborated version with elimination rule and iota schemes.
> data RawDatatype =
> RData { rtycon :: (Name,Raw),
> rdatacons :: [(Name,Raw)],
+> rnum_params :: Int,
> rerule :: (Name,Raw),
> rcrule :: (Name,Raw),
> re_ischemes :: [RawScheme],
@@ -34,6 +35,7 @@ Elaborated version with elimination rule and iota schemes.
> data Datatype n =
> Data { tycon :: (n, Gval n),
> datacons :: [(n, Gval n)],
+> num_params :: Int,
> erule :: (n, Indexed n),
> crule :: (n, Indexed n),
> e_ischemes :: [Scheme n],
@@ -56,7 +58,7 @@ schemes, and returns a DataType, ready for compilation to entries in
the context and an executable elimination rule.
> checkType :: Monad m => Gamma Name -> RawDatatype -> m (Datatype Name)
-> checkType gamma (RData (ty,kind) cons (er,erty) (cr,crty) eschemes cschemes) =
+> checkType gamma (RData (ty,kind) cons numps (er,erty) (cr,crty) eschemes cschemes) =
> do (kv, _) <- typecheck gamma kind
> let erdata = Elims er cr
> let gamma' = extend gamma (ty,G (TCon (arity gamma kv) erdata) kv)
@@ -66,7 +68,7 @@ the context and an executable elimination rule.
> let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev)
> esch <- checkSchemes gamma''' er eschemes
> csch <- checkSchemes gamma''' er cschemes
-> return (Data (ty,G (TCon (arity gamma kv) erdata) kv) consv
+> return (Data (ty,G (TCon (arity gamma kv) erdata) kv) consv numps
> (er,ev) (cr,cv) esch csch)
> where checkCons gamma t [] = return ([], gamma)
View
2 Ivor/MakeData.lhs
@@ -30,7 +30,7 @@ the target, methods and the motives are unique.
> params datacons motiveName methNames
> tycontype = mkCon params contype in
> return $ --(trace (show ischemes)) $
-> RData (name,tycontype) datacons
+> RData (name,tycontype) datacons (length params)
> (ruleName name "Elim", ecasetype) -- elim rule
> (ruleName name "Case", ccasetype) -- case rule
> eischemes -- elim rule iota schemes
View
2 Ivor/Nobby.lhs
@@ -1,6 +1,6 @@
> {-# OPTIONS_GHC -fglasgow-exts #-}
-> module Ivor.Nobby where {- *chortle* -}
+> module Ivor.Nobby where
> import Ivor.TTCore
> import Ivor.Gadgets
View
3 Ivor/Primitives.lhs
@@ -110,8 +110,7 @@
> return $ Constant x
> parseInt :: Parser Int
-> parseInt = lexeme $ do inttok <- many1 digit
-> return $ read inttok
+> parseInt = lexeme $ fmap read (many1 digit)
> -- | Parse a term including primitives
> parsePrimTerm :: Monad m => String -> m ViewTerm
View
6 Ivor/Shell.lhs
@@ -22,7 +22,7 @@
> import Ivor.TT as TT
> import Ivor.Gadgets
> import Ivor.Primitives
-> import Ivor.Plugin
+> -- import Ivor.Plugin
> import IO
> import System
@@ -235,12 +235,14 @@ function which doesn't need to be in the IO Monad.
> process (Failure err) st = return $ respondLn st err
> process (Success (Command (Load f))) st = do importFile f st
> process (Success (Command (Plugin f))) st = do
+> fail "Plugins currently unsupported"
+> {-
> (ctxt, exts) <- load f (context st)
> let st' = st { context = ctxt }
> let st'' = case exts of
> Nothing -> st'
> Just p -> extendParser st' p
-> return st''
+> return st'' -}
> process (Success (Command (Compile f))) st = do compile (context st) f
> putStrLn $ "Output " ++ f ++ ".hs"
> return st
View
19 Ivor/State.lhs
@@ -26,19 +26,32 @@ State of the system, include all definitions, pattern matching rules,
compiled terms, etc.
> data IState = ISt {
+> -- All definitions
> defs :: !(Gamma Name),
+> -- All datatype definitions
> datadefs :: [(Name,Datatype Name)],
+> -- All elimination rules in their pattern matching form
+> -- (with type)
+> eliminators :: [(Name, (Indexed Name, [Scheme Name]))],
+> -- Supercombinators for each definition
> runtt :: SCs,
+> -- Bytecode for each definitions
> bcdefs :: ByteDef,
+> -- List of holes to be solved in proof state
> holequeue :: ![Name],
+> -- Current proof term (FIXME: Combine with holequeue, and make it efficient)
> proofstate :: !(Maybe (Indexed Name)),
+> -- Actions required of last tactic
> actions :: ![TacticAction],
+> -- List of fresh names for tactics to use
> namesupply :: [Name],
+> -- Output from last operation
> response :: String,
+> -- Previous state
> undoState :: !(Maybe IState)
> }
-> initstate = ISt (Gam []) [] [] [] [] Nothing [] mknames "" Nothing
+> initstate = ISt (Gam []) [] [] [] [] [] Nothing [] mknames "" Nothing
> where mknames = [MN ("myName",x) | x <- [1..]]
> respond :: IState -> String -> IState
@@ -74,8 +87,12 @@ Take a data type definition and add constructors and elim rule to the context.
> addElim ctxt runtts bcs (erule dt) (e_ischemes dt)
> (newdefs, newruntts, newbc) <-
> addElim ctxt newruntts newbc (crule dt) (c_ischemes dt)
+> let newelims = (fst (erule dt), (snd (erule dt), e_ischemes dt)):
+> (fst (crule dt), (snd (crule dt), c_ischemes dt)):
+> eliminators st
> let newdatadefs = (n,dt):(datadefs st)
> return $ st { defs = newdefs, datadefs = newdatadefs,
+> eliminators = newelims,
> bcdefs = newbc, runtt = newruntts }
> where addCons [] ctxt = return ctxt
> addCons ((n,gl):xs) ctxt = do
View
2 Ivor/TT.lhs
@@ -272,7 +272,7 @@
> rerule <- eqElimType (show ty) (show con) "Elim"
> rcrule <- eqElimType (show ty) (show con) "Case"
> rischeme <- eqElimSch (show con)
-> let rdata = (RData rtycon [rdatacon] rerule rcrule [rischeme] [rischeme])
+> let rdata = (RData rtycon [rdatacon] 2 rerule rcrule [rischeme] [rischeme])
> st <- doData st ty rdata
> return $ Ctxt st
View
6 TODO
@@ -1,6 +1,12 @@
Short term things to do:
+* Current naive proof state representation is far too slow. Come up
+ with something better.
+* API shouldn't really need to require use of attack/solve except in
+ specialised cases (e.g. fine control over refinement). Change it so
+ that shell and api are more or less consistent.
* Keep track of level in proof state.
+* Allow dump of global context to disk, for fast reloading.
* Syntax for equality.
* Elimination with a motive.
* Unit tests - at least check nat.tt, vect.tt, JM equality,
View
10 docs/HCAR.tex
@@ -5,14 +5,12 @@
\begin{document}
-\newcommand{\Libname}{Ivor}
-
-\begin{hcarentry}{\Libname{}}
+\begin{hcarentry}{Ivor}
\report{Edwin Brady}
\status{Active Development}
\makeheader
-\Libname{} is a tactic-based theorem proving engine with a Haskell API. Unlike
+Ivor is a tactic-based theorem proving engine with a Haskell API. Unlike
other systems such as Coq and Agda, the tactic engine is primarily
intended to be used by programs, rather than a human operator. To this
end, the API provides a collection of primitive tactics and
@@ -24,7 +22,7 @@
programming and resource bounded computation in Hume
(\url{http://www.hume-lang.org/}). In this setting, we have developed a
dependently typed framework for representing program execution cost,
-and used the \Libname{} library to implement domain specific tactics for
+and used the Ivor library to implement domain specific tactics for
constructing programs within this framework. However the library is
more widely applicable, some potential uses being:
@@ -37,7 +35,7 @@
strong correctness properties.
\end{itemize}
-\Libname{} features a dependent type theory similar to Luo's ECC with
+Ivor features a dependent type theory similar to Luo's ECC with
definitions, with additional (experimental) multi-stage programming
support. Optionally, it can be extended with heterogenous equality,
primitive types and operations, new parser rules and user defined
View
5 ivor.cabal
@@ -6,13 +6,14 @@ License-file: LICENSE
Maintainer: eb@dcs.st-and.ac.uk
Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/
Stability: experimental
-Build-depends: base, haskell98, util, parsec, mtl, plugins, Cabal
+Build-depends: base, haskell98, util, parsec, mtl, Cabal
Extensions: MultiParamTypeClasses, FunctionalDependencies,
ExistentialQuantification, OverlappingInstances
+ghc-prof-options: -auto-all
Synopsis: Theorem proving library based on dependent type theory
Exposed-modules:
Ivor.TT, Ivor.Shell, Ivor.Primitives,
- Ivor.TermParser, Ivor.ViewTerm, Ivor.Plugin
+ Ivor.TermParser, Ivor.ViewTerm
Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State,
Ivor.Tactics, Ivor.Typecheck,
Ivor.Gadgets, Ivor.SC, Ivor.Bytecode,
View
2 release/Release.lhs
@@ -45,7 +45,7 @@ and upload it.
> setCurrentDirectory ".."
> shell $ "gpg -b " ++ rootname ++ ".tgz"
> shell $ "gpg -b " ++ rootname ++ "/Jones/jones"
-> shell $ "scp "++rootname++".tgz " ++ rootname ++"/Jones/jones "
+> shell $ "scp "++rootname++".tgz " -- ++ rootname ++"/Jones/jones "
> ++rootname++".tgz.sig " ++ rootname ++ "/Jones/jones.sig " ++ dest
> shell $ "scp "++rootname++"/dist/doc/html/* "++dest++"doc"
> shell $ "rm -rf " ++ rootname

0 comments on commit 5c7172d

Please sign in to comment.