version 1.0.3 compatible with metacoq 1.0~beta1+8.11

vzaliva · Sep 22, 2020 · 1015cd2 · 1015cd2
1 parent db7dd15
commit 1015cd2
Show file tree

Hide file tree

Showing 5 changed files with 36 additions and 35 deletions.
diff --git a/.gitignore b/.gitignore
@@ -32,3 +32,4 @@ nra.cache
 /.coqdeps.d
 /Makefile.coq
 /Makefile.coq.conf
+/theories/*.vos
diff --git a/README.md b/README.md
@@ -73,7 +73,7 @@ template program `mkSwitch` providing the following parameters:
 For example, running:
 
 ```
- Run TemplateProgram
+ MetaCoq Run
      (mkSwitch nat
                beq_nat
                [(0,"Love") ; (10,"Ten") ; (20, "twenty")]

diff --git a/coq-switch.opam b/coq-switch.opam
@@ -12,12 +12,12 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.10.2"}
-  "coq-metacoq-template" {>= "1.0~alpha2+8.10"}
+  "coq" {>= "8.11.2"}
+  "coq-metacoq-template" {>= "1.0~beta1+8.11"}
 ]
 tags: [
   "category:Miscellaneous/Coq Extensions"
-  "date:2020-03-13"
+  "date:2020-09-22"
   "logpath:Switch"
 ]
 synopsis: "A plugin to implement functionality similar to `switch` statement in C language."
@@ -29,7 +29,7 @@ an inductive type with constructors, one for each of the choices, and
 a function mapping values to this type."""
 
 url {
-  src: "https://github.com/vzaliva/coq-switch/archive/v1.0.2.tar.gz"
-  checksum: "51ad3d8d53edb2334854d8bc976b75ed"
+  src: "https://github.com/vzaliva/coq-switch/archive/v1.0.3.tar.gz"
+  checksum: ""
 }
 
diff --git a/demo.v b/demo.v
@@ -11,7 +11,7 @@ Section NatExample.
 
   (* This example uses standard list notation for choices *)
 
-  Run TemplateProgram
+MetaCoq Run
       (mkSwitch nat
                 beq_nat
                 [(0,"Love") ; (10,"Ten") ; (20, "twenty")]
@@ -40,7 +40,7 @@ Section StringExample.
   (* This example custom -> notation for choices *)
   Infix "->" := pair.
 
-  Run TemplateProgram
+  MetaCoq Run
       (mkSwitch string string_beq [
                   "love" -> "SLove" ;
                 "ten" -> "STen"  ;

diff --git a/theories/Switch.v b/theories/Switch.v
@@ -7,42 +7,43 @@ Import ListNotations.
 
 Open Scope string_scope.
 
-
 Fixpoint mkSwitchCases
-         (type_name: string)
+         (type_name: kername)
          (A_t: term)
          (P_t: term)
          (choices_t: list term)
          (n: nat) : term :=
   let ind_0 n := {| inductive_mind := n; inductive_ind := 0 |} in
   let T_i := ind_0 type_name in
-  let bool_i := ind_0 "Coq.Init.Datatypes.bool" in
-  let opt_i := ind_0 "Coq.Init.Datatypes.option" in
+
+  let bool_i := ind_0 (MPfile ["Datatypes"; "Init"; "Coq"], "bool") in
+  let opt_i := ind_0 (MPfile ["Datatypes"; "Init"; "Coq"], "option") in
   match choices_t with
   | [] => tApp (tConstruct opt_i 1 []) [tInd T_i []]
-
   | (x::xs) => tCase
-                (* # of parameters *)
-                (bool_i, 0)
+               (* # of parameters *)
+               (bool_i, 0)
 
-                (* type info *)
-                (tLambda (nNamed "b") (tInd bool_i []) (tApp (tInd opt_i []) [tInd T_i []]))
+               (* type info *)
+               (tLambda (nNamed "b") (tInd bool_i []) (tApp (tInd opt_i []) [tInd T_i []]))
 
-                (* discriminee *)
-                (tApp P_t [tRel 0; x])
+               (* discriminee *)
+               (tApp P_t [tRel 0; x])
 
-                (* branches *)
-                [
-                  (0, tApp (tConstruct opt_i 0 []) [tInd T_i []; tConstruct T_i n []]) ;
-                    (0, mkSwitchCases type_name A_t P_t xs (S n))
-                ]
+               (* branches *)
+               [
+                 (0, tApp (tConstruct opt_i 0 []) [tInd T_i []; tConstruct T_i n []]) ;
+               (0, mkSwitchCases type_name A_t P_t xs (S n))
+               ]
   end.
 
+
 Definition mkSwitch
            (A: Type)
            (P: A -> A -> bool)
            (choices: list (A*string))
-           (type_name: string) (def_name: string): TemplateMonad unit
+           (type_name: string)
+           (def_name: string): TemplateMonad unit
   :=
     let one_i : one_inductive_entry :=
         {|
@@ -61,14 +62,13 @@ Definition mkSwitch
           mind_entry_variance  := None;
           mind_entry_private   := None (* or (Some false)? *)
         |} in
+    mp <- tmCurrentModPath tt ;;
     ind_t <- tmMkInductive ind ;;
-          T <- tmUnquoteTyped Type (tInd {| inductive_mind := type_name; inductive_ind := 0 |} []) ;;
-          A_t <- tmQuote A ;;
-          P_t <- tmQuote P ;;
-          choices_t <- monad_map (fun x => tmQuote (fst x)) choices ;;
-          let body_t := tLambda (nNamed "x") A_t (mkSwitchCases type_name A_t P_t choices_t 0) in
-          body <- tmUnquoteTyped (A -> option T) body_t ;;
-               def_t <- tmDefinition def_name body ;;
-               tmReturn tt.
-
-
+    T <- tmUnquoteTyped Type (tInd {| inductive_mind := (mp, type_name); inductive_ind := 0 |} []) ;;
+    A_t <- tmQuote A ;;
+    P_t <- tmQuote P ;;
+    choices_t <- monad_map (fun x => tmQuote (fst x)) choices ;;
+    let body_t := tLambda (nNamed "x") A_t (mkSwitchCases (mp, type_name) A_t P_t choices_t 0) in
+    body <- tmUnquoteTyped (A -> option T) body_t ;;
+    def_t <- tmDefinition def_name body ;;
+    tmReturn tt.