From fbcc27ca1bd3801beac0338e657b933d6a9c8f95 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Thu, 27 Dec 2018 12:19:44 +0000
Subject: refactor val-spec AST to store externs as an assoc-list rather than a
 function (preparing for marshalling)

---
 language/sail.ott | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'language/sail.ott')

diff --git a/language/sail.ott b/language/sail.ott
index 59d51d68..5c8b6a01 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -943,8 +943,8 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::=
 
 val_spec_aux :: 'VS_' ::=
   {{ com value type specification }}
-  {{ ocaml  VS_val_spec of typschm * id * (string -> string option) * bool }}
-  {{ lem VS_val_spec of typschm * id * (string -> maybe string) * bool }}
+  {{ ocaml  VS_val_spec of typschm * id * (string * string) list * bool }}
+  {{ lem VS_val_spec of typschm * id * list (string * string) * bool }}
   | val typschm id                                  :: S :: val_spec
     {{ com specify the type of an upcoming definition }}
     {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }}
-- 
cgit v1.2.3


From 1f421b865a87a161a82550443a0cf39aa2642d9c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 15 Apr 2019 12:08:28 +0100
Subject: Basic loop termination measures for Coq Currently only supports pure
 termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
---
 language/sail.ott | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'language/sail.ott')

diff --git a/language/sail.ott b/language/sail.ott
index 1a3148d0..1956f339 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -494,6 +494,13 @@ loop :: loop ::= {{ phantom }}
   | while ::   :: while 
   | until ::  :: until 
 
+internal_loop_measure :: 'Measure_' ::=
+  {{ com internal syntax for an optional termination measure for a loop }}
+  {{ auxparam 'a }}
+  {{ aux _ l }}
+  |                               :: :: none
+  | 'termination_measure' { exp } :: :: some
+
 exp :: 'E_' ::=
   {{ com expression }}
   {{ aux _ annot }} {{ auxparam 'a }}  
@@ -529,10 +536,10 @@ exp :: 'E_' ::=
     {{ com conditional }}
 
   | if exp1 then exp2                                   :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
-  | loop exp1 exp2 :: :: loop
-  | while exp1 do exp2  :: S :: while        {{ ichlo [[ loop while exp1 exp2 ]] }}
-  | repeat exp1 until exp2 :: S :: until      {{ ichlo [[ loop until exp2 exp1 ]] }}
-  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for {{ com loop }}
+  | loop internal_loop_measure exp1 exp2                    :: :: loop
+  | while internal_loop_measure exp1 do exp2                :: S :: while {{ ichlo [[ loop internal_loop_measure while exp1 exp2 ]] }}
+  | repeat internal_loop_measure exp1 until exp2            :: S :: until {{ ichlo [[ loop internal_loop_measure until exp2 exp1 ]] }}
+  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for   {{ com loop }}
 
 % vectors
   | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
@@ -894,6 +901,10 @@ prec :: '' ::=
    | infixl :: :: InfixL
    | infixr :: :: InfixR
 
+loop_measure :: '' ::=
+   {{ auxparam 'a }}
+   | loop exp :: :: Loop
+
 def :: 'DEF_' ::=
   {{ com top-level definition }}
   {{ auxparam 'a }}
@@ -917,6 +928,8 @@ def :: 'DEF_' ::=
     {{ com scattered function and type definition }}
   | 'termination_measure' id pat = exp                 :: :: measure
     {{ com separate termination measure declaration }}
+  | 'termination_measure' id loop_measure1 , .. , loop_measuren :: :: loop_measures
+    {{ com separate termination measure declaration }}
   | dec_spec                                           :: :: reg_dec
     {{ com register declaration }}
   | fundef1 .. fundefn                                 :: I :: internal_mutrec
-- 
cgit v1.2.3