# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264606816 -3600
# Node ID cc5d18c784464f6194373163d284636b4e39054b
# Parent  362402adfb882831ffb5ddd6845d14f4eb807df2
Parsing of the input as terms and types, and passing them as such to the function package.

diff -r 362402adfb88 -r cc5d18c78446 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Jan 27 16:07:49 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 16:40:16 2010 +0100
@@ -82,9 +82,9 @@
   | print_str_option (SOME s) = (s:bstring)
 *}
 
-ML {* 
-fun print_anno_typ (NONE, ty) = ty
-  | print_anno_typ (SOME x, ty) = x ^ ":" ^ ty     
+ML {*
+fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
+  | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
 *}
 
 ML {*
@@ -93,39 +93,51 @@
 *}
 
 ML {*
-fun print_constr (((name, anno_tys), bds), syn) =
-  (Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ "   " 
-   ^ (commas (map print_bind bds)) ^ "  "  
+fun print_constr lthy (((name, anno_tys), bds), syn) =
+  (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ "   "
+   ^ (commas (map print_bind bds)) ^ "  "
    ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
 *}
 
 ML Local_Theory.exit_global
 
+(* TODO: replace with proper thing *)
 ML {*
-fun fv_constr prefix (((name, anno_tys), bds), syn) =
-  prefix ^ " (" ^ (Binding.name_of name) ^ ") = "
+fun is_atom ty = Binding.name_of ty = "name"
 *}
 
 ML {*
-fun single_dt (((s2, s3), syn), constrs) =
+fun fv_constr lthy prefix (((name, anno_tys), bds), syn) =
+let
+  fun prepare_name (NONE, ty) = ("", ty)
+    | prepare_name (SOME n, ty) = (n, ty);
+  val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys));
+  val var_strs = map (Syntax.string_of_term lthy) vars;
+in
+  prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = "
+end
+*}
+
+ML {*
+fun single_dt lthy (((s2, s3), syn), constrs) =
    ["constructor declaration"]
  @ ["type arguments: "] @ s2 
  @ ["datatype name: ", Binding.name_of s3] 
  @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
- @ ["constructors: "] @ (map print_constr constrs)
+ @ ["constructors: "] @ (map (print_constr lthy) constrs)
  |> separate "\n"
  |> implode
 *}
 
 ML {*
-fun fv_dt (((s2, s3), syn), constrs) =
-    map (fv_constr ("fv_" ^ Binding.name_of s3)) constrs
+fun fv_dt lthy (((s2, s3), syn), constrs) =
+    map (fv_constr lthy ("fv_" ^ Binding.name_of s3)) constrs
  |> separate "\n"
  |> implode
 *}
 
-ML {* fun single_fun_eq (at, s) = 
-  ["function equations: ", s] 
+ML {* fun single_fun_eq lthy (at, s) = 
+  ["function equations: ", (Syntax.string_of_term lthy s)] 
   |> separate "\n"
   |> implode
 *}
@@ -137,12 +149,12 @@
 *}
 
 ML {*
-fun print_dts (dts, (funs, feqs)) lthy = 
+fun print_dts (dts, (funs, feqs)) lthy =
 let
-  val _ = warning (implode (separate "\n" (map single_dt dts)))
-  val _ = warning (implode (separate "\n" (map single_fun_fix funs)))
-  val _ = warning (implode (separate "\n" (map single_fun_eq feqs)))
-  val _ = warning (implode (separate "\n" (map fv_dt dts)))
+  val _ = warning (implode (separate "\n" (map (single_dt lthy) dts)));
+  val _ = warning (implode (separate "\n" (map single_fun_fix funs)));
+  val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs)));
+  val _ = warning (implode (separate "\n" (map (fv_dt lthy) dts)));
 in
   lthy
 end   
@@ -176,17 +188,30 @@
 ML {*
 fun fn_defn [] [] lthy = lthy
   | fn_defn funs feqs lthy =
-      Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
+      Function_Fun.add_fun  Function_Common.default_config funs feqs false lthy
 *}
 
-
 ML {*
 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
-   dt_defn (map transp_dt dts) thy
-|> Theory_Target.init NONE
-|> fn_defn funs feqs
+let
+  val thy' = dt_defn (map transp_dt dts) thy
+  val lthy = Theory_Target.init NONE thy'
+  fun parse_fun (b, NONE, m) = (b, NONE, m)
+    | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m);
+  val funs = map parse_fun funs
+  fun parse_feq (b, t) = (b, Syntax.read_prop lthy t);
+  val feqs = map parse_feq feqs
+  fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy ty);
+  fun parse_constr (((constr_name, ty_args), bind), mx) =
+    (((constr_name, map parse_anno_ty ty_args), bind), mx);
+  fun parse_dt (((ty_args, ty_name), mx), constrs) =
+   (((ty_args, ty_name), mx), map parse_constr constrs);
+  val dts = map parse_dt dts
+in
+   fn_defn funs feqs lthy
 |> print_dts (dts, (funs, feqs))
 |> Local_Theory.exit_global
+end
 *}
 
 (* Command Keyword *)