diff --git a/example/Example.v b/example/Example.v index 1d122032e96365e3f9d2b786d118aa1b8dc746e9..71d032246d83679f2f6bc5311306ff5d8cc95c1e 100644 --- a/example/Example.v +++ b/example/Example.v @@ -45,6 +45,8 @@ Fixpoint prepare recBound : M unit := prepare b end. +Definition fullPrepare := prepare bound. + Eval compute in runM (id true) 12. Eval compute in runM (neg true) 12. Eval compute in runM (prepare 1) 1. diff --git a/example/Internals.c b/example/Internals.c index 41482d5ef224328ee06bb8816df9a0dd95e096b4..e4058f4a2a4a9cd5ded2c983c2652c90ba5bf12b 100644 --- a/example/Internals.c +++ b/example/Internals.c @@ -30,6 +30,8 @@ #include "base.h" #include "Monad.h" +unsigned bound = 10; + bool ready() { return state % 2 == 0; } diff --git a/example/Internals.h b/example/Internals.h index efb7cbf3531d78e87e7a3eee199378da49132935..759e3445ef3fbabc39a8e6b0c3fa0408b54cfbda 100644 --- a/example/Internals.h +++ b/example/Internals.h @@ -27,5 +27,6 @@ /* This C header provides the prototypes for the "primitive" functions */ +extern unsigned bound; bool ready(); void getReady(); diff --git a/example/Internals.v b/example/Internals.v index f5653a37d681a7a410c5a45b587e3d672a7d5ef1..78ec3a09d4c03295e9e3f286ad1a8dcc98dee7f3 100644 --- a/example/Internals.v +++ b/example/Internals.v @@ -31,6 +31,8 @@ Require Import Nat Monad. Open Scope monad_scope. +Parameter bound : nat. + Definition ready : M bool := do s <- get ; returnM (even s). diff --git a/src/Language/Coq/ExtractedAST.hs b/src/Language/Coq/ExtractedAST.hs index 7af363f7a4aea6ed9bf3c5f9652044ea62f11029..8b5ad3a68eda97eed6a25ac62a608ed55aae77bb 100644 --- a/src/Language/Coq/ExtractedAST.hs +++ b/src/Language/Coq/ExtractedAST.hs @@ -56,7 +56,7 @@ data FixgrpT = ItemFT deriving (Show,Eq) data TypeT = ArrowTT | GlobTT | VaridxTT deriving (Show,Eq) -data ExprT = LambdaET| ApplyET | GlobalET | ConstructorET | RelET | CaseET | LetET +data ExprT = LambdaET| ApplyET | GlobalET | ConstructorET | RelET | CaseET | LetET | AxiomET deriving (Show,Eq) data PatT = ConstructorPT | WildPT deriving (Show,Eq) @@ -80,6 +80,7 @@ toWhatType strType = "expr:rel" -> pure $ ExprT RelET "expr:case" -> pure $ ExprT CaseET "expr:let" -> pure $ ExprT LetET + "expr:axiom" -> pure $ ExprT AxiomET "pat:constructor" -> pure $ PatT ConstructorPT "pat:wild" -> pure $ PatT WildPT strError -> fail $ "Error: WhatType \"" ++ strError ++ "\" undefined" @@ -179,6 +180,7 @@ data Expr = Lambda { argnamesLambda :: [Name] , namevalLet :: Expr , bodyLet :: Expr } + | Axiom deriving (Show,Eq) instance Renamable Expr where @@ -189,6 +191,7 @@ instance Renamable Expr where rename f (Rel n) = Rel (f n) rename f (Case e cs) = Case (rename f e) (map (rename f) cs) rename f (Let n v b) = Let (f n) (rename f v) (rename f b) + rename _ Axiom = Axiom instance FromJSON Expr where parseJSON (Object v) = do @@ -201,6 +204,7 @@ instance FromJSON Expr where ExprT RelET -> Rel <$> v .: "name" ExprT CaseET -> Case <$> v .: "expr" <*> v .: "cases" ExprT LetET -> Let <$> v .: "name" <*> v .: "nameval" <*> v .: "body" + ExprT AxiomET -> pure Axiom _ -> fail "Error: Expr case undefined" parseJSON _ = fail "Error: Expr kind undefined" @@ -512,6 +516,7 @@ extractRecCalls cn self recs expr = deDup <$> isConsistent (go expr) pure (calls ++ calls', let'') go e@(Global _) = pure ([], e) go e@(Rel _) = pure ([], e) + go e@Axiom = pure ([], e) drills f exprs = do (calls, exprs') <- unzip <$> traverse go exprs pure (concat calls, f exprs')