Commit f2082e90 authored by Robbert Krebbers's avatar Robbert Krebbers

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).
parent 6a054461
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment