From 919796a75a4515a76e3a5236a839175abe7b32d9 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Fri, 8 Dec 2023 23:17:19 +0000 Subject: [PATCH 1/3] coq-8.18 port --- coq-switch.opam | 4 ++-- demo.v | 18 +++++++++--------- theories/Switch.v | 21 +++++++++------------ 3 files changed, 20 insertions(+), 23 deletions(-) diff --git a/coq-switch.opam b/coq-switch.opam index 0f244bf..bad69c6 100644 --- a/coq-switch.opam +++ b/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" diff --git a/demo.v b/demo.v index 246a3e9..8179189 100644 --- a/demo.v +++ b/demo.v @@ -13,9 +13,9 @@ Section NatExample. MetaCoq Run (mkSwitch nat - beq_nat - [(0,"Love") ; (10,"Ten") ; (20, "twenty")] - "Ex1_Choices" "ex1_select" + Nat.eqb + [(0,"Love"%bs) ; (10,"Ten"%bs) ; (20, "twenty"%bs)] + "Ex1_Choices"%bs "ex1_select"%bs ). Print Ex1_Choices. @@ -43,18 +43,18 @@ Section StringExample. Infix "->" := pair. MetaCoq Run - (mkSwitch string string_beq [ - "love" -> "SLove" ; - "ten" -> "STen" ; - "twenty" -> "STwenty" - ] "Ex2_Choices" "ex2_select" + (mkSwitch String.string string_beq [ + "love"%string -> "SLove"%bs ; + "ten"%string -> "STen"%bs ; + "twenty"%string -> "STwenty"%bs + ] "Ex2_Choices"%bs "ex2_select"%bs ). 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 diff --git a/theories/Switch.v b/theories/Switch.v index 655c12a..66bd9ed 100644 --- a/theories/Switch.v +++ b/theories/Switch.v @@ -1,11 +1,8 @@ -Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import MetaCoq.Template.All. -Import MonadNotation. Import ListNotations. - -Open Scope string_scope. +Import MCMonadNotation. Definition rname (s:string) := {| binder_name := nNamed s; binder_relevance := Relevant |}. @@ -18,24 +15,24 @@ 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 opt_i := ind_0 (MPfile ["Datatypes"; "Init"; "Coq"], "option") in + let bool_i := ind_0 (MPfile ["Datatypes"%bs; "Init"%bs ; "Coq"%bs], "bool"%bs) in + let opt_i := ind_0 (MPfile ["Datatypes"%bs; "Init"%bs; "Coq"%bs], "option"%bs) 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. @@ -65,12 +62,12 @@ Definition mkSwitch mind_entry_private := None (* or (Some false)? *) |} in mp <- tmCurrentModPath tt ;; - ind_t <- tmMkInductive ind ;; + 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 + let body_t := tLambda (rname "x"%bs) 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. From 8bd2425e776c88bbea67ce4e8d62aafb34cb114b Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Sat, 9 Dec 2023 01:04:45 +0000 Subject: [PATCH 2/3] open bytestrings scope This allows not to specify `%bs` everywhere --- demo.v | 12 ++++++------ theories/Switch.v | 8 +++++--- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/demo.v b/demo.v index 8179189..d38a905 100644 --- a/demo.v +++ b/demo.v @@ -14,8 +14,8 @@ Section NatExample. MetaCoq Run (mkSwitch nat Nat.eqb - [(0,"Love"%bs) ; (10,"Ten"%bs) ; (20, "twenty"%bs)] - "Ex1_Choices"%bs "ex1_select"%bs + [(0,"Love") ; (10,"Ten") ; (20, "twenty")] + "Ex1_Choices" "ex1_select" ). Print Ex1_Choices. @@ -44,10 +44,10 @@ Section StringExample. MetaCoq Run (mkSwitch String.string string_beq [ - "love"%string -> "SLove"%bs ; - "ten"%string -> "STen"%bs ; - "twenty"%string -> "STwenty"%bs - ] "Ex2_Choices"%bs "ex2_select"%bs + "love"%string -> "SLove" ; + "ten"%string -> "STen" ; + "twenty"%string -> "STwenty" + ] "Ex2_Choices" "ex2_select" ). Print Ex2_Choices. diff --git a/theories/Switch.v b/theories/Switch.v index 66bd9ed..08337a9 100644 --- a/theories/Switch.v +++ b/theories/Switch.v @@ -4,6 +4,8 @@ Require Import MetaCoq.Template.All. Import ListNotations. Import MCMonadNotation. +Open Scope bs_scope. + Definition rname (s:string) := {| binder_name := nNamed s; binder_relevance := Relevant |}. Fixpoint mkSwitchCases @@ -15,8 +17,8 @@ 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"%bs; "Init"%bs ; "Coq"%bs], "bool"%bs) in - let opt_i := ind_0 (MPfile ["Datatypes"%bs; "Init"%bs; "Coq"%bs], "option"%bs) 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 @@ -67,7 +69,7 @@ Definition mkSwitch A_t <- tmQuote A ;; P_t <- tmQuote P ;; choices_t <- monad_map (fun x => tmQuote (fst x)) choices ;; - let body_t := tLambda (rname "x"%bs) A_t (mkSwitchCases (mp, type_name) A_t P_t choices_t 0) in + 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 ;; tmReturn tt. From 6021d08d953693b86fc3b3149e5dbcf281dca2dd Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Sat, 9 Dec 2023 01:19:45 +0000 Subject: [PATCH 3/3] ask user to provide name of type constructors as strings instead of bytestrings --- demo.v | 7 ++++--- theories/Switch.v | 24 +++++++++++++----------- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/demo.v b/demo.v index d38a905..52f08ed 100644 --- a/demo.v +++ b/demo.v @@ -6,6 +6,7 @@ Require Import Coq.Lists.List. Require Import MetaCoq.Template.All. Import ListNotations. +Open Scope string_scope. Section NatExample. @@ -44,9 +45,9 @@ Section StringExample. MetaCoq Run (mkSwitch String.string string_beq [ - "love"%string -> "SLove" ; - "ten"%string -> "STen" ; - "twenty"%string -> "STwenty" + "love" -> "SLove" ; + "ten" -> "STen" ; + "twenty" -> "STwenty" ] "Ex2_Choices" "ex2_select" ). diff --git a/theories/Switch.v b/theories/Switch.v index 08337a9..135febf 100644 --- a/theories/Switch.v +++ b/theories/Switch.v @@ -38,20 +38,22 @@ Fixpoint mkSwitchCases ] 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,11 +67,11 @@ Definition mkSwitch |} in mp <- tmCurrentModPath tt ;; ind_t <- tmMkInductive false ind ;; - T <- tmUnquoteTyped Type (tInd {| inductive_mind := (mp, type_name); inductive_ind := 0 |} []) ;; + 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.