wneuper/isa: comparison src/Tools/isac/ME/ptyps.sml

equal deleted inserted replaced

-:d957275620d4
+:e6fc98fbcb85
 ppc   : pat list,
 (*this is the model-pattern;
 it contains "#Given","#Where","#Find","#Relate"-patterns*)
 met   : metID list}; (* methods solving the pbt*)
 val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy,
-	     cas=None,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
+	     cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
 fun pbt2 (str, (t1, t2)) =
 pair2str (str, pair2str (term2str t1, term2str t2));
 fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;
 fun guh2kestoreID (guh:guh) =
 case (implode o (take_fromto 1 4) o explode) guh of
 	"pbl_" =>
 	let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
 		if gu = guh
-		then Some ((ids@[id]) : kestoreID)
+		then SOME ((ids@[id]) : kestoreID)
 		else nodes (ids@[id]) gu ns
-	    and nodes _ _ [] = None
+	    and nodes _ _ [] = NONE
 	      | nodes ids gu (n::ns) =
-		case node ids gu n of Some id => Some id
+		case node ids gu n of SOME id => SOME id
-				    | None =>  nodes ids gu ns
+				    | NONE =>  nodes ids gu ns
 	in case nodes [] guh (!ptyps) of
-	       Some id => rev id
+	       SOME id => rev id
-	     | None => error ("guh2kestoreID: '" ^ guh ^ "' " ^
+	     | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
 				    "not found in (!ptyps)")
 	end
 | "met_" =>
 	let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =
 		if gu = guh
-		then Some ((ids@[id]) : kestoreID)
+		then SOME ((ids@[id]) : kestoreID)
 		else nodes (ids@[id]) gu ns
-	    and nodes _ _ [] = None
+	    and nodes _ _ [] = NONE
 	      | nodes ids gu (n::ns) =
-		case node ids gu n of Some id => Some id
+		case node ids gu n of SOME id => SOME id
-				    | None =>  nodes ids gu ns
+				    | NONE =>  nodes ids gu ns
 	in case nodes [] guh (!mets) of
-	       Some id => id
+	       SOME id => id
-	     | None => error ("guh2kestoreID: '" ^ guh ^ "' " ^
+	     | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
 				    "not found in (!mets)") end
 | _ => error ("guh2kestoreID called with '" ^ guh ^ "'");
 (*> guh2kestoreID "pbl_equ_univ_lin";
 val it = ["linear", "univariate", "equation"] : string list*)
 ((EqSystem.thy, (["system"],
 		       [("#Given" ,["equalities es_", "solveForVars vs_"]),
 			("#Find"  ,["solution ss___"](*___ is copy-named*))
 			],
 		       append_rls "e_rls" e_rls [(*for preds in where_*)],
-		       Some "solveSystem es_ vs_",
+		       SOME "solveSystem es_ vs_",
 		       [])));
 *)
 let fun eq f (f', _) = f = f';
 	val gi = filter (eq "#Given") dsc_dats;
 (*val gi = [("#Given",["equality e_","solveFor v_"])]
 			 (strs2str pblID)))
 		   | _ =>
 		     (raise error ("prep_pbt: more than one '#Where' in "^
 				  (strs2str pblID))));
 in ({guh=guh,mathauthors=maa,init=init,
-	 thy=thy,cas= case ca of None => None
+	 thy=thy,cas= case ca of NONE => NONE
-			       | Some s =>
+			       | SOME s =>
-				 Some ((term_of o the o (parse thy)) s),
+				 SOME ((term_of o the o (parse thy)) s),
 	 prls=ev,where_=wh,ppc= gi @ fi @ re,
 	 met=metIDs}, pblID):pbt * pblID end;
 (* prep_pbt thy (pblID, dsc_dats, metIDs);
 val it =
 ({met=[],
 (*. check an item (with arbitrary itm_ from previous matchings)
 for matching a problemtype; returns true only for itms found in pbt .*)
 fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
 (case find_first (eq1 d) pbt of
-	 Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
+	 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
 					      (id, pbl_ids' thy d vs))):itm)
-| None => (i,vats,false,f,Sup (d,vs)))
+| NONE => (i,vats,false,f,Sup (d,vs)))
 | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
 (case find_first (eq1 d) pbt of
-	Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
+	SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
 					     (id, pbl_ids' thy d vs))):itm)
-| None => (i,vats,false,f,Sup (d,vs)))
+| NONE => (i,vats,false,f,Sup (d,vs)))
 | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
 | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm
 | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
 (case find_first (eq1 d) pbt of
-	Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
+	SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
 					     (id, pbl_ids' thy d vs))):itm)
-| None => (i,vats,false,f,Sup (d,vs)))
+| NONE => (i,vats,false,f,Sup (d,vs)))
 (* val (i,vats,b,f,Mis (d,vs)) = i4;
 *)
 | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
 (case find_first (eq1 d) pbt of
-(* val Some (_,(_,id)) = find_first (eq1 d) pbt;
+(* val SOME (_,(_,id)) = find_first (eq1 d) pbt;
 *)
-	Some (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
+	SOME (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
 				   \(id, pbl_ids' d vs))):itm)"
-| None => (i,vats,false,f,Sup (d,[vs])));
+| NONE => (i,vats,false,f,Sup (d,[vs])));
 (* chk_ thy pbt i
 *)
 fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;
 (*. find elements of pbt not contained in itms;
 if such one is untouched, return this one, otherwise create new itm .*)
 fun chk_m (itms:itm list) untouched (p as (f,(d,id))) =
 case find_first (eq2 p) itms of
-	Some _ => []
+	SOME _ => []
-| None => (case find_first (eq2 p) untouched of
+| NONE => (case find_first (eq2 p) untouched of
-		     Some itm => [itm]
+		     SOME itm => [itm]
-		   | None => [(0,[],false,f,Mis (d,id)):itm]);
+		   | NONE => [(0,[],false,f,Mis (d,id)):itm]);
 (* val itms = itms'';
 *)
 fun chk_mis mvat itms untouched pbt =
 let val mis = (flat o (map (chk_m itms untouched))) pbt;
 val mid = max_id itms;
 let
 (*0*)val mv = max_vt pbl;
 fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
-				Some _ => false | None => true;
+				SOME _ => false | NONE => true;
 (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;
 fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
 fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) =
 	  (i,v,false,f,Mis (d,pid)):itm;
 (*. check an ori for matching a problemtype by description;
 returns true only for itms found in pbt .*)
 fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
 case find_first (eq1 d) pbt of
-	Some (_,(_,id)) => [(i,vats,true,f,
+	SOME (_,(_,id)) => [(i,vats,true,f,
 			     Cor ((d,vs), (id, pbl_ids' thy d vs))):itm]
-| None => [];
+| NONE => [];
 (* elem 'p' of pbt contained in itms ? *)
 fun chk1_m (itms:itm list) p =
 case find_first (eq2 p) itms of
-	Some _ => true | None => false;
+	SOME _ => true | NONE => false;
 fun chk1_m' (oris: ori list) (p as (f,(d,t))) =
 case find_first (eq2' p) oris of
-	Some _ => []
+	SOME _ => []
-| None => [(f, Mis (d, t))];
+| NONE => [(f, Mis (d, t))];
 fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;
 fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
 fun chk1_mis' oris ppc =
 map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
 *)
 fun refin (pblRD:pblRD) ori
 ((Ptyp (pI,[py],[])):pbt ptyp) =
 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
-then Some ((pblRD @ [pI]):pblRD)
+then SOME ((pblRD @ [pI]):pblRD)
-else None
+else NONE
 | refin pblRD ori (Ptyp (pI,[py],pys)) =
 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
 then (case refins (pblRD @ [pI]) ori pys of
-	      Some pblRD' => Some pblRD'
+	      SOME pblRD' => SOME pblRD'
-	    | None => Some (pblRD @ [pI]))
+	    | NONE => SOME (pblRD @ [pI]))
-else None
+else NONE
-and refins pblRD ori [] = None
+and refins pblRD ori [] = NONE
 | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =
 (case refin pblRD ori p of
-	 Some pblRD' => Some pblRD'
+	 SOME pblRD' => SOME pblRD'
-| None => refins pblRD ori pts);
+| NONE => refins pblRD ori pts);
 (*. refine a problem; version providing output for math-experts .*)
 fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
 (rev ["linear","system"], fmz, [(*match list*)],
 *)
 fun refine_ori oris (pblID:pblID) =
 let val opt = app_ptyp (refin ((rev o tl) pblID) oris)
 			   pblID (rev pblID) (!ptyps);
 in case opt of
-	   Some pblRD => let val (pblID':pblID) =(rev pblRD)
+	   SOME pblRD => let val (pblID':pblID) =(rev pblRD)
-			 in if pblID' = pblID then None
+			 in if pblID' = pblID then NONE
-			    else Some pblID' end
+			    else SOME pblID' end
-	 | None => None end;
+	 | NONE => NONE end;
 fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
 (*. for tactic Refine_Problem .*);
 (* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
 (* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);
 *)
 fun refine_pbl thy (pblID:pblID) itms =
 case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms [])
 			    pblID (rev pblID) (!ptyps)) of
-	None => None
+	NONE => NONE
-| Some (Match_ (rfd as (pI',_))) =>
+| SOME (Match_ (rfd as (pI',_))) =>
-	if pblID = pI' then None else Some rfd;
+	if pblID = pI' then NONE else SOME rfd;
 (*. for math-experts .*)
 (*19.10.02FIXME: needs thy for parsing fmz*)
 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;

branch	isac-update-Isa09-2
changeset 37926	e6fc98fbcb85
parent 37906	e2b23ba9df13
child 37928	dfec2cf32f77