1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Jul 31 14:21:49 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Jul 31 14:32:05 2014 +0200
     1.3 @@ -534,27 +534,25 @@
     1.4  
     1.5  (*fo = ifo excluded already in inform*)
     1.6  fun concat_deriv rew_ord erls rules fo ifo =
     1.7 -    let fun derivat ([]:(term * rule * (term * term list)) list) = e_term
     1.8 -	  | derivat dt = (#1 o #3 o last_elem) dt
     1.9 -        fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
    1.10 -	val  fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo
    1.11 -	val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
    1.12 -    in case (fod, ifod) of
    1.13 -	   ([], []) => if fo = ifo then (true, [])
    1.14 -		       else (false, [])
    1.15 -	 | (fod, []) => if derivat fod = ifo 
    1.16 -			then (true, fod) (*ifo is normal form*)
    1.17 -			else (false, [])
    1.18 -	 | ([], ifod) => if fo = derivat ifod 
    1.19 -			 then (true, ((map rev_deriv') o rev) ifod)
    1.20 -			 else (false, [])
    1.21 -	 | (fod, ifod) =>
    1.22 -	   if derivat fod = derivat ifod (*common normal form found*)
    1.23 -	   then let val (fod', rifod') = 
    1.24 -			dropwhile' equal (rev fod) (rev ifod)
    1.25 -		in (true, fod' @ (map rev_deriv' rifod')) end
    1.26 -	   else (false, [])
    1.27 -    end;
    1.28 +  let 
    1.29 +    fun derivat ([]:(term * rule * (term * term list)) list) = e_term
    1.30 +      | derivat dt = (#1 o #3 o last_elem) dt
    1.31 +    fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
    1.32 +    val  fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE  fo
    1.33 +    val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
    1.34 +  in 
    1.35 +    case (fod, ifod) of
    1.36 +      ([], []) => if fo = ifo then (true, []) else (false, [])
    1.37 +    | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
    1.38 +    | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
    1.39 +    | (fod, ifod) =>
    1.40 +      if derivat fod = derivat ifod (*common normal form found*)
    1.41 +      then
    1.42 +        let 
    1.43 +          val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
    1.44 +        in (true, fod' @ (map rev_deriv' rifod')) end
    1.45 +      else (false, [])
    1.46 +  end;
    1.47  (*
    1.48   val ({rew_ord, erls, rules,...}, fo, ifo) = 
    1.49       (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
    1.50 @@ -598,7 +596,7 @@
    1.51  		     val (c', ptp) = embed_deriv tacis' ptp;
    1.52  	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
    1.53       else 
    1.54 -	     if pos = ([], Res) 
    1.55 +	     if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
    1.56  	     then ("no derivation found", (tacis, c, ptp): calcstate') 
    1.57  	     else
    1.58           let
    1.59 @@ -607,7 +605,7 @@
    1.60  			       case tacis of
    1.61  			         ((Subproblem _, _, _)::_) => 
    1.62  			           let
    1.63 -                   val ptp as (pt, (p,_)) = all_modspec ptp
    1.64 +                   val ptp as (pt, (p,_)) = all_modspec ptp (*<------------------*)
    1.65  				           val mI = get_obj g_metID pt p
    1.66  			           in
    1.67  			             nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp