Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
  • 12 commits
  • 6 files changed
  • 0 comments
  • 1 contributor
Apr 04, 2012
Edward Z. Yang Coq parsing code
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
a3d5619
Edward Z. Yang A more efficient, but harder to read version of the parser.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
47f87b6
Edward Z. Yang Some more Haskell in progress.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
8304c7e
Edward Z. Yang Actually parse.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
4f562ef
Apr 05, 2012
Edward Z. Yang Transform into DSL first-order logic
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
9a4b3fb
Apr 09, 2012
Edward Z. Yang CoqTop interaction.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
7b9e773
Apr 12, 2012
Edward Z. Yang Lots of updates yo.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
aff13c6
Edward Z. Yang Start developing recursion.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
38029c7
Apr 13, 2012
Edward Z. Yang Minor mods.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
6e18e59
Edward Z. Yang Writing the fold functions will be bitchy.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
7dacee4
Edward Z. Yang Add proofComplete, update things.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
67f0101
Edward Z. Yang Build out some of the more boring stuff.
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
67aefc7
327 ClassicalFOL.hs
... ... @@ -0,0 +1,327 @@
  1 +{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures, ExistentialQuantification, ScopedTypeVariables, DeriveDataTypeable, DeriveFunctor, NoMonomorphismRestriction #-}
  2 +
  3 +module ClassicalFOL where
  4 +
  5 +import qualified Coq as C
  6 +import Coq (CoqTerm(..))
  7 +import Ltac
  8 +import CoqTop
  9 +import Data.Set (Set)
  10 +import qualified Data.Set as Set
  11 +import Data.Maybe
  12 +import Data.Either
  13 +import Data.List
  14 +import Data.Foldable (traverse_)
  15 +import Data.IORef
  16 +import Data.Typeable
  17 +import Control.Applicative
  18 +import Control.Exception
  19 +import Control.Monad
  20 +import Debug.Trace
  21 +
  22 +import Text.XML.Light
  23 +
  24 +-- We rely on naming being deterministic, so that we can have 'pure'
  25 +-- proof data structures. This is really not practical for real
  26 +-- proofs, where we really can't keep the all of the old proof states.
  27 +
  28 +type V = String
  29 +type PredV = String
  30 +type FunV = String
  31 +
  32 +-- Sequent
  33 +data S = S [L] [L]
  34 + deriving (Show, Eq)
  35 +
  36 +-- Elements in the universe. Distinguish between a constant and a
  37 +-- bound variable (probably not strictly necessary, but convenient)
  38 +data U = Fun FunV [U]
  39 + | Var V
  40 + deriving (Show, Eq)
  41 +
  42 +instance CoqTerm U where
  43 + toCoq (Fun f xs) = C.App (C.Atom f) (map toCoq xs)
  44 + toCoq (Var x) = C.Atom x
  45 +
  46 + fromCoq = coqToU Set.empty where
  47 +
  48 +-- XXX A bit specialized (not fromCoq because we need sets)
  49 +coqToU s (C.Atom n) | n `Set.member` s = Var n
  50 + | otherwise = Fun n []
  51 +coqToU s (C.App (C.Atom n) us) = Fun n (map (coqToU s) us)
  52 +coqToU _ _ = error "U.fromCoq"
  53 +
  54 +data L = Pred PredV [U] -- could be (Pred "A" [])
  55 + | Conj L L
  56 + | Disj L L
  57 + | Imp L L
  58 + | Not L
  59 + | Top
  60 + | Bot
  61 + | Forall V L
  62 + | Exists V L
  63 + deriving (Show, Eq)
  64 +
  65 +instance CoqTerm L where
  66 + toCoq (Pred p []) = C.Atom p
  67 + toCoq (Pred p xs) = C.App (C.Atom p) (map toCoq xs)
  68 + toCoq (Conj a b) = C.App (C.Atom "and") [toCoq a, toCoq b]
  69 + toCoq (Disj a b) = C.App (C.Atom "or") [toCoq a, toCoq b]
  70 + toCoq (Imp a b) = C.Imp (toCoq a) (toCoq b)
  71 + toCoq (Not a) = C.App (C.Atom "not") [toCoq a]
  72 + toCoq Top = C.Atom "True"
  73 + toCoq Bot = C.Atom "False"
  74 + toCoq (Forall x a) = C.Forall [("x", C.Atom "U")] (toCoq a)
  75 + toCoq (Exists x a) = C.App (C.Atom "@ex") [C.Atom "U", C.Fun [(x, C.Atom "U")] (toCoq a)]
  76 +
  77 + fromCoq = f Set.empty where
  78 + f s (C.Forall [] t) = f s t
  79 + f s (C.Forall ((n, C.Atom "U"):bs) t) = Forall n (f (Set.insert n s) (C.Forall bs t))
  80 + f s (C.Fun _ _) = error "L.fromCoq Fun"
  81 + f s (C.Typed t _) = f s t
  82 + f s (C.Imp t t') = Imp (f s t) (f s t')
  83 + f s (C.App (C.Atom "@ex") [C.Atom "U", C.Fun [(n, C.Atom "U")] t]) = Exists n (f (Set.insert n s) t)
  84 + f s (C.App (C.Atom "@ex") _) = error "L.fromCoq App ex"
  85 + f s (C.App (C.Atom "and") [t1, t2]) = Conj (f s t1) (f s t2)
  86 + f s (C.App (C.Atom "and") _) = error "L.fromCoq App and"
  87 + f s (C.App (C.Atom "or") [t1, t2]) = Disj (f s t1) (f s t2)
  88 + f s (C.App (C.Atom "or") _) = error "L.fromCoq App or"
  89 + f s (C.App (C.Atom "not") [t]) = Not (f s t)
  90 + f s (C.App (C.Atom "not") _) = error "L.fromCoq App not"
  91 + f s (C.App (C.Atom p) ts) = Pred p (map (coqToU s) ts)
  92 + f s (C.App _ _) = error "L.fromCoq App"
  93 + f s (C.Sort _) = error "L.fromCoq Sort"
  94 + f s (C.Num _) = error "L.fromCoq Num"
  95 + f s (C.Atom "True") = Top
  96 + f s (C.Atom "False") = Bot
  97 + f s (C.Atom n) = Pred n []
  98 +
  99 +listifyDisj :: L -> [L]
  100 +listifyDisj Bot = []
  101 +listifyDisj (Disj t ts) = t : listifyDisj ts
  102 +listifyDisj _ = error "listifyDisj"
  103 +
  104 +disjList :: [L] -> L
  105 +disjList [] = Bot
  106 +disjList (x:xs) = Disj x (disjList xs)
  107 +
  108 +-- quickcheck: listifyDisj (disjList xs) == xs
  109 +
  110 +-- Building up a proof tree is a multi-stage process.
  111 +--
  112 +-- You start off with a Goal S, where S is the thing you want to prove,
  113 +-- but not knowing what the right proof step is.
  114 +--
  115 +-- You might suggest some inference rule Q, in which case
  116 +-- you now have an Pending _ (Q _). It's unknown if it will work, nor do
  117 +-- we know what the subgoals will be.
  118 +--
  119 +-- Finally, after passing it to Coq, we discover if it's successful
  120 +-- and replace it with a Proof term.
  121 +
  122 +data P = Goal S | Pending S (Q Int) | Proof S (Q P)
  123 + deriving (Show)
  124 +
  125 +data Q a = Exact Int
  126 + | Cut L a a
  127 + | LConj Int a
  128 + | LDisj Int a a
  129 + | LImp Int a a
  130 + | LBot Int
  131 + | LNot Int a
  132 + | LForall Int U a
  133 + | LExists Int a
  134 + | LContract Int a
  135 + | LWeaken Int a
  136 + | RConj Int a a
  137 + | RDisj Int a
  138 + | RImp Int a
  139 + | RNot Int a
  140 + | RForall Int a
  141 + | RExists Int U a
  142 + | RWeaken Int a
  143 + | RContract Int a
  144 + deriving (Functor, Show)
  145 +
  146 +-- preorder traversal (does a full rebuild)
  147 +preorder fp fq a = tp a
  148 + where
  149 + -- XXX eep, only needs to be partial! Could use some GADTs here...
  150 + tp p@(Goal _) = fp p -- used for Goal -> Pending transition
  151 + tp p@(Pending _ _) = fp p -- used for Pending -> Proof transition
  152 + tp p@(Proof s q) = Proof s <$ fp p <*> tq q -- result discarded
  153 +
  154 + tq q@(Exact n) = Exact n <$ fq q
  155 + tq q@(Cut l x y) = Cut l <$ fq q <*> tp x <*> tp y
  156 + tq q@(LConj n x) = LConj n <$ fq q <*> tp x
  157 + tq q@(LDisj n x y) = LDisj n <$ fq q <*> tp x <*> tp y
  158 + tq q@(LImp n x y) = LImp n <$ fq q <*> tp x <*> tp y
  159 + tq q@(LBot n) = LBot n <$ fq q
  160 + tq q@(LNot n x) = LNot n <$ fq q <*> tp x
  161 + tq q@(LForall n v x) = LForall n v <$ fq q <*> tp x
  162 + tq q@(LExists n x) = LExists n <$ fq q <*> tp x
  163 + tq q@(LContract n x) = LContract n <$ fq q <*> tp x
  164 + tq q@(LWeaken n x) = LWeaken n <$ fq q <*> tp x
  165 + tq q@(RConj n x y) = RConj n <$ fq q <*> tp x <*> tp y
  166 + tq q@(RDisj n x) = RDisj n <$ fq q <*> tp x
  167 + tq q@(RImp n x) = RImp n <$ fq q <*> tp x
  168 + tq q@(RNot n x) = RNot n <$ fq q <*> tp x
  169 + tq q@(RForall n x) = RForall n <$ fq q <*> tp x
  170 + tq q@(RExists n v x) = RExists n v <$ fq q <*> tp x
  171 + tq q@(RWeaken n x) = RWeaken n <$ fq q <*> tp x
  172 + tq q@(RContract n x) = RContract n <$ fq q <*> tp x
  173 +
  174 +proofComplete a = isJust (preorder fp fq a)
  175 + where fp p@(Goal _) = mzero
  176 + fp p@(Pending _ _) = mzero
  177 + fp p@(Proof _ _) = return undefined
  178 + fq _ = return undefined
  179 +
  180 +hyp n = "Hyp" ++ show n
  181 +con n = "Con" ++ show n
  182 +
  183 +qNum Exact{} = 0
  184 +qNum Cut{} = 2
  185 +qNum LConj{} = 1
  186 +qNum LDisj{} = 2
  187 +qNum LImp{} = 2
  188 +qNum LBot{} = 0
  189 +qNum LNot{} = 1
  190 +qNum LForall{} = 1
  191 +qNum LExists{} = 1
  192 +qNum LContract{} = 1
  193 +qNum LWeaken{} = 1
  194 +qNum RConj{} = 2
  195 +qNum RDisj{} = 1
  196 +qNum RImp{} = 1
  197 +qNum RNot{} = 1
  198 +qNum RForall{} = 1
  199 +qNum RExists{} = 1
  200 +qNum RWeaken{} = 1
  201 +qNum RContract{} = 1
  202 +
  203 +qToTac (Exact n) = Tac "myExact" [hyp n]
  204 +qToTac (Cut l _ _) = Tac "myCut" [C.render (toCoq l)]
  205 +qToTac (LConj n _) = Tac "lConj" [hyp n]
  206 +qToTac (LDisj n _ _) = Tac "lDisj" [hyp n]
  207 +qToTac (LImp n _ _) = Tac "lImp" [hyp n]
  208 +qToTac (LBot n) = Tac "lBot" []
  209 +qToTac (LNot n _) = Tac "lNot" [hyp n]
  210 +qToTac (LForall n v _) = Tac "lForall" [hyp n, C.render (toCoq v)]
  211 +qToTac (LExists n _) = Tac "lExists" [hyp n]
  212 +qToTac (LContract n _) = Tac "lContract" [hyp n]
  213 +qToTac (LWeaken n _) = Tac "lWeaken" [hyp n]
  214 +qToTac (RConj n _ _) = Tac "rConj" [con n]
  215 +qToTac (RDisj n _) = Tac "rDisj" [con n]
  216 +qToTac (RImp n _) = Tac "rImp" [con n]
  217 +qToTac (RNot n _) = Tac "rNot" [con n]
  218 +qToTac (RForall n _) = Tac "rForall" [con n]
  219 +qToTac (RExists n v _) = Tac "rExists" [con n, C.render (toCoq v)]
  220 +qToTac (RWeaken n _) = Tac "rWeaken" [con n]
  221 +qToTac (RContract n _) = Tac "rContract" [con n]
  222 +
  223 +-- We need to do a rather special mechanism of feeding the proof to Coq,
  224 +-- because we need to find out what the intermediate proof state at
  225 +-- various steps looks like. (Also, we'd kind of like to save work...)
  226 +
  227 +-- using error, not fail! fail will have the wrong semantics
  228 +-- when we're using Maybe
  229 +maybeError s m = maybe (error s) return m
  230 +eitherError = either (error . show) return
  231 +
  232 +-- NOTE Tactic failure may be from a built in (i.e. no clauses for
  233 +-- match) or from an explicit fail, which can have a string resulting
  234 +-- in "Error: Tactic failure: foo." We don't appear to have any
  235 +-- need for sophisticated failure matching yet, and the errors are
  236 +-- in general kind of useless, but maybe it will be useful later.
  237 +-- Note that we have an opportunity for *unsound* error generation:
  238 +-- "if there is an error, this message might be useful" (kind of like
  239 +-- how humans, faced with a fact that is in fact false, can still make
  240 +-- up plausible excuses.)
  241 +
  242 +data CoqError = TacticFailure | NoMoreSubgoals
  243 + deriving (Show)
  244 +
  245 +-- but bottom on input we don't understand
  246 +parseResponse :: [Content] -> Either CoqError S
  247 +parseResponse raw = do
  248 + let fake = Element (qn "fake") [] raw Nothing
  249 + extractHyp (C.Typed (C.Atom _) (C.App (C.Atom "Hyp") [l])) = Just l
  250 + extractHyp _ = Nothing
  251 + qn s = QName s Nothing Nothing
  252 + -- showElement fake `trace` return ()
  253 + when (isJust (findElement (qn "errorresponse") fake)) (Left TacticFailure)
  254 + -- yes, we're being partial here, but using ordering to
  255 + -- ensure that the errors get sequenced correctly
  256 + resp <- maybeError "pendingToHole: no response found" (findChild (qn "normalresponse") (Element (qn "fake") [] raw Nothing))
  257 + (\s -> when (s == "no-more-subgoals") (Left NoMoreSubgoals)) `traverse_` findAttr (qn "status") resp
  258 + hyps <- mapMaybe extractHyp
  259 + . rights
  260 + . map (C.parseTerm . strContent)
  261 + . findChildren (qn "hyp")
  262 + <$> maybeError "pendingToHole: no hyps found" (findChild (qn "hyps") resp)
  263 + goal <- eitherError . C.parseTerm . strContent =<< maybeError "pendingToHole: no goal found" (findChild (qn "goal") resp)
  264 + return (S (map fromCoq hyps) (listifyDisj (fromCoq goal)))
  265 +
  266 +refine :: P -> IO P
  267 +refine p@(Goal s) = refine' s p
  268 +refine p@(Pending s _) = refine' s p
  269 +refine p@(Proof s _) = refine' s p
  270 +
  271 +data UpdateFailure = UpdateFailure
  272 + deriving (Typeable, Show)
  273 +instance Exception UpdateFailure
  274 +
  275 +-- the S is kind of redundant but makes my life easier
  276 +refine' :: S -> P -> IO P
  277 +-- XXX not quite right
  278 +refine' s@(S [] cs) p = coqtop "ClassicalFOL" $ \f -> do
  279 + -- XXX demand no errors
  280 + mapM_ f [ "Section scratch"
  281 + , "Parameter U : Set"
  282 + -- XXX factor these constants out
  283 + , "Variable z : U"
  284 + , "Variable f g h : U -> U"
  285 + , "Variable A B C : Prop"
  286 + , "Variable P Q R : Prop"
  287 + , "Set Printing All"
  288 + ]
  289 + -- despite being horrible mutation, this plays an important
  290 + -- synchronizing role for us; it lets us make sure that "what we
  291 + -- see" is what we expect; also, immediately after we run a tactic
  292 + -- is not /quite/ the right place to check the result
  293 + currentState <- newIORef Nothing
  294 + let run tac = do
  295 + -- putStrLn tac
  296 + r <- evaluate . parseResponse =<< f tac
  297 + case r of
  298 + Right x -> writeIORef currentState (Just x) >> return True
  299 + Left TacticFailure -> return False
  300 + Left NoMoreSubgoals -> writeIORef currentState Nothing >> return True
  301 + readState = readIORef currentState
  302 + checkState s = readState >>= \s' -> assert (Just s == s') (return ())
  303 + r <- run ("Goal " ++ C.render (toCoq (disjList cs)))
  304 + when (not r) $ error "refine: setting goal failed"
  305 + let fp p@(Goal s) = checkState s >> return p
  306 + -- TODO also check if change in number of subgoals is correct
  307 + fp p@(Pending s q) = do
  308 + checkState s
  309 + run (show (qToTac q)) >>= (`unless` throwIO UpdateFailure)
  310 + gs <- replicateM (qNum q) (fromJust <$> readState <* (run "admit" >>= (`unless` error "refine: could not admit")))
  311 + return (Proof s (fmap (Goal . (gs !!)) q))
  312 + fp (Proof s _) = checkState s >> return undefined
  313 + fq q = run (show (qToTac q)) >>= (`unless` error "refine: inconsistent proof state")
  314 + preorder fp fq p
  315 +
  316 +-- XXX partial (not a particularly stringent requirement; you can get
  317 +-- around it with a few intros / tactic applications
  318 +refine' _ _ = error "pendingToHole: meta-implication must be phrased as implication"
  319 +
  320 +main = do
  321 + let s = S [] [Pred "A" [], Not (Pred "A" [])]
  322 + -- XXX actually kinda slow...
  323 + print =<< refine (Goal s)
  324 + print =<< refine (Pending s (RNot 1 0))
  325 + print =<< refine (Proof s (RNot 1 (Goal (S [Pred "A" []] [Pred "A" []]))))
  326 + print =<< refine (Proof s (RNot 1 (Pending (S [Pred "A" []] [Pred "A" []]) (Exact 0))))
  327 + print =<< refine (Proof s (RNot 1 (Proof (S [Pred "A" []] [Pred "A" []]) (Exact 0))))
3  ClassicalFOL.v
@@ -215,9 +215,12 @@ Section universe.
215 215
216 216 Parameter U : Set.
217 217 Variable z : U. (* non-empty domain *)
  218 +Variable f : U -> U. (* FOL function *)
218 219 Variables A B C : Prop. (* some convenient things to instantiate with *)
219 220 Variables P Q R : U -> Prop.
220 221
  222 +Set Printing All.
  223 +
221 224 (* an example *)
222 225 Goal denote ( [ True; C /\ C; (~ True) \/ True ] |= [ False; False; False; ((A -> B) -> A) -> A ] ).
223 226 sequent.
239 Coq.hs
... ... @@ -0,0 +1,239 @@
  1 +{-# LANGUAGE RankNTypes, TupleSections #-}
  2 +
  3 +module Coq (
  4 + Term(..)
  5 + , Binder
  6 + , Name
  7 + , Sort(..)
  8 + , term
  9 + , parseTerm
  10 + , CoqTerm(..)
  11 + , render
  12 + ) where
  13 +
  14 +import Control.Applicative hiding ((<|>), many)
  15 +import Text.Parsec
  16 +import qualified Text.Parsec.Token as P
  17 +import Text.Parsec.Language (emptyDef)
  18 +import Data.Functor.Identity
  19 +import Data.List hiding (sort)
  20 +
  21 +coqStyle :: P.LanguageDef st
  22 +coqStyle = emptyDef
  23 + { P.commentStart = "(*"
  24 + , P.commentEnd = "*)"
  25 + , P.nestedComments = True
  26 + , P.identStart = letter <|> oneOf "_"
  27 + , P.identLetter = alphaNum <|> oneOf "_'"
  28 + -- Ops are sloppy, but should work OK for our use case.
  29 + -- There might be a bug here.
  30 + , P.opStart = P.opLetter coqStyle
  31 + , P.opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
  32 + -- Lifted straight out of the manual
  33 + , P.reservedOpNames =
  34 + ["!","%","&","&&","(","()",")",
  35 + "*","+","++",",","-","->",".",
  36 + ".(","..","/","/\\",":","::",":<",
  37 + ":=",":>",";","<","<-","<->","<:",
  38 + "<=","<>","=","=>","=_D",">",">->",
  39 + ">=","?","?=","@","[","\\/","]",
  40 + "^","{","|","|-","||","}","~"]
  41 + , P.reservedNames =
  42 + ["_","as","at","cofix","else","end",
  43 + "exists","exists2","fix","for","forall","fun",
  44 + "if","IF","in","let","match","mod",
  45 + "Prop","return","Set","then","Type","using",
  46 + "where","with"]
  47 + , P.caseSensitive = True
  48 + }
  49 +
  50 +lexer = P.makeTokenParser coqStyle
  51 +
  52 +reserved = P.reserved lexer
  53 +identifier = P.identifier lexer
  54 +reservedOp = P.reservedOp lexer
  55 +integer = P.integer lexer
  56 +whiteSpace = P.whiteSpace lexer
  57 +
  58 +-- http://coq.inria.fr/doc/Reference-Manual003.html
  59 +
  60 +-- Here is the restricted BNF we will support:
  61 +--
  62 +-- term ::= forall binders , term
  63 +-- | fun binders => term
  64 +-- | term : term
  65 +-- | term -> term
  66 +-- | term arg ... arg
  67 +-- | @ qualid term ... term
  68 +-- | qualid
  69 +-- | sort
  70 +-- | num
  71 +-- arg ::= term
  72 +-- binders ::= binder .. binder
  73 +-- binder ::= name | ( name ... name : term )
  74 +-- name ::= ident
  75 +-- qualid ::= ident
  76 +-- sort ::= Prop | Set | Type
  77 +
  78 +data Term = Forall [Binder] Term
  79 + | Fun [Binder] Term
  80 + | Typed Term Term -- extra info
  81 + | Imp Term Term
  82 + | App Term [Term]
  83 + | Sort Sort
  84 + | Num Integer
  85 + | Atom Name
  86 + deriving (Show, Eq)
  87 +
  88 +render :: Term -> String
  89 +render (Forall bs t) = "(forall " ++ renderBinders bs ++ ", " ++ render t ++ ")"
  90 +render (Fun bs t) = "(fun " ++ renderBinders bs ++ " => " ++ render t ++ ")"
  91 +render (Typed t t') = "(" ++ render t ++ " : " ++ render t' ++ ")"
  92 +render (Imp t t') = "(" ++ render t ++ " -> " ++ render t' ++ ")"
  93 +render (App t ts) = "(" ++ render t ++ " " ++ intercalate " " (map render ts) ++ ")"
  94 +render (Sort Prop) = "Prop"
  95 +render (Sort Set) = "Set"
  96 +render (Sort Type) = "Type"
  97 +render (Num i) = show i
  98 +render (Atom n) = n
  99 +
  100 +renderBinders :: [Binder] -> String
  101 +renderBinders [] = error "renderBinders: empty binder"
  102 +renderBinders [(n, t)] = "(" ++ n ++ ":" ++ render t ++ ")"
  103 +renderBinders (x:xs) = renderBinders [x] ++ " " ++ renderBinders xs -- XXX code reuse at its finest
  104 +
  105 +-- We require the types of our binders! If you Set Printing All you
  106 +-- should get them.
  107 +type Binder = (Name, Term)
  108 +type Name = String -- qualid's are squashed in here
  109 +data Sort = Prop | Set | Type
  110 + deriving (Show, Eq)
  111 +
  112 +-- But the BNF is not enough to actually properly parse...
  113 +-- (precedences?)
  114 +--
  115 +-- Fortunately, we already have a nice converted definition in
  116 +-- parsing/g_constr.ml4. They also have some batshit weird interaction
  117 +-- between their infix and prefix operators, so we don't use Parsec's
  118 +-- nice table support.
  119 +--
  120 +-- Levels are pretty important to understanding g_constr.ml4; there is a
  121 +-- good treatment here:
  122 +-- http://caml.inria.fr/pub/docs/tutorial-camlp4/tutorial003.html
  123 +-- Notationally, operconstr.90 === operconstr LEVEL 90; we've translated
  124 +-- all of the NEXT and SELF identifiers.
  125 +--
  126 +-- We had to manually resolve some levels, so if you add more levels you
  127 +-- will need to fix them.
  128 +
  129 +type P a = forall u. ParsecT String u Identity a
  130 +
  131 +global :: P Term
  132 +global = Atom <$> identifier
  133 +
  134 +name :: P String
  135 +name = identifier
  136 +
  137 +-- operconstr:
  138 +-- 200 RIGHTA binder_constr
  139 +-- 100 RIGHTA operconstr.90 ":" binder_constr
  140 +-- operconstr.90 ":" operconstr.100
  141 +-- 90 RIGHTA operconstr.10 "->" binder_constr
  142 +-- operconstr.10 "->" operconstr.90
  143 +-- 10 LEFTA operconstr.0 appl_arg+ // this one might be wrong
  144 +-- "@" global operconstr.0*
  145 +-- 0 atomic_constr
  146 +-- "(" operconstr.200 ")"
  147 +
  148 +term :: P Term
  149 +term = operconstr200
  150 +
  151 +-- There is a more efficient, left-factored representation for many of
  152 +-- these rules, and some of the tries are not necessary, but sprinkling
  153 +-- in try makes it easier to tell that things are correct, and
  154 +-- performance is not a primary concern. If you're curious what the
  155 +-- left-factored representation looks like, see Coq_efficient.hs
  156 +
  157 +operconstr200, operconstr100, operconstr90, operconstr10, operconstr0 :: P Term
  158 +operconstr200 = try binder_constr <|> operconstr100
  159 +operconstr100 = try (Typed <$> operconstr90 <* reservedOp ":" <*> binder_constr)
  160 + <|> try (Typed <$> operconstr90 <* reservedOp ":" <*> operconstr100)
  161 + <|> operconstr90
  162 +operconstr90 = try (Imp <$> operconstr10 <* reservedOp "->" <*> binder_constr)
  163 + <|> try (Imp <$> operconstr10 <* reservedOp "->" <*> operconstr90)
  164 + <|> operconstr10
  165 +operconstr10 = try (App <$> operconstr0 <*> many1 appl_arg)
  166 + -- XXX dropping the @ cuz we're lazy
  167 + <|> try (reservedOp "@" >> App <$> global <*> many operconstr0)
  168 + <|> operconstr0
  169 +operconstr0 = try atomic_constr
  170 + <|> reservedOp "(" *> operconstr200 <* reservedOp ")"
  171 +
  172 +-- lconstr: operconstr.200
  173 +lconstr :: P Term
  174 +lconstr = operconstr200
  175 +
  176 +-- constr:
  177 +-- operconstr.8
  178 +-- "@" global
  179 +constr :: P Term
  180 +constr = try operconstr0
  181 + <|> (reservedOp "@" >> Atom . ('@':) <$> identifier)
  182 +
  183 +-- binder_constr:
  184 +-- "forall" open_binders "," operconstr.200
  185 +-- "fun" open_binders "=>" operconstr.200
  186 +binder_constr :: P Term
  187 +binder_constr = try (reserved "forall" >> Forall <$> open_binders <* reservedOp "," <*> operconstr200)
  188 + <|> (reserved "fun" >> Fun <$> open_binders <* reservedOp "=>" <*> operconstr200)
  189 +
  190 +-- open_binders:
  191 +-- name name* ":" lconstr
  192 +-- name name* binders
  193 +-- closed_binder binders
  194 +msBinder ns t = map (,t) ns
  195 +open_binders :: P [Binder]
  196 +open_binders = try (msBinder <$> many1 name <* reservedOp ":" <*> lconstr)
  197 + <|> ((++) <$> closed_binder <*> binders)
  198 +
  199 +-- binders: binder*
  200 +binders :: P [Binder]
  201 +binders = concat <$> many binder
  202 +
  203 +-- binder:
  204 +-- closed_binder
  205 +binder :: P [Binder]
  206 +binder = closed_binder
  207 +
  208 +-- closed_binder:
  209 +-- "(" name+ ":" lconstr ")"
  210 +closed_binder :: P [Binder]
  211 +closed_binder = reservedOp "(" >> msBinder <$> many name <* reservedOp ":" <*> lconstr <* reservedOp ")"
  212 +
  213 +-- appl_arg:
  214 +-- "(" lconstr ")" -- we don't need the hack yay!
  215 +-- operconstr.0
  216 +appl_arg = try (reservedOp "(" >> lconstr <* reservedOp ")")
  217 + <|> operconstr0
  218 +
  219 +-- atomic_constr:
  220 +-- global
  221 +-- sort
  222 +-- INT
  223 +atomic_constr :: P Term
  224 +atomic_constr = try global
  225 + <|> try (Sort <$> sort)
  226 + <|> Num <$> integer
  227 +sort :: P Sort
  228 +sort = Prop <$ reserved "Prop" <|> Set <$ reserved "Set" <|> Type <$ reserved "Type"
  229 +
  230 +parse_sample = "or ((forall x : U, P x) -> @ex U (fun x : U => P x)) False"
  231 +sample = parse (term <* eof) "" parse_sample
  232 +
  233 +parseTerm = parse (whiteSpace >> term <* eof) ""
  234 +
  235 +-- XXX can haz test please (do it before you make changes)
  236 +
  237 +class CoqTerm a where
  238 + toCoq :: a -> Term
  239 + fromCoq :: Term -> a
84 CoqTop.hs
... ... @@ -0,0 +1,84 @@
  1 +{-# LANGUAGE RankNTypes, NoMonomorphismRestriction, ScopedTypeVariables #-}
  2 +
  3 +module CoqTop
  4 + ( coqtop
  5 + ) where
  6 +
  7 +import Prelude hiding (catch)
  8 +import System.IO
  9 +import System.Process
  10 +import Control.Concurrent
  11 +import Control.Concurrent.Chan
  12 +import Control.Concurrent.MVar
  13 +import Control.Exception
  14 +import Control.Monad
  15 +import Text.XML.Light.Input
  16 +import Text.XML.Light
  17 +import Data.List.Split
  18 +
  19 +-- You'll need ezyang's private copy of Coq https://github.com/ezyang/coq
  20 +
  21 +coqtopProcess theory err = CreateProcess
  22 + -- XXX Filepaths should be more generic...
  23 + { cmdspec = RawCommand "/home/ezyang/Dev/coq-git/bin/coqtop.opt"
  24 + [ "-coqlib"
  25 + , "/home/ezyang/Dev/coq-git"
  26 + , "-l"
  27 + , "/home/ezyang/Dev/logitext/" ++ theory ++ ".v"
  28 + , "-pgip"]
  29 + , cwd = Nothing
  30 + , env = Nothing
  31 + , std_in = CreatePipe
  32 + , std_out = CreatePipe
  33 + , std_err = UseHandle err
  34 + , close_fds = True
  35 + }
  36 +
  37 +onlyOnce :: IO () -> IO (IO ())
  38 +onlyOnce m = do
  39 + i <- newMVar m
  40 + return (modifyMVar_ i (\m -> m >> return (return ())))
  41 +
  42 +coqtopRaw theory = do
  43 + -- XXX We're not really doing good things with warnings.
  44 + -- Fortunately, fatal errors DO get put on stdout.
  45 + err <- openFile "/dev/null" WriteMode -- XXX gimme a platform independent version!
  46 + (Just fin, Just fout, _, pid) <- createProcess (coqtopProcess theory err)
  47 + hSetBuffering fin LineBuffering
  48 + hSetBuffering fout LineBuffering -- should be good enough to pick up on <ready/>
  49 + resultChan <- newChan
  50 + -- XXX do we really want to give them the <ready/> marker? (elim
  51 + -- keepDelimsR if not)
  52 + tout <- forkIO $
  53 + -- Lazy IO at its finest
  54 + let p (Elem e) | qName (elName e) == "ready" = True
  55 + p _ = False
  56 + in writeList2Chan resultChan . split (keepDelimsR (whenElt p)) =<< parseXML `fmap` hGetContents fout
  57 + _ <- readChan resultChan -- read out the intro message
  58 + -- XXX this doesn't do particularly good things if you don't
  59 + -- pass it enough information. Correct thing to do is on COQ
  60 + -- side say "I want more information!" Nor does it do good things
  61 + -- if you give it too much information... (de-synchronization risk)
  62 + interactVar <- newMVar (\s -> hPutStr fin (s ++ ".\n") >> readChan resultChan)
  63 + let interact s = withMVar interactVar (\f -> f s)
  64 + end <- onlyOnce $ do
  65 + killThread tout
  66 + hClose fin
  67 + hClose fout
  68 + m <- getProcessExitCode pid
  69 + maybe (terminateProcess pid) (const (return ())) m
  70 + -- We're erring on the safe side here. If no escape of coqtop
  71 + -- from bracket is enforced, this is impossible
  72 + modifyMVar_ interactVar (\_ -> return (error "coqtopRaw/end: coqtop is dead"))
  73 + return (interact, end)
  74 +
  75 +coqtop theory inner = bracket (coqtopRaw theory) snd (inner . fst)
  76 +
  77 +{-
  78 +main =
  79 + coqtop "ClassicalFOL" $ \f -> do
  80 + let run s = f s >>= print >> putStrLn ""
  81 + run "Goal True."
  82 + run "trivial."
  83 + run "Qed."
  84 +-}
152 Coq_efficient.hs
... ... @@ -0,0 +1,152 @@
  1 +module Coq where
  2 +
  3 +import Text.Parsec
  4 +import qualified Text.Parsec.Token as P
  5 +import Text.Parsec.Language (emptyDef)
  6 +import Text.Parsec.Expr
  7 +import Data.Functor.Identity
  8 +
  9 +coqStyle :: P.LanguageDef st
  10 +coqStyle = emptyDef
  11 + { P.commentStart = "(*"
  12 + , P.commentEnd = "*)"
  13 + , P.nestedComments = True
  14 + , P.identStart = letter <|> oneOf "_"
  15 + , P.identLetter = alphaNum <|> oneOf "_'"
  16 + -- Ops are sloppy, but should work OK for our use case.
  17 + -- There might be a bug here.
  18 + , P.opStart = P.opLetter coqStyle
  19 + , P.opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
  20 + -- Lifted straight out of the manual
  21 + , P.reservedOpNames =
  22 + ["!","%","&","&&","(","()",")",
  23 + "*","+","++",",","-","->",".",
  24 + ".(","..","/","/\\",":","::",":<",
  25 + ":=",":>",";","<","<-","<->","<:",
  26 + "<=","<>","=","=>","=_D",">",">->",
  27 + ">=","?","?=","@","[","\\/","]",
  28 + "^","{","|","|-","||","}","~"]
  29 + , P.reservedNames =
  30 + ["_","as","at","cofix","else","end",
  31 + "exists","exists2","fix","for","forall","fun",
  32 + "if","IF","in","let","match","mod",
  33 + "Prop","return","Set","then","Type","using",
  34 + "where","with"]
  35 + , P.caseSensitive = True
  36 + }
  37 +
  38 +lexer = P.makeTokenParser coqStyle
  39 +
  40 +reserved = P.reserved lexer
  41 +identifier = P.identifier lexer
  42 +reservedOp = P.reservedOp lexer
  43 +integer = P.integer lexer
  44 +
  45 +-- http://coq.inria.fr/doc/Reference-Manual003.html
  46 +
  47 +-- Here is the restricted BNF we will support:
  48 +--
  49 +-- term ::= forall binders , term
  50 +-- | fun binders => term
  51 +-- | term : term
  52 +-- | term -> term
  53 +-- | term arg ... arg
  54 +-- | @ qualid term ... term
  55 +-- | qualid
  56 +-- | sort
  57 +-- | num
  58 +-- arg ::= term
  59 +-- binders ::= binder .. binder
  60 +-- binder ::= name | ( name ... name : term )
  61 +-- name ::= ident
  62 +-- qualid ::= ident
  63 +-- sort ::= Prop | Set | Type
  64 +--
  65 +-- But the BNF is not enough to actually properly parse...
  66 +-- (precedences?)
  67 +--
  68 +-- Fortunately, we already have a nice converted definition in
  69 +-- parsing/g_constr.ml4. They also have some batshit weird interaction
  70 +-- between their infix and prefix operators, so we don't use Parsec's
  71 +-- nice table support.
  72 +--
  73 +-- Levels are pretty important to understanding g_constr.ml4; there is a
  74 +-- good treatment here:
  75 +-- http://caml.inria.fr/pub/docs/tutorial-camlp4/tutorial003.html
  76 +-- Notationally, operconstr.90 === operconstr LEVEL 90; we've translated
  77 +-- all of the NEXT and SELF identifiers.
  78 +--
  79 +-- We had to manually resolve some levels, so if you add more levels you
  80 +-- will need to fix them.
  81 +
  82 +global = identifier >> return ()
  83 +name = identifier
  84 +
  85 +-- operconstr:
  86 +-- 200 RIGHTA binder_constr
  87 +-- 100 RIGHTA operconstr.90 ":" binder_constr
  88 +-- operconstr.90 ":" operconstr.100
  89 +-- 90 RIGHTA operconstr.10 "->" binder_constr
  90 +-- operconstr.10 "->" operconstr.90
  91 +-- 10 LEFTA operconstr.0 appl_arg+ // this one might be wrong
  92 +-- "@" global operconstr.0*
  93 +-- 0 atomic_constr
  94 +-- "(" operconstr.200 ")"
  95 +
  96 +term = operconstr200
  97 +operconstr200 = binder_constr <|> operconstr100
  98 +operconstr100 = operconstr90 >> ((reservedOp ":" >> (binder_constr <|> operconstr100)) <|> return ())
  99 +operconstr90 = operconstr10 >> ((reservedOp "->" >> (binder_constr <|> operconstr90)) <|> return ())
  100 +operconstr10 = try (operconstr0 >> many1 appl_arg >> return ())
  101 + <|> (reservedOp "@" >> global >> many operconstr0 >> return ())
  102 + <|> operconstr0
  103 +operconstr0 = atomic_constr
  104 + <|> (reservedOp "(" >> operconstr200 >> reservedOp ")")
  105 +
  106 +-- lconstr: operconstr.200
  107 +lconstr = operconstr200
  108 +
  109 +-- constr:
  110 +-- operconstr.8
  111 +-- "@" global
  112 +constr = operconstr0 <|> (reservedOp "@" >> global >> return ())
  113 +
  114 +-- binder_constr:
  115 +-- "forall" open_binders "," operconstr.200
  116 +-- "fun" open_binders "=>" operconstr.200
  117 +binder_constr = (reserved "forall" >> open_binders >> reservedOp "," >> operconstr200)
  118 + <|> (reserved "fun" >> open_binders >> reservedOp "=>" >> operconstr200)
  119 +
  120 +-- open_binders:
  121 +-- name name* ":" lconstr
  122 +-- name name* binders
  123 +-- closed_binder binders
  124 +open_binders = (many1 name >> ((reservedOp ":" >> lconstr) <|> binders))
  125 + <|> (closed_binder >> binders)
  126 +
  127 +-- binders: binder*
  128 +binders = many binder >> return ()
  129 +
  130 +-- binder:
  131 +-- name
  132 +-- closed_binder
  133 +binder = (name >> return ()) <|> closed_binder
  134 +
  135 +-- closed_binder:
  136 +-- "(" name+ ":" lconstr ")"
  137 +closed_binder = reservedOp "(" >> many name >> reservedOp ":" >> lconstr >> reservedOp ")" >> return ()
  138 +
  139 +-- appl_arg:
  140 +-- "(" lconstr ")" -- we don't need the hack yay!
  141 +-- operconstr.0
  142 +appl_arg = (reservedOp "(" >> lconstr >> reservedOp ")") <|> operconstr0
  143 +
  144 +-- atomic_constr:
  145 +-- global
  146 +-- sort
  147 +-- INT
  148 +atomic_constr = global <|> sort <|> (integer >> return ())
  149 +sort = (reserved "Prop" <|> reserved "Set" <|> reserved "Type") >> return ()
  150 +
  151 +parse_sample = "or ((forall x : U, P x) -> @ex U (fun x : U => P x)) False"
  152 +main = parseTest (term >> eof) "forall x : U, foo -> bar" -- parse_sample
22 Ltac.hs
... ... @@ -0,0 +1,22 @@
  1 +module Ltac where
  2 +
  3 +import Data.List
  4 +
  5 +data Expr = Seq Expr [Expr]
  6 + -- | Progress Expr
  7 + -- | Solve [Expr]
  8 + | Tac String [String] -- technically should point to tacarg; we only allow qualids for now
  9 +
  10 +-- Useful atomic tactics
  11 +admit = Tac "admit" []
  12 +
  13 +-- This is kind of deficient for handling tacexpr_1, tacexpr_2,
  14 +-- tacexpr_3 parsing rules
  15 +instance Show Expr where
  16 + show (Seq e1 [e2]) = show e1 ++ "; " ++ show e2
  17 + show (Seq e es) = show e ++ "; [ " ++ intercalate " | " (map show es) ++ " ]"
  18 + -- show (Progress e) = "progress " ++ show e
  19 + -- show (Solve es) = "solve [" ++ intercalate "|" (map show es) ++ "]"
  20 + show (Tac s []) = s
  21 + -- XXX invariant: args must be appropriately parenthesized
  22 + show (Tac s as) = s ++ " " ++ intercalate " " as

No commit comments for this range

Something went wrong with that request. Please try again.