# HG changeset patch # User haftmann # Date 1246392220 -7200 # Node ID bf6207c7444874eae7cec682d590642ca6084f71 # Parent 905a27100f556ee95fa1b495a3782769e2b7b32f# Parent 7d8a89390cbf8d1c30163162c953fee3a4b23f3d merged diff -r 905a27100f55 -r bf6207c74448 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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)] diff -r 905a27100f55 -r bf6207c74448 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- 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 diff -r 905a27100f55 -r bf6207c74448 src/Pure/Isar/code.ML --- 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); diff -r 905a27100f55 -r bf6207c74448 src/Tools/Code/code_haskell.ML --- 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] diff -r 905a27100f55 -r bf6207c74448 src/Tools/Code/code_ml.ML --- 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) diff -r 905a27100f55 -r bf6207c74448 src/Tools/Code/code_printer.ML --- 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 *) diff -r 905a27100f55 -r bf6207c74448 src/Tools/Code/code_thingol.ML --- 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)) diff -r 905a27100f55 -r bf6207c74448 src/Tools/nbe.ML --- 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 _) = []