1.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Tue Apr 03 15:48:39 2018 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Tue Apr 03 16:53:18 2018 +0200
     1.3 @@ -25,7 +25,51 @@
     1.4  val pt = update_ctxt pt [] pctxt
     1.5  ;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;
     1.6  
     1.7 +(* INVESTIGATE val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];*)
     1.8 +(*///----------------------------------------- save for final check ------------------------\\\*)
     1.9 +val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))];
    1.10 +"~~~~~ fun CalcTreeTEST, args:"; val ([(fmz, sp)]) = ([(fmz, (dI',pI',mI'))]);
    1.11 +    val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
    1.12 +(*ADD check*) 
    1.13 +val PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} = get_obj I pt (fst p);
    1.14 +(* ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt
    1.15 +   IN Minimsubpbl/150-add-given.sml IS CAUSED HEREBY:*)
    1.16 +case oris of
    1.17 +  ((1, [1], "#Given", Const ("Descript.equality", _),
    1.18 +    [Const ("HOL.eq", _) $ _ $ Free ("2", _)]) :: _) => ()
    1.19 +| ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
    1.20 +| _ => error ""
    1.21 +
    1.22 +"~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
    1.23 +	    val thy = Celem.assoc_thy dI;
    1.24 +(*if*) mI = ["no_met"] = false (*else*);
    1.25 +val xxx = Specify.get_pbt pI
    1.26 +val yyy = #ppc xxx
    1.27 +val (oris, ctxt) = Specify.prep_ori fmz thy yyy
    1.28 +;
    1.29 +case oris of
    1.30 +  ((1, [1], "#Given", Const ("Descript.equality", _),
    1.31 +    [Const ("HOL.eq", _) $ _ $ Free ("2", _)]) :: _) => ()
    1.32 +| ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
    1.33 +| _ => error ""
    1.34 +
    1.35 +"~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);
    1.36 +      val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz;
    1.37 +(*ADD check*) 
    1.38 +case TermC.parseNEW ctxt "equality (x+1=(2::real))" of
    1.39 +  SOME (Const ("Descript.equality", _) (* <<< ---------------- this needs to be recognised *) $
    1.40 +    (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
    1.41 +      Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => ()
    1.42 +| SOME (Free ("equality", _) $
    1.43 +    (Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
    1.44 +      Free ("x", _) $ Free ("1", _)) $ Free ("2", _))) => error ""
    1.45 +| _ => error "something is wrong with initialising Minisubpnl";
    1.46 +
    1.47 +val [(fmz, (dI',pI',mI'))] = [(fmz''''', spec''''')];
    1.48 +(*\\\----------------------------------------- saved for final check -----------------------///*)
    1.49 +
    1.50  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.51  case nxt of ("Model_Problem", _) => ()
    1.52  | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
    1.53  
    1.54 +