Permalink
Browse files

Started a "compact_closed" theory

  • Loading branch information...
wetneb committed Apr 12, 2015
1 parent 76aa66c commit ec408cda207e37b4dd128d3a3e3bbf7f339b7f51
View
@@ -22,6 +22,11 @@ ML_file "theories/ghz_w/io.ML";
ML_file "theories/ghz_w/theory.ML";
(*ML_file "theories/ghz_w/test/test.ML";*)
+(* Graphs have Epsilon/Eta nodes and strings as data *)
+ML_file "theories/compact_closed/data.ML";
+ML_file "theories/compact_closed/io.ML";
+ML_file "theories/compact_closed/theory.ML";
+
(* Graphs having vertices with strings as data, substring as matching *)
ML_file "theories/substrings/data.ML";
ML_file "theories/substrings/io.ML";
@@ -0,0 +1,36 @@
+structure EE_Data =
+struct
+ val pretty_theory_name = Pretty.str "compact_closed"
+ type psubst = unit
+ type subst = unit
+
+ datatype nvdata = EEnd (* Epsilon/Eta node *)
+ | Var of string
+ val default_nvdata = Var ""
+
+ fun init_psubst_from_data _ _ = ()
+
+ fun default_nvdata_of_typestring s =
+ case s of "EEnd" => EEnd
+ | "var" => Var ""
+ | _ => raise unknown_typestring_exp s
+
+ fun nvdata_eq (EEnd, EEnd) = true
+ | nvdata_eq (Var s, Var t) = (s = t)
+ | nvdata_eq _ = false
+
+ fun pretty_nvdata EEnd =
+ Pretty.str "EE"
+ | pretty_nvdata (Var s) = Pretty.block [Pretty.str "Var(", Pretty.str s, Pretty.str ")"]
+
+ fun match_nvdata (EEnd, EEnd) m = SOME m
+ | match_nvdata (Var s, Var t) m = if s = t then SOME m else NONE
+ | match_nvdata _ _ = NONE
+
+ fun subst_in_nvdata sub EEnd = (sub, EEnd)
+ | subst_in_nvdata sub (Var s) = (sub, Var s)
+
+ open EmptyEdgeData
+
+ val solve_psubst = Seq.single
+end
@@ -0,0 +1,56 @@
+(* Data input for red-green graphs. The input strives to be as backward-compatible
+ * as possible, while output always outputs the newest format. As a consequence,
+ * the old Quantomatic GUI will no longer talk to the core. *)
+
+structure EE_ComponentDataIO : GRAPH_COMPONENT_DATA_IO
+= struct
+ type nvdata = EE_Data.nvdata
+ type edata = EE_Data.edata
+
+ structure IVDataInputJSON : INPUT_JSON =
+ struct
+ open JsonInputUtils
+ type data = nvdata
+ val to_lower = String.implode o (map Char.toLower) o String.explode
+ fun input (Json.String t) =
+ (case to_lower t
+ of "ee" => EE_Data.EEnd
+ | "var" => EE_Data.Var ""
+ | _ => raise bad_input_exp ("Unknown vertex type "^t,""))
+ | input (Json.Object obj) =
+ (case to_lower (get_string obj "type")
+ of "ee" => EE_Data.EEnd
+ | "var" => EE_Data.Var (case Json.lookup obj "value"
+ of SOME (Json.String s) => s
+ | NONE => "")
+ | t => raise bad_input_exp ("Unknown vertex type "^t,"type"))
+ | input _ = raise bad_input_exp ("Expected object","")
+ end
+ structure IVDataOutputJSON : OUTPUT_JSON =
+ struct
+ open JsonOutputUtils
+ type data = nvdata
+ fun output EE_Data.EEnd =
+ Json.Object (
+ Json.empty_obj |> update ("type",Json.String "EE")
+ )
+ | output (EE_Data.Var s) =
+ Json.Object (
+ Json.empty_obj |> update ("type", Json.String "var")
+ |> update ("value", Json.String s)
+ )
+ end
+ structure EDataInputJSON = InputUnitJSON
+ structure EDataOutputJSON = OutputUnitJSON
+
+ structure DotStyle : DOT_STYLE =
+ struct
+ type nvdata = nvdata
+ fun style_for_ivertex_data (EE_Data.Var _) =
+ "[style=filled,fillcolor=white,fontcolor=black,shape=circle]"
+ | style_for_ivertex_data EE_Data.EEnd =
+ "[style=filled,fillcolor=yellow,fontcolor=white,shape=square]"
+ end
+end
+
+
@@ -0,0 +1,7 @@
+
+
+structure EE_Theory = GraphicalTheory(
+ structure Data = EE_Data
+ structure DataIO = EE_ComponentDataIO)
+
+

0 comments on commit ec408cd

Please sign in to comment.