src/Tools/isac/Interpret/script.sml
changeset 59240 bd9f7f08000c
parent 59186 d9c3e373f8f5
child 59250 727dff4f6b2c
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Sat Aug 27 11:26:28 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat Aug 27 16:57:18 2016 +0200
     1.3 @@ -303,6 +303,8 @@
     1.4  !: FIXXXME penv: push it here in itms2args into script-evaluation*)
     1.5  (* val (thy, mI, itms) = (thy, metID, itms);
     1.6     *)
     1.7 +val errmsg = 
     1.8 +  "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
     1.9  fun itms2args thy mI (itms:itm list) =
    1.10      let val mvat = max_vt itms
    1.11  	fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b
    1.12 @@ -317,6 +319,7 @@
    1.13  	      | SOME (_,_,_,_,itm_) => penvval_in itm_
    1.14  	fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")
    1.15  	val pats = (#ppc o get_met) mI
    1.16 +	val _ = if pats = [] then raise ERROR errmsg else ()
    1.17      in (flat o (map (itm2arg itms))) pats end;
    1.18  (*
    1.19  > val sc = ... Solve_root_equation ...
    1.20 @@ -1483,9 +1486,11 @@
    1.21  
    1.22  
    1.23  (*.create the initial interpreter state from the items of the guard.*)
    1.24 +val errmsg = "ERROR: found no actual arguments for prog. of "
    1.25  fun init_scrstate thy itms metID =
    1.26    let
    1.27      val actuals = itms2args thy metID itms
    1.28 +    val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
    1.29  	  val scr as Prog sc = (#scr o get_met) metID
    1.30      val formals = formal_args sc    
    1.31  	  (*expects same sequence of (actual) args in itms and (formal) args in met*)