# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273743299 -3600
# Node ID 24ca435ead1477fe2e5ca094881914388d919708
# Parent  f435d8efd751d411bb3b66b281841ac0ea602b28
added term4 back to the examples

diff -r f435d8efd751 -r 24ca435ead14 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu May 13 07:41:18 2010 +0200
+++ b/Nominal/NewParser.thy	Thu May 13 10:34:59 2010 +0100
@@ -188,7 +188,7 @@
 ML {* print_depth 50 *}
 
 ML {*
-fun prep_bn dt_names dts eqs = 
+fun prep_bn lthy dt_names dts eqs = 
 let
   fun aux eq = 
   let
@@ -205,6 +205,22 @@
     val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
   in
     (dt_index, (bn_fun, (cnstr_head, included)))
+  end
+  fun aux2 eq = 
+  let
+    val (lhs, rhs) = eq
+      |> strip_qnt_body "all" 
+      |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_eq
+    val (bn_fun, [cnstr]) = strip_comb lhs
+    val (_, ty) = dest_Free bn_fun
+    val (ty_name, _) = dest_Type (domain_type ty)
+    val dt_index = find_index (fn x => x = ty_name) dt_names
+    val (cnstr_head, cnstr_args) = strip_comb cnstr
+    val rhs_elements = strip_bn_fun rhs
+    val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
+  in
+    (bn_fun, dt_index, (cnstr_head, included))
   end 
   fun order dts i ts = 
   let
@@ -219,8 +235,12 @@
   val unordered' = map (fn (x, y) =>  (x, AList.group (op=) y)) unordered
   val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
   val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
+
+  val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))
+  val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))
+  val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
 in
-  ordered'
+  ordered' (*map aux2 eqs*)
 end
 *}
 
@@ -254,7 +274,7 @@
    
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
 
-  val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
+  val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
 in
   lthy 
   |> add_datatype_wrapper raw_dt_names raw_dts 
diff -r f435d8efd751 -r 24ca435ead14 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Thu May 13 07:41:18 2010 +0200
+++ b/Nominal/ROOT.ML	Thu May 13 10:34:59 2010 +0100
@@ -14,6 +14,6 @@
     "Ex/ExPS3",
     "Ex/ExPS7",
     "Ex/CoreHaskell",
-    "Ex/Test"(*,
-    "Manual/Term4"*)
+    "Ex/Test",
+    "Manual/Term4"
     ];