global state setters generation

Makefile

@@ -1,3 +1,5 @@
+PYTHON=python2.7
+
 all: Makefile.coq
 	+$(MAKE) -f Makefile.coq all
 
@@ -8,6 +10,9 @@ clean: Makefile.coq
 Makefile.coq: _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
+theories/GlobalState.v: theories/GlobalState.v.rec
+	$(PYTHON) script/extract_record_notation.py theories/GlobalState.v.rec GState > theories/GlobalState.v
+
 _CoqProject Makefile: ;
 
 %: Makefile.coq

scripts/extract_record_notation.py

@@ -0,0 +1,51 @@
+# This is the hackiest thing, but it will come in handy.
+
+import sys
+import re
+
+file_name = sys.argv[1]
+record_name = sys.argv[2]
+
+file = open(file_name).read()
+
+comment_regex = r'\(\*.*\*\)'
+record_regex = r'(Record %s.*\{(.*)\}\.)' % record_name
+record_sep = ';'
+field_name_regex = r'\s*(\w+)\s*:\s*'
+#field_name_regex = r'\s*(\w+)\s*:\D+'
+variable_regex = r'Variable ([^.]*)\.'
+
+n_variables = len(re.findall(variable_regex, file))
+
+uncommented_file = re.sub(comment_regex, '', file)
+fields = re.search(record_regex, uncommented_file, re.DOTALL).group(2).split(record_sep)
+field_names = [re.match(field_name_regex, field).group(1) for field in fields]
+
+setters = ""
+notations = ""
+arguments = ""
+variables = ' _' * n_variables
+
+constructor_name = "mk" + record_name[0].upper() + record_name[1:]
+
+for field_name in field_names:
+    setters += "\n\nDefinition set_%s_%s a v := %s" % (record_name,field_name,constructor_name)
+    for fn in field_names:
+        if fn == field_name:
+            setters += " v"
+        else:
+            setters += " (%s a)" % fn
+    setters += "."
+
+    notations += "\n\nNotation \"{[ a 'with' '%s' := v ]}\" := (set_%s_%s %s a v)." % (field_name, record_name,field_name,variables)
+    arguments += "\n\nArguments set_%s_%s %s/." % (record_name, field_name, " _" * (n_variables + 2))
+
+setters += "\n"
+
+lines = file.split("\n")
+
+print "\n".join(lines[:-2])
+print setters
+print "\n".join(lines[-2:])
+print notations
+print arguments

theories/GlobalState.v

@@ -0,0 +1,58 @@
+(* Remember to re-run
+   python2 scripts/extract_record_notation.py theories/GlobalState.v.rec GState > theories/GlobalState.v
+   after editing this file!
+   Running `make theories/GlobalState.v` should take care of this for you. *)
+
+From mathcomp.ssreflect
+Require Import all_ssreflect.
+
+From mathcomp.finmap
+Require Import finmap multiset.
+
+Require Import Coq.Reals.Reals.
+From Algorand Require Import Rstruct.
+
+Section GlobalState.
+
+Variable UserId : choiceType.
+Variable UState : Type.
+Variable Msg : choiceType.
+
+Record GState :=
+  mkGState {
+    now : R ;
+    network_partition : bool ;
+    users : @finmap_of UserId UState (Phant _) ;
+    msg_in_transit : @finmap_of UserId (@multiset_of _ (Phant (R * Msg))) (Phant _)
+  }.
+
+
+
+Definition set_GState_now a v := mkGState v (network_partition a) (users a) (msg_in_transit a).
+
+Definition set_GState_network_partition a v := mkGState (now a) v (users a) (msg_in_transit a).
+
+Definition set_GState_users a v := mkGState (now a) (network_partition a) v (msg_in_transit a).
+
+Definition set_GState_msg_in_transit a v := mkGState (now a) (network_partition a) (users a) v.
+
+End GlobalState.
+
+
+
+Notation "{[ a 'with' 'now' := v ]}" := (set_GState_now  _ _ _ a v).
+
+Notation "{[ a 'with' 'network_partition' := v ]}" := (set_GState_network_partition  _ _ _ a v).
+
+Notation "{[ a 'with' 'users' := v ]}" := (set_GState_users  _ _ _ a v).
+
+Notation "{[ a 'with' 'msg_in_transit' := v ]}" := (set_GState_msg_in_transit  _ _ _ a v).
+
+
+Arguments set_GState_now  _ _ _ _ _/.
+
+Arguments set_GState_network_partition  _ _ _ _ _/.
+
+Arguments set_GState_users  _ _ _ _ _/.
+
+Arguments set_GState_msg_in_transit  _ _ _ _ _/.

theories/GlobalState.v.rec

@@ -0,0 +1,29 @@
+(* Remember to re-run
+   python2 scripts/extract_record_notation.py theories/GlobalState.v.rec GState > theories/GlobalState.v
+   after editing this file!
+   Running `make theories/GlobalState.v` should take care of this for you. *)
+
+From mathcomp.ssreflect
+Require Import all_ssreflect.
+
+From mathcomp.finmap
+Require Import finmap multiset.
+
+Require Import Coq.Reals.Reals.
+From Algorand Require Import Rstruct.
+
+Section GlobalState.
+
+Variable UserId : choiceType.
+Variable UState : Type.
+Variable Msg : choiceType.
+
+Record GState :=
+  mkGState {
+    now : R ;
+    network_partition : bool ;
+    users : @finmap_of UserId UState (Phant _) ;
+    msg_in_transit : @finmap_of UserId (@multiset_of _ (Phant (R * Msg))) (Phant _)
+  }.
+
+End GlobalState.