src/Sequents/prover.ML
changeset 3538 ed9de44032e0
parent 2073 fb0655539d05
child 3948 3428c0a88449
equal deleted inserted replaced
3537:79ac9b475621 3538:ed9de44032e0
    83   The abstraction over state prevents needless divergence in recursion.
    83   The abstraction over state prevents needless divergence in recursion.
    84   The 9999 should be a parameter, to delay treatment of flexible goals. *)
    84   The 9999 should be a parameter, to delay treatment of flexible goals. *)
    85 
    85 
    86 fun RESOLVE_THEN rules =
    86 fun RESOLVE_THEN rules =
    87   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
    87   let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
    88       fun tac nextac i = STATE (fn state =>  
    88       fun tac nextac i state = state |>
    89 	  filseq_resolve_tac rls0 9999 i 
    89 	     (filseq_resolve_tac rls0 9999 i 
    90 	  ORELSE
    90 	      ORELSE
    91 	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    91 	      (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
    92 	  ORELSE
    92 	      ORELSE
    93 	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    93 	      (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
    94 					THEN  TRY(nextac i)) )
    94 					    THEN  TRY(nextac i)))
    95   in  tac  end;
    95   in  tac  end;
    96 
    96 
    97 
    97 
    98 
    98 
    99 (*repeated resolution applied to the designated goal*)
    99 (*repeated resolution applied to the designated goal*)
   200 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
   200 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
   201 val fres_bound_tac = fresolve_tac bound_rls;
   201 val fres_bound_tac = fresolve_tac bound_rls;
   202 
   202 
   203 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
   203 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
   204                                     else tf(i) THEN tac(i-1)
   204                                     else tf(i) THEN tac(i-1)
   205                     in STATE(fn state=> tac(nprems_of state)) end;
   205                     in fn st => tac (nprems_of st) st end;
   206 
   206 
   207 (* Depth first search bounded by d *)
   207 (* Depth first search bounded by d *)
   208 fun solven_tac d n = STATE (fn state =>
   208 fun solven_tac d n state = state |>
   209         if d<0 then no_tac
   209        (if d<0 then no_tac
   210         else if (nprems_of state = 0) then all_tac 
   210         else if (nprems_of state = 0) then all_tac 
   211         else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
   211         else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
   212                  ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
   212                  ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
   213                    (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
   213                    (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
   214 
   214 
   215 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
   215 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
   216 
   216 
   217 fun step_tac n = STATE (fn state =>  
   217 fun step_tac n = 
   218       if (nprems_of state = 0) then all_tac 
   218     COND (has_fewer_prems 1) all_tac 
   219       else (DETERM(fres_safe_tac n)) ORELSE 
   219          (DETERM(fres_safe_tac n) ORELSE 
   220            (fres_unsafe_tac n APPEND fres_bound_tac n));
   220 	  (fres_unsafe_tac n APPEND fres_bound_tac n));
   221 
   221 
   222 end;
   222 end;
   223 end;
   223 end;