Semantics preservation for removing choice

IlmariReissumies · Feb 5, 2018 · 27b4db4 · 27b4db4
1 parent 5561616
commit 27b4db4
Show file tree

Hide file tree

Showing 2 changed files with 612 additions and 35 deletions.
diff --git a/projection/payload_choiceScript.sml b/projection/payload_choiceScript.sml
@@ -2,36 +2,6 @@ open preamble payloadLangTheory
 
 val _ = new_theory "payload_choice";
 
-val var_names_endpoint_def = Define `
-   (var_names_endpoint Nil = [])
-/\ (var_names_endpoint (Send p v n e) = v::var_names_endpoint e)
-/\ (var_names_endpoint (Receive p v d e) = v::var_names_endpoint e)
-/\ (var_names_endpoint (IntChoice b p e) = var_names_endpoint e)
-/\ (var_names_endpoint (ExtChoice p e1 e2) = var_names_endpoint e1 ++ var_names_endpoint e2)
-/\ (var_names_endpoint (IfThen v e1 e2) = v::var_names_endpoint e1 ++ var_names_endpoint e2)
-/\ (var_names_endpoint (Let v f vl e) = v::vl ++ var_names_endpoint e)
-`
-
-val free_var_names_endpoint_def = Define `
-   (free_var_names_endpoint Nil = [])
-/\ (free_var_names_endpoint (Send p v n e) = v::free_var_names_endpoint e)
-/\ (free_var_names_endpoint (Receive p v d e) = FILTER ($= v) (free_var_names_endpoint e))
-/\ (free_var_names_endpoint (IntChoice b p e) = free_var_names_endpoint e)
-/\ (free_var_names_endpoint (ExtChoice p e1 e2) = free_var_names_endpoint e1 ++ free_var_names_endpoint e2)
-/\ (free_var_names_endpoint (IfThen v e1 e2) = v::free_var_names_endpoint e1 ++ free_var_names_endpoint e2)
-/\ (free_var_names_endpoint (Let v f vl e) = vl ++ FILTER ($= v) (free_var_names_endpoint e))
-`
-
-val var_names_network_def = Define `
-   (var_names_network NNil = [])
-/\ (var_names_network (NEndpoint p s e) = var_names_endpoint e)
-/\ (var_names_network (NPar n1 n2) = var_names_network n1 ++ var_names_network n2)`
-
-val free_var_names_network_def = Define `
-   (free_var_names_network NNil = [])
-/\ (free_var_names_network (NEndpoint p s e) = free_var_names_endpoint e)
-/\ (free_var_names_network (NPar n1 n2) = free_var_names_network n1 ++ free_var_names_network n2)`
-
 val gen_fresh_name_def = Define `
    (gen_fresh_name [] = "a")
 /\ (gen_fresh_name (n::ns) = #"a" :: FOLDR (λe b. if LENGTH e ≥ LENGTH b then e else b) n ns)
@@ -51,12 +21,12 @@ val compile_endpoint_def = Define `
 ∧ (compile_endpoint fv (Let v f vl e) = Let v f vl (compile_endpoint fv e))`
 
 val compile_network_fv_def = Define `
-   (compile_network_fv conf fv payloadLang$NNil = NNil)
-∧ (compile_network_fv conf fv (NPar n1 n2) = NPar (compile_network_fv conf fv n1)
-                                                  (compile_network_fv conf fv n2))
-∧ (compile_network_fv conf fv (NEndpoint p s e) = NEndpoint p s (compile_endpoint fv e))`
+   (compile_network_fv fv payloadLang$NNil = NNil)
+∧ (compile_network_fv fv (NPar n1 n2) = NPar (compile_network_fv fv n1)
+                                                  (compile_network_fv fv n2))
+∧ (compile_network_fv fv (NEndpoint p s e) = NEndpoint p s (compile_endpoint fv e))`
 
 val compile_network_def = Define `
-   compile_network conf n = compile_network_fv conf (gen_fresh_name (var_names_network n)) n`
+   compile_network n = compile_network_fv (gen_fresh_name (var_names_network n)) n`
 
 val _ = export_theory ()