From 3aa662a669b6a98caabd6198324a9662f8d0ac0e Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@univ-lille.fr>
Date: Thu, 5 Nov 2020 18:42:53 +0100
Subject: [PATCH] Accept Axioms in JSON
Of course, axioms cannot be converted but they can now appear in modules
and be correctly parsed
---
example/Example.v | 2 ++
example/Internals.c | 2 ++
example/Internals.h | 1 +
example/Internals.v | 2 ++
src/Language/Coq/ExtractedAST.hs | 7 ++++++-
5 files changed, 13 insertions(+), 1 deletion(-)
diff --git a/example/Example.v b/example/Example.v
index 1d12203..71d0322 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 41482d5..e4058f4 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 efb7cbf..759e344 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 f5653a3..78ec3a0 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 7af363f..8b5ad3a 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')
--
GitLab