# HG changeset patch # User haftmann # Date 1246379043 -7200 # Node ID 3404c8cb9e144ff81e642e8c925bfea81049cff2 # Parent 39bff8d9b032c861818cd3606739d910ce349ec4# Parent e943b039f0ac3ba09175bdb2d7c8be6f2742e25c merged diff -r 39bff8d9b032 -r 3404c8cb9e14 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 15:58:12 2009 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 18:24:03 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 39bff8d9b032 -r 3404c8cb9e14 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jun 30 15:58:12 2009 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 30 18:24:03 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 39bff8d9b032 -r 3404c8cb9e14 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Jun 30 15:58:12 2009 +0200 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 30 18:24:03 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 39bff8d9b032 -r 3404c8cb9e14 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jun 30 15:58:12 2009 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Jun 30 18:24:03 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 39bff8d9b032 -r 3404c8cb9e14 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Tue Jun 30 15:58:12 2009 +0200 +++ b/src/Tools/Code/code_printer.ML Tue Jun 30 18:24:03 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 39bff8d9b032 -r 3404c8cb9e14 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jun 30 15:58:12 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 30 18:24:03 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 @@ -617,11 +635,12 @@ val t = nth ts t_pos; val ty = nth tys t_pos; val ts_clause = nth_drop t_pos ts; + val undefineds = Code.undefineds thy; fun mk_clause (co, num_co_args) t = 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) + of (Const (c, _)) => not (member (op =) undefineds c) | _ => true; val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs); in (not_undefined, (pat, body)) end; @@ -630,12 +649,12 @@ 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 + fun retermify ty (_, (IVar v, body)) = + (v, ty) `|=> body | retermify _ (_, (pat, body)) = let val (IConst (_, (_, tys)), ts) = unfold_app pat; - val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys; + val vs = map2 (fn IVar v => fn ty => (v, ty)) ts tys; in vs `|==> body end; fun mk_icase const t ty clauses = let @@ -653,6 +672,45 @@ #>> pair b) clauses #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds) end + +(*and translate_case' thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) = + let + fun casify naming ts tys = + let + val t = nth ts t_pos; + val ty = nth tys t_pos; + val ts_clause = nth_drop t_pos ts; + val tyss_clause = map (fst o unfold_fun) (nth_drop t_pos tys); + + val undefineds = map_filter (lookup_const naming) (*Code.undefineds thy*) []; + + fun mk_clause co (tys, t) = + let + val (vs, t') = unfold_abs_eta tys t; + val is_undefined = case t + of Const (c, _) => member (op =) undefineds c + | _ => false; + in if is_undefined then NONE else (_, t) end; + + 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, _)], t) = + unfold_abs_eta (the_single tyss_clause) (the_single ts_clause) + in [(IVar v, t)] end + else map2 mk_clause case_pats (tyss_clause ~~ ts_clause); + + in ((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses) end; + in + translate_const thy algbr funcgr thm c_ty + ##>> fold_map (translate_term thy algbr funcgr thm) ts + #-> (fn (t as IConst (c, (_, tys)), ts) => + `(fn (naming, _) => pair (ICase (casify naming ts tys, 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 let @@ -663,7 +721,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 39bff8d9b032 -r 3404c8cb9e14 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Jun 30 15:58:12 2009 +0200 +++ b/src/Tools/nbe.ML Tue Jun 30 18:24:03 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 _) = []