--- a/src/Tools/Code/code_haskell.ML Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 30 17:33:30 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 "{"])
@@ -251,11 +247,10 @@
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) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
- val vs' = map the vs;
val vars = init_syms
|> Code_Printer.intro_vars (the_list const)
- |> Code_Printer.intro_vars vs';
- val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar 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
semicolon [
@@ -444,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 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 30 17:33:30 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 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 30 17:33:30 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 16:43:28 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 30 17:33:30 2009 +0200
@@ -23,7 +23,7 @@
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 option * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
@@ -43,8 +43,8 @@
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,7 +125,7 @@
datatype iterm =
IConst of const
- | IVar of vname
+ | IVar of vname option
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
@@ -167,7 +167,7 @@
fun fold_varnames f =
let
- fun add (IVar v) = f v
+ fun add (IVar (SOME v)) = f v
| add ((SOME v, _) `|=> _) = f v
| add _ = I;
in fold_aiterms add end;
@@ -175,7 +175,8 @@
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 ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
| add vs ((NONE, _) `|=> t) = add vs t
@@ -185,13 +186,13 @@
fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
-fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((NONE, ty), t)
+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 w, _), [(p, t')]), _) =>
+ of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
if v = w andalso (exists_var p v orelse not (exists_var t' v))
- then ((SOME p, ty), t')
- else ((SOME (IVar v), ty), t)
- | _ => ((SOME (IVar v), ty), t))
+ 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;
@@ -201,8 +202,9 @@
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 (map o apfst) SOME vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) 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
@@ -572,7 +574,7 @@
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;
@@ -635,12 +637,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)) =
- (SOME 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 => (SOME 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
@@ -658,6 +660,39 @@
#>> pair b) clauses
#>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
end
+
+(*and translate_case' thy algbr funcgr thm case_scheme (c_ty, ts) =
+ let
+ fun casify ts tys =
+ let
+ val t = nth ts t_pos;
+ val ty = nth tys t_pos;
+ val ts_clause = nth_drop t_pos ts;
+ fun strip_abs_eta t [] = t
+ | strip_abs_eta ((`|=>
+
+ 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)
+ | _ => 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);
+
+ 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) => ICase (casify 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
--- a/src/Tools/nbe.ML Tue Jun 30 16:43:28 2009 +0200
+++ b/src/Tools/nbe.ML Tue Jun 30 17:33:30 2009 +0200
@@ -193,7 +193,7 @@
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_optional v]) (of_iterm NONE t))) ts
| of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
@@ -214,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
@@ -297,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 _) =
[]