From 11c85494203cf6b107d83bedf7d3d23719b028f1 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Tue, 27 Feb 2024 18:29:13 +0100
Subject: [PATCH] add coq-stdpp as dependency, add abs_examples module (#12)

* add coq-stdpp as dependency, add abs_examples module

* Typing examples

* nits

---------

Co-authored-by: Aqissiaq <aqissiaq@gmail.com>
---
 README.md               |  3 ++-
 _CoqProject             |  1 +
 coq-abs-metatheory.opam |  1 +
 meta.yml                |  8 ++++++--
 theories/abs_examples.v | 37 +++++++++++++++++++++++++++++++++++++
 5 files changed, 47 insertions(+), 3 deletions(-)
 create mode 100644 theories/abs_examples.v

diff --git a/README.md b/README.md
index e5302f2..6651ce7 100644
--- a/README.md
+++ b/README.md
@@ -23,6 +23,7 @@ Formal metatheory in Coq for the ABS language.
 - Additional dependencies:
   - [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later
   - [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later
+  - [Coq-Std++](https://gitlab.mpi-sws.org/iris/stdpp) 1.9.0 or later
 - Coq namespace: `ABS`
 - Related publication(s):
   - [ABS: A Core Language for Abstract Behavioral Specification](https://link.springer.com/chapter/10.1007/978-3-642-25271-6_8) doi:[10.1007/978-3-642-25271-6_8](https://doi.org/10.1007/978-3-642-25271-6_8)
@@ -33,7 +34,7 @@ To install all dependencies, do:
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.18.0 coq-ott
+opam install coq.8.18.0 coq-ott coq-equations coq-stdpp
 ```
 
 To build when dependencies are installed, do:
diff --git a/_CoqProject b/_CoqProject
index 3e6d0d6..62c7654 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,4 +3,5 @@
 -arg -w -arg -deprecated-hint-without-locality
 
 theories/abs_defs.v
+theories/abs_examples.v
 theories/abs_functional_metatheory.v
diff --git a/coq-abs-metatheory.opam b/coq-abs-metatheory.opam
index 5168bf6..903e6b3 100644
--- a/coq-abs-metatheory.opam
+++ b/coq-abs-metatheory.opam
@@ -20,6 +20,7 @@ depends: [
   "coq" {>= "8.16"}
   "coq-ott" {>= "0.33"}
   "coq-equations" {>= "1.3"}
+  "coq-stdpp" {>= "1.9.0"}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index 45c5eac..4661988 100644
--- a/meta.yml
+++ b/meta.yml
@@ -33,12 +33,16 @@ dependencies:
     version: '{>= "0.33"}'
   description: |-
     [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later
-
 - opam:
     name: coq-equations
     version: '{>= "1.3"}'
   description: |-
     [Equations Coq library](https://github.com/mattam82/Coq-Equations) 1.3 or later
+- opam:
+    name: coq-stdpp
+    version: '{>= "1.9.0"}'
+  description: |-
+    [Coq-Std++](https://gitlab.mpi-sws.org/iris/stdpp) 1.9.0 or later
 
 tested_coq_opam_versions:
 - version: '8.18'
@@ -60,7 +64,7 @@ build: |-
   
   ```shell
   opam repo add coq-released https://coq.inria.fr/opam/released
-  opam install coq.8.18.0 coq-ott
+  opam install coq.8.18.0 coq-ott coq-equations coq-stdpp
   ```
   
   To build when dependencies are installed, do:
diff --git a/theories/abs_examples.v b/theories/abs_examples.v
new file mode 100644
index 0000000..c21ed60
--- /dev/null
+++ b/theories/abs_examples.v
@@ -0,0 +1,37 @@
+From ABS Require Import abs_defs.
+From stdpp Require Import prelude base.
+
+(** * ABS Examples *)
+
+Definition e_const_5 : e := 
+  e_t (t_int 5%Z).
+
+Definition func_const_5 : F := 
+  F_fn T_int "const_5"%string [] e_const_5.
+
+Definition e_call_const_5 : e :=
+  e_fn_call "const_5"%string [].
+
+Definition Ctx : G :=
+  Map.add ("const_5"%string) (ctxv_sig (sig_sig [] T_int)) (Map.empty ctxv).
+
+Lemma e_const_5_T_int :
+ typ_e Ctx e_const_5 T_int.
+Proof. by apply typ_int. Qed.
+
+Lemma e_call_const_typ_F :
+ typ_F Ctx func_const_5.
+Proof.
+  apply typ_func_decl.
+  - easy.
+  - apply e_const_5_T_int.
+Qed.
+
+Lemma e_call_const_5_T_int :
+ typ_e Ctx e_call_const_5 T_int.
+Proof.
+  unfold e_call_const_5.
+  replace [] with (map (fun (pat_:(e*T)) => match pat_ with (e_,T_) => e_ end ) [])
+    by auto.
+  by apply typ_func_expr.
+Qed.