# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267001772 -3600
# Node ID 35bc8f7b66f8e4ba4279e5b3864b7d30310053cd
# Parent  06f40e1c6982909f5fe5d4bc21df74dc43d3b2bb
parsing of function definitions almost works now; still an error with undefined constants

diff -r 06f40e1c6982 -r 35bc8f7b66f8 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Tue Feb 23 16:32:04 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Feb 24 09:56:12 2010 +0100
@@ -112,8 +112,15 @@
   map raw_dts_aux2 dts
 end
 
+fun get_constrs dts =
+  flat (map (fn (_, _, _, constrs) => map (fn (bn, tys, mx) => (bn, tys, mx)) constrs) dts)
+
 fun get_constr_strs dts =
-  flat (map (fn (_, _, _, constrs) => map (fn (bn, _, _) => Binding.name_of bn) constrs) dts)
+  map (fn (bn, _, _) => Binding.name_of bn) (get_constrs dts)
+
+fun get_constrs2 dts =
+  flat (map (fn (tvrs, tname, _, constrs) => 
+    map (fn (bn, tys, mx) => (bn, tys ---> Type ("Test." ^ Binding.name_of tname, map (fn s => TVar ((s,0),[])) tvrs), mx)) constrs) dts)
 
 fun get_bn_fun_strs bn_funs =
   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
@@ -141,8 +148,7 @@
   val bn_eqs' = map (fn trm => 
     (Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs
 in
-  (*Primrec.add_primrec bn_funs' bn_eqs' lthy*)
-  ((), lthy)
+  Primrec.add_primrec bn_funs' bn_eqs' lthy
 end 
 *}
 
@@ -158,13 +164,14 @@
 end
 *}
 
+
 ML {*
 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy =
 let
   val lthy_tmp = lthy
-    |> (Local_Theory.theory
+    |> Local_Theory.theory
         (Sign.add_types (map (fn ((tvs, tname, mx), _) =>
-          (tname, length tvs, mx)) dt_strs)))
+          (tname, length tvs, mx)) dt_strs))
 
   fun prep_cnstr lthy (((cname, atys), mx), binders) =
     (cname, map (Syntax.read_typ lthy o snd) atys, mx)
@@ -172,16 +179,23 @@
   fun prep_dt lthy ((tvs, tname, mx), cnstrs) = 
     (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
 
-  fun prep_bn_fun lthy (bn, ty_str, mx) =
-    (bn, Option.map (Syntax.read_typ lthy) ty_str, mx) 
+  val dts_prep = map (prep_dt lthy_tmp) dt_strs
 
-  fun prep_bn_eq lthy (attr, trm_str) = Syntax.read_term lthy trm_str
+  val lthy_tmp2 = lthy_tmp
+    |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 dts_prep))
+
+  fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx) 
+
+  fun prep_bn_eq (attr, t) = t
 
-  val dts_prep = map (prep_dt lthy_tmp) dt_strs
-  val bn_fun_prep = map (prep_bn_fun lthy_tmp) bn_fun_strs
-  val bn_eq_prep = map (prep_bn_eq lthy_tmp) bn_eq_strs
+  val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
+  
+  val bn_fun_prep = map prep_bn_fun bn_fun_aux
+  val bn_eq_prep = map prep_bn_eq bn_eq_aux 
+
+  val _ = tracing (cat_lines (map (Syntax.string_of_term lthy_tmp2) bn_eq_prep))
 in
-  nominal_datatype2 dts_prep bn_fun_prep [] lthy |> snd
+  nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
 end
 *}