From bb5dab84859088d70074444cfbf0e51f14e3c782 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 23 Apr 2021 18:29:20 +0200 Subject: Move `$` notation in submodule `ClightNotations` and scope `clight_scope` This avoids a nasty conflict with Ltac2 notations as reported in #392. The old `$` notation in scope `string_scope` was not used yet, AFAIK. The new submodule and the new scope are the right places to add future notations to facilitate working with the output of clightgen. Fixes: #392 --- exportclight/Clightdefs.v | 34 +++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) (limited to 'exportclight/Clightdefs.v') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 8af920df..f96513d1 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -18,6 +18,8 @@ From Coq Require Import Ascii String List ZArith. From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. +(** ** Short names for types *) + Definition tvoid := Tvoid. Definition tschar := Tint I8 Signed noattr. Definition tuchar := Tint I8 Unsigned noattr. @@ -56,6 +58,8 @@ Definition talignas (n: N) (ty: type) := Definition tvolatile_alignas (n: N) (ty: type) := tattr {| attr_volatile := true; attr_alignas := Some n |} ty. +(** ** Constructor for programs and compilation units *) + Definition wf_composites (types: list composite_definition) : Prop := match build_composite_env types with OK _ => True | Error _ => False end. @@ -81,6 +85,8 @@ Definition mkprogram (types: list composite_definition) prog_comp_env := ce; prog_comp_env_eq := EQ |}. +(** ** Encoding character strings as positive numbers *) + (** The following encoding of character strings as positive numbers must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) @@ -169,17 +175,6 @@ Fixpoint ident_of_string (s: string) : ident := | String c s => append_char_pos c (ident_of_string s) end. -(** A convenient notation [$ "ident"] to force evaluation of - [ident_of_string "ident"] *) - -Ltac ident_of_string s := - let x := constr:(ident_of_string s) in - let y := eval compute in x in - exact y. - -Notation "$ s" := (ltac:(ident_of_string s)) - (at level 1, only parsing) : string_scope. - (** The inverse conversion, from encoded strings to strings *) Section DECODE_BITS. @@ -289,3 +284,20 @@ Proof. intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). congruence. Qed. + +(** ** Notations *) + +Module ClightNotations. + +(** A convenient notation [$ "ident"] to force evaluation of + [ident_of_string "ident"] *) + +Ltac ident_of_string s := + let x := constr:(ident_of_string s) in + let y := eval compute in x in + exact y. + +Notation "$ s" := (ltac:(ident_of_string s)) + (at level 1, only parsing) : clight_scope. + +End ClightNotations. -- cgit From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 May 2021 10:46:17 +0200 Subject: Use the LGPL instead of the GPL for dual-licensed files The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. --- exportclight/Clightdefs.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'exportclight/Clightdefs.v') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index f96513d1..708be1cb 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) -- cgit