--- a/src/HOL/IsaMakefile Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 19 18:08:44 2005 +0200
@@ -114,10 +114,10 @@
blastdata.ML cladata.ML \
Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
Tools/res_axioms.ML Tools/res_types_sorts.ML \
- Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
+ Tools/ATP/recon_prelim.ML Tools/ATP/recon_order_clauses.ML\
Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \
Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
- Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \
+ Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \
Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\
document/root.tex hologic.ML simpdata.ML thy_syntax.ML
@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
--- a/src/HOL/Reconstruction.thy Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Reconstruction.thy Tue Apr 19 18:08:44 2005 +0200
@@ -15,7 +15,6 @@
"Tools/res_types_sorts.ML"
"Tools/ATP/recon_prelim.ML"
- "Tools/ATP/recon_gandalf_base.ML"
"Tools/ATP/recon_order_clauses.ML"
"Tools/ATP/recon_translate_proof.ML"
"Tools/ATP/recon_parse.ML"
--- a/src/HOL/Tools/ATP/recon_gandalf_base.ML Tue Apr 19 15:15:06 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-structure Recon_Base =
-struct
-
-(* Auxiliary functions *)
-
-exception Assertion of string;
-
-val DEBUG = ref true;
-fun TRACE s = if !DEBUG then print s else ();
-
-exception Noassoc;
-fun assoc a [] = raise Noassoc
- | assoc a ((x, y)::t) = if a = x then y else assoc a t;
-fun assoc_exists a [] = false
- | assoc_exists a ((x, y)::t) = if a = x then true else assoc_exists a t;
-fun assoc_update (a, b) [] = raise Noassoc
- | assoc_update (a, b) ((x, y)::t)
- = if a = x then (a, b)::t else (x, y)::(assoc_update (a, b) t)
-fun assoc_inv a [] = raise Noassoc
- | assoc_inv a ((x, y)::t) = if a = y then x else assoc a t;
-fun assoc_inv_exists a [] = false
- | assoc_inv_exists a ((x, y)::t) = if a = y then true else assoc_inv_exists a t;
-
-fun is_mem x [] = false
- | is_mem x (h::t) = (x = h) orelse is_mem x t;
-fun elt 0 (h::t) = h
- | elt n (h::t) = elt (n - 1) t
- | elt n l = raise (Assertion "elt: out of range");
-fun remove_elt _ [] = raise (Assertion "remove_elt: out of range")
- | remove_elt 0 (h::t) = t
- | remove_elt n (h::t) = h::(remove_elt (n - 1) t);
-fun elt_num x [] = raise (Assertion "elt_num: not in list")
- | elt_num x (h::t) = if h = x then 0 else 1 + elt_num x t;
-fun set_add x l = if is_mem x l then l else x::l;
-
-fun iter f a [] = a
- | iter f a (h::t) = f h (iter f a t);
-
-end;
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 19 18:08:44 2005 +0200
@@ -2,27 +2,16 @@
(* Reorder clauses for use in binary resolution *)
(*----------------------------------------------*)
-fun drop n [] = []
-| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
-
fun remove_nth n [] = []
| remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
-fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
+(*Differs from List.nth: it counts from 1 rather than from 0*)
+fun get_nth n (x::xs) = hd (Library.drop (n-1, x::xs))
exception Not_in_list;
-fun zip xs [] = []
-| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
-
-
-fun unzip [] = ([],[])
- | unzip((x,y)::pairs) =
- let val (xs,ys) = unzip pairs
- in (x::xs, y::ys) end;
-
fun numlist 0 = []
| numlist n = (numlist (n - 1))@[n]
@@ -39,13 +28,6 @@
(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
-fun assoc3 a [] = raise Recon_Base.Noassoc
- | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
-
-
-fun third (a,b,c) = c;
-
-
fun takeUntil ch [] res = (res, [])
| takeUntil ch (x::xs) res = if x = ch
then
@@ -70,12 +52,12 @@
then
let val (left, right) = takeUntil "=" str []
in
- ((butlast left), (drop 1 right))
+ (butlast left, tl right)
end
else (* is an inequality *)
let val (left, right) = takeUntil "~" str []
in
- ((butlast left), (drop 2 right))
+ (butlast left, tl (tl right))
end
@@ -101,23 +83,16 @@
-fun var_pos_eq vars x y = let val xs = explode x
+fun var_pos_eq vars x y = String.size x = String.size y andalso
+ let val xs = explode x
val ys = explode y
+ val xsys = ListPair.zip (xs,ys)
+ val are_var_pairs = map (var_equiv vars) xsys
in
- if not_equal (length xs) (length ys)
- then
- false
- else
- let val xsys = zip xs ys
- val are_var_pairs = map (var_equiv vars) xsys
- in
- all_true are_var_pairs
- end
+ all_true are_var_pairs
end
-
-
fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list
|pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) =
let val y = explode x
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 19 18:08:44 2005 +0200
@@ -116,7 +116,9 @@
fun get_step_nums [] nums = nums
| get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
-fun assoc_snd a [] = raise Recon_Base.Noassoc
+exception Noassoc;
+
+fun assoc_snd a [] = raise Noassoc
| assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
(* change to be something using check_order instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
@@ -125,13 +127,10 @@
| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
*)
(*FIX - should this have vars in it? *)
-fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))
- in
- true
- end
- handle EXCEP => false
+fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true)
+ handle _ => false
-fun assoc_out_of_order a [] = raise Recon_Base.Noassoc
+fun assoc_out_of_order a [] = raise Noassoc
| assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
fun get_assoc_snds [] xs assocs= assocs
@@ -180,7 +179,7 @@
(* literals of -all- axioms, not just those used by spass *)
val meta_strs = map get_meta_lits metas
- val metas_and_strs = zip metas meta_strs
+ val metas_and_strs = ListPair.zip (metas,meta_strs)
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));
val _ = TextIO.output (outfile, onestr ax_strs)
@@ -193,14 +192,14 @@
val ax_metas = get_assoc_snds ax_strs metas_and_strs []
val ax_vars = map thm_vars ax_metas
- val ax_with_vars = zip ax_metas ax_vars
+ val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
(* get list of extra axioms as thms with their variables *)
val extra_metas = add_if_not_inlist metas ax_metas []
val extra_vars = map thm_vars extra_metas
val extra_with_vars = if (not (extra_metas = []) )
then
- zip extra_metas extra_vars
+ ListPair.zip (extra_metas,extra_vars)
else
[]
@@ -218,7 +217,7 @@
val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
in
- (distfrees,distvars, extra_with_vars,ax_with_vars, (zip step_nums ax_metas))
+ (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
end
fun thmstrings [] str = str
@@ -347,12 +346,12 @@
(* do the bit for the Isabelle ordered axioms at the top *)
val ax_nums = map #1 numcls
val ax_strs = map get_meta_lits_bracket (map #2 numcls)
- val numcls_strs = zip ax_nums ax_strs
+ val numcls_strs = ListPair.zip (ax_nums,ax_strs)
val num_cls_vars = map (addvars vars) numcls_strs;
- val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
+ val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
- val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
+ val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
val frees_str = "["^(thmvars_to_string frees "")^"]"
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
@@ -640,15 +639,15 @@
fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
val extraax_num = length extraaxioms
- val origaxioms_and_steps = drop (extraax_num) xs
+ val origaxioms_and_steps = Library.drop (extraax_num, xs)
val origaxioms = get_origaxioms origaxioms_and_steps
val origax_num = length origaxioms
- val axioms_and_steps = drop (origax_num + extraax_num) xs
+ val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)
val axioms = get_axioms axioms_and_steps
- val steps = drop origax_num axioms_and_steps
+ val steps = Library.drop (origax_num, axioms_and_steps)
val firststeps = butlast steps
val laststep = last steps
val goalstring = implode(butlast(explode goalstring))
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue Apr 19 18:08:44 2005 +0200
@@ -62,18 +62,20 @@
implode(List.filter is_alpha_space_digit_or_neg exp_term)
end
+fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
(****************************************)
(* Reconstruct an axiom resolution step *)
(****************************************)
- fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
- let val this_axiom =(Recon_Base.assoc clausenum clauses)
+fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
+ let val this_axiom = valOf (assoc (clauses,clausenum))
val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)
val thmvars = thm_vars res
in
(res, (Axiom,clause_strs,thmvars ) )
end
+ handle Option => reconstruction_failed "follow_axiom"
(****************************************)
(* Reconstruct a binary resolution step *)
@@ -82,14 +84,15 @@
(* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
= let
- val thm1 = select_literal (lit1 + 1) (Recon_Base.assoc clause1 thml)
- val thm2 = Recon_Base.assoc clause2 thml
+ val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
+ val thm2 = valOf (assoc (thml,clause2))
val res = thm1 RSN ((lit2 +1), thm2)
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
val thmvars = thm_vars res
in
(res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
end
+ handle Option => reconstruction_failed "follow_binary"
@@ -100,14 +103,15 @@
fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
= let
- val thm1 = select_literal (lit1 + 1) (Recon_Base.assoc clause1 thml)
- val thm2 = Recon_Base.assoc clause2 thml
+ val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
+ val thm2 = valOf (assoc (thml,clause2))
val res = thm1 RSN ((lit2 +1), thm2)
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
val thmvars = thm_vars res
in
(res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
end
+ handle Option => reconstruction_failed "follow_mrr"
(*******************************************)
@@ -144,7 +148,7 @@
(*FIXME: share code with that in Tools/reconstruction.ML*)
fun follow_factor clause lit1 lit2 allvars thml clause_strs=
let
- val th = Recon_Base.assoc clause thml
+ val th = valOf (assoc (thml,clause))
val prems = prems_of th
val sign = sign_of_thm th
val fac1 = get_nth (lit1+1) prems
@@ -178,15 +182,8 @@
in
(res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars))
end
- end;
-
-
-
-Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
-val prems = it;
-br (hd prems) 1;
-br (hd(tl(tl prems))) 1;
-qed "merge";
+ end
+ handle Option => reconstruction_failed "follow_factor"
@@ -217,8 +214,8 @@
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
let
- val th1 = Recon_Base.assoc clause1 thml
- val th2 = Recon_Base.assoc clause2 thml
+ val th1 = valOf (assoc (thml,clause1))
+ val th2 = valOf (assoc (thml,clause2))
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -236,12 +233,13 @@
in
(res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
end
+ handle Option => reconstruction_failed "follow_standard_para"
(*
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
let
- val th1 = Recon_Base.assoc clause1 thml
- val th2 = Recon_Base.assoc clause2 thml
+ val th1 = valOf (assoc (thml,clause1))
+ val th2 = valOf (assoc (thml,clause2))
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -252,6 +250,7 @@
in
(res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
end
+ handle Option => reconstruction_failed "follow_standard_para"
*)
@@ -292,8 +291,8 @@
(* clause1, lit1 is thing to rewrite with *)
fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs=
- let val th1 = Recon_Base.assoc clause1 thml
- val th2 = Recon_Base.assoc clause2 thml
+ let val th1 = valOf (assoc (thml,clause1))
+ val th2 = valOf (assoc (thml,clause2))
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -309,6 +308,7 @@
in
(res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars))
end
+ handle Option => reconstruction_failed "follow_rewrite"
@@ -318,7 +318,7 @@
fun follow_obvious (clause1, lit1) allvars thml clause_strs=
- let val th1 = Recon_Base.assoc clause1 thml
+ let val th1 = valOf (assoc (thml,clause1))
val prems1 = prems_of th1
val newthm = refl RSN ((lit1+ 1), th1)
handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
@@ -327,6 +327,7 @@
in
(res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
end
+ handle Option => reconstruction_failed "follow_obvious"
(**************************************************************************************)
(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue Apr 19 18:08:44 2005 +0200
@@ -32,7 +32,7 @@
val numbers = 0 upto (num_of_cls -1)
val multi_name = multi name num_of_cls []
in
- zip multi_name numbers
+ ListPair.zip (multi_name,numbers)
end;
fun stick [] = []
@@ -108,7 +108,7 @@
(* get (name, thm) pairs for claset rules *)
(*******************************************)
- val names_rules = zip good_names name_fol_cs;
+ val names_rules = ListPair.zip (good_names,name_fol_cs);
val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
@@ -118,7 +118,7 @@
val stick_clasrls = map stick claset_tptp_strs;
(* stick stick_clasrls length is 172*)
- val name_stick = zip good_names stick_clasrls;
+ val name_stick = ListPair.zip (good_names,stick_clasrls);
val cl_name_nums =map clause_numbering name_stick;
@@ -169,7 +169,7 @@
val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
val stick_strs = map stick simpset_tptp_strs;
- val name_stick = zip simp_names stick_strs;
+ val name_stick = ListPair.zip (simp_names,stick_strs);
val name_nums =map clause_numbering name_stick;
(* length 2409*)
--- a/src/HOL/Tools/ATP/watcher.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Apr 19 18:08:44 2005 +0200
@@ -605,7 +605,7 @@
let val thm = thm_of_string thmstring
val clauses = make_clauses [thm]
- val numcls = zip (numlist (length clauses)) (map make_meta_clause clauses)
+ val numcls = ListPair.zip (numlist (length clauses), map make_meta_clause clauses)
in
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
--- a/src/HOL/Tools/res_atp.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Apr 19 18:08:44 2005 +0200
@@ -104,7 +104,7 @@
val prems'' = make_clauses prems'
val prems''' = ResAxioms.rm_Eps [] prems''
val clss = map ResClause.make_conjecture_clause prems'''
- val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
+ val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val tfree_lits = ResLib.flat_noDup tfree_litss
val tfree_clss = map ResClause.tfree_clause tfree_lits
val hypsfile = File.sysify_path hyps_file
@@ -123,7 +123,7 @@
let val _ = (warning ("in tptp_inputs_tfrees 0"))
val clss = map (ResClause.make_conjecture_clause_thm) thms
val _ = (warning ("in tptp_inputs_tfrees 1"))
- val (tptp_clss,tfree_litss) = ResLib.unzip (map ResClause.clause2tptp clss)
+ val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val _ = (warning ("in tptp_inputs_tfrees 2"))
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
val _ = (warning ("in tptp_inputs_tfrees 3"))
--- a/src/HOL/Tools/res_clause.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Tue Apr 19 18:08:44 2005 +0200
@@ -212,7 +212,7 @@
fun type_of (Type (a, [])) = (make_fixed_type_const a,[])
| type_of (Type (a, Ts)) =
let val foltyps_ts = map type_of Ts
- val (folTyps,ts) = ResLib.unzip foltyps_ts
+ val (folTyps,ts) = ListPair.unzip foltyps_ts
val ts' = ResLib.flat_noDup ts
in
(((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)),ts')
@@ -279,14 +279,14 @@
let val (f,args) = strip_comb app
fun term_of_aux () =
let val (funName,(funType,ts1)) = fun_name_type f
- val (args',ts2) = ResLib.unzip (map term_of args)
+ val (args',ts2) = ListPair.unzip (map term_of args)
val ts3 = ResLib.flat_noDup (ts1::ts2)
in
(Fun(funName,funType,args'),ts3)
end
fun term_of_eq ((Const ("op =", typ)),args) =
let val arg_typ = eq_arg_type typ
- val (args',ts) = ResLib.unzip (map term_of args)
+ val (args',ts) = ListPair.unzip (map term_of args)
val equal_name = lookup_const ("op =")
in
(Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
@@ -304,7 +304,7 @@
fun pred_of_eq ((Const ("op =", typ)),args) =
let val arg_typ = eq_arg_type typ
- val (args',ts) = ResLib.unzip (map term_of args)
+ val (args',ts) = ListPair.unzip (map term_of args)
val equal_name = lookup_const "op ="
in
(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
@@ -315,7 +315,7 @@
(* The input "pred" cannot be an equality *)
fun pred_of_nonEq (pred,args) =
let val (predName,(predType,ts1)) = pred_name_type pred
- val (args',ts2) = ResLib.unzip (map term_of args)
+ val (args',ts2) = ListPair.unzip (map term_of args)
val ts3 = ResLib.flat_noDup (ts1::ts2)
in
(Predicate(predName,predType,args'),ts3)
@@ -507,7 +507,7 @@
val nargs = length args
val tvars = get_TVars nargs
val conclLit = make_TConsLit(true,(res,tcons,tvars))
- val tvars_srts = ResLib.zip tvars args
+ val tvars_srts = ListPair.zip (tvars,args)
val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
val premLits = map make_TVarLit false_tvars_srts'
--- a/src/HOL/Tools/res_lib.ML Tue Apr 19 15:15:06 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML Tue Apr 19 18:08:44 2005 +0200
@@ -22,10 +22,8 @@
val no_rep_app : ''a list -> ''a list -> ''a list
val pair_ins : 'a -> 'b list -> ('a * 'b) list
val rm_rep : ''a list -> ''a list
- val unzip : ('a * 'b) list -> 'a list * 'b list
val write_strs : TextIO.outstream -> TextIO.vector list -> unit
val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
- val zip : 'a list -> 'b list -> ('a * 'b) list
end;
@@ -80,18 +78,6 @@
fun rm_rep [] = []
| rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
- fun unzip [] =
- ([], [])
- | unzip ((x1, y1)::zs) =
- let
- val (xs, ys) = unzip zs
- in
- (x1::xs, y1::ys)
- end;
-
- fun zip [] [] = []
- | zip (x::xs) (y::ys) = (x, y)::(zip xs ys);
-
fun flat_noDup [] = []
| flat_noDup (x::y) = no_rep_app x (flat_noDup y);