# HG changeset patch # User clasohm # Date 822921373 -3600 # Node ID 5a6f2aabd53846b935a29b9ae1e0cffbbc9719c1 # Parent d12da312eff42dec9d3441b425a3d0be040ddbd3 inserted tabs again diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/drule.ML --- 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 = diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/envir.ML --- 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 = diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/goals.ML --- 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); diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/library.ML --- 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 (?) *) diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/logic.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/net.ML --- 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 ab*) (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 ab*) (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 ab*) (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 ab*) (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); diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/pattern.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/section_utils.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/sequence.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/sign.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/tactic.ML --- 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)) diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/tctical.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/term.ML --- 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=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 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 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/thm.ML --- 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; diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/type.ML --- 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. diff -r d12da312eff4 -r 5a6f2aabd538 src/Pure/unify.ML --- 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 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 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. *)