From 3ea3c04b729433ad3bebc5cff934ca2fabcb95c0 Mon Sep 17 00:00:00 2001
From: Cesar Roux Dit Buisson <cr1013@imperial.ac.uk>
Date: Fri, 11 Sep 2015 14:04:50 +0100
Subject: [PATCH] Add automatic annotation of ml
---
Makefile | 1 +
generator/tests/lambda/Lambda.ml | 28 ++++++++++++++--------------
ml-add-cstr-annots.pl | 25 +++++++++++++++++++++++++
3 files changed, 40 insertions(+), 14 deletions(-)
create mode 100755 ml-add-cstr-annots.pl
diff --git a/Makefile b/Makefile
index 3b2872f..dfdb659 100644
--- a/Makefile
+++ b/Makefile
@@ -7,3 +7,4 @@ fresh_interp:
$(MAKE) -C .. extract_interpreter
cp ../interp/src/*.ml{,i} ../interp/src/extract/*.ml{,i} src
./convert-ml-strings.pl -i.bak src/*
+ ./ml-add-cstr-annots.pl src/*.ml
diff --git a/generator/tests/lambda/Lambda.ml b/generator/tests/lambda/Lambda.ml
index 4929701..a3d81c6 100644
--- a/generator/tests/lambda/Lambda.ml
+++ b/generator/tests/lambda/Lambda.ml
@@ -5,16 +5,16 @@ open LibVar
open Specif
type coq_val =
-| Coq_val_int of coq_Z
-| Coq_val_clo of Variables.var * trm
-| Coq_val_err
+| Coq_val_int [@f label0] of coq_Z (** Auto Generated Attributes **)
+| Coq_val_clo [@f label0 label1] of Variables.var * trm (** Auto Generated Attributes **)
+| Coq_val_err [@f] (** Auto Generated Attributes **)
and trm =
-| Coq_trm_val of coq_val
-| Coq_trm_var of Variables.var
-| Coq_trm_abs of Variables.var * trm
-| Coq_trm_app of trm * trm
-| Coq_trm_try of trm * trm
-| Coq_trm_raise of trm
+| Coq_trm_val [@f label0] of coq_val (** Auto Generated Attributes **)
+| Coq_trm_var [@f label0] of Variables.var (** Auto Generated Attributes **)
+| Coq_trm_abs [@f label0 label1] of Variables.var * trm (** Auto Generated Attributes **)
+| Coq_trm_app [@f label0 label1] of trm * trm (** Auto Generated Attributes **)
+| Coq_trm_try [@f label0 label1] of trm * trm (** Auto Generated Attributes **)
+| Coq_trm_raise [@f label0] of trm (** Auto Generated Attributes **)
(** val subst : Variables.var -> coq_val -> trm -> trm **)
@@ -36,13 +36,13 @@ let rec subst x v t =
| Coq_trm_raise t1 -> Coq_trm_raise (s t1))
type beh =
-| Coq_beh_ret of coq_val
-| Coq_beh_exn of coq_val
-| Coq_beh_err
+| Coq_beh_ret [@f label0] of coq_val (** Auto Generated Attributes **)
+| Coq_beh_exn [@f label0] of coq_val (** Auto Generated Attributes **)
+| Coq_beh_err [@f] (** Auto Generated Attributes **)
type res =
-| Coq_res_return of beh
-| Coq_res_bottom
+| Coq_res_return [@f label0] of beh (** Auto Generated Attributes **)
+| Coq_res_bottom [@f] (** Auto Generated Attributes **)
(** val if_success : res -> (coq_val -> res) -> res **)
diff --git a/ml-add-cstr-annots.pl b/ml-add-cstr-annots.pl
new file mode 100755
index 0000000..5d2d3af
--- /dev/null
+++ b/ml-add-cstr-annots.pl
@@ -0,0 +1,25 @@
+#!/usr/bin/perl
+# An attempt at automatic annotation generation for OCaml files.
+# Takes multiple filenames as input.
+
+foreach $fname (@ARGV) {
+
+ open(FILE, "< $fname") or die("Could not open $fname\n");
+ open(NEW, "> $fname.temp");
+ while($line = <FILE>) {
+ if ($line =~ m/^(?!.*\[.*?\])(?!.*->)(\s*\|.*?)(of (.*))?$/) {
+ $no = split(/\*/, $3);
+ $annot = " [\@f";
+ for (my $i=0; $i < $no; $i++) {
+ $annot = $annot . " label" . $i . "";
+ }
+ $annot = $annot . "] ";
+ print NEW $1 . $annot . $2 . " (** Auto Generated Attributes **)\n";
+ } else {
+ print NEW $line;
+ }
+ }
+ close(FILE);
+ close(NEW);
+ rename("$fname.temp", $fname) or die "can't rename $fname.temp to $fname: $!";
+}
\ No newline at end of file
--
GitLab