1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri Jul 15 13:51:50 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Jul 18 09:29:17 2011 +0200
     1.3 @@ -111,6 +111,7 @@
     1.4         (int list * string * Term.term * Term.term list) list
     1.5      val match_ags :
     1.6         theory -> pat list -> Term.term list -> SpecifyTools.ori list
     1.7 +    val oris2fmz_vals : ori list -> string list * term list
     1.8      val maxl : int list -> int
     1.9      val match_ags_msg : string list -> Term.term -> Term.term list -> unit
    1.10      val memI : ''a list -> ''a -> bool
    1.11 @@ -252,6 +253,13 @@
    1.12      foldl and_ (true, map #1 pre) andalso 
    1.13      dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
    1.14  
    1.15 +(*["BOOL (1+x=2)","REAL x"] --match_ags--> oris 
    1.16 +  --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
    1.17 +fun oris2fmz_vals oris =
    1.18 +    let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) = 
    1.19 +	    ((term2str o comp_dts') (dsc, ts), last_elem ts) 
    1.20 +	    handle _ => error ("ori2fmz_env called with "^terms2str ts)
    1.21 +    in (split_list o (map ori2fmz_vals)) oris end;
    1.22  
    1.23  (* make a term 'typeless' for comparing with another 'typeless' term;
    1.24     'type-less' usually is illtyped                                  *)
    1.25 @@ -1082,7 +1090,7 @@
    1.26          then ([], e_ctxt)
    1.27    	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy
    1.28        val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.29 -  			(oris, (dI',pI',mI'),e_term)
    1.30 +  			(oris, (dI',pI',mI'), e_term)
    1.31        val pt = update_ctxt pt [] ctxt
    1.32        val {ppc, prls, where_, ...} = get_pbt pI'
    1.33        val (pbl, pre, pb) = ([], [], false)
    1.34 @@ -1727,10 +1735,20 @@
    1.35      val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
    1.36      val thy = assoc_thy dI;
    1.37  	  val {ppc, ...} = get_met mI;
    1.38 +    val (fmz_, vals) = oris2fmz_vals pors;
    1.39 +	  val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
    1.40 +      |> declare_constraints' vals
    1.41 +    val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
    1.42 +	  val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)
    1.43 +	  val pt = update_spec pt p (dI,pI,mI);
    1.44 +    val pt = update_ctxt pt p ctxt
    1.45 +(*
    1.46  	  val mors = prep_ori fmz_ thy ppc |> #1;
    1.47      val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
    1.48  	  val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
    1.49 +    (*WN110715: why pors, mors handled so differently?*)
    1.50  	  val pt = update_spec pt p (dI,pI,mI);
    1.51 +*)
    1.52    in (pt, (p,Met): pos') end;
    1.53  
    1.54  (*WN0312: use in nxt_spec, too ? what about variants ???*)