Merge pull request #2 from vzaliva/coq-8.18

coq-8.18 port

coq-switch.opam

@@ -12,8 +12,8 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.13.0"}
-  "coq-metacoq-template" {>= "1.0~beta2+8.13"}
+  "coq" {>= "8.18.0"}
+  "coq-metacoq-template" {>= "1.2.1+8.18"}
 ]
 tags: [
   "category:Miscellaneous/Coq Extensions"

demo.v

@@ -6,14 +6,15 @@ Require Import Coq.Lists.List.
 Require Import MetaCoq.Template.All.
 
 Import ListNotations.
+Open Scope string_scope.
 
 Section NatExample.
 
   (* This example uses standard list notation for choices *)
 
 MetaCoq Run
       (mkSwitch nat
-                beq_nat
+                Nat.eqb
                 [(0,"Love") ; (10,"Ten") ; (20, "twenty")]
                 "Ex1_Choices" "ex1_select"
       ).
@@ -43,18 +44,18 @@ Section StringExample.
   Infix "->" := pair.
 
   MetaCoq Run
-      (mkSwitch string string_beq [
-                  "love" -> "SLove" ;
-                "ten" -> "STen"  ;
-                "twenty" -> "STwenty"
+      (mkSwitch String.string string_beq [
+                  "love"   -> "SLove" ;
+                  "ten"    -> "STen"  ;
+                  "twenty" -> "STwenty"
                 ] "Ex2_Choices" "ex2_select"
       ).
 
   Print Ex2_Choices.
   Print ex2_select.
 
 
-  Definition Ex2 (s:string) : nat :=
+  Definition Ex2 (s:String.string) : nat :=
     match ex2_select s with
     | Some SLove => 100
     | Some STen => 110

theories/Switch.v

@@ -1,11 +1,10 @@
-Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import MetaCoq.Template.All.
 
-Import MonadNotation.
 Import ListNotations.
+Import MCMonadNotation.
 
-Open Scope string_scope.
+Open Scope bs_scope.
 
 Definition rname (s:string) := {| binder_name := nNamed s; binder_relevance := Relevant |}.
 
@@ -18,41 +17,43 @@ Fixpoint mkSwitchCases
   let ind_0 n := {| inductive_mind := n; inductive_ind := 0 |} in
   let T_i := ind_0 type_name in
 
-  let bool_i := ind_0 (MPfile ["Datatypes"; "Init"; "Coq"], "bool") 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), Relevant)
+               (mk_case_info bool_i 0 Relevant)
 
                (* type info *)
-               (tLambda (rname "b") (tInd bool_i []) (tApp (tInd opt_i []) [tInd T_i []]))
+               (mk_predicate [] [] [mkBindAnn nAnon Relevant] (tApp (tInd opt_i []) [tInd T_i []]))
 
                (* 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))
+                 mk_branch [] (tApp (tConstruct opt_i 0 []) [tInd T_i []; tConstruct T_i n []]);
+                 mk_branch [] (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
+           (choices: list (A*String.string))
+           (type_name: String.string)
+           (def_name: String.string): TemplateMonad unit
   :=
+  let choices' := map (fun '(a, s) => (a, String.of_string s)) choices in
+  let type_name' := String.of_string type_name in
+  let def_name' := String.of_string def_name in
     let one_i : one_inductive_entry :=
         {|
-          mind_entry_typename := type_name ;
+          mind_entry_typename := type_name' ;
           mind_entry_arity := tSort Universe.type0 ;
-          mind_entry_consnames := map snd choices ;
-          mind_entry_lc := map (fun _ => tRel 0) choices;
+          mind_entry_consnames := map snd choices' ;
+          mind_entry_lc := map (fun _ => tRel 0) choices';
         |} in
     let ind:mutual_inductive_entry := {|
           mind_entry_record    := None ;
@@ -65,12 +66,12 @@ Definition mkSwitch
           mind_entry_private   := None (* or (Some false)? *)
         |} in
     mp <- tmCurrentModPath tt ;;
-    ind_t <- tmMkInductive ind ;;
-    T <- tmUnquoteTyped Type (tInd {| inductive_mind := (mp, type_name); inductive_ind := 0 |} []) ;;
+    ind_t <- tmMkInductive false ind ;;
+    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 (rname "x") A_t (mkSwitchCases (mp, type_name) A_t P_t choices_t 0) in
+    choices_t <- monad_map (fun x => tmQuote (fst x)) choices' ;;
+    let body_t := tLambda (rname "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 ;;
+    def_t <- tmDefinition def_name' body ;;
     tmReturn tt.