--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 30 21:51:44 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 30 22:03:40 2009 +0200
@@ -320,9 +320,9 @@
| NONE => K false;
val is_bindM = is_const @{const_name bindM};
val is_return = is_const @{const_name return};
- val dummy_name = "X";
+ val dummy_name = "";
val dummy_type = ITyVar dummy_name;
- val dummy_case_term = IVar "";
+ val dummy_case_term = IVar NONE;
(*assumption: dummy values are not relevant for serialization*)
val unitt = case lookup_const naming @{const_name Unity}
of SOME unit' => IConst (unit', (([], []), []))
@@ -333,7 +333,7 @@
val vs = fold_varnames cons t [];
val v = Name.variant vs "x";
val ty' = (hd o fst o unfold_fun) ty;
- in ((v, ty'), t `$ IVar v) end;
+ in ((SOME v, ty'), t `$ IVar (SOME v)) end;
fun force (t as IConst (c, _) `$ t') = if is_return c
then t' else t `$ unitt
| force t = t `$ unitt;
@@ -346,7 +346,7 @@
then tr_bind' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
- fun imp_monad_bind'' ts = (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
+ fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
[(unitt, tr_bind' ts)]), dummy_case_term)
and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 21:51:44 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 22:03:40 2009 +0200
@@ -631,9 +631,9 @@
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
-(*export_code qsort in SML_imp module_name QSort*)
+export_code qsort in SML_imp module_name QSort
export_code qsort in OCaml module_name QSort file -
-(*export_code qsort in OCaml_imp module_name QSort file -*)
+export_code qsort in OCaml_imp module_name QSort file -
export_code qsort in Haskell module_name QSort file -
end
\ No newline at end of file
--- a/src/Pure/Isar/code.ML Tue Jun 30 21:51:44 2009 +0200
+++ b/src/Pure/Isar/code.ML Tue Jun 30 22:03:40 2009 +0200
@@ -75,7 +75,7 @@
val these_eqns: theory -> string -> (thm * bool) list
val all_eqns: theory -> (thm * bool) list
val get_case_scheme: theory -> string -> (int * (int * string list)) option
- val is_undefined: theory -> string -> bool
+ val undefineds: theory -> string list
val print_codesetup: theory -> unit
end;
@@ -898,7 +898,7 @@
fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
-val is_undefined = Symtab.defined o snd o the_cases o the_exec;
+val undefineds = Symtab.keys o snd o the_cases o the_exec;
structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
--- a/src/Tools/Code/code_haskell.ML Tue Jun 30 21:51:44 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 30 22:03:40 2009 +0200
@@ -23,12 +23,6 @@
(** Haskell serializer **)
-fun pr_haskell_bind pr_term =
- let
- fun pr_bind (NONE, _) = str "_"
- | pr_bind (SOME p, _) = p;
- in gen_pr_bind pr_bind pr_term end;
-
fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
init_syms deresolve is_cons contr_classparam_typs deriving_show =
let
@@ -66,12 +60,14 @@
pr_term tyvars thm vars NOBR t1,
pr_term tyvars thm vars BR t2
])
- | pr_term tyvars thm vars fxy (IVar v) =
+ | pr_term tyvars thm vars fxy (IVar NONE) =
+ str "_"
+ | pr_term tyvars thm vars fxy (IVar (SOME v)) =
(str o Code_Printer.lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
- val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars;
+ val (ps, vars') = fold_map (pr_bind tyvars thm BR o fst) binds vars;
in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
| pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
@@ -94,13 +90,13 @@
else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
end
and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
- and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
+ and pr_bind tyvars thm fxy p = gen_pr_bind (pr_term tyvars) thm fxy p
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind tyvars thm BR (SOME pat, ty)
+ |> pr_bind tyvars thm BR pat
|>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in brackify_block fxy (str "let {")
@@ -111,7 +107,7 @@
let
fun pr (pat, body) =
let
- val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars;
+ val (p, vars') = pr_bind tyvars thm NOBR pat vars;
in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
in brackify_block fxy
(concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
@@ -253,7 +249,7 @@
val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
val vars = init_syms
|> Code_Printer.intro_vars (the_list const)
- |> Code_Printer.intro_vars vs;
+ |> Code_Printer.intro_vars (map_filter I vs);
val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
@@ -443,29 +439,29 @@
fun pretty_haskell_monad c_bind =
let
fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
- of SOME ((some_pat, ty), t') =>
- SOME ((SOME ((some_pat, ty), true), t1), t')
+ of SOME ((pat, ty), t') =>
+ SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
if c = c_bind_name then dest_bind t1 t2
else NONE
| dest_monad _ t = case Code_Thingol.split_let t
of SOME (((pat, ty), tbind), t') =>
- SOME ((SOME ((SOME pat, ty), false), tbind), t')
+ SOME ((SOME ((pat, ty), false), tbind), t')
| NONE => NONE;
fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
fun pr_monad pr_bind pr (NONE, t) vars =
(semicolon [pr vars NOBR t], vars)
- | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
+ | pr_monad pr_bind pr (SOME ((bind, _), true), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
- | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
+ | pr_monad pr_bind pr (SOME ((bind, _), false), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
val (binds, t'') = implode_monad c_bind' t'
- val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
+ val (ps, vars') = fold_map (pr_monad (gen_pr_bind (K pr) thm) pr) (bind :: binds) vars;
in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
| NONE => brackify_infix (1, L) fxy
[pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
--- a/src/Tools/Code/code_ml.ML Tue Jun 30 21:51:44 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 30 22:03:40 2009 +0200
@@ -85,7 +85,9 @@
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
- | pr_term is_closure thm vars fxy (IVar v) =
+ | pr_term is_closure thm vars fxy (IVar NONE) =
+ str "_"
+ | pr_term is_closure thm vars fxy (IVar (SOME v)) =
str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
@@ -95,8 +97,8 @@
| pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
- fun pr (some_pat, ty) =
- pr_bind is_closure thm NOBR (some_pat, ty)
+ fun pr (pat, ty) =
+ pr_bind is_closure thm NOBR pat
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map pr binds vars;
in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
@@ -122,15 +124,13 @@
:: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
syntax_const thm vars
- and pr_bind' (NONE, _) = str "_"
- | pr_bind' (SOME p, _) = p
- and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
+ and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind is_closure thm NOBR (SOME pat, ty)
+ |> pr_bind is_closure thm NOBR pat
|>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in
@@ -144,7 +144,7 @@
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
+ val (p, vars') = pr_bind is_closure thm NOBR pat vars;
in
concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
end;
@@ -392,7 +392,9 @@
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
fun pr_term is_closure thm vars fxy (IConst c) =
pr_app is_closure thm vars fxy (c, [])
- | pr_term is_closure thm vars fxy (IVar v) =
+ | pr_term is_closure thm vars fxy (IVar NONE) =
+ str "_"
+ | pr_term is_closure thm vars fxy (IVar (SOME v)) =
str (Code_Printer.lookup_var vars v)
| pr_term is_closure thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
@@ -402,7 +404,7 @@
| pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
- val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
+ val (ps, vars') = fold_map (pr_bind is_closure thm BR o fst) binds vars;
in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
| pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
@@ -424,15 +426,13 @@
:: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
syntax_const
- and pr_bind' (NONE, _) = str "_"
- | pr_bind' (SOME p, _) = p
- and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
+ and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind is_closure thm NOBR (SOME pat, ty)
+ |> pr_bind is_closure thm NOBR pat
|>> (fn p => concat
[str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
@@ -444,7 +444,7 @@
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
+ val (p, vars') = pr_bind is_closure thm NOBR pat vars;
in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
in
brackets (
@@ -459,7 +459,7 @@
fun fish_params vars eqs =
let
fun fish_param _ (w as SOME _) = w
- | fish_param (IVar v) NONE = SOME v
+ | fish_param (IVar (SOME v)) NONE = SOME v
| fish_param _ NONE = NONE;
fun fillup_param _ (_, SOME v) = v
| fillup_param x (i, NONE) = x ^ string_of_int i;
@@ -776,7 +776,7 @@
val eqs = filter (snd o snd) raw_eqs;
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
- then ([(([IVar "x"], t `$ IVar "x"), thm)], false)
+ then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
else (eqs, not (Code_Thingol.fold_constnames
(fn name' => fn b => b orelse name = name') t false))
| _ => (eqs, false)
--- a/src/Tools/Code/code_printer.ML Tue Jun 30 21:51:44 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 30 22:03:40 2009 +0200
@@ -68,10 +68,9 @@
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option)
-> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
- val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
- -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
+ val gen_pr_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
- -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
+ -> iterm -> var_ctxt -> Pretty.T * var_ctxt
val mk_name_module: Name.context -> string option -> (string -> string option)
-> 'a Graph.T -> string -> string
@@ -216,14 +215,11 @@
else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
end;
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
+fun gen_pr_bind pr_term thm (fxy : fixity) pat vars =
let
- val vs = case some_pat
- of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
- | NONE => [];
+ val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
val vars' = intro_vars vs vars;
- val some_pat' = Option.map (pr_term thm vars' fxy) some_pat;
- in (pr_bind (some_pat', ty), vars') end;
+ in (pr_term thm vars' fxy pat, vars') end;
(* mixfix syntax *)
--- a/src/Tools/Code/code_thingol.ML Tue Jun 30 21:51:44 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 30 22:03:40 2009 +0200
@@ -23,13 +23,13 @@
type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
datatype iterm =
IConst of const
- | IVar of vname
+ | IVar of vname option
| `$ of iterm * iterm
- | `|=> of (vname * itype) * iterm
+ | `|=> of (vname option * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*((term, type), [(selector pattern, body term )]), primitive term)*)
val `$$ : iterm * iterm list -> iterm;
- val `|==> : (vname * itype) list * iterm -> iterm;
+ val `|==> : (vname option * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
end;
@@ -40,11 +40,11 @@
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
val unfold_fun: itype -> itype list * itype
val unfold_app: iterm -> iterm * iterm list
- val unfold_abs: iterm -> (vname * itype) list * iterm
+ val unfold_abs: iterm -> (vname option * itype) list * iterm
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
- val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option
- val unfold_pat_abs: iterm -> (iterm option * itype) list * iterm
+ val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
+ val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
val unfold_const_app: iterm -> (const * iterm list) option
val eta_expand: int -> const * iterm list -> iterm
val contains_dictvar: iterm -> bool
@@ -125,9 +125,9 @@
datatype iterm =
IConst of const
- | IVar of vname
+ | IVar of vname option
| `$ of iterm * iterm
- | `|=> of (vname * itype) * iterm
+ | `|=> of (vname option * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*see also signature*)
@@ -167,39 +167,55 @@
fun fold_varnames f =
let
- fun add (IVar v) = f v
- | add ((v, _) `|=> _) = f v
+ fun add (IVar (SOME v)) = f v
+ | add ((SOME v, _) `|=> _) = f v
| add _ = I;
in fold_aiterms add end;
fun fold_unbound_varnames f =
let
fun add _ (IConst _) = I
- | add vs (IVar v) = if not (member (op =) vs v) then f v else I
+ | add vs (IVar (SOME v)) = if not (member (op =) vs v) then f v else I
+ | add _ (IVar NONE) = I
| add vs (t1 `$ t2) = add vs t1 #> add vs t2
- | add vs ((v, _) `|=> t) = add (insert (op =) v vs) t
- | add vs (ICase (_, t)) = add vs t;
+ | add vs ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
+ | add vs ((NONE, _) `|=> t) = add vs t
+ | add vs (ICase (((t, _), ds), _)) = add vs t #> fold (add_case vs) ds
+ and add_case vs (p, t) = add (fold_varnames (insert (op =)) p vs) t;
in add [] end;
fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
-val split_pat_abs = (fn (v, ty) `|=> t => (case t
- of ICase (((IVar w, _), [(p, t')]), _) =>
- if v = w andalso (exists_var p v orelse not (exists_var t' v))
- then SOME ((SOME p, ty), t')
- else SOME ((SOME (IVar v), ty), t)
- | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t))
- | _ => NONE);
+fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
+ | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
+ of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
+ if v = w andalso (exists_var p v orelse not (exists_var t' v))
+ then ((p, ty), t')
+ else ((IVar (SOME v), ty), t)
+ | _ => ((IVar (SOME v), ty), t))
+ | split_pat_abs _ = NONE;
val unfold_pat_abs = unfoldr split_pat_abs;
+fun unfold_abs_eta [] t = ([], t)
+ | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
+ let
+ val (vs_tys, t') = unfold_abs_eta tys t;
+ in (v_ty :: vs_tys, t') end
+ | unfold_abs_eta tys t =
+ let
+ val ctxt = fold_varnames Name.declare t Name.context;
+ val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
+ in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
+
fun eta_expand k (c as (_, (_, tys)), ts) =
let
val j = length ts;
val l = k - j;
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
- val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
- in vs_tys `|==> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
+ val vs_tys = (map o apfst) SOME
+ (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
+ in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dictvar t =
let
@@ -569,14 +585,16 @@
and translate_term thy algbr funcgr thm (Const (c, ty)) =
translate_app thy algbr funcgr thm ((c, ty), [])
| translate_term thy algbr funcgr thm (Free (v, _)) =
- pair (IVar v)
+ pair (IVar (SOME v))
| translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
let
val (v, t) = Syntax.variant_abs abs;
+ val v' = if member (op =) (Term.add_free_names t []) v
+ then SOME v else NONE
in
translate_typ thy algbr funcgr ty
##>> translate_term thy algbr funcgr thm t
- #>> (fn (ty, t) => (v, ty) `|=> t)
+ #>> (fn (ty, t) => (v', ty) `|=> t)
end
| translate_term thy algbr funcgr thm (t as _ $ _) =
case strip_comb t
@@ -613,45 +631,37 @@
#>> (fn (t, ts) => t `$$ ts)
and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
- val (tys, _) = (chop num_args o fst o strip_type o snd) c_ty;
- val t = nth ts t_pos;
+ fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
+ val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
- val ts_clause = nth_drop t_pos ts;
- fun mk_clause (co, num_co_args) t =
+ fun mk_constr c t = let val n = Code.no_args thy c
+ in ((c, arg_types (Code.no_args thy c) (fastype_of t) ---> ty), n) end;
+ val constrs = if null case_pats then []
+ else map2 mk_constr case_pats (nth_drop t_pos ts);
+ fun casify naming constrs ty ts =
let
- val (vs, body) = Term.strip_abs_eta num_co_args t;
- val not_undefined = case body
- of (Const (c, _)) => not (Code.is_undefined thy c)
- | _ => true;
- val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
- in (not_undefined, (pat, body)) end;
- val clauses = if null case_pats then let val ([v_ty], body) =
- Term.strip_abs_eta 1 (the_single ts_clause)
- in [(true, (Free v_ty, body))] end
- else map (uncurry mk_clause)
- (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
- fun retermify ty (_, (IVar x, body)) =
- (x, ty) `|=> body
- | retermify _ (_, (pat, body)) =
+ val t = nth ts t_pos;
+ val ts_clause = nth_drop t_pos ts;
+ val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
+ fun mk_clause ((constr as IConst (_, (_, tys)), n), t) =
let
- val (IConst (_, (_, tys)), ts) = unfold_app pat;
- val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
- in vs `|==> body end;
- fun mk_icase const t ty clauses =
- let
- val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
- in
- ICase (((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses),
- const `$$ (ts1 @ t :: ts2))
- end;
+ val (vs, t') = unfold_abs_eta (curry Library.take n tys) t;
+ val is_undefined = case t
+ of IConst (c, _) => member (op =) undefineds c
+ | _ => false;
+ in if is_undefined then NONE else SOME (constr `$$ map (IVar o fst) vs, t') end;
+ val clauses = if null case_pats then let val ([(v, _)], t) =
+ unfold_abs_eta [ty] (the_single ts_clause)
+ in [(IVar v, t)] end
+ else map_filter mk_clause (constrs ~~ ts_clause);
+ in ((t, ty), clauses) end;
in
translate_const thy algbr funcgr thm c_ty
- ##>> translate_term thy algbr funcgr thm t
+ ##>> fold_map (fn (constr, n) => translate_const thy algbr funcgr thm constr #>> rpair n) constrs
##>> translate_typ thy algbr funcgr ty
- ##>> fold_map (fn (b, (pat, body)) => translate_term thy algbr funcgr thm pat
- ##>> translate_term thy algbr funcgr thm body
- #>> pair b) clauses
- #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
+ ##>> fold_map (translate_term thy algbr funcgr thm) ts
+ #-> (fn (((t, constrs), ty), ts) =>
+ `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
end
and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
@@ -663,7 +673,7 @@
in
fold_map (translate_typ thy algbr funcgr) tys
##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
- #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|==> t)
+ #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
end
else if length ts > num_args then
translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
--- a/src/Tools/nbe.ML Tue Jun 30 21:51:44 2009 +0200
+++ b/src/Tools/nbe.ML Tue Jun 30 22:03:40 2009 +0200
@@ -135,6 +135,8 @@
| nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
+fun nbe_bound_optional NONE = "_"
+ | nbe_bound_optional (SOME v) = nbe_bound v;
fun nbe_default v = "w_" ^ v;
(*note: these three are the "turning spots" where proper argument order is established!*)
@@ -191,9 +193,9 @@
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
- | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
+ | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
- nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
+ nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
| of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
nbe_apps (ml_cases (of_iterm NONE t)
(map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
@@ -212,8 +214,9 @@
else pair (v, [])) vs names;
val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
fun subst_vars (t as IConst _) samepairs = (t, samepairs)
- | subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v
- of SOME v' => (IVar v', AList.delete (op =) v samepairs)
+ | subst_vars (t as IVar NONE) samepairs = (t, samepairs)
+ | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v
+ of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs)
| NONE => (t, samepairs))
| subst_vars (t1 `$ t2) samepairs = samepairs
|> subst_vars t1
@@ -295,7 +298,8 @@
val params = Name.invent_list [] "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))]));
+ [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+ IVar (SOME (nth params k)))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]