--- a/src/Pure/drule.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/drule.ML Mon Jan 29 14:16:13 1996 +0100
@@ -12,77 +12,77 @@
sig
structure Thm : THM
local open Thm in
- val add_defs : (string * string) list -> theory -> theory
- val add_defs_i : (string * term) list -> theory -> theory
- val asm_rl : thm
- val assume_ax : theory -> string -> thm
- val COMP : thm * thm -> thm
- val compose : thm * int * thm -> thm list
- val cprems_of : thm -> cterm list
- val cskip_flexpairs : cterm -> cterm
- val cstrip_imp_prems : cterm -> cterm list
- val cterm_instantiate : (cterm*cterm)list -> thm -> thm
- val cut_rl : thm
- val equal_abs_elim : cterm -> thm -> thm
+ val add_defs : (string * string) list -> theory -> theory
+ val add_defs_i : (string * term) list -> theory -> theory
+ val asm_rl : thm
+ val assume_ax : theory -> string -> thm
+ val COMP : thm * thm -> thm
+ val compose : thm * int * thm -> thm list
+ val cprems_of : thm -> cterm list
+ val cskip_flexpairs : cterm -> cterm
+ val cstrip_imp_prems : cterm -> cterm list
+ val cterm_instantiate : (cterm*cterm)list -> thm -> thm
+ val cut_rl : thm
+ val equal_abs_elim : cterm -> thm -> thm
val equal_abs_elim_list: cterm list -> thm -> thm
- val eq_thm : thm * thm -> bool
- val same_thm : thm * thm -> bool
- val eq_thm_sg : thm * thm -> bool
+ val eq_thm : thm * thm -> bool
+ val same_thm : thm * thm -> bool
+ val eq_thm_sg : thm * thm -> bool
val flexpair_abs_elim_list: cterm list -> thm -> thm
- val forall_intr_list : cterm list -> thm -> thm
- val forall_intr_frees : thm -> thm
- val forall_intr_vars : thm -> thm
- val forall_elim_list : cterm list -> thm -> thm
- val forall_elim_var : int -> thm -> thm
- val forall_elim_vars : int -> thm -> thm
- val implies_elim_list : thm -> thm list -> thm
- val implies_intr_list : cterm list -> thm -> thm
- val MRL : thm list list * thm list -> thm list
- val MRS : thm list * thm -> thm
- val pprint_cterm : cterm -> pprint_args -> unit
- val pprint_ctyp : ctyp -> pprint_args -> unit
- val pprint_theory : theory -> pprint_args -> unit
- val pprint_thm : thm -> pprint_args -> unit
- val pretty_thm : thm -> Sign.Syntax.Pretty.T
- val print_cterm : cterm -> unit
- val print_ctyp : ctyp -> unit
- val print_goals : int -> thm -> unit
- val print_goals_ref : (int -> thm -> unit) ref
- val print_syntax : theory -> unit
- val print_theory : theory -> unit
- val print_thm : thm -> unit
- val prth : thm -> thm
- val prthq : thm Sequence.seq -> thm Sequence.seq
- val prths : thm list -> thm list
- val read_instantiate : (string*string)list -> thm -> thm
+ val forall_intr_list : cterm list -> thm -> thm
+ val forall_intr_frees : thm -> thm
+ val forall_intr_vars : thm -> thm
+ val forall_elim_list : cterm list -> thm -> thm
+ val forall_elim_var : int -> thm -> thm
+ val forall_elim_vars : int -> thm -> thm
+ val implies_elim_list : thm -> thm list -> thm
+ val implies_intr_list : cterm list -> thm -> thm
+ val MRL : thm list list * thm list -> thm list
+ val MRS : thm list * thm -> thm
+ val pprint_cterm : cterm -> pprint_args -> unit
+ val pprint_ctyp : ctyp -> pprint_args -> unit
+ val pprint_theory : theory -> pprint_args -> unit
+ val pprint_thm : thm -> pprint_args -> unit
+ val pretty_thm : thm -> Sign.Syntax.Pretty.T
+ val print_cterm : cterm -> unit
+ val print_ctyp : ctyp -> unit
+ val print_goals : int -> thm -> unit
+ val print_goals_ref : (int -> thm -> unit) ref
+ val print_syntax : theory -> unit
+ val print_theory : theory -> unit
+ val print_thm : thm -> unit
+ val prth : thm -> thm
+ val prthq : thm Sequence.seq -> thm Sequence.seq
+ val prths : thm list -> thm list
+ val read_instantiate : (string*string)list -> thm -> thm
val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
- val read_insts :
+ val read_insts :
Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
-> (indexname -> typ option) * (indexname -> sort option)
-> string list -> (string*string)list
-> (indexname*ctyp)list * (cterm*cterm)list
- val reflexive_thm : thm
- val revcut_rl : thm
- val rewrite_goal_rule : bool*bool -> (meta_simpset -> thm -> thm option)
+ val reflexive_thm : thm
+ val revcut_rl : thm
+ val rewrite_goal_rule : bool*bool -> (meta_simpset -> thm -> thm option)
-> meta_simpset -> int -> thm -> thm
val rewrite_goals_rule: thm list -> thm -> thm
- val rewrite_rule : thm list -> thm -> thm
- val RS : thm * thm -> thm
- val RSN : thm * (int * thm) -> thm
- val RL : thm list * thm list -> thm list
- val RLN : thm list * (int * thm list) -> thm list
- val show_hyps : bool ref
- val size_of_thm : thm -> int
- val standard : thm -> thm
- val string_of_cterm : cterm -> string
- val string_of_ctyp : ctyp -> string
- val string_of_thm : thm -> string
- val symmetric_thm : thm
- val thin_rl : thm
- val transitive_thm : thm
+ val rewrite_rule : thm list -> thm -> thm
+ val RS : thm * thm -> thm
+ val RSN : thm * (int * thm) -> thm
+ val RL : thm list * thm list -> thm list
+ val RLN : thm list * (int * thm list) -> thm list
+ val show_hyps : bool ref
+ val size_of_thm : thm -> int
+ val standard : thm -> thm
+ val string_of_cterm : cterm -> string
+ val string_of_ctyp : ctyp -> string
+ val string_of_thm : thm -> string
+ val symmetric_thm : thm
+ val thin_rl : thm
+ val transitive_thm : thm
val triv_forall_equality: thm
val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
- val zero_var_indexes : thm -> thm
+ val zero_var_indexes : thm -> thm
end
end;
@@ -226,8 +226,8 @@
(*Discard flexflex pairs; return a cterm*)
fun cskip_flexpairs ct =
case term_of ct of
- (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
- cskip_flexpairs (#2 (dest_cimplies ct))
+ (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
+ cskip_flexpairs (#2 (dest_cimplies ct))
| _ => ct;
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
@@ -732,15 +732,15 @@
(*Rewrite a theorem*)
fun rewrite_rule [] th = th
| rewrite_rule thms th =
- fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
+ fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
(*Rewrite the subgoals of a proof state (represented by a theorem) *)
fun rewrite_goals_rule [] th = th
| rewrite_goals_rule thms th =
- fconv_rule (goals_conv (K true)
- (rew_conv (true,false) (K(K None))
- (Thm.mss_of thms)))
- th;
+ fconv_rule (goals_conv (K true)
+ (rew_conv (true,false) (K(K None))
+ (Thm.mss_of thms)))
+ th;
(*Rewrite the subgoal of a proof state (represented by a theorem) *)
fun rewrite_goal_rule mode prover mss i thm =
--- a/src/Pure/envir.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/envir.ML Mon Jan 29 14:16:13 1996 +0100
@@ -18,19 +18,19 @@
datatype env = Envir of {asol: term xolist,
iTs: (indexname * typ) list,
maxidx: int}
- val alist_of : env -> (indexname * term) list
- val alist_of_olist : 'a xolist -> (indexname * 'a) list
- val empty : int->env
- val is_empty : env -> bool
- val minidx : env -> int option
- val genvar : string -> env * typ -> env * term
- val genvars : string -> env * typ list -> env * term list
- val lookup : env * indexname -> term option
- val norm_term : env -> term -> term
- val null_olist : 'a xolist
- val olist_of_alist : (indexname * 'a) list -> 'a xolist
- val update : (indexname * term) * env -> env
- val vupdate : (indexname * term) * env -> env
+ val alist_of : env -> (indexname * term) list
+ val alist_of_olist : 'a xolist -> (indexname * 'a) list
+ val empty : int->env
+ val is_empty : env -> bool
+ val minidx : env -> int option
+ val genvar : string -> env * typ -> env * term
+ val genvars : string -> env * typ list -> env * term list
+ val lookup : env * indexname -> term option
+ val norm_term : env -> term -> term
+ val null_olist : 'a xolist
+ val olist_of_alist : (indexname * 'a) list -> 'a xolist
+ val update : (indexname * term) * env -> env
+ val vupdate : (indexname * term) * env -> env
end;
functor EnvirFun () : ENVIR =
--- a/src/Pure/goals.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/goals.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Pure/goals.ML
+(* Title: Pure/goals.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Goal stack package. The goal stack initially holds a dummy proof, and can
@@ -15,63 +15,63 @@
structure Tactical: TACTICAL
local open Tactical Tactical.Thm in
type proof
- val ba : int -> unit
- val back : unit -> unit
- val bd : thm -> int -> unit
- val bds : thm list -> int -> unit
- val be : thm -> int -> unit
- val bes : thm list -> int -> unit
- val br : thm -> int -> unit
- val brs : thm list -> int -> unit
- val bw : thm -> unit
- val bws : thm list -> unit
- val by : tactic -> unit
- val byev : tactic list -> unit
- val chop : unit -> unit
- val choplev : int -> unit
- val fa : unit -> unit
- val fd : thm -> unit
- val fds : thm list -> unit
- val fe : thm -> unit
- val fes : thm list -> unit
- val filter_goal : (term*term->bool) -> thm list -> int -> thm list
- val fr : thm -> unit
- val frs : thm list -> unit
- val getgoal : int -> term
- val gethyps : int -> thm list
- val goal : theory -> string -> thm list
- val goalw : theory -> thm list -> string -> thm list
- val goalw_cterm : thm list -> cterm -> thm list
- val pop_proof : unit -> thm list
- val pr : unit -> unit
- val premises : unit -> thm list
- val prin : term -> unit
- val printyp : typ -> unit
- val pprint_term : term -> pprint_args -> unit
- val pprint_typ : typ -> pprint_args -> unit
- val print_exn : exn -> 'a
- val print_sign_exn : Sign.sg -> exn -> 'a
- val prlev : int -> unit
- val proof_timing : bool ref
- val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
+ val ba : int -> unit
+ val back : unit -> unit
+ val bd : thm -> int -> unit
+ val bds : thm list -> int -> unit
+ val be : thm -> int -> unit
+ val bes : thm list -> int -> unit
+ val br : thm -> int -> unit
+ val brs : thm list -> int -> unit
+ val bw : thm -> unit
+ val bws : thm list -> unit
+ val by : tactic -> unit
+ val byev : tactic list -> unit
+ val chop : unit -> unit
+ val choplev : int -> unit
+ val fa : unit -> unit
+ val fd : thm -> unit
+ val fds : thm list -> unit
+ val fe : thm -> unit
+ val fes : thm list -> unit
+ val filter_goal : (term*term->bool) -> thm list -> int -> thm list
+ val fr : thm -> unit
+ val frs : thm list -> unit
+ val getgoal : int -> term
+ val gethyps : int -> thm list
+ val goal : theory -> string -> thm list
+ val goalw : theory -> thm list -> string -> thm list
+ val goalw_cterm : thm list -> cterm -> thm list
+ val pop_proof : unit -> thm list
+ val pr : unit -> unit
+ val premises : unit -> thm list
+ val prin : term -> unit
+ val printyp : typ -> unit
+ val pprint_term : term -> pprint_args -> unit
+ val pprint_typ : typ -> pprint_args -> unit
+ val print_exn : exn -> 'a
+ val print_sign_exn : Sign.sg -> exn -> 'a
+ val prlev : int -> unit
+ val proof_timing : bool ref
+ val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
val prove_goalw : theory->thm list->string->(thm list->tactic list)->thm
- val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
- val push_proof : unit -> unit
- val read : string -> term
- val ren : string -> int -> unit
- val restore_proof : proof -> thm list
- val result : unit -> thm
- val rotate_proof : unit -> thm list
- val uresult : unit -> thm
- val save_proof : unit -> proof
- val topthm : unit -> thm
- val undo : unit -> unit
+ val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
+ val push_proof : unit -> unit
+ val read : string -> term
+ val ren : string -> int -> unit
+ val restore_proof : proof -> thm list
+ val result : unit -> thm
+ val rotate_proof : unit -> thm list
+ val uresult : unit -> thm
+ val save_proof : unit -> proof
+ val topthm : unit -> thm
+ val undo : unit -> unit
end
end;
functor GoalsFun (structure Logic: LOGIC and Drule: DRULE and Tactic: TACTIC
and Pattern:PATTERN
- sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig
+ sharing type Pattern.type_sig = Drule.Thm.Sign.Type.type_sig
and Drule.Thm = Tactic.Tactical.Thm) : GOALS =
struct
structure Tactical = Tactic.Tactical
@@ -132,39 +132,39 @@
and st0 = (rewrite_goals_rule rths o trivial) (cterm_of sign B)
fun result_error state msg =
(writeln ("Bad final proof state:");
- !print_goals_ref (!goals_limit) state;
- error msg)
+ !print_goals_ref (!goals_limit) state;
+ error msg)
(*discharges assumptions from state in the order they appear in goal;
- checks (if requested) that resulting theorem is equivalent to goal. *)
+ checks (if requested) that resulting theorem is equivalent to goal. *)
fun mkresult (check,state) =
let val state = Sequence.hd (flexflex_rule state)
- handle _ => state (*smash flexflex pairs*)
- val ngoals = nprems_of state
+ handle _ => state (*smash flexflex pairs*)
+ val ngoals = nprems_of state
val th = strip_shyps (implies_intr_list cAs state)
val {hyps,prop,sign=sign',...} = rep_thm th
val xshyps = extra_shyps th;
in if not check then standard th
- else if not (Sign.eq_sg(sign,sign')) then result_error state
- ("Signature of proof state has changed!" ^
- sign_error (sign,sign'))
+ else if not (Sign.eq_sg(sign,sign')) then result_error state
+ ("Signature of proof state has changed!" ^
+ sign_error (sign,sign'))
else if ngoals>0 then result_error state
- (string_of_int ngoals ^ " unsolved goals!")
+ (string_of_int ngoals ^ " unsolved goals!")
else if not (null hyps) then result_error state
("Additional hypotheses:\n" ^
cat_lines (map (Sign.string_of_term sign) hyps))
- else if not (null xshyps) then result_error state
+ else if not (null xshyps) then result_error state
("Extra sort hypotheses: " ^
commas (map Sign.Type.str_of_sort xshyps))
- else if Pattern.matches (#tsig(Sign.rep_sg sign))
- (term_of chorn, prop)
- then standard th
- else result_error state "proved a different theorem"
+ else if Pattern.matches (#tsig(Sign.rep_sg sign))
+ (term_of chorn, prop)
+ then standard th
+ else result_error state "proved a different theorem"
end
in
if Sign.eq_sg(sign, #sign(rep_thm st0))
then (prems, st0, mkresult)
else error ("Definitions would change the proof state's signature" ^
- sign_error (sign, #sign(rep_thm st0)))
+ sign_error (sign, #sign(rep_thm st0)))
end
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
@@ -172,18 +172,18 @@
fun print_sign_exn_unit sign e =
case e of
THM (msg,i,thms) =>
- (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- seq print_thm thms)
+ (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
+ seq print_thm thms)
| THEORY (msg,thys) =>
- (writeln ("Exception THEORY raised:\n" ^ msg);
- seq print_theory thys)
+ (writeln ("Exception THEORY raised:\n" ^ msg);
+ seq print_theory thys)
| TERM (msg,ts) =>
- (writeln ("Exception TERM raised:\n" ^ msg);
- seq (writeln o Sign.string_of_term sign) ts)
+ (writeln ("Exception TERM raised:\n" ^ msg);
+ seq (writeln o Sign.string_of_term sign) ts)
| TYPE (msg,Ts,ts) =>
- (writeln ("Exception TYPE raised:\n" ^ msg);
- seq (writeln o Sign.string_of_typ sign) Ts;
- seq (writeln o Sign.string_of_term sign) ts)
+ (writeln ("Exception TYPE raised:\n" ^ msg);
+ seq (writeln o Sign.string_of_typ sign) Ts;
+ seq (writeln o Sign.string_of_term sign) ts)
| e => raise e;
(*Prints an exception, then fails*)
@@ -199,13 +199,13 @@
let val (prems, st0, mkresult) = prepare_proof rths chorn
val tac = EVERY (tacsf prems)
fun statef() =
- (case Sequence.pull (tapply(tac,st0)) of
- Some(st,_) => st
- | _ => error ("prove_goal: tactic failed"))
+ (case Sequence.pull (tapply(tac,st0)) of
+ Some(st,_) => st
+ | _ => error ("prove_goal: tactic failed"))
in mkresult (true, cond_timeit (!proof_timing) statef) end
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
- error ("The exception above was raised for\n" ^
- string_of_cterm chorn));
+ error ("The exception above was raised for\n" ^
+ string_of_cterm chorn));
(*Version taking the goal as a string*)
@@ -214,7 +214,7 @@
val chorn = read_cterm sign (agoal,propT)
in prove_goalw_cterm rths chorn tacsf end
handle ERROR => error (*from read_cterm?*)
- ("The error above occurred for " ^ quote agoal);
+ ("The error above occurred for " ^ quote agoal);
(*String version with no meta-rewrite-rules*)
fun prove_goal thy = prove_goalw thy [];
@@ -262,8 +262,8 @@
(*Get subgoal i from goal stack*)
fun getgoal i =
(case drop (i-1, prems_of (topthm())) of
- [] => error"getgoal: Goal number out of range"
- | Q::_ => Q);
+ [] => error"getgoal: Goal number out of range"
+ | Q::_ => Q);
(*Return subgoal i's hypotheses as meta-level assumptions.
For debugging uses of METAHYPS*)
@@ -283,7 +283,7 @@
in if 0<=n andalso n<= level
then drop (level - n, pair::pairs)
else error ("Level number must lie between 0 and " ^
- string_of_int level)
+ string_of_int level)
end;
(*Print the given level of the proof*)
@@ -309,7 +309,7 @@
fun goalw thy rths agoal =
goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
handle ERROR => error (*from type_assign, etc via prepare_proof*)
- ("The error above occurred for " ^ quote agoal);
+ ("The error above occurred for " ^ quote agoal);
(*String version with no meta-rewrite-rules*)
fun goal thy = goalw thy [];
@@ -320,10 +320,10 @@
None => error"by: tactic failed"
| Some(th2,ths2) =>
(if eq_thm(th,th2)
- then writeln"Warning: same as previous level"
- else if eq_thm_sg(th,th2) then ()
- else writeln("Warning: signature of proof state has changed" ^
- sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
+ then writeln"Warning: same as previous level"
+ else if eq_thm_sg(th,th2) then ()
+ else writeln("Warning: signature of proof state has changed" ^
+ sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
((th2,ths2)::(th,ths)::pairs)));
fun by tac = cond_timeit (!proof_timing)
@@ -339,13 +339,13 @@
fun backtrack [] = error"back: no alternatives"
| backtrack ((th,thstr) :: pairs) =
(case Sequence.pull thstr of
- None => (writeln"Going back a level..."; backtrack pairs)
- | Some(th2,thstr2) =>
- (if eq_thm(th,th2)
- then writeln"Warning: same as previous choice at this level"
- else if eq_thm_sg(th,th2) then ()
- else writeln"Warning: signature of proof state has changed";
- (th2,thstr2)::pairs));
+ None => (writeln"Going back a level..."; backtrack pairs)
+ | Some(th2,thstr2) =>
+ (if eq_thm(th,th2)
+ then writeln"Warning: same as previous choice at this level"
+ else if eq_thm_sg(th,th2) then ()
+ else writeln"Warning: signature of proof state has changed";
+ (th2,thstr2)::pairs));
fun back() = setstate (backtrack (getstate()));
@@ -371,7 +371,7 @@
fun top_proof() = case !proofstack of
- [] => error("Stack of proof attempts is empty!")
+ [] => error("Stack of proof attempts is empty!")
| p::ps => (p,ps);
(* push a copy of the current proof state on to the stack *)
@@ -385,11 +385,11 @@
(* rotate the stack so that the top element goes to the bottom *)
fun rotate_proof() = let val (p,ps) = top_proof()
- in proofstack := ps@[save_proof()];
- restore_proof p;
- pr();
- !curr_prems
- end;
+ in proofstack := ps@[save_proof()];
+ restore_proof p;
+ pr();
+ !curr_prems
+ end;
(** Shortcuts for commonly-used tactics **)
@@ -428,7 +428,7 @@
fun top_sg() = #sign(rep_thm(topthm()));
fun read s = term_of (read_cterm (top_sg())
- (s, (TVar(("DUMMY",0),[]))));
+ (s, (TVar(("DUMMY",0),[]))));
(*Print a term under the current signature of the proof state*)
fun prin t = writeln (Sign.string_of_term (top_sg()) t);
--- a/src/Pure/library.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/library.ML Mon Jan 29 14:16:13 1996 +0100
@@ -650,8 +650,8 @@
(*Assert pred for every member of l, generating a message if pred fails*)
fun assert_all pred l msg_fn =
let fun asl [] = ()
- | asl (x::xs) = if pred x then asl xs
- else error (msg_fn x)
+ | asl (x::xs) = if pred x then asl xs
+ else error (msg_fn x)
in asl l end;
(* FIXME close file (?) *)
--- a/src/Pure/logic.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/logic.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Pure/logic.ML
+(* Title: Pure/logic.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright Cambridge University 1992
Supporting code for defining the abstract type "thm"
@@ -10,43 +10,43 @@
signature LOGIC =
sig
- val assum_pairs : term -> (term*term)list
- val auto_rename : bool ref
- val close_form : term -> term
- val count_prems : term * int -> int
- val dest_equals : term -> term * term
- val dest_flexpair : term -> term * term
- val dest_implies : term -> term * term
- val dest_inclass : term -> typ * class
- val dest_type : term -> typ
- val flatten_params : int -> term -> term
- val freeze_vars : term -> term
- val incr_indexes : typ list * int -> term -> term
- val lift_fns : term * int -> (term -> term) * (term -> term)
- val list_flexpairs : (term*term)list * term -> term
- val list_implies : term list * term -> term
+ val assum_pairs : term -> (term*term)list
+ val auto_rename : bool ref
+ val close_form : term -> term
+ val count_prems : term * int -> int
+ val dest_equals : term -> term * term
+ val dest_flexpair : term -> term * term
+ val dest_implies : term -> term * term
+ val dest_inclass : term -> typ * class
+ val dest_type : term -> typ
+ val flatten_params : int -> term -> term
+ val freeze_vars : term -> term
+ val incr_indexes : typ list * int -> term -> term
+ val lift_fns : term * int -> (term -> term) * (term -> term)
+ val list_flexpairs : (term*term)list * term -> term
+ val list_implies : term list * term -> term
val list_rename_params: string list * term -> term
val is_equals : term -> bool
- val mk_equals : term * term -> term
- val mk_flexpair : term * term -> term
- val mk_implies : term * term -> term
- val mk_inclass : typ * class -> term
- val mk_type : typ -> term
- val occs : term * term -> bool
- val rule_of : (term*term)list * term list * term -> term
- val set_rename_prefix : string -> unit
- val skip_flexpairs : term -> term
+ val mk_equals : term * term -> term
+ val mk_flexpair : term * term -> term
+ val mk_implies : term * term -> term
+ val mk_inclass : typ * class -> term
+ val mk_type : typ -> term
+ val occs : term * term -> bool
+ val rule_of : (term*term)list * term list * term -> term
+ val set_rename_prefix : string -> unit
+ val skip_flexpairs : term -> term
val strip_assums_concl: term -> term
- val strip_assums_hyp : term -> term list
- val strip_flexpairs : term -> (term*term)list * term
- val strip_horn : term -> (term*term)list * term list * term
- val strip_imp_concl : term -> term
- val strip_imp_prems : term -> term list
- val strip_params : term -> (string * typ) list
- val strip_prems : int * term list * term -> term list * term
- val thaw_vars : term -> term
- val unvarify : term -> term
- val varify : term -> term
+ val strip_assums_hyp : term -> term list
+ val strip_flexpairs : term -> (term*term)list * term
+ val strip_horn : term -> (term*term)list * term list * term
+ val strip_imp_concl : term -> term
+ val strip_imp_prems : term -> term list
+ val strip_params : term -> (string * typ) list
+ val strip_prems : int * term list * term -> term list * term
+ val thaw_vars : term -> term
+ val unvarify : term -> term
+ val varify : term -> term
end;
functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =
@@ -91,11 +91,11 @@
| strip_imp_concl A = A : term;
(*Strip and return premises: (i, [], A1==>...Ai==>B)
- goes to ([Ai, A(i-1),...,A1] , B) (REVERSED)
+ goes to ([Ai, A(i-1),...,A1] , B) (REVERSED)
if i<0 or else i too big then raises TERM*)
fun strip_prems (0, As, B) = (As, B)
| strip_prems (i, As, Const("==>", _) $ A $ B) =
- strip_prems (i-1, A::As, B)
+ strip_prems (i-1, A::As, B)
| strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
(*Count premises -- quicker than (length ostrip_prems) *)
@@ -114,13 +114,13 @@
goes to (a1=?=b1) ==>...(an=?=bn)==>C *)
fun list_flexpairs ([], A) = A
| list_flexpairs ((t,u)::pairs, A) =
- implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
+ implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
(*Make the object-rule tpairs==>As==>B *)
fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B));
(*Remove and return flexflex pairs:
- (a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C )
+ (a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C )
[Tail recursive in order to return a pair of results] *)
fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) =
strip_flex_aux ((t,u)::pairs, C)
@@ -130,7 +130,7 @@
(*Discard flexflex pairs*)
fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) =
- skip_flexpairs C
+ skip_flexpairs C
| skip_flexpairs C = C;
(*strip a proof state (Horn clause):
@@ -165,13 +165,13 @@
fun t occs u = (t aconv u) orelse
(case u of
Abs(_,_,body) => t occs body
- | f$t' => t occs f orelse t occs t'
- | _ => false);
+ | f$t' => t occs f orelse t occs t'
+ | _ => false);
(*Close up a formula over all free variables by quantification*)
fun close_form A =
list_all_free (map dest_Free (sort atless (term_frees A)),
- A);
+ A);
(*Freeze all (T)Vars by turning them into (T)Frees*)
@@ -188,9 +188,9 @@
| thaw_vars(Free(a,T)) =
let val T' = Type.thaw_vars T
in case explode a of
- "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
+ "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
in Var(ixn,T') end
- | _ => Free(a,T')
+ | _ => Free(a,T')
end
| thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t)
| thaw_vars(s$t) = thaw_vars s $ thaw_vars t
@@ -203,14 +203,14 @@
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
fun incr_indexes (Us: typ list, inc:int) t =
let fun incr (Var ((a,i), T), lev) =
- Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
- lev, length Us)
- | incr (Abs (a,T,body), lev) =
- Abs (a, incr_tvar inc T, incr(body,lev+1))
- | incr (Const(a,T),_) = Const(a, incr_tvar inc T)
- | incr (Free(a,T),_) = Free(a, incr_tvar inc T)
- | incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
- | incr (t,lev) = t
+ Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
+ lev, length Us)
+ | incr (Abs (a,T,body), lev) =
+ Abs (a, incr_tvar inc T, incr(body,lev+1))
+ | incr (Const(a,T),_) = Const(a, incr_tvar inc T)
+ | incr (Free(a,T),_) = Free(a, incr_tvar inc T)
+ | incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
+ | incr (t,lev) = t
in incr(t,0) end;
(*Make lifting functions from subgoal and increment.
@@ -218,14 +218,14 @@
lift_all operates on propositions *)
fun lift_fns (B,inc) =
let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
- | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
- Abs(a, T, lift_abs (T::Us, t) u)
- | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
+ | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
+ Abs(a, T, lift_abs (T::Us, t) u)
+ | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
fun lift_all (Us, Const("==>", _) $ A $ B) u =
- implies $ A $ lift_all (Us,B) u
- | lift_all (Us, Const("all",_)$Abs(a,T,t)) u =
- all T $ Abs(a, T, lift_all (T::Us,t) u)
- | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
+ implies $ A $ lift_all (Us,B) u
+ | lift_all (Us, Const("all",_)$Abs(a,T,t)) u =
+ all T $ Abs(a, T, lift_all (T::Us,t) u)
+ | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
in (lift_abs([],B), lift_all([],B)) end;
(*Strips assumptions in goal, yielding list of hypotheses. *)
@@ -250,8 +250,8 @@
if j=0 andalso n<=0 then A (*nothing left to do...*)
else case A of
Const("==>", _) $ H $ B =>
- if n=1 then (remove_params j (n-1) B)
- else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
+ if n=1 then (remove_params j (n-1) B)
+ else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
| Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
| _ => if n>0 then raise TERM("remove_params", [A])
else A;
@@ -278,9 +278,9 @@
if n>0 then deletes assumption n. *)
fun flatten_params n A =
let val params = strip_params A;
- val vars = if !auto_rename
- then rename_vars (!rename_prefix, params)
- else variantlist(map #1 params,[]) ~~ map #2 params
+ val vars = if !auto_rename
+ then rename_vars (!rename_prefix, params)
+ else variantlist(map #1 params,[]) ~~ map #2 params
in list_all (vars, remove_params (length vars) n A)
end;
@@ -294,9 +294,9 @@
(*Strips assumptions in goal yielding ( [Hn,...,H1], [xm,...,x1], B )
where H1,...,Hn are the hypotheses and x1...xm are the parameters. *)
fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) =
- strip_assums_aux (H::Hs, params, B)
+ strip_assums_aux (H::Hs, params, B)
| strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) =
- strip_assums_aux (Hs, (a,T)::params, t)
+ strip_assums_aux (Hs, (a,T)::params, t)
| strip_assums_aux (Hs, params, B) = (Hs, params, B);
fun strip_assums A = strip_assums_aux ([],[],A);
@@ -310,7 +310,7 @@
val D = Unify.rlist_abs(params, B)
fun pairrev ([],pairs) = pairs
| pairrev (H::Hs,pairs) =
- pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
+ pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
in pairrev (Hs,[]) (*WAS: map pair (rev Hs) *)
end;
--- a/src/Pure/net.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/net.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: net
+(* Title: net
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Discrimination nets: a data structure for indexing items
@@ -46,9 +46,9 @@
*)
fun add_key_of_terms (t, cs) =
let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
- | rands (Const(c,_), cs) = AtomK c :: cs
- | rands (Free(c,_), cs) = AtomK c :: cs
- | rands (Bound i, cs) = AtomK (string_of_bound i) :: cs
+ | rands (Const(c,_), cs) = AtomK c :: cs
+ | rands (Free(c,_), cs) = AtomK c :: cs
+ | rands (Bound i, cs) = AtomK (string_of_bound i) :: cs
in case (head_of t) of
Var _ => VarK :: cs
| Abs _ => VarK :: cs
@@ -66,9 +66,9 @@
Lookup functions preserve order in items stored at same level.
*)
datatype 'a net = Leaf of 'a list
- | Net of {comb: 'a net,
- var: 'a net,
- alist: (string * 'a net) list};
+ | Net of {comb: 'a net,
+ var: 'a net,
+ alist: (string * 'a net) list};
val empty = Leaf[];
val emptynet = Net{comb=empty, var=empty, alist=[]};
@@ -76,7 +76,7 @@
(*** Insertion into a discrimination net ***)
-exception INSERT; (*duplicate item in the net*)
+exception INSERT; (*duplicate item in the net*)
(*Adds item x to the list at the node addressed by the keys.
@@ -89,25 +89,25 @@
if gen_mem eq (x,xs) then raise INSERT else Leaf(x::xs)
| ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*)
| ins1 (CombK :: keys, Net{comb,var,alist}) =
- Net{comb=ins1(keys,comb), var=var, alist=alist}
- | ins1 (VarK :: keys, Net{comb,var,alist}) =
- Net{comb=comb, var=ins1(keys,var), alist=alist}
- | ins1 (AtomK a :: keys, Net{comb,var,alist}) =
- let fun newpair net = (a, ins1(keys,net))
- fun inslist [] = [newpair empty]
- | inslist((b: string, netb) :: alist) =
- if a=b then newpair netb :: alist
- else if a<b then (*absent, ins1ert in alist*)
- newpair empty :: (b,netb) :: alist
- else (*a>b*) (b,netb) :: inslist alist
- in Net{comb=comb, var=var, alist= inslist alist} end
+ Net{comb=ins1(keys,comb), var=var, alist=alist}
+ | ins1 (VarK :: keys, Net{comb,var,alist}) =
+ Net{comb=comb, var=ins1(keys,var), alist=alist}
+ | ins1 (AtomK a :: keys, Net{comb,var,alist}) =
+ let fun newpair net = (a, ins1(keys,net))
+ fun inslist [] = [newpair empty]
+ | inslist((b: string, netb) :: alist) =
+ if a=b then newpair netb :: alist
+ else if a<b then (*absent, ins1ert in alist*)
+ newpair empty :: (b,netb) :: alist
+ else (*a>b*) (b,netb) :: inslist alist
+ in Net{comb=comb, var=var, alist= inslist alist} end
in ins1 (keys,net) end;
fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
(*** Deletion from a discrimination net ***)
-exception DELETE; (*missing item in the net*)
+exception DELETE; (*missing item in the net*)
(*Create a new Net node if it would be nonempty*)
fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
@@ -124,19 +124,19 @@
let fun del1 ([], Leaf xs) =
if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x))
else raise DELETE
- | del1 (keys, Leaf[]) = raise DELETE
- | del1 (CombK :: keys, Net{comb,var,alist}) =
- newnet{comb=del1(keys,comb), var=var, alist=alist}
- | del1 (VarK :: keys, Net{comb,var,alist}) =
- newnet{comb=comb, var=del1(keys,var), alist=alist}
- | del1 (AtomK a :: keys, Net{comb,var,alist}) =
- let fun newpair net = (a, del1(keys,net))
- fun dellist [] = raise DELETE
- | dellist((b: string, netb) :: alist) =
- if a=b then conspair(newpair netb, alist)
- else if a<b then (*absent*) raise DELETE
- else (*a>b*) (b,netb) :: dellist alist
- in newnet{comb=comb, var=var, alist= dellist alist} end
+ | del1 (keys, Leaf[]) = raise DELETE
+ | del1 (CombK :: keys, Net{comb,var,alist}) =
+ newnet{comb=del1(keys,comb), var=var, alist=alist}
+ | del1 (VarK :: keys, Net{comb,var,alist}) =
+ newnet{comb=comb, var=del1(keys,var), alist=alist}
+ | del1 (AtomK a :: keys, Net{comb,var,alist}) =
+ let fun newpair net = (a, del1(keys,net))
+ fun dellist [] = raise DELETE
+ | dellist((b: string, netb) :: alist) =
+ if a=b then conspair(newpair netb, alist)
+ else if a<b then (*absent*) raise DELETE
+ else (*a>b*) (b,netb) :: dellist alist
+ in newnet{comb=comb, var=var, alist= dellist alist} end
in del1 (keys,net) end;
fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
@@ -154,7 +154,7 @@
(*Return the list of items at the given node, [] if no such node*)
fun lookup (Leaf(xs), []) = xs
- | lookup (Leaf _, _::_) = [] (*non-empty keys and empty net*)
+ | lookup (Leaf _, _::_) = [] (*non-empty keys and empty net*)
| lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
| lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
| lookup (Net{comb,var,alist}, AtomK a :: keys) =
@@ -166,7 +166,7 @@
| net_skip (Net{comb,var,alist}, nets) =
foldr net_skip
(net_skip (comb,[]),
- foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
+ foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
(** Matching and Unification**)
@@ -182,25 +182,25 @@
*)
fun matching unif t (net,nets) =
let fun rands _ (Leaf _, nets) = nets
- | rands t (Net{comb,alist,...}, nets) =
- case t of
- f$t => foldr (matching unif t) (rands f (comb,[]), nets)
- | Const(c,_) => look1 (alist, c) nets
- | Free(c,_) => look1 (alist, c) nets
- | Bound i => look1 (alist, string_of_bound i) nets
- | _ => nets
+ | rands t (Net{comb,alist,...}, nets) =
+ case t of
+ f$t => foldr (matching unif t) (rands f (comb,[]), nets)
+ | Const(c,_) => look1 (alist, c) nets
+ | Free(c,_) => look1 (alist, c) nets
+ | Bound i => look1 (alist, string_of_bound i) nets
+ | _ => nets
in
case net of
- Leaf _ => nets
+ Leaf _ => nets
| Net{var,...} =>
- case (head_of t) of
- Var _ => if unif then net_skip (net,nets)
- else var::nets (*only matches Var in net*)
+ case (head_of t) of
+ Var _ => if unif then net_skip (net,nets)
+ else var::nets (*only matches Var in net*)
(*If "unif" then a var instantiation in the abstraction could allow
an eta-reduction, so regard the abstraction as a wildcard.*)
- | Abs _ => if unif then net_skip (net,nets)
- else var::nets (*only a Var can match*)
- | _ => rands t (net, var::nets) (*var could match also*)
+ | Abs _ => if unif then net_skip (net,nets)
+ else var::nets (*only a Var can match*)
+ | _ => rands t (net, var::nets) (*var could match also*)
end;
val extract_leaves = flat o map (fn Leaf(xs) => xs);
--- a/src/Pure/pattern.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/pattern.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: pattern
+(* Title: pattern
ID: $Id$
- Author: Tobias Nipkow and Christine Heinzelmann, TU Muenchen
+ Author: Tobias Nipkow and Christine Heinzelmann, TU Muenchen
Copyright 1993 TU Muenchen
Unification of Higher-Order Patterns.
@@ -229,8 +229,8 @@
fun eta_contract (Abs(a,T,body)) =
(case eta_contract body of
body' as (f $ Bound i) =>
- if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f
- else Abs(a,T,body')
+ if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f
+ else Abs(a,T,body')
| body' => Abs(a,T,body'))
| eta_contract(f$t) = eta_contract f $ eta_contract t
| eta_contract t = t;
@@ -247,22 +247,22 @@
Does not notice eta-equality, thus f does not match %(x)f(x) *)
fun fomatch tsig (pat,obj) =
let fun typ_match args = (Type.typ_match tsig args)
- handle Type.TYPE_MATCH => raise MATCH;
+ handle Type.TYPE_MATCH => raise MATCH;
fun mtch (tyinsts,insts) = fn
- (Var(ixn,T), t) =>
- if loose_bvar(t,0) then raise MATCH
- else (case assoc(insts,ixn) of
- None => (typ_match (tyinsts, (T, fastype_of t)),
- (ixn,t)::insts)
- | Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
+ (Var(ixn,T), t) =>
+ if loose_bvar(t,0) then raise MATCH
+ else (case assoc(insts,ixn) of
+ None => (typ_match (tyinsts, (T, fastype_of t)),
+ (ixn,t)::insts)
+ | Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
| (Free (a,T), Free (b,U)) =>
- if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
+ if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
| (Const (a,T), Const (b,U)) =>
- if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
+ if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
| (Bound i, Bound j) =>
if i=j then (tyinsts,insts) else raise MATCH
| (Abs(_,T,t), Abs(_,U,u)) =>
- mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
+ mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
| (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u)
| _ => raise MATCH
in mtch([],[]) (eta_contract pat,eta_contract obj) end;
--- a/src/Pure/section_utils.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/section_utils.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Pure/section-utils
+(* Title: Pure/section-utils
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Utilities for writing new theory sections
@@ -49,16 +49,16 @@
Does not handle the \ddd form; no error checking*)
fun escape [] = []
| escape cs = (case take_prefix (not o is_backslash) cs of
- (front, []) => front
+ (front, []) => front
| (front, _::"n"::rest) => front @ ("\n" :: escape rest)
| (front, _::"t"::rest) => front @ ("\t" :: escape rest)
| (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
| (front, _::"\""::rest) => front @ ("\"" :: escape rest)
| (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
| (front, b::c::rest) =>
- if is_blank c (*remove any further blanks and the following \ *)
- then front @ escape (tl (snd (take_prefix is_blank rest)))
- else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
+ if is_blank c (*remove any further blanks and the following \ *)
+ then front @ escape (tl (snd (take_prefix is_blank rest)))
+ else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
(*Remove the first and last charaters -- presumed to be quotes*)
val trim = implode o escape o rev o tl o rev o tl o explode;
--- a/src/Pure/sequence.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/sequence.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: sequence
+(* Title: sequence
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1988 University of Cambridge
Unbounded sequences implemented by closures.
@@ -14,24 +14,24 @@
signature SEQUENCE =
sig
type 'a seq
- val append : 'a seq * 'a seq -> 'a seq
- val chop : int * 'a seq -> 'a list * 'a seq
- val cons : 'a * 'a seq -> 'a seq
- val filters : ('a -> bool) -> 'a seq -> 'a seq
- val flats : 'a seq seq -> 'a seq
- val hd : 'a seq -> 'a
+ val append : 'a seq * 'a seq -> 'a seq
+ val chop : int * 'a seq -> 'a list * 'a seq
+ val cons : 'a * 'a seq -> 'a seq
+ val filters : ('a -> bool) -> 'a seq -> 'a seq
+ val flats : 'a seq seq -> 'a seq
+ val hd : 'a seq -> 'a
val interleave: 'a seq * 'a seq -> 'a seq
- val its_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
- val list_of_s : 'a seq -> 'a list
- val mapp : ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
- val maps : ('a -> 'b) -> 'a seq -> 'b seq
- val null : 'a seq
- val prints : (int -> 'a -> unit) -> int -> 'a seq -> unit
- val pull : 'a seq -> ('a * 'a seq) option
- val s_of_list : 'a list -> 'a seq
- val seqof : (unit -> ('a * 'a seq) option) -> 'a seq
- val single : 'a -> 'a seq
- val tl : 'a seq -> 'a seq
+ val its_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+ val list_of_s : 'a seq -> 'a list
+ val mapp : ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
+ val maps : ('a -> 'b) -> 'a seq -> 'b seq
+ val null : 'a seq
+ val prints : (int -> 'a -> unit) -> int -> 'a seq -> unit
+ val pull : 'a seq -> ('a * 'a seq) option
+ val s_of_list : 'a list -> 'a seq
+ val seqof : (unit -> ('a * 'a seq) option) -> 'a seq
+ val single : 'a -> 'a seq
+ val tl : 'a seq -> 'a seq
end;
@@ -67,7 +67,7 @@
else case pull(s) of
None => ([],s)
| Some(x,s') => let val (xs,s'') = chop (n-1,s')
- in (x::xs, s'') end;
+ in (x::xs, s'') end;
(*conversion from sequence to list*)
fun list_of_s (s: 'a seq) : 'a list = case pull(s) of
@@ -84,10 +84,10 @@
the function prelem should print the element number and also the element*)
fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
let fun pr (k,s) =
- if k>count then ()
- else case pull(s) of
- None => ()
- | Some(x,s') => (prelem k x; prs"\n"; pr (k+1, s'))
+ if k>count then ()
+ else case pull(s) of
+ None => ()
+ | Some(x,s') => (prelem k x; prs"\n"; pr (k+1, s'))
in pr(1,s) end;
(*Map the function f over the sequence, making a new sequence*)
@@ -98,22 +98,22 @@
(*Sequence append: put the elements of xq in front of those of yq*)
fun append (xq,yq) =
let fun copy xq = seqof (fn()=>
- case pull xq of
- None => pull yq
- | Some(x,xq') => Some (x, copy xq'))
+ case pull xq of
+ None => pull yq
+ | Some(x,xq') => Some (x, copy xq'))
in copy xq end;
(*Interleave elements of xq with those of yq -- fairer than append*)
fun interleave (xq,yq) = seqof (fn()=>
case pull(xq) of
None => pull yq
- | Some(x,xq') => Some (x, interleave(yq, xq')));
+ | Some(x,xq') => Some (x, interleave(yq, xq')));
(*map over a sequence xq, append the sequence yq*)
fun mapp f xq yq =
let fun copy s = seqof (fn()=>
case pull(s) of
- None => pull(yq)
+ None => pull(yq)
| Some(x,xq') => Some(f x, copy xq'))
in copy xq end;
@@ -126,16 +126,16 @@
fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq =
let fun its s = seqof (fn()=>
case pull(s) of
- None => pull bstr
- | Some(a,s') => pull(f(a, its s')))
+ None => pull bstr
+ | Some(a,s') => pull(f(a, its s')))
in its s end;
fun filters pred xq =
let fun copy s = seqof (fn()=>
case pull(s) of
- None => None
+ None => None
| Some(x,xq') => if pred x then Some(x, copy xq')
- else pull (copy xq') )
+ else pull (copy xq') )
in copy xq end
end;
--- a/src/Pure/sign.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/sign.ML Mon Jan 29 14:16:13 1996 +0100
@@ -266,13 +266,13 @@
(*Package error messages from type checking*)
fun exn_type_msg sg (msg, Ts, ts) =
let val show_typ = string_of_typ sg
- val show_term = string_of_term sg
- fun term_err [] = ""
- | term_err [t] = "\nInvolving this term:\n" ^ show_term t
- | term_err ts =
- "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
+ val show_term = string_of_term sg
+ fun term_err [] = ""
+ | term_err [t] = "\nInvolving this term:\n" ^ show_term t
+ | term_err ts =
+ "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
in "\nType checking error: " ^ msg ^ "\n" ^
- cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
+ cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
end;
@@ -308,7 +308,7 @@
fun process_term(res,(t,i)) =
let val ([u],tye) =
- Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
+ Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
in case res of
One(_,t0,_) => Ambigs([u,t0])
| Errs _ => One(i,u,tye)
@@ -406,9 +406,9 @@
fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
let
fun prep_const (c, ty, mx) =
- (c,
- compress_type (varifyT (cert_typ tsig (no_tvars ty))),
- mx)
+ (c,
+ compress_type (varifyT (cert_typ tsig (no_tvars ty))),
+ mx)
handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
val consts = map (prep_const o rd_const syn tsig) raw_consts;
--- a/src/Pure/tactic.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/tactic.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: tactic
+(* Title: tactic
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Tactics
@@ -83,8 +83,8 @@
functor TacticFun (structure Logic: LOGIC and Drule: DRULE and
- Tactical: TACTICAL and Net: NET
- sharing Drule.Thm = Tactical.Thm) : TACTIC =
+ Tactical: TACTICAL and Net: NET
+ sharing Drule.Thm = Tactical.Thm) : TACTIC =
struct
structure Tactical = Tactical;
structure Thm = Tactical.Thm;
@@ -97,9 +97,9 @@
(*Discover what goal is chosen: SOMEGOAL(trace_goalno_tac tac) *)
fun trace_goalno_tac tf i = Tactic (fn state =>
case Sequence.pull(tapply(tf i, state)) of
- None => Sequence.null
+ None => Sequence.null
| seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n");
- Sequence.seqof(fn()=> seqcell)));
+ Sequence.seqof(fn()=> seqcell)));
fun string_of (a,0) = a
| string_of (a,i) = a ^ "_" ^ string_of_int i;
@@ -109,22 +109,22 @@
let val fth = freezeT th
val {prop,sign,...} = rep_thm fth
fun mk_inst (Var(v,T)) =
- (cterm_of sign (Var(v,T)),
- cterm_of sign (Free(string_of v, T)))
+ (cterm_of sign (Var(v,T)),
+ cterm_of sign (Free(string_of v, T)))
val insts = map mk_inst (term_vars prop)
in instantiate ([],insts) fth end;
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic (Tactic tf) rl =
case Sequence.pull(tf (freeze (standard rl))) of
- None => raise THM("rule_by_tactic", 0, [rl])
+ None => raise THM("rule_by_tactic", 0, [rl])
| Some(rl',_) => standard rl';
(*** Basic tactics ***)
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
- handle THM _ => Sequence.null);
+ handle THM _ => Sequence.null);
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
@@ -164,9 +164,9 @@
fun dresolve_tac rls = eresolve_tac (map make_elim rls);
(*Shorthand versions: for resolution with a single theorem*)
-fun rtac rl = rtac rl ;
-fun etac rl = etac rl ;
-fun dtac rl = dtac rl ;
+fun rtac rl = resolve_tac [rl];
+fun etac rl = eresolve_tac [rl];
+fun dtac rl = dresolve_tac [rl];
val atac = assume_tac;
(*Use an assumption or some rules ... A popular combination!*)
@@ -185,19 +185,19 @@
fun lift_inst_rule (state, i, sinsts, rule) =
let val {maxidx,sign,...} = rep_thm state
val (_, _, Bi, _) = dest_state(state,i)
- val params = Logic.strip_params Bi (*params of subgoal i*)
+ val params = Logic.strip_params Bi (*params of subgoal i*)
val params = rev(rename_wrt_term Bi params) (*as they are printed*)
val paramTs = map #2 params
and inc = maxidx+1
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
| liftvar t = raise TERM("Variable expected", [t]);
fun liftterm t = list_abs_free (params,
- Logic.incr_indexes(paramTs,inc) t)
+ Logic.incr_indexes(paramTs,inc) t)
(*Lifts instantiation pair over params*)
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
fun lifttvar((a,i),ctyp) =
- let val {T,sign} = rep_ctyp ctyp
- in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+ let val {T,sign} = rep_ctyp ctyp
+ in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
val rts = types_sorts rule and (types,sorts) = types_sorts state
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
| types'(ixn) = types ixn;
@@ -215,10 +215,10 @@
(*compose version: arguments are as for bicompose.*)
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
STATE ( fn state =>
- compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
- nsubgoal) i
- handle TERM (msg,_) => (writeln msg; no_tac)
- | THM (msg,_,_) => (writeln msg; no_tac) );
+ compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
+ nsubgoal) i
+ handle TERM (msg,_) => (writeln msg; no_tac)
+ | THM (msg,_,_) => (writeln msg; no_tac) );
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the
terms that are substituted contain (term or type) unknowns from the
@@ -242,8 +242,8 @@
let val {maxidx,...} = rep_thm rl
fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
val revcut_rl' =
- instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)),
- (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
+ instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)),
+ (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
val arg = (false, rl, nprems_of rl)
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
in th end
@@ -262,7 +262,7 @@
(*Used by metacut_tac*)
fun bires_cut_tac arg i =
- rtac cut_rl i THEN biresolve_tac arg (i+1) ;
+ resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ;
(*The conclusion of the rule gets assumed in subgoal i,
while subgoal i+1,... are the premises of the rule.*)
@@ -271,7 +271,7 @@
(*Recognizes theorems that are not rules, but simple propositions*)
fun is_fact rl =
case prems_of rl of
- [] => true | _::_ => false;
+ [] => true | _::_ => false;
(*"Cut" all facts from theorem list into the goal as assumptions. *)
fun cut_facts_tac ths i =
@@ -287,15 +287,15 @@
(**** Indexing and filtering of theorems ****)
(*Returns the list of potentially resolvable theorems for the goal "prem",
- using the predicate could(subgoal,concl).
+ using the predicate could(subgoal,concl).
Resulting list is no longer than "limit"*)
fun filter_thms could (limit, prem, ths) =
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*)
fun filtr (limit, []) = []
- | filtr (limit, th::ths) =
- if limit=0 then []
- else if could(pb, concl_of th) then th :: filtr(limit-1, ths)
- else filtr(limit,ths)
+ | filtr (limit, th::ths) =
+ if limit=0 then []
+ else if could(pb, concl_of th) then th :: filtr(limit-1, ths)
+ else filtr(limit,ths)
in filtr(limit,ths) end;
@@ -320,9 +320,9 @@
(*insert one tagged brl into the pair of nets*)
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
if eres then
- case prems_of th of
- prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
- | [] => error"insert_tagged_brl: elimination rule with no premises"
+ case prems_of th of
+ prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
+ | [] => error"insert_tagged_brl: elimination rule with no premises"
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
(*build a pair of nets for biresolution*)
@@ -366,9 +366,9 @@
(fn (prem,i) =>
let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
in
- if pred krls
+ if pred krls
then PRIMSEQ
- (biresolution match (map (pair false) (orderlist krls)) i)
+ (biresolution match (map (pair false) (orderlist krls)) i)
else no_tac
end);
@@ -414,7 +414,7 @@
(*Rewrite subgoals only, not main goal. *)
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
-fun rewtac def = rewtac def;
+fun rewtac def = rewrite_goals_tac [def];
(*** Tactic for folding definitions, handling critical pairs ***)
@@ -451,7 +451,7 @@
in
if !Logic.auto_rename
then (writeln"Note: setting Logic.auto_rename := false";
- Logic.auto_rename := false)
+ Logic.auto_rename := false)
else ();
case #2 (take_prefix (is_letdig orf is_blank) cs) of
[] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
--- a/src/Pure/tctical.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/tctical.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: tctical
+(* Title: tctical
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Tacticals
@@ -17,65 +17,65 @@
structure Thm : THM
local open Thm in
datatype tactic = Tactic of thm -> thm Sequence.seq
- val all_tac : tactic
- val ALLGOALS : (int -> tactic) -> tactic
- val APPEND : tactic * tactic -> tactic
- val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
- val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
- val CHANGED : tactic -> tactic
- val COND : (thm -> bool) -> tactic -> tactic -> tactic
- val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
- val DEPTH_SOLVE : tactic -> tactic
- val DEPTH_SOLVE_1 : tactic -> tactic
- val DETERM : tactic -> tactic
- val EVERY : tactic list -> tactic
- val EVERY' : ('a -> tactic) list -> 'a -> tactic
- val EVERY1 : (int -> tactic) list -> tactic
- val FILTER : (thm -> bool) -> tactic -> tactic
- val FIRST : tactic list -> tactic
- val FIRST' : ('a -> tactic) list -> 'a -> tactic
- val FIRST1 : (int -> tactic) list -> tactic
- val FIRSTGOAL : (int -> tactic) -> tactic
- val goals_limit : int ref
- val has_fewer_prems : int -> thm -> bool
- val IF_UNSOLVED : tactic -> tactic
- val INTLEAVE : tactic * tactic -> tactic
- val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val METAHYPS : (thm list -> tactic) -> int -> tactic
- val no_tac : tactic
- val ORELSE : tactic * tactic -> tactic
- val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val pause_tac : tactic
- val print_tac : tactic
- val REPEAT : tactic -> tactic
- val REPEAT1 : tactic -> tactic
- val REPEAT_DETERM_N : int -> tactic -> tactic
- val REPEAT_DETERM : tactic -> tactic
- val REPEAT_DETERM1 : tactic -> tactic
+ val all_tac : tactic
+ val ALLGOALS : (int -> tactic) -> tactic
+ val APPEND : tactic * tactic -> tactic
+ val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
+ val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
+ val CHANGED : tactic -> tactic
+ val COND : (thm -> bool) -> tactic -> tactic -> tactic
+ val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
+ val DEPTH_SOLVE : tactic -> tactic
+ val DEPTH_SOLVE_1 : tactic -> tactic
+ val DETERM : tactic -> tactic
+ val EVERY : tactic list -> tactic
+ val EVERY' : ('a -> tactic) list -> 'a -> tactic
+ val EVERY1 : (int -> tactic) list -> tactic
+ val FILTER : (thm -> bool) -> tactic -> tactic
+ val FIRST : tactic list -> tactic
+ val FIRST' : ('a -> tactic) list -> 'a -> tactic
+ val FIRST1 : (int -> tactic) list -> tactic
+ val FIRSTGOAL : (int -> tactic) -> tactic
+ val goals_limit : int ref
+ val has_fewer_prems : int -> thm -> bool
+ val IF_UNSOLVED : tactic -> tactic
+ val INTLEAVE : tactic * tactic -> tactic
+ val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val METAHYPS : (thm list -> tactic) -> int -> tactic
+ val no_tac : tactic
+ val ORELSE : tactic * tactic -> tactic
+ val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val pause_tac : tactic
+ val print_tac : tactic
+ val REPEAT : tactic -> tactic
+ val REPEAT1 : tactic -> tactic
+ val REPEAT_DETERM_N : int -> tactic -> tactic
+ val REPEAT_DETERM : tactic -> tactic
+ val REPEAT_DETERM1 : tactic -> tactic
val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
- val REPEAT_FIRST : (int -> tactic) -> tactic
- val REPEAT_SOME : (int -> tactic) -> tactic
- val SELECT_GOAL : tactic -> int -> tactic
- val SOMEGOAL : (int -> tactic) -> tactic
- val STATE : (thm -> tactic) -> tactic
- val strip_context : term -> (string * typ) list * term list * term
- val SUBGOAL : ((term*int) -> tactic) -> int -> tactic
- val suppress_tracing : bool ref
- val tapply : tactic * thm -> thm Sequence.seq
- val THEN : tactic * tactic -> tactic
- val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
- val THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
- -> tactic
- val THEN_ELSE : tactic * (tactic*tactic) -> tactic
- val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic
- val tracify : bool ref -> tactic -> thm -> thm Sequence.seq
- val trace_BEST_FIRST : bool ref
- val trace_DEPTH_FIRST : bool ref
- val trace_REPEAT : bool ref
- val TRY : tactic -> tactic
- val TRYALL : (int -> tactic) -> tactic
+ val REPEAT_FIRST : (int -> tactic) -> tactic
+ val REPEAT_SOME : (int -> tactic) -> tactic
+ val SELECT_GOAL : tactic -> int -> tactic
+ val SOMEGOAL : (int -> tactic) -> tactic
+ val STATE : (thm -> tactic) -> tactic
+ val strip_context : term -> (string * typ) list * term list * term
+ val SUBGOAL : ((term*int) -> tactic) -> int -> tactic
+ val suppress_tracing : bool ref
+ val tapply : tactic * thm -> thm Sequence.seq
+ val THEN : tactic * tactic -> tactic
+ val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+ val THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
+ -> tactic
+ val THEN_ELSE : tactic * (tactic*tactic) -> tactic
+ val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic
+ val tracify : bool ref -> tactic -> thm -> thm Sequence.seq
+ val trace_BEST_FIRST : bool ref
+ val trace_DEPTH_FIRST : bool ref
+ val trace_REPEAT : bool ref
+ val TRY : tactic -> tactic
+ val TRYALL : (int -> tactic) -> tactic
end
end;
@@ -115,7 +115,7 @@
fun (Tactic tf1) ORELSE (Tactic tf2) =
Tactic (fn state =>
case Sequence.pull(tf1 state) of
- None => tf2 state
+ None => tf2 state
| sequencecell => Sequence.seqof(fn()=> sequencecell));
@@ -132,15 +132,15 @@
Sequence.seqof(fn()=> Sequence.pull (tf2 state))));
(*Conditional tactic.
- tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
- tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
+ tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
+ tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
*)
fun (Tactic tf) THEN_ELSE (Tactic tf1, Tactic tf2) =
Tactic (fn state =>
case Sequence.pull(tf state) of
- None => tf2 state (*failed; try tactic 2*)
- | seqcell => Sequence.flats (*succeeded; use tactic 1*)
- (Sequence.maps tf1 (Sequence.seqof(fn()=> seqcell))));
+ None => tf2 state (*failed; try tactic 2*)
+ | seqcell => Sequence.flats (*succeeded; use tactic 1*)
+ (Sequence.maps tf1 (Sequence.seqof(fn()=> seqcell))));
(*Versions for combining tactic-valued functions, as in
@@ -160,7 +160,7 @@
(*Make a tactic deterministic by chopping the tail of the proof sequence*)
fun DETERM (Tactic tf) = Tactic (fn state =>
case Sequence.pull (tf state) of
- None => Sequence.null
+ None => Sequence.null
| Some(x,_) => Sequence.cons(x, Sequence.null));
@@ -242,15 +242,15 @@
fun tracify flag (Tactic tf) state =
if !flag andalso not (!suppress_tracing)
then (!print_goals_ref (!goals_limit) state;
- prs"** Press RETURN to continue: ";
- exec_trace_command flag (tf,state))
+ prs"** Press RETURN to continue: ";
+ exec_trace_command flag (tf,state))
else tf state;
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
fun traced_tac seqf = Tactic (fn st =>
(suppress_tracing := false;
Sequence.seqof (fn()=> seqf st
- handle TRACE_EXIT st' => Some(st', Sequence.null))));
+ handle TRACE_EXIT st' => Some(st', Sequence.null))));
(*Deterministic REPEAT: only retains the first outcome;
@@ -259,10 +259,10 @@
fun REPEAT_DETERM_N n tac =
let val tf = tracify trace_REPEAT tac
fun drep 0 st = Some(st, Sequence.null)
- | drep n st =
- (case Sequence.pull(tf st) of
- None => Some(st, Sequence.null)
- | Some(st',_) => drep (n-1) st')
+ | drep n st =
+ (case Sequence.pull(tf st) of
+ None => Some(st, Sequence.null)
+ | Some(st',_) => drep (n-1) st')
in traced_tac (drep n) end;
(*Allows any number of repetitions*)
@@ -272,12 +272,12 @@
fun REPEAT tac =
let val tf = tracify trace_REPEAT tac
fun rep qs st =
- case Sequence.pull(tf st) of
- None => Some(st, Sequence.seqof(fn()=> repq qs))
+ case Sequence.pull(tf st) of
+ None => Some(st, Sequence.seqof(fn()=> repq qs))
| Some(st',q) => rep (q::qs) st'
and repq [] = None
| repq(q::qs) = case Sequence.pull q of
- None => repq qs
+ None => repq qs
| Some(st,q) => rep (q::qs) st
in traced_tac (rep []) end;
@@ -294,13 +294,13 @@
let val tf = tracify trace_DEPTH_FIRST tac
fun depth used [] = None
| depth used (q::qs) =
- case Sequence.pull q of
- None => depth used qs
- | Some(st,stq) =>
- if satp st andalso not (gen_mem eq_thm (st, used))
- then Some(st, Sequence.seqof
- (fn()=> depth (st::used) (stq::qs)))
- else depth used (tf st :: stq :: qs)
+ case Sequence.pull q of
+ None => depth used qs
+ | Some(st,stq) =>
+ if satp st andalso not (gen_mem eq_thm (st, used))
+ then Some(st, Sequence.seqof
+ (fn()=> depth (st::used) (stq::qs)))
+ else depth used (tf st :: stq :: qs)
in traced_tac (fn st => depth [] ([Sequence.single st])) end;
@@ -316,7 +316,7 @@
fun DEPTH_SOLVE_1 tac = STATE
(fn state =>
(case nprems_of state of
- 0 => no_tac
+ 0 => no_tac
| n => DEPTH_FIRST (has_fewer_prems n) tac));
(*Uses depth-first search to solve ALL subgoals*)
@@ -344,17 +344,17 @@
let val tf = tracify trace_BEST_FIRST tac
fun pairsize th = (sizef th, th);
fun bfs (news,nprfs) =
- (case partition satp news of
- ([],nonsats) => next(foldr insert
- (map pairsize nonsats, nprfs))
- | (sats,_) => some_of_list sats)
+ (case partition satp news of
+ ([],nonsats) => next(foldr insert
+ (map pairsize nonsats, nprfs))
+ | (sats,_) => some_of_list sats)
and next [] = None
| next ((n,prf)::nprfs) =
- (if !trace_BEST_FIRST
- then writeln("state size = " ^ string_of_int n ^
- " queue length =" ^ string_of_int (length nprfs))
+ (if !trace_BEST_FIRST
+ then writeln("state size = " ^ string_of_int n ^
+ " queue length =" ^ string_of_int (length nprfs))
else ();
- bfs (Sequence.list_of_s (tf prf), nprfs))
+ bfs (Sequence.list_of_s (tf prf), nprfs))
fun tf st = bfs (Sequence.list_of_s (tf0 st), [])
in traced_tac tf end;
@@ -366,12 +366,12 @@
fun BREADTH_FIRST satpred (Tactic tf) =
let val tacf = Sequence.list_of_s o tf;
fun bfs prfs =
- (case partition satpred prfs of
- ([],[]) => []
- | ([],nonsats) =>
- (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
- bfs (flat (map tacf nonsats)))
- | (sats,_) => sats)
+ (case partition satpred prfs of
+ ([],[]) => []
+ | ([],nonsats) =>
+ (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
+ bfs (flat (map tacf nonsats)))
+ | (sats,_) => sats)
in Tactic (fn state => Sequence.s_of_list (bfs [state])) end;
@@ -395,13 +395,13 @@
Essential to work backwards since tf(i) may add/delete subgoals at i. *)
fun ALLGOALS tf =
let fun tac 0 = all_tac
- | tac n = tf(n) THEN tac(n-1)
+ | tac n = tf(n) THEN tac(n-1)
in Tactic(fn state => tapply(tac(nprems_of state), state)) end;
(*For n subgoals, performs tf(n) ORELSE ... ORELSE tf(1) *)
fun SOMEGOAL tf =
let fun tac 0 = no_tac
- | tac n = tf(n) ORELSE tac(n-1)
+ | tac n = tf(n) ORELSE tac(n-1)
in Tactic(fn state => tapply(tac(nprems_of state), state)) end;
(*For n subgoals, performs tf(1) ORELSE ... ORELSE tf(n).
@@ -442,8 +442,8 @@
(* Prevent the subgoal's assumptions from becoming additional subgoals in the
new proof state by enclosing them by a universal quantification *)
fun protect_subgoal state i =
- Sequence.hd (bicompose false (false,dummy_quant_rl,1) i state)
- handle _ => error"SELECT_GOAL -- impossible error???";
+ Sequence.hd (bicompose false (false,dummy_quant_rl,1) i state)
+ handle _ => error"SELECT_GOAL -- impossible error???";
(*Does the work of SELECT_GOAL. *)
fun select (Tactic tf) state i =
@@ -465,10 +465,10 @@
Main difference from strip_assums concerns parameters:
it replaces the bound variables by free variables. *)
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
- strip_context_aux (params, H::Hs, B)
+ strip_context_aux (params, H::Hs, B)
| strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
let val (b,u) = variant_abs(a,T,t)
- in strip_context_aux ((b,T)::params, Hs, u) end
+ in strip_context_aux ((b,T)::params, Hs, u) end
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
fun strip_context A = strip_context_aux ([],[],A);
@@ -498,7 +498,7 @@
fun free_of s ((a,i), T) =
Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i),
- T)
+ T)
fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T))
in
@@ -520,17 +520,17 @@
(*Subgoal variables: make Free; lift type over params*)
fun mk_subgoal_inst concl_vars (var as Var(v,T)) =
if var mem concl_vars
- then (var, true, free_of "METAHYP2_" (v,T))
- else (var, false,
- free_of "METAHYP2_" (v, map #2 params --->T))
+ then (var, true, free_of "METAHYP2_" (v,T))
+ else (var, false,
+ free_of "METAHYP2_" (v, map #2 params --->T))
(*Instantiate subgoal vars by Free applied to params*)
fun mk_ctpair (t,in_concl,u) =
- if in_concl then (cterm t, cterm u)
+ if in_concl then (cterm t, cterm u)
else (cterm t, cterm (list_comb (u,fparams)))
(*Restore Vars with higher type and index*)
fun mk_subgoal_swap_ctpair
- (t as Var((a,i),_), in_concl, u as Free(_,U)) =
- if in_concl then (cterm u, cterm t)
+ (t as Var((a,i),_), in_concl, u as Free(_,U)) =
+ if in_concl then (cterm u, cterm t)
else (cterm u, cterm(Var((a, i+maxidx), U)))
(*Embed B in the original context of params and hyps*)
fun embed B = list_all_free (params, list_implies (hyps, B))
@@ -538,34 +538,34 @@
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
(*Embed an ff pair in the original params*)
fun embed_ff(t,u) =
- mk_flexpair (list_abs_free (params, t), list_abs_free (params, u))
+ mk_flexpair (list_abs_free (params, t), list_abs_free (params, u))
(*Remove parameter abstractions from the ff pairs*)
fun elim_ff ff = flexpair_abs_elim_list cparams ff
(*A form of lifting that discharges assumptions.*)
fun relift st =
- let val prop = #prop(rep_thm st)
- val subgoal_vars = (*Vars introduced in the subgoals*)
- foldr add_term_vars (strip_imp_prems prop, [])
- and concl_vars = add_term_vars (strip_imp_concl prop, [])
- val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
- val st' = instantiate ([], map mk_ctpair subgoal_insts) st
- val emBs = map (cterm o embed) (prems_of st')
+ let val prop = #prop(rep_thm st)
+ val subgoal_vars = (*Vars introduced in the subgoals*)
+ foldr add_term_vars (strip_imp_prems prop, [])
+ and concl_vars = add_term_vars (strip_imp_concl prop, [])
+ val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
+ val st' = instantiate ([], map mk_ctpair subgoal_insts) st
+ val emBs = map (cterm o embed) (prems_of st')
and ffs = map (cterm o embed_ff) (tpairs_of st')
- val Cth = implies_elim_list st'
- (map (elim_ff o assume) ffs @
- map (elim o assume) emBs)
- in (*restore the unknowns to the hypotheses*)
- free_instantiate (map swap_ctpair insts @
- map mk_subgoal_swap_ctpair subgoal_insts)
- (*discharge assumptions from state in same order*)
- (implies_intr_list (ffs@emBs)
- (forall_intr_list cparams (implies_intr_list chyps Cth)))
- end
+ val Cth = implies_elim_list st'
+ (map (elim_ff o assume) ffs @
+ map (elim o assume) emBs)
+ in (*restore the unknowns to the hypotheses*)
+ free_instantiate (map swap_ctpair insts @
+ map mk_subgoal_swap_ctpair subgoal_insts)
+ (*discharge assumptions from state in same order*)
+ (implies_intr_list (ffs@emBs)
+ (forall_intr_list cparams (implies_intr_list chyps Cth)))
+ end
val subprems = map (forall_elim_vars 0) hypths
and st0 = trivial (cterm concl)
(*function to replace the current subgoal*)
fun next st = bicompose false (false, relift st, nprems_of st)
- i state
+ i state
in Sequence.flats (Sequence.maps next (tapply(tacf subprems, st0)))
end);
end;
--- a/src/Pure/term.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/term.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Pure/term.ML
+(* Title: Pure/term.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright Cambridge University 1992
Simply typed lambda-calculus: types, terms, and basic operations
@@ -26,7 +26,7 @@
(* The sorts attached to TFrees and TVars specify the sort of that variable *)
datatype typ = Type of string * typ list
| TFree of string * sort
- | TVar of indexname * sort;
+ | TVar of indexname * sort;
fun S --> T = Type("fun",[S,T]);
@@ -120,19 +120,19 @@
fun type_of1 (Ts, Const (_,T)) = T
| type_of1 (Ts, Free (_,T)) = T
| type_of1 (Ts, Bound i) = (nth_elem (i,Ts)
- handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
+ handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
| type_of1 (Ts, Var (_,T)) = T
| type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
| type_of1 (Ts, f$u) =
let val U = type_of1(Ts,u)
and T = type_of1(Ts,f)
in case T of
- Type("fun",[T1,T2]) =>
- if T1=U then T2 else raise TYPE
- ("type_of: type mismatch in application", [T1,U], [f$u])
- | _ => raise TYPE
- ("type_of: function type is expected in application",
- [T,U], [f$u])
+ Type("fun",[T1,T2]) =>
+ if T1=U then T2 else raise TYPE
+ ("type_of: type mismatch in application", [T1,U], [f$u])
+ | _ => raise TYPE
+ ("type_of: function type is expected in application",
+ [T,U], [f$u])
end;
fun type_of t : typ = type_of1 ([],t);
@@ -140,12 +140,12 @@
(*Determines the type of a term, with minimal checking*)
fun fastype_of1 (Ts, f$u) =
(case fastype_of1 (Ts,f) of
- Type("fun",[_,T]) => T
- | _ => raise TERM("fastype_of: expected function type", [f$u]))
+ Type("fun",[_,T]) => T
+ | _ => raise TERM("fastype_of: expected function type", [f$u]))
| fastype_of1 (_, Const (_,T)) = T
| fastype_of1 (_, Free (_,T)) = T
| fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
- handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
+ handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
| fastype_of1 (_, Var (_,T)) = T
| fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
@@ -247,7 +247,7 @@
(* maps !!x1...xn. t to [x1, ..., xn] *)
fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =
- (a,T) :: strip_all_vars t
+ (a,T) :: strip_all_vars t
| strip_all_vars t = [] : (string*typ) list;
(*increments a term's non-local bound variables
@@ -256,7 +256,7 @@
lev is level at which a bound variable is considered 'loose'*)
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
| incr_bv (inc, lev, Abs(a,T,body)) =
- Abs(a, T, incr_bv(inc,lev+1,body))
+ Abs(a, T, incr_bv(inc,lev+1,body))
| incr_bv (inc, lev, f$t) =
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
| incr_bv (inc, lev, u) = u;
@@ -268,10 +268,10 @@
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
(Bound 0) is loose at level 0 *)
fun add_loose_bnos (Bound i, lev, js) =
- if i<lev then js else (i-lev) ins js
+ if i<lev then js else (i-lev) ins js
| add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
| add_loose_bnos (f$t, lev, js) =
- add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
+ add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
| add_loose_bnos (_, _, js) = js;
fun loose_bnos t = add_loose_bnos (t, 0, []);
@@ -287,20 +287,20 @@
(*Substitute arguments for loose bound variables.
Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0
- and the appropriate call is subst_bounds([b,a], c) .
+ and the appropriate call is subst_bounds([b,a], c) .
Loose bound variables >=n are reduced by "n" to
compensate for the disappearance of lambdas.
*)
fun subst_bounds (args: term list, t) : term =
let val n = length args;
fun subst (t as Bound i, lev) =
- if i<lev then t (*var is locally bound*)
- else (case (drop (i-lev,args)) of
- [] => Bound(i-n) (*loose: change it*)
- | arg::_ => incr_boundvars lev arg)
- | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
- | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
- | subst (t,lev) = t
+ if i<lev then t (*var is locally bound*)
+ else (case (drop (i-lev,args)) of
+ [] => Bound(i-n) (*loose: change it*)
+ | arg::_ => incr_boundvars lev arg)
+ | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
+ | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
+ | subst (t,lev) = t
in case args of [] => t | _ => subst (t,0) end;
(*beta-reduce if possible, else form application*)
@@ -326,9 +326,9 @@
Terms must be NORMAL. Treats all Vars as distinct. *)
fun could_unify (t,u) =
let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g)
- | matchrands _ = true
+ | matchrands _ = true
in case (head_of t , head_of u) of
- (_, Var _) => true
+ (_, Var _) => true
| (Var _, _) => true
| (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u)
| (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u)
@@ -342,11 +342,11 @@
fun subst_free [] = (fn t=>t)
| subst_free pairs =
let fun substf u =
- case gen_assoc (op aconv) (pairs, u) of
- Some u' => u'
- | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
- | t$u' => substf t $ substf u'
- | _ => u)
+ case gen_assoc (op aconv) (pairs, u) of
+ Some u' => u'
+ | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
+ | t$u' => substf t $ substf u'
+ | _ => u)
in substf end;
(*a total, irreflexive ordering on index names*)
@@ -360,8 +360,8 @@
let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
(case u of
Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
- | f$rand => abst(lev,f) $ abst(lev,rand)
- | _ => u)
+ | f$rand => abst(lev,f) $ abst(lev,rand)
+ | _ => u)
in abst(0,body) end;
@@ -388,16 +388,16 @@
fun subst_atomic [] t = t : term
| subst_atomic (instl: (term*term) list) t =
let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
- | subst (f$t') = subst f $ subst t'
- | subst t = (case assoc(instl,t) of
- Some u => u | None => t)
+ | subst (f$t') = subst f $ subst t'
+ | subst t = (case assoc(instl,t) of
+ Some u => u | None => t)
in subst t end;
(*Substitute for type Vars in a type*)
fun typ_subst_TVars iTs T = if null iTs then T else
let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
- | subst(T as TFree _) = T
- | subst(T as TVar(ixn,_)) =
+ | subst(T as TFree _) = T
+ | subst(T as TVar(ixn,_)) =
(case assoc(iTs,ixn) of None => T | Some(U) => U)
in subst T end;
@@ -428,7 +428,7 @@
(*Computing the maximum index of a typ*)
fun maxidx_of_typ(Type(_,Ts)) =
- if Ts=[] then ~1 else max(map maxidx_of_typ Ts)
+ if Ts=[] then ~1 else max(map maxidx_of_typ Ts)
| maxidx_of_typ(TFree _) = ~1
| maxidx_of_typ(TVar((_,i),_)) = i;
@@ -457,10 +457,10 @@
let val zero = ord"0"
val limit = zero+radix
fun scan (num,[]) = (num,[])
- | scan (num, c::cs) =
- if zero <= ord c andalso ord c < limit
- then scan(radix*num + ord c - zero, cs)
- else (num, c::cs)
+ | scan (num, c::cs) =
+ if zero <= ord c andalso ord c < limit
+ then scan(radix*num + ord c - zero, cs)
+ else (num, c::cs)
in scan(0,cs) end;
fun scan_int cs = scan_radixint(10,cs);
@@ -556,9 +556,9 @@
fun insert_aterm (t,us) =
let fun inserta [] = [t]
| inserta (us as u::us') =
- if atless(t,u) then t::us
- else if t=u then us (*duplicate*)
- else u :: inserta(us')
+ if atless(t,u) then t::us
+ else if t=u then us (*duplicate*)
+ else u :: inserta(us')
in inserta us end;
(*Accumulates the Vars in the term, suppressing duplicates*)
@@ -588,7 +588,7 @@
(* renames and reverses the strings in vars away from names *)
fun rename_aTs names vars : (string*typ)list =
let fun rename_aT (vars,(a,T)) =
- (variant (map #1 vars @ names) a, T) :: vars
+ (variant (map #1 vars @ names) a, T) :: vars
in foldl rename_aT ([],vars) end;
fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
@@ -618,18 +618,18 @@
fun compress_type T =
let val tag = type_tag T
val tylist = the (Symtab.lookup (!memo_types, tag))
- handle _ => []
+ handle _ => []
in
case find_type (T,tylist) of
- Some T' => T'
+ Some T' => T'
| None =>
- let val T' =
- case T of
- Type (a,Ts) => Type (a, map compress_type Ts)
- | _ => T
- in memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
- T
- end
+ let val T' =
+ case T of
+ Type (a,Ts) => Type (a, map compress_type Ts)
+ | _ => T
+ in memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
+ T
+ end
end
handle Match =>
let val Type (a,Ts) = T
@@ -653,13 +653,13 @@
| share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
| share_term t =
let val tag = const_tag t
- val ts = the (Symtab.lookup (!memo_terms, tag))
- handle _ => []
+ val ts = the (Symtab.lookup (!memo_terms, tag))
+ handle _ => []
in
- case find_term (t,ts) of
- Some t' => t'
- | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
- t)
+ case find_term (t,ts) of
+ Some t' => t'
+ | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
+ t)
end;
val compress_term = share_term o map_term_types compress_type;
--- a/src/Pure/thm.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/thm.ML Mon Jan 29 14:16:13 1996 +0100
@@ -219,7 +219,7 @@
Sign.infer_types sign types sorts used freeze (ts, T');
val ct = cterm_of sign t'
handle TYPE arg => error (Sign.exn_type_msg sign arg)
- | TERM (msg, _) => error msg;
+ | TERM (msg, _) => error msg;
in (ct, tye) end;
fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
@@ -231,14 +231,14 @@
let
val {tsig, syn, ...} = Sign.rep_sg sign
fun read (b,T) =
- case Syntax.read syn T b of
- [t] => t
- | _ => error("Error or ambiguity in parsing of " ^ b)
+ case Syntax.read syn T b of
+ [t] => t
+ | _ => error("Error or ambiguity in parsing of " ^ b)
val (us,_) = Type.infer_types(tsig, Sign.const_type sign,
- K None, K None,
- [], true,
- map (Sign.certify_typ sign) Ts,
- map read (bs~~Ts))
+ K None, K None,
+ [], true,
+ map (Sign.certify_typ sign) Ts,
+ map read (bs~~Ts))
in map (cterm_of sign) us end
handle TYPE arg => error (Sign.exn_type_msg sign arg)
| TERM (msg, _) => error msg;
@@ -248,11 +248,11 @@
(*** Meta theorems ***)
datatype thm = Thm of
- {sign: Sign.sg, (*signature for hyps and prop*)
- maxidx: int, (*maximum index of any Var or TVar*)
- shyps: sort list, (* FIXME comment *)
- hyps: term list, (*hypotheses*)
- prop: term}; (*conclusion*)
+ {sign: Sign.sg, (*signature for hyps and prop*)
+ maxidx: int, (*maximum index of any Var or TVar*)
+ shyps: sort list, (* FIXME comment *)
+ hyps: term list, (*hypotheses*)
+ prop: term}; (*conclusion*)
fun rep_thm (Thm args) = args;
@@ -335,10 +335,10 @@
as it could be slow.*)
fun compress (Thm {sign, maxidx, shyps, hyps, prop}) =
Thm {sign = sign,
- maxidx = maxidx,
- shyps = shyps,
- hyps = map Term.compress_term hyps,
- prop = Term.compress_term prop};
+ maxidx = maxidx,
+ shyps = shyps,
+ hyps = map Term.compress_term hyps,
+ prop = Term.compress_term prop};
(* fix_shyps *)
@@ -518,7 +518,7 @@
let
val Cterm {t, T, ...} = cterm_of sg raw_tm
handle TYPE arg => error (Sign.exn_type_msg sg arg)
- | TERM (msg, _) => error msg;
+ | TERM (msg, _) => error msg;
in
assert (T = propT) "Term not of type prop";
(name, no_vars t)
@@ -542,8 +542,8 @@
let
val sign1 = Sign.make_draft sign;
val axioms = map (apsnd (Term.compress_term o Logic.varify) o
- prep_axm sign)
- axms;
+ prep_axm sign)
+ axms;
in
ext_thy thy sign1 axioms
end;
--- a/src/Pure/type.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/type.ML Mon Jan 29 14:16:13 1996 +0100
@@ -904,7 +904,7 @@
val (T, tyeT) = inf(Ts, f, tyeU);
fun err s =
raise TYPE(s, [inst_typ tyeT T, inst_typ tyeT U], [f$u])
- val msg = "function type is incompatible with argument type"
+ val msg = "function type is incompatible with argument type"
in case T of
Type("fun", [T1, T2]) =>
( (T2, unify1 tsig ((T1, U), tyeT))
@@ -1049,7 +1049,7 @@
(*Infer types for terms. Given Ts=[T1,...,Tn] and ts=[t1,...,tn], ensure that
- the type of ti unifies with Ti (i=1,...,n).
+ the type of ti unifies with Ti (i=1,...,n).
types is a partial map from indexnames to types (constrains Free, Var).
sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
used is the list of already used type variables.
--- a/src/Pure/unify.ML Mon Jan 29 13:58:15 1996 +0100
+++ b/src/Pure/unify.ML Mon Jan 29 14:16:13 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: unify
+(* Title: unify
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright Cambridge University 1992
Higher-Order Unification
@@ -28,16 +28,16 @@
val combound : (term*int*int) -> term
val rlist_abs: (string*typ)list * term -> term
val smash_unifiers : Sign.sg * Envir.env * (term*term)list
- -> (Envir.env Sequence.seq)
+ -> (Envir.env Sequence.seq)
val unifiers: Sign.sg * Envir.env * ((term*term)list)
- -> (Envir.env * (term * term)list) Sequence.seq
+ -> (Envir.env * (term * term)list) Sequence.seq
end;
functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
and Pattern:PATTERN
sharing type Sign.sg = Pattern.sg
and type Envir.env = Pattern.env)
- : UNIFY =
+ : UNIFY =
struct
structure Sign = Sign;
@@ -47,11 +47,11 @@
(*Unification options*)
-val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*)
-and search_bound = ref 20 (*unification quits above this depth*)
-and trace_simp = ref false (*print dpairs before calling SIMPL*)
-and trace_types = ref false (*announce potential incompleteness
- of type unification*)
+val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*)
+and search_bound = ref 20 (*unification quits above this depth*)
+and trace_simp = ref false (*print dpairs before calling SIMPL*)
+and trace_types = ref false (*announce potential incompleteness
+ of type unification*)
val sgr = ref(Sign.proto_pure);
@@ -62,14 +62,14 @@
fun body_type(Envir.Envir{iTs,...}) =
let fun bT(Type("fun",[_,T])) = bT T
| bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
- None => T | Some(T') => bT T')
+ None => T | Some(T') => bT T')
| bT T = T
in bT end;
fun binder_types(Envir.Envir{iTs,...}) =
let fun bTs(Type("fun",[T,U])) = T :: bTs U
| bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
- None => [] | Some(T') => bTs T')
+ None => [] | Some(T') => bTs T')
| bTs _ = []
in bTs end;
@@ -82,7 +82,7 @@
inefficiency, avoid partial application: if an atom is applied to
any arguments at all, apply it to its full number of arguments.
For
- rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!)
+ rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!)
args = [arg1,...,argn]
the value of
(xm,...,x1)(head(arg1,...,argn)) remains invariant.
@@ -92,18 +92,18 @@
in
fun head_norm (env,t) : term =
let fun hnorm (Var (v,T)) =
- (case Envir.lookup (env,v) of
- Some u => head_norm (env, u)
- | None => raise SAME)
- | hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body)
- | hnorm (Abs(_,_,body) $ t) =
- head_norm (env, subst_bounds([t], body))
- | hnorm (f $ t) =
- (case hnorm f of
- Abs(_,_,body) =>
- head_norm (env, subst_bounds([t], body))
- | nf => nf $ t)
- | hnorm _ = raise SAME
+ (case Envir.lookup (env,v) of
+ Some u => head_norm (env, u)
+ | None => raise SAME)
+ | hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body)
+ | hnorm (Abs(_,_,body) $ t) =
+ head_norm (env, subst_bounds([t], body))
+ | hnorm (f $ t) =
+ (case hnorm f of
+ Abs(_,_,body) =>
+ head_norm (env, subst_bounds([t], body))
+ | nf => nf $ t)
+ | hnorm _ = raise SAME
in hnorm t handle SAME=> t end
end;
@@ -113,18 +113,18 @@
fun fastype (Envir.Envir{iTs,...}) =
let val funerr = "fastype: expected function type";
fun fast(rbinder, f$u) =
- (case (fast (rbinder, f)) of
- Type("fun",[_,T]) => T
- | TVar(ixn,_) =>
- (case assoc(iTs,ixn) of
- Some(Type("fun",[_,T])) => T
- | _ => raise TERM(funerr, [f$u]))
- | _ => raise TERM(funerr, [f$u]))
+ (case (fast (rbinder, f)) of
+ Type("fun",[_,T]) => T
+ | TVar(ixn,_) =>
+ (case assoc(iTs,ixn) of
+ Some(Type("fun",[_,T])) => T
+ | _ => raise TERM(funerr, [f$u]))
+ | _ => raise TERM(funerr, [f$u]))
| fast (rbinder, Const (_,T)) = T
| fast (rbinder, Free (_,T)) = T
| fast (rbinder, Bound i) =
- (#2 (nth_elem (i,rbinder))
- handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
+ (#2 (nth_elem (i,rbinder))
+ handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
| fast (rbinder, Var (_,T)) = T
| fast (rbinder, Abs (_,T,u)) = T --> fast (("",T) :: rbinder, u)
in fast end;
@@ -133,14 +133,14 @@
(*Eta normal form*)
fun eta_norm(env as Envir.Envir{iTs,...}) =
let fun etif (Type("fun",[T,U]), t) =
- Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
- | etif (TVar(ixn,_),t) =
- (case assoc(iTs,ixn) of
- None => t | Some(T) => etif(T,t))
- | etif (_,t) = t;
+ Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
+ | etif (TVar(ixn,_),t) =
+ (case assoc(iTs,ixn) of
+ None => t | Some(T) => etif(T,t))
+ | etif (_,t) = t;
fun eta_nm (rbinder, Abs(a,T,body)) =
- Abs(a, T, eta_nm ((a,T)::rbinder, body))
- | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
+ Abs(a, T, eta_nm ((a,T)::rbinder, body))
+ | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
in eta_nm end;
@@ -150,22 +150,22 @@
"seen" is list of variables passed thru, is a memo variable for sharing.
This version searches for nonrigid occurrence, returns true if found. *)
fun occurs_terms (seen: (indexname list) ref,
- env: Envir.env, v: indexname, ts: term list): bool =
+ env: Envir.env, v: indexname, ts: term list): bool =
let fun occurs [] = false
- | occurs (t::ts) = occur t orelse occurs ts
+ | occurs (t::ts) = occur t orelse occurs ts
and occur (Const _) = false
- | occur (Bound _) = false
- | occur (Free _) = false
- | occur (Var (w,_)) =
- if w mem !seen then false
- else if v=w then true
- (*no need to lookup: v has no assignment*)
- else (seen := w:: !seen;
- case Envir.lookup(env,w) of
- None => false
- | Some t => occur t)
- | occur (Abs(_,_,body)) = occur body
- | occur (f$t) = occur t orelse occur f
+ | occur (Bound _) = false
+ | occur (Free _) = false
+ | occur (Var (w,_)) =
+ if w mem !seen then false
+ else if v=w then true
+ (*no need to lookup: v has no assignment*)
+ else (seen := w:: !seen;
+ case Envir.lookup(env,w) of
+ None => false
+ | Some t => occur t)
+ | occur (Abs(_,_,body)) = occur body
+ | occur (f$t) = occur t orelse occur f
in occurs ts end;
@@ -174,7 +174,7 @@
fun head_of_in (env,t) : term = case t of
f$_ => head_of_in(env,f)
| Var (v,_) => (case Envir.lookup(env,v) of
- Some u => head_of_in(env,u) | None => t)
+ Some u => head_of_in(env,u) | None => t)
| _ => t;
@@ -205,9 +205,9 @@
*)
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
- else NoOcc
+ else NoOcc
fun occurs [] = NoOcc
- | occurs (t::ts) =
+ | occurs (t::ts) =
(case occur t of
Rigid => Rigid
| oc => (case occurs ts of NoOcc => oc | oc2 => oc2))
@@ -217,28 +217,28 @@
| oc => (case occomb f of NoOcc => oc | oc2 => oc2))
| occomb t = occur t
and occur (Const _) = NoOcc
- | occur (Bound _) = NoOcc
- | occur (Free _) = NoOcc
- | occur (Var (w,_)) =
- if w mem !seen then NoOcc
- else if v=w then Rigid
- else (seen := w:: !seen;
- case Envir.lookup(env,w) of
- None => NoOcc
- | Some t => occur t)
- | occur (Abs(_,_,body)) = occur body
- | occur (t as f$_) = (*switch to nonrigid search?*)
- (case head_of_in (env,f) of
- Var (w,_) => (*w is not assigned*)
- if v=w then Rigid
- else nonrigid t
- | Abs(_,_,body) => nonrigid t (*not in normal form*)
- | _ => occomb t)
+ | occur (Bound _) = NoOcc
+ | occur (Free _) = NoOcc
+ | occur (Var (w,_)) =
+ if w mem !seen then NoOcc
+ else if v=w then Rigid
+ else (seen := w:: !seen;
+ case Envir.lookup(env,w) of
+ None => NoOcc
+ | Some t => occur t)
+ | occur (Abs(_,_,body)) = occur body
+ | occur (t as f$_) = (*switch to nonrigid search?*)
+ (case head_of_in (env,f) of
+ Var (w,_) => (*w is not assigned*)
+ if v=w then Rigid
+ else nonrigid t
+ | Abs(_,_,body) => nonrigid t (*not in normal form*)
+ | _ => occomb t)
in occur t end;
-exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*)
-exception ASSIGN; (*Raised if not an assignment*)
+exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*)
+exception ASSIGN; (*Raised if not an assignment*)
fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
@@ -261,8 +261,8 @@
Result is var a for use in SIMPL. *)
fun get_eta_var ([], _, Var vT) = vT
| get_eta_var (_::rbinder, n, f $ Bound i) =
- if n=i then get_eta_var (rbinder, n+1, f)
- else raise ASSIGN
+ if n=i then get_eta_var (rbinder, n+1, f)
+ else raise ASSIGN
| get_eta_var _ = raise ASSIGN;
@@ -277,11 +277,11 @@
fun assignment (env, rbinder, t, u) =
let val (v,T) = get_eta_var(rbinder,0,t)
in case rigid_occurs_term (ref[], env, v, u) of
- NoOcc => let val env = unify_types(body_type env T,
- fastype env (rbinder,u),env)
- in Envir.update ((v, rlist_abs(rbinder,u)), env) end
- | Nonrigid => raise ASSIGN
- | Rigid => raise CANTUNIFY
+ NoOcc => let val env = unify_types(body_type env T,
+ fastype env (rbinder,u),env)
+ in Envir.update ((v, rlist_abs(rbinder,u)), env) end
+ | Nonrigid => raise ASSIGN
+ | Rigid => raise CANTUNIFY
end;
@@ -291,9 +291,9 @@
if not, raises TERM, probably indicating type mismatch.
Uses variable a (unless the null string) to preserve user's naming.*)
fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
- let val env' = unify_types(T,U,env)
- val c = if a="" then b else a
- in new_dpair((c,T) :: rbinder, body1, body2, env') end
+ let val env' = unify_types(T,U,env)
+ val c = if a="" then b else a
+ in new_dpair((c,T) :: rbinder, body1, body2, env') end
| new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
| new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
| new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
@@ -301,8 +301,8 @@
fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
new_dpair (rbinder,
- eta_norm env (rbinder, head_norm(env,t)),
- eta_norm env (rbinder, head_norm(env,u)), env);
+ eta_norm env (rbinder, head_norm(env,t)),
+ eta_norm env (rbinder, head_norm(env,u)), env);
@@ -313,34 +313,34 @@
do so caused numerous problems with no compensating advantage.
*)
fun SIMPL0 (dp0, (env,flexflex,flexrigid))
- : Envir.env * dpair list * dpair list =
+ : Envir.env * dpair list * dpair list =
let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
- fun SIMRANDS(f$t, g$u, env) =
- SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
- | SIMRANDS (t as _$_, _, _) =
- raise TERM ("SIMPL: operands mismatch", [t,u])
- | SIMRANDS (t, u as _$_, _) =
- raise TERM ("SIMPL: operands mismatch", [t,u])
- | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
+ fun SIMRANDS(f$t, g$u, env) =
+ SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
+ | SIMRANDS (t as _$_, _, _) =
+ raise TERM ("SIMPL: operands mismatch", [t,u])
+ | SIMRANDS (t, u as _$_, _) =
+ raise TERM ("SIMPL: operands mismatch", [t,u])
+ | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
in case (head_of t, head_of u) of
(Var(_,T), Var(_,U)) =>
- let val T' = body_type env T and U' = body_type env U;
- val env = unify_types(T',U',env)
- in (env, dp::flexflex, flexrigid) end
+ let val T' = body_type env T and U' = body_type env U;
+ val env = unify_types(T',U',env)
+ in (env, dp::flexflex, flexrigid) end
| (Var _, _) =>
- ((assignment (env,rbinder,t,u), flexflex, flexrigid)
- handle ASSIGN => (env, flexflex, dp::flexrigid))
+ ((assignment (env,rbinder,t,u), flexflex, flexrigid)
+ handle ASSIGN => (env, flexflex, dp::flexrigid))
| (_, Var _) =>
- ((assignment (env,rbinder,u,t), flexflex, flexrigid)
- handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
+ ((assignment (env,rbinder,u,t), flexflex, flexrigid)
+ handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
| (Const(a,T), Const(b,U)) =>
- if a=b then SIMRANDS(t,u, unify_types(T,U,env))
- else raise CANTUNIFY
+ if a=b then SIMRANDS(t,u, unify_types(T,U,env))
+ else raise CANTUNIFY
| (Bound i, Bound j) =>
- if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY
+ if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY
| (Free(a,T), Free(b,U)) =>
- if a=b then SIMRANDS(t,u, unify_types(T,U,env))
- else raise CANTUNIFY
+ if a=b then SIMRANDS(t,u, unify_types(T,U,env))
+ else raise CANTUNIFY
| _ => raise CANTUNIFY
end;
@@ -356,8 +356,8 @@
Clever would be to re-do just the affected dpairs*)
fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
let val all as (env',flexflex,flexrigid) =
- foldr SIMPL0 (dpairs, (env,[],[]));
- val dps = flexrigid@flexflex
+ foldr SIMPL0 (dpairs, (env,[],[]));
+ val dps = flexrigid@flexflex
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
then SIMPL(env',dps) else all
end;
@@ -376,7 +376,7 @@
fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*)
| make_args name (binder: typ list, env, Ts) : Envir.env * term list =
let fun funtype T = binder--->T;
- val (env', vars) = Envir.genvars name (env, map funtype Ts)
+ val (env', vars) = Envir.genvars name (env, map funtype Ts)
in (env', map (fn var=> combound(var, 0, length binder)) vars) end;
@@ -398,60 +398,60 @@
The order for trying projections is crucial in ?b'(?a)
NB "vname" is only used in the call to make_args!! *)
fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
- : (term * (Envir.env * dpair list))Sequence.seq =
+ : (term * (Envir.env * dpair list))Sequence.seq =
let (*Produce copies of uarg and cons them in front of uargs*)
fun copycons uarg (uargs, (env, dpairs)) =
- Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
- (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
- (env, dpairs)));
- (*Produce sequence of all possible ways of copying the arg list*)
+ Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
+ (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
+ (env, dpairs)));
+ (*Produce sequence of all possible ways of copying the arg list*)
fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
| copyargs (uarg::uargs) =
- Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
+ Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
val (uhead,uargs) = strip_comb u;
val base = body_type env (fastype env (rbinder,uhead));
fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
(*attempt projection on argument with given typ*)
val Ts = map (curry (fastype env) rbinder) targs;
fun projenv (head, (Us,bary), targ, tail) =
- let val env = if !trace_types then test_unify_types(base,bary,env)
- else unify_types(base,bary,env)
- in Sequence.seqof (fn () =>
- let val (env',args) = make_args vname (Ts,env,Us);
- (*higher-order projection: plug in targs for bound vars*)
- fun plugin arg = list_comb(head_of arg, targs);
- val dp = (rbinder, list_comb(targ, map plugin args), u);
- val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
- (*may raise exception CANTUNIFY*)
- in Some ((list_comb(head,args), (env2, frigid@fflex)),
- tail)
- end handle CANTUNIFY => Sequence.pull tail)
- end handle CANTUNIFY => tail;
+ let val env = if !trace_types then test_unify_types(base,bary,env)
+ else unify_types(base,bary,env)
+ in Sequence.seqof (fn () =>
+ let val (env',args) = make_args vname (Ts,env,Us);
+ (*higher-order projection: plug in targs for bound vars*)
+ fun plugin arg = list_comb(head_of arg, targs);
+ val dp = (rbinder, list_comb(targ, map plugin args), u);
+ val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
+ (*may raise exception CANTUNIFY*)
+ in Some ((list_comb(head,args), (env2, frigid@fflex)),
+ tail)
+ end handle CANTUNIFY => Sequence.pull tail)
+ end handle CANTUNIFY => tail;
(*make a list of projections*)
fun make_projs (T::Ts, targ::targs) =
- (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
+ (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
| make_projs ([],[]) = []
| make_projs _ = raise TERM ("make_projs", u::targs);
(*try projections and imitation*)
fun matchfun ((bvar,T,targ)::projs) =
- (projenv(bvar, strip_type env T, targ, matchfun projs))
+ (projenv(bvar, strip_type env T, targ, matchfun projs))
| matchfun [] = (*imitation last of all*)
- (case uhead of
- Const _ => Sequence.maps joinargs (copyargs uargs)
- | Free _ => Sequence.maps joinargs (copyargs uargs)
- | _ => Sequence.null) (*if Var, would be a loop!*)
+ (case uhead of
+ Const _ => Sequence.maps joinargs (copyargs uargs)
+ | Free _ => Sequence.maps joinargs (copyargs uargs)
+ | _ => Sequence.null) (*if Var, would be a loop!*)
in case uhead of
- Abs(a, T, body) =>
- Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed'))
- (mc ((a,T)::rbinder,
- (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
+ Abs(a, T, body) =>
+ Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed'))
+ (mc ((a,T)::rbinder,
+ (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
| Var (w,uary) =>
- (*a flex-flex dpair: make variable for t*)
- let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
- val tabs = combound(newhd, 0, length Ts)
- val tsub = list_comb(newhd,targs)
- in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs))
- end
+ (*a flex-flex dpair: make variable for t*)
+ let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
+ val tabs = combound(newhd, 0, length Ts)
+ val tsub = list_comb(newhd,targs)
+ in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs))
+ end
| _ => matchfun(rev(make_projs(Ts, targs)))
end
in mc end;
@@ -459,14 +459,14 @@
(*Call matchcopy to produce assignments to the variable in the dpair*)
fun MATCH (env, (rbinder,t,u), dpairs)
- : (Envir.env * dpair list)Sequence.seq =
+ : (Envir.env * dpair list)Sequence.seq =
let val (Var(v,T), targs) = strip_comb t;
val Ts = binder_types env T;
fun new_dset (u', (env',dpairs')) =
- (*if v was updated to s, must unify s with u' *)
- case Envir.lookup(env',v) of
- None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs')
- | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
+ (*if v was updated to s, must unify s with u' *)
+ case Envir.lookup(env',v) of
+ None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs')
+ | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
in Sequence.maps new_dset
(matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
end;
@@ -481,9 +481,9 @@
let val (v,T) = get_eta_var(rbinder,0,t)
in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
else let val env = unify_types(body_type env T,
- fastype env (rbinder,u),
- env)
- in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
+ fastype env (rbinder,u),
+ env)
+ in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
end;
@@ -508,30 +508,30 @@
let val (head,args) = strip_comb t
in
case head of
- Bound i => (i-lev) mem banned orelse
- exists (rigid_bound (lev, banned)) args
- | Var _ => false (*no rigid occurrences here!*)
- | Abs (_,_,u) =>
- rigid_bound(lev+1, banned) u orelse
- exists (rigid_bound (lev, banned)) args
- | _ => exists (rigid_bound (lev, banned)) args
+ Bound i => (i-lev) mem banned orelse
+ exists (rigid_bound (lev, banned)) args
+ | Var _ => false (*no rigid occurrences here!*)
+ | Abs (_,_,u) =>
+ rigid_bound(lev+1, banned) u orelse
+ exists (rigid_bound (lev, banned)) args
+ | _ => exists (rigid_bound (lev, banned)) args
end;
(*Squash down indices at level >=lev to delete the banned from a term.*)
fun change_bnos banned =
let fun change lev (Bound i) =
- if i<lev then Bound i
- else if (i-lev) mem banned
- then raise CHANGE_FAIL (**flexible occurrence: give up**)
- else Bound (i - length (filter (fn j => j < i-lev) banned))
- | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
- | change lev (t$u) = change lev t $ change lev u
- | change lev t = t
+ if i<lev then Bound i
+ else if (i-lev) mem banned
+ then raise CHANGE_FAIL (**flexible occurrence: give up**)
+ else Bound (i - length (filter (fn j => j < i-lev) banned))
+ | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
+ | change lev (t$u) = change lev t $ change lev u
+ | change lev t = t
in change 0 end;
(*Change indices, delete the argument if it contains a banned Bound*)
fun change_arg banned ({j,t,T}, args) : flarg list =
- if rigid_bound (0, banned) t then args (*delete argument!*)
+ if rigid_bound (0, banned) t then args (*delete argument!*)
else {j=j, t= change_bnos banned t, T=T} :: args;
@@ -550,19 +550,19 @@
Update its head; squash indices in arguments. *)
fun clean_term banned (env,t) =
let val (Var(v,T), ts) = strip_comb t
- val (Ts,U) = strip_type env T
- and js = length ts - 1 downto 0
- val args = sort arg_less
- (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
- val ts' = map (#t) args
+ val (Ts,U) = strip_type env T
+ and js = length ts - 1 downto 0
+ val args = sort arg_less
+ (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
+ val ts' = map (#t) args
in
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
- val body = list_comb(v', map (Bound o #j) args)
- val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env'))
- (*the vupdate affects ts' if they contain v*)
- in
- (env2, Envir.norm_term env2 (list_comb(v',ts')))
+ val body = list_comb(v', map (Bound o #j) args)
+ val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env'))
+ (*the vupdate affects ts' if they contain v*)
+ in
+ (env2, Envir.norm_term env2 (list_comb(v',ts')))
end
end;
@@ -583,8 +583,8 @@
let val loot = loose_bnos t and loou = loose_bnos u
fun add_index (((a,T), j), (bnos, newbinder)) =
if j mem loot andalso j mem loou
- then (bnos, (a,T)::newbinder) (*needed by both: keep*)
- else (j::bnos, newbinder); (*remove*)
+ then (bnos, (a,T)::newbinder) (*needed by both: keep*)
+ else (j::bnos, newbinder); (*remove*)
val indices = 0 upto (length rbinder - 1);
val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
val (env', t') = clean_term banned (env, t);
@@ -605,11 +605,11 @@
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0
in case (head_of t, head_of u) of
(Var(v,T), Var(w,U)) => (*Check for identical variables...*)
- if v=w then (*...occur check would falsely return true!*)
- if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
- else raise TERM ("add_ffpair: Var name confusion", [t,u])
- else if xless(v,w) then (*prefer to update the LARGER variable*)
- clean_ffpair ((rbinder, u, t), (env,tpairs))
+ if v=w then (*...occur check would falsely return true!*)
+ if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
+ else raise TERM ("add_ffpair: Var name confusion", [t,u])
+ else if xless(v,w) then (*prefer to update the LARGER variable*)
+ clean_ffpair ((rbinder, u, t), (env,tpairs))
else clean_ffpair ((rbinder, t, u), (env,tpairs))
| _ => raise TERM ("add_ffpair: Vars expected", [t,u])
end;
@@ -634,26 +634,26 @@
fun hounifiers (sg,env, tus : (term*term)list)
: (Envir.env * (term*term)list)Sequence.seq =
let fun add_unify tdepth ((env,dpairs), reseq) =
- Sequence.seqof (fn()=>
- let val (env',flexflex,flexrigid) =
- (if tdepth> !trace_bound andalso !trace_simp
- then print_dpairs "Enter SIMPL" (env,dpairs) else ();
- SIMPL (env,dpairs))
- in case flexrigid of
- [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
- | dp::frigid' =>
- if tdepth > !search_bound then
- (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
- else
- (if tdepth > !trace_bound then
- print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
- else ();
- Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
- (MATCH (env',dp, frigid'@flexflex), reseq)))
- end
- handle CANTUNIFY =>
- (if tdepth > !trace_bound then writeln"Failure node" else ();
- Sequence.pull reseq));
+ Sequence.seqof (fn()=>
+ let val (env',flexflex,flexrigid) =
+ (if tdepth> !trace_bound andalso !trace_simp
+ then print_dpairs "Enter SIMPL" (env,dpairs) else ();
+ SIMPL (env,dpairs))
+ in case flexrigid of
+ [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
+ | dp::frigid' =>
+ if tdepth > !search_bound then
+ (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
+ else
+ (if tdepth > !trace_bound then
+ print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
+ else ();
+ Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
+ (MATCH (env',dp, frigid'@flexflex), reseq)))
+ end
+ handle CANTUNIFY =>
+ (if tdepth > !trace_bound then writeln"Failure node" else ();
+ Sequence.pull reseq));
val dps = map (fn(t,u)=> ([],t,u)) tus
in sgr := sg;
add_unify 1 ((env,dps), Sequence.null)
@@ -675,7 +675,7 @@
(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
- though just ?g->?f is a more general unifier.
+ though just ?g->?f is a more general unifier.
Unlike Huet (1975), does not smash together all variables of same type --
requires more work yet gives a less general unifier (fewer variables).
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)