From 49e1f78a3311d470da3e07f4349d39ee436b8724 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 26 May 2014 15:16:29 -0700
Subject: [PATCH] feat(library/kernel_serializer): add serializer/deserializer
 for inductive decls

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/kernel_serializer.cpp | 40 +++++++++++++++++++++++++++++++
 src/library/kernel_serializer.h   | 11 ++++++---
 2 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 60326a69f..af5227c8a 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -301,4 +301,44 @@ declaration read_declaration(deserializer & d, unsigned module_idx) {
             return mk_var_decl(n, ps, t);
     }
 }
+
+using inductive::inductive_decl;
+using inductive::intro_rule;
+using inductive::inductive_decl_name;
+using inductive::inductive_decl_type;
+using inductive::inductive_decl_intros;
+using inductive::intro_rule_name;
+using inductive::intro_rule_type;
+
+serializer & operator<<(serializer & s, inductive_decls const & ds) {
+    s << std::get<0>(ds) << std::get<1>(ds);
+    auto const & ls = std::get<2>(ds);
+    s << length(ls);
+    for (inductive_decl const & d : ls) {
+        s << inductive_decl_name(d) << inductive_decl_type(d) << length(inductive_decl_intros(d));
+        for (intro_rule const & r : inductive_decl_intros(d))
+            s << intro_rule_name(r) << intro_rule_type(r);
+    }
+    return s;
+}
+
+inductive_decls read_inductive_decls(deserializer & d) {
+    level_param_names ps = read_level_params(d);
+    unsigned num_params, num_decls;
+    d >> num_params >> num_decls;
+    buffer<inductive_decl> decls;
+    for (unsigned i = 0; i < num_decls; i++) {
+        name d_name = read_name(d);
+        expr d_type = read_expr(d);
+        unsigned num_intros = d.read_unsigned();
+        buffer<intro_rule> rules;
+        for (unsigned j = 0; j < num_intros; j++) {
+            name r_name = read_name(d);
+            expr r_type = read_expr(d);
+            rules.push_back(intro_rule(r_name, r_type));
+        }
+        decls.push_back(inductive_decl(d_name, d_type, to_list(rules.begin(), rules.end())));
+    }
+    return inductive_decls(ps, num_params, to_list(decls.begin(), decls.end()));
+}
 }
diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h
index 9dfaa1953..cfa06f8f6 100644
--- a/src/library/kernel_serializer.h
+++ b/src/library/kernel_serializer.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/serializer.h"
 #include "kernel/declaration.h"
+#include "kernel/inductive/inductive.h"
 
 namespace lean {
 serializer & operator<<(serializer & s, level const & l);
@@ -21,11 +22,15 @@ serializer & operator<<(serializer & s, expr const & e);
 expr read_expr(deserializer & d);
 inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
 
-serializer & operator<<(serializer & s, declaration const & d);
-declaration read_declaration(deserializer & d, unsigned module_idx);
-
 void register_macro_deserializer(std::string const & k, macro_definition_cell::reader rd);
 struct register_macro_deserializer_fn {
     register_macro_deserializer_fn(std::string const & k, macro_definition_cell::reader rd) { register_macro_deserializer(k, rd); }
 };
+
+serializer & operator<<(serializer & s, declaration const & d);
+declaration read_declaration(deserializer & d, unsigned module_idx);
+
+typedef std::tuple<level_param_names, unsigned, list<inductive::inductive_decl>> inductive_decls;
+serializer & operator<<(serializer & s, inductive_decls const & ds);
+inductive_decls read_inductive_decls(deserializer & d);
 }