From f2082e90b633866ffa7a452021ae7be115422374 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 21:43:47 +0100
Subject: [PATCH] Make language notations stable under simpl.
Before they were not, for example:
Check ('10 + '10 )%L. (* prints ('10 + '10)%L *)
Eval simpl in ('10 + '10 )%L. (* prints (Lit 10 + Lit 10)%L *)
The notation added by this comment is ambigious, for example the
notation '10 + '10 is used for both:
BinOp PlusOp (Lit (LitNat 10)) (Lit (LitNat 10))
BinOp PlusOp (of_val (LitV (LitNat 10))) (of_val (LitV (LitNat 10)))
But fortunatelly, these terms are convertible.
Note that literals 'x are now parsed as values (as a LitV), but still
pretty printed when they appear as expressions (as a Lit).
---
heap_lang/notation.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index f7ff70f72..72aa0f2eb 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -15,6 +15,7 @@ Coercion of_val : val >-> expr.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* What about Arguments for hoare triples?. *)
+Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope.
Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
--
GitLab