--- a/src/HOL/Imperative_HOL/Array.thy Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jun 30 14:54:32 2009 +0200
@@ -1,5 +1,4 @@
-(* Title: HOL/Library/Array.thy
- ID: $Id$
+(* Title: HOL/Imperative_HOL/Array.thy
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 30 14:54:32 2009 +0200
@@ -306,67 +306,75 @@
code_const "Heap_Monad.Fail" (OCaml "Failure")
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
-setup {* let
- open Code_Thingol;
+setup {*
+
+let
- fun lookup naming = the o Code_Thingol.lookup_const naming;
+open Code_Thingol;
+
+fun imp_program naming =
- fun imp_monad_bind'' bind' return' unit' ts =
- let
- val dummy_name = "";
- val dummy_type = ITyVar dummy_name;
- val dummy_case_term = IVar dummy_name;
- (*assumption: dummy values are not relevant for serialization*)
- val unitt = IConst (unit', (([], []), []));
- fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
- | dest_abs (t, ty) =
- let
- val vs = Code_Thingol.fold_varnames cons t [];
- val v = Name.variant vs "x";
- val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
- in ((v, ty'), t `$ IVar v) end;
- fun force (t as IConst (c, _) `$ t') = if c = return'
- then t' else t `$ unitt
- | force t = t `$ unitt;
- fun tr_bind' [(t1, _), (t2, ty2)] =
- let
- val ((v, ty), t) = dest_abs (t2, ty2);
- in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
- and tr_bind'' t = case Code_Thingol.unfold_app t
- of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
- then tr_bind' [(x1, ty1), (x2, ty2)]
- else force t
- | _ => force t;
- in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
- [(unitt, tr_bind' ts)]), dummy_case_term) end
- and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
- of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
- | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
- | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
- else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
- and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
- | imp_monad_bind bind' return' unit' (t as IVar _) = t
- | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
- of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
- | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
- | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
- | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
- (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
+ let
+ fun is_const c = case lookup_const naming c
+ of SOME c' => (fn c'' => c' = c'')
+ | 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_type = ITyVar dummy_name;
+ val dummy_case_term = IVar "";
+ (*assumption: dummy values are not relevant for serialization*)
+ val unitt = case lookup_const naming @{const_name Unity}
+ of SOME unit' => IConst (unit', (([], []), []))
+ | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
+ fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
+ | dest_abs (t, ty) =
+ let
+ 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;
+ fun force (t as IConst (c, _) `$ t') = if is_return c
+ then t' else t `$ unitt
+ | force t = t `$ unitt;
+ fun tr_bind' [(t1, _), (t2, ty2)] =
+ let
+ val ((v, ty), t) = dest_abs (t2, ty2);
+ in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
+ and tr_bind'' t = case unfold_app t
+ of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c
+ 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),
+ [(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)]
+ | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
+ | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
+ else IConst const `$$ map imp_monad_bind ts
+ and imp_monad_bind (IConst const) = imp_monad_bind' const []
+ | imp_monad_bind (t as IVar _) = t
+ | imp_monad_bind (t as _ `$ _) = (case unfold_app t
+ of (IConst const, ts) => imp_monad_bind' const ts
+ | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
+ | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
+ | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
+ (((imp_monad_bind t, ty),
+ (map o pairself) imp_monad_bind pats),
+ imp_monad_bind t0);
- fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
- (imp_monad_bind (lookup naming @{const_name bindM})
- (lookup naming @{const_name return})
- (lookup naming @{const_name Unity}));
+ in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
in
- Code_Target.extend_target ("SML_imp", ("SML", imp_program))
- #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
+Code_Target.extend_target ("SML_imp", ("SML", imp_program))
+#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
end
+
*}
-
code_reserved OCaml Failure raise
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Tue Jun 30 14:54:32 2009 +0200
@@ -1,8 +1,9 @@
(* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy
- Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+ Author: John Matthews, Galois Connections;
+ Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
-header {* Mmonadic imperative HOL with examples *}
+header {* Monadic imperative HOL with examples *}
theory Imperative_HOL_ex
imports Imperative_HOL "ex/Imperative_Quicksort"
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jun 30 14:54:32 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/HOL/MicroJava/BV/BVExample.thy Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Jun 30 14:54:32 2009 +0200
@@ -450,7 +450,7 @@
qed
lemma [code]:
- "iter f step ss w = while (\<lambda>(ss, w). \<not> (is_empty w))
+ "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
(\<lambda>(ss, w).
let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
(ss, w)"
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Jun 30 14:54:32 2009 +0200
@@ -18,7 +18,7 @@
val the_info : theory -> string -> info
val the_descr : theory -> string list
-> descr * (string * sort) list * string list
- * (string list * string list) * (typ list * typ list)
+ * string * (string list * string list) * (typ list * typ list)
val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
val get_constrs : theory -> string -> (string * typ) list option
val get_all : theory -> info Symtab.table
@@ -125,9 +125,10 @@
val names = map Long_Name.base_name (the_default tycos (#alt_names info));
val (auxnames, _) = Name.make_context names
- |> fold_map (yield_singleton Name.variants o name_of_typ) Us
+ |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
+ val prefix = space_implode "_" names;
- in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
+ in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
fun get_constrs thy dtco =
case try (the_spec thy) dtco
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Jun 30 14:54:32 2009 +0200
@@ -11,10 +11,10 @@
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
val ensure_random_typecopy: string -> theory -> theory
- val random_aux_specification: string -> term list -> local_theory -> local_theory
+ val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
-> string list -> string list * string list -> typ list * typ list
- -> string * (term list * (term * term) list)
+ -> term list * (term * term) list
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
val setup: theory -> theory
@@ -184,18 +184,18 @@
end;
-fun random_aux_primrec_multi prefix [eq] lthy =
+fun random_aux_primrec_multi auxname [eq] lthy =
lthy
|> random_aux_primrec eq
|>> (fn simp => [simp])
- | random_aux_primrec_multi prefix (eqs as _ :: _ :: _) lthy =
+ | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
let
val thy = ProofContext.theory_of lthy;
val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs;
val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss;
val Ts = map fastype_of lhss;
val tupleT = foldr1 HOLogic.mk_prodT Ts;
- val aux_lhs = Free ("mutual_" ^ prefix, fastype_of arg --> tupleT) $ arg;
+ val aux_lhs = Free ("mutual_" ^ auxname, fastype_of arg --> tupleT) $ arg;
val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(aux_lhs, foldr1 HOLogic.mk_prod rhss);
fun mk_proj t [T] = [t]
@@ -223,7 +223,7 @@
|-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
end;
-fun random_aux_specification prefix eqs lthy =
+fun random_aux_specification prfx name eqs lthy =
let
val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
o HOLogic.dest_Trueprop o hd) eqs) [];
@@ -237,10 +237,10 @@
val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
- val b = Binding.qualify true prefix (Binding.name "simps");
+ val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
in
lthy
- |> random_aux_primrec_multi prefix proto_eqs
+ |> random_aux_primrec_multi (name ^ prfx) proto_eqs
|-> (fn proto_simps => prove_simps proto_simps)
|-> (fn simps => LocalTheory.note Thm.generatedK ((b,
Code.add_default_eqn_attrib :: map (Attrib.internal o K)
@@ -252,6 +252,8 @@
(* constructing random instances on datatypes *)
+val random_auxN = "random_aux";
+
fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
let
val mk_const = curry (Sign.mk_const thy);
@@ -259,7 +261,6 @@
val i1 = @{term "(i\<Colon>code_numeral) - 1"};
val j = @{term "j\<Colon>code_numeral"};
val seed = @{term "s\<Colon>Random.seed"};
- val random_auxN = "random_aux";
val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
val rTs = Ts @ Us;
@@ -316,10 +317,9 @@
$ seed;
val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
val auxs_rhss = map mk_select gen_exprss;
- val prefix = space_implode "_" (random_auxN :: names);
- in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
+ in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
-fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = DatatypeAux.message config "Creating quickcheck generators ...";
val i = @{term "i\<Colon>code_numeral"};
@@ -329,14 +329,14 @@
else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
$ HOLogic.mk_number @{typ code_numeral} l $ i
| NONE => i;
- val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq
+ val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
(mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
val random_defs = map_index (fn (k, T) => mk_prop_eq
(HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
in
thy
|> TheoryTarget.instantiation (tycos, vs, @{sort random})
- |> random_aux_specification prefix auxs_eqs
+ |> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
Specification.definition (NONE, (Attrib.empty_binding,
@@ -359,7 +359,7 @@
let
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
- val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
+ val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
Datatype.the_descr thy raw_tycos;
val typrep_vs = (map o apsnd)
(curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
@@ -374,7 +374,7 @@
in if has_inst then thy
else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
of SOME constrain => mk_random_datatype config descr
- (map constrain typrep_vs) tycos (names, auxnames)
+ (map constrain typrep_vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;
--- a/src/Pure/Isar/class_target.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Tue Jun 30 14:54:32 2009 +0200
@@ -32,6 +32,7 @@
(*instances*)
val init_instantiation: string list * (string * sort) list * sort
-> theory -> local_theory
+ val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
val instantiation_instance: (local_theory -> local_theory)
-> local_theory -> Proof.state
val prove_instantiation_instance: (Proof.context -> tactic)
@@ -44,7 +45,8 @@
val instantiation_param: local_theory -> binding -> string option
val confirm_declaration: binding -> local_theory -> local_theory
val pretty_instantiation: local_theory -> Pretty.T
- val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
+ val read_multi_arity: theory -> xstring list * xstring list * xstring
+ -> string list * (string * sort) list * sort
val type_name: string -> string
(*subclasses*)
@@ -419,6 +421,15 @@
|> find_first (fn (_, (v, _)) => Binding.name_of b = v)
|> Option.map (fst o fst);
+fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
+ let
+ val all_arities = map (fn raw_tyco => Sign.read_arity thy
+ (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
+ val tycos = map #1 all_arities;
+ val (_, sorts, sort) = hd all_arities;
+ val vs = Name.names Name.context Name.aT sorts;
+ in (tycos, vs, sort) end;
+
(* syntax *)
@@ -578,15 +589,17 @@
(* simplified instantiation interface with no class parameter *)
-fun instance_arity_cmd arities thy =
+fun instance_arity_cmd raw_arities thy =
let
+ val (tycos, vs, sort) = read_multi_arity thy raw_arities;
+ val sorts = map snd vs;
+ val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
fun after_qed results = ProofContext.theory
((fold o fold) AxClass.add_arity results);
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
- o Logic.mk_arities o Sign.read_arity thy) arities)
+ |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
end;
--- a/src/Pure/Isar/isar_syn.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 30 14:54:32 2009 +0200
@@ -465,7 +465,7 @@
val _ =
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
- P.arity >> Class.instance_arity_cmd)
+ P.multi_arity >> Class.instance_arity_cmd)
>> (Toplevel.print oo Toplevel.theory_to_proof)
|| Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
--- a/src/Pure/Isar/theory_target.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Tue Jun 30 14:54:32 2009 +0200
@@ -330,15 +330,6 @@
else I)}
and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
-fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
- let
- val all_arities = map (fn raw_tyco => Sign.read_arity thy
- (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
- val tycos = map #1 all_arities;
- val (_, sorts, sort) = hd all_arities;
- val vs = Name.names Name.context Name.aT sorts;
- in (tycos, vs, sort) end;
-
fun gen_overloading prep_const raw_ops thy =
let
val ctxt = ProofContext.init thy;
@@ -356,7 +347,7 @@
fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
fun instantiation_cmd raw_arities thy =
- instantiation (read_multi_arity thy raw_arities) thy;
+ instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
val overloading_cmd = gen_overloading Syntax.read_term;
--- a/src/Tools/Code/code_haskell.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 30 14:54:32 2009 +0200
@@ -25,10 +25,8 @@
fun pr_haskell_bind pr_term =
let
- fun pr_bind ((NONE, NONE), _) = str "_"
- | pr_bind ((SOME v, NONE), _) = str v
- | pr_bind ((NONE, SOME p), _) = p
- | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
+ 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
@@ -72,9 +70,8 @@
(str o Code_Printer.lookup_var vars) v
| pr_term tyvars thm vars fxy (t as _ `|=> _) =
let
- val (binds, t') = Code_Thingol.unfold_abs t;
- fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
- val (ps, vars') = fold_map pr binds vars;
+ val (binds, t') = Code_Thingol.unfold_pat_abs t;
+ val (ps, vars') = fold_map (pr_bind tyvars thm BR) 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
@@ -103,7 +100,7 @@
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+ |> pr_bind tyvars thm BR (SOME pat, ty)
|>> (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 {")
@@ -114,7 +111,7 @@
let
fun pr (pat, body) =
let
- val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+ val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) 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 "{"])
@@ -240,8 +237,6 @@
end
| pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
let
- val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
- val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
of NONE => semicolon [
@@ -255,7 +250,7 @@
val const = if (is_some o syntax_const) c_inst_name
then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
- val (vs, rhs) = unfold_abs_pure proto_rhs;
+ 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;
@@ -447,16 +442,16 @@
fun pretty_haskell_monad c_bind =
let
- fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
- of SOME (((v, pat), ty), t') =>
- SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+ 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')
| 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 (((NONE, SOME pat), ty), false), tbind), t')
+ SOME ((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 =
--- a/src/Tools/Code/code_ml.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 30 14:54:32 2009 +0200
@@ -94,9 +94,9 @@
[pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
| pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
- val (binds, t') = Code_Thingol.unfold_abs t;
- fun pr ((v, pat), ty) =
- pr_bind is_closure thm NOBR ((SOME v, pat), ty)
+ val (binds, t') = Code_Thingol.unfold_pat_abs t;
+ fun pr (some_pat, ty) =
+ pr_bind is_closure thm NOBR (some_pat, ty)
#>> (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,17 +122,15 @@
:: (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, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+ 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_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 ((NONE, SOME pat), ty)
+ |> pr_bind is_closure thm NOBR (SOME pat, ty)
|>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in
@@ -146,7 +144,7 @@
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+ val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
in
concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
end;
@@ -403,9 +401,8 @@
brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
| pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
- val (binds, t') = Code_Thingol.unfold_abs t;
- fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
- val (ps, vars') = fold_map pr binds vars;
+ val (binds, t') = Code_Thingol.unfold_pat_abs t;
+ val (ps, vars') = fold_map (pr_bind is_closure thm BR) 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)
@@ -427,17 +424,15 @@
:: ((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, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
+ 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_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 ((NONE, SOME pat), ty)
+ |> pr_bind is_closure thm NOBR (SOME pat, ty)
|>> (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;
@@ -449,7 +444,7 @@
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+ val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
in
brackets (
--- a/src/Tools/Code/code_printer.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 30 14:54:32 2009 +0200
@@ -68,10 +68,10 @@
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option)
-> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
- val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
+ val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
-> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
- -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+ -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
val mk_name_module: Name.context -> string option -> (string -> string option)
-> 'a Graph.T -> string -> string
@@ -216,16 +216,14 @@
else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
end;
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
+fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
let
- val vs = case pat
+ val vs = case some_pat
of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
| NONE => [];
- val vars' = intro_vars (the_list v) vars;
- val vars'' = intro_vars vs vars';
- val v' = Option.map (lookup_var vars') v;
- val pat' = Option.map (pr_term thm vars'' fxy) pat;
- in (pr_bind ((v', pat'), ty), vars'') end;
+ 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;
(* mixfix syntax *)
--- a/src/Tools/Code/code_thingol.ML Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 30 14:54:32 2009 +0200
@@ -40,13 +40,12 @@
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 split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
- val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
+ val unfold_abs: iterm -> (vname * 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 unfold_const_app: iterm -> (const * iterm list) option
- val collapse_let: ((vname * itype) * iterm) * iterm
- -> (iterm * itype) * (iterm * iterm) list
val eta_expand: int -> const * iterm list -> iterm
val contains_dictvar: iterm -> bool
val locally_monomorphic: iterm -> bool
@@ -139,14 +138,10 @@
(fn op `$ t => SOME t
| _ => NONE);
-val split_abs =
- (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
- if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
- | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
+val unfold_abs = unfoldr
+ (fn op `|=> t => SOME t
| _ => NONE);
-val unfold_abs = unfoldr split_abs;
-
val split_let =
(fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
| _ => NONE);
@@ -186,17 +181,17 @@
| add vs (ICase (_, t)) = add vs t;
in add [] end;
-fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
- let
- fun exists_v t = fold_unbound_varnames (fn w => fn b =>
- b orelse v = w) t false;
- in if v = w andalso forall (fn (t1, t2) =>
- exists_v t1 orelse not (exists_v t2)) ds
- then ((se, ty), ds)
- else ((se, ty), [(IVar v, be)])
- end
- | collapse_let (((v, ty), se), be) =
- ((se, ty), [(IVar v, be)])
+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);
+
+val unfold_pat_abs = unfoldr split_pat_abs;
fun eta_expand k (c as (_, (_, tys)), ts) =
let