/seL4-l4v-master/HOL4/src/portableML/monads/ |
H A D | errormonad.sml | 4 datatype ('a,'b) fs = Some of 'a | Error of 'b 7 fun error (e:'error) : ('s,'a,'error) t = fn env => Error e 19 | Error e => Error e (* pat and rhs have different types *) 25 Error _ => m2 env 30 Error e => fm2 e env 57 NONE => Error errv 62 Error _ => NONE 67 Error e => Error [all...] |
H A D | errormonad.sig | 4 datatype ('a,'b) fs = Some of 'a | Error of 'b
|
H A D | seqmonad.sml | 68 NONE => errormonad.Error e 74 errormonad.Error e => fail s0
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | errormsg.sml | 9 exception Error exception 10 val impossible : string -> 'a (* raises Error *) 29 exception Error exception 48 (app print ["Error: Compiler bug: ",msg,"\n"]; 50 raise Error)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | errormsg.sml | 9 exception Error exception 10 val impossible : string -> 'a (* raises Error *) 29 exception Error exception 48 (app print ["Error: Compiler bug: ",msg,"\n"]; 50 raise Error)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | errormsg.sml | 9 exception Error exception 10 val impossible : string -> 'a (* raises Error *) 29 exception Error exception 48 (app print ["Error: Compiler bug: ",msg,"\n"]; 50 raise Error)
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | type_tokens_dtype.sml | 15 | Error of 'a base_tokens.base_token
|
H A D | type_tokens.sml | 76 | SOME _ => Error (BT_Numeral (Arbnum.fromString (munge pfx), sfx)) 117 else if s0 = "\"" then ((fn () => advance fb), (Error (BT_Ident s),locn)) 124 | (num, SOME _) => Error (BT_Numeral numinfo) 132 | BT_EOI => ((fn () => ()), (Error bt,locn)) 134 | BT_DecimalFraction r => ((fn () => ()), (Error bt, locn)) 135 | BT_StrLit _ => ((fn () => ()), (Error bt, locn)) 146 Error BT_EOI => List.rev acc 163 | token_string _ (Error bt) = "Error(" ^ base_tokens.toString bt ^ ")"
|
/seL4-l4v-master/seL4/src/arch/x86/64/kernel/ |
H A D | thread.c | 21 : [value] "r"(&tcb->tcbArch.tcbContext.registers[Error + 1]), 55 : [value] "r"(&tcb->tcbArch.tcbContext.registers[Error + 1]), 67 /* Setting Error to 0 will force a return by the interrupt path, which 71 setRegister(tptr, Error, 0);
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibMatch.sml | 33 else raise Error "match: one var trying to match two different terms"); 40 else raise Error "match: can't match two different functions" 41 | matchl _ _ = raise Error "match: different structure"; 50 | conv _ = raise Error "match_literals: incompatible"; 69 else if occurs x tm then raise Error "unify: occurs check" 78 else raise Error "unify: different structure"; 92 | conv _ = raise Error "unify_literals: incompatible";
|
H A D | mlibUseful.sml | 13 exception Error of string; exception 16 fun Error_to_string (Error message) = 18 | Error_to_string _ = raise Bug "Error_to_string: not an Error exception"; 24 fun report (e as Error _) = Error_to_string e 26 | report _ = raise Bug "report: not an Error or Bug exception"; 31 handle h as Error _ => (print (Error_to_string h); raise h) 35 fun total f x = SOME (f x) handle Error _ => NONE; 39 fun partial (e as Error _) f x = (case f x of SOME y => y | NONE => raise e) 40 | partial _ _ _ = raise Bug "partial: must take an Error exception"; 194 | z _ _ _ = raise Error "zipwit [all...] |
H A D | mlibClause.sml | 105 val () = assert (x = y) (Error "dest_refl") 118 val () = assert (x <> y) (Error "psym: refl") 155 if l = r then raise Error "term_order: refl" 162 | f (Pred x) (Eq y) = raise Error "obj_order: Pred > Eq" 195 raise Error "consistent: inconsistent orderings"); 232 val () = assert (#term_order parm) (Error "dest_rewr: no rewrs") 234 val () = assert (x <> y) (Error "dest_rewr: refl") 268 fun fail _ = raise Error "gen_largest_lits: fail"; 416 | _ => raise Error "match_occurs: not a variable" 417 val () = assert (not (mem v (FVT r))) (Error "match_occur [all...] |
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holdep_tokens.sml | 91 fun Error(SCR {filename,colnum,linenum,...}, msg) = function 120 else Error(scr, "Bad character >"^str c^"< after open") 152 NONE => Error(scr, "Don't expect to see 'in'-EOF") 167 NONE => Error(scr, "Don't expect to see 'infix'-EOF") 183 else Error(scr, "Bad character >"^str c^"< after 'open'") 186 NONE => Error(scr, "Don't expect to see '('-EOF") 188 | SOME c => Error(scr, "Don't expect to see '("^str c^"' after 'open'") 191 NONE => Error(scr, "Don't expect to see 'open'-'#'") 194 else Error(scr, "Don't expect to see 'open'-'#'") 197 NONE => Error(sc [all...] |
/seL4-l4v-master/seL4/src/arch/x86/machine/ |
H A D | registerset.c | 15 context->registers[Error] = 0;
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sig | 75 val union : subst -> subst -> subst (* raises Error *) 81 val invert : subst -> subst (* raises Error *) 111 val match : subst -> Term.term -> Term.term -> subst (* raises Error *) 117 val unify : subst -> Term.term -> Term.term -> subst (* raises Error *)
|
H A D | Rule.sml | 143 handle Error err => 144 raise Error ("Rule.transEqn:\neqn1 = " ^ equationToString eqn1 ^ 151 (* 2. Raises an Error exception. *) 158 val noConv : conv = fn _ => raise Error "noConv"; 169 handle Error err => 170 (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n"); 171 raise Error (s ^ ": " ^ err)); 191 fun orelseConv (conv1 : conv) conv2 tm = conv1 tm handle Error _ => conv2 tm; 199 if tm = tm' then raise Error "changedConv" else res 204 fun firstConv [] _ = raise Error "firstCon [all...] |
H A D | Atom.sig | 87 val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *) 93 val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *) 115 val sym : atom -> atom (* raises Error if given a refl *)
|
H A D | Atom.sml | 52 if Name.equal x p then (a,b) else raise Error "Atom.destBinop: wrong binop" 53 | destBinop _ _ = raise Error "Atom.destBinop: not a binop"; 82 if h >= length tms then raise Error "Atom.subterm: bad path" 94 if h >= length tms then raise Error "Atom.replace: bad path" 148 raise Error "Atom.match" 164 raise Error "Atom.unify" 191 val _ = Term.equal l r orelse raise Error "Atom.destRefl" 201 val _ = not (Term.equal l r) orelse raise Error "Atom.sym: refl"
|
H A D | Subst.sml | 126 else raise Error "Subst.union: incompatible"; 140 if NameMap.inDomain w s then raise Error "Subst.invert: non-injective" 142 | inv (_, Term.Fn _, _) = raise Error "Subst.invert: non-variable"; 209 else raise Error "Subst.match: incompatible matches" 216 else raise Error "Subst.match: different structure" 217 | matchList _ _ = raise Error "Subst.match: functions can't match vars"; 234 else if Term.freeIn v tm then raise Error "Subst.unify: occurs check" 244 raise Error "Subst.unify: different structure";
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sig | 75 val union : subst -> subst -> subst (* raises Error *) 81 val invert : subst -> subst (* raises Error *) 111 val match : subst -> Term.term -> Term.term -> subst (* raises Error *) 117 val unify : subst -> Term.term -> Term.term -> subst (* raises Error *)
|
H A D | Rule.sml | 143 handle Error err => 144 raise Error ("Rule.transEqn:\neqn1 = " ^ equationToString eqn1 ^ 151 (* 2. Raises an Error exception. *) 158 val noConv : conv = fn _ => raise Error "noConv"; 169 handle Error err => 170 (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n"); 171 raise Error (s ^ ": " ^ err)); 191 fun orelseConv (conv1 : conv) conv2 tm = conv1 tm handle Error _ => conv2 tm; 199 if tm = tm' then raise Error "changedConv" else res 204 fun firstConv [] _ = raise Error "firstCon [all...] |
H A D | Atom.sig | 87 val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *) 93 val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *) 115 val sym : atom -> atom (* raises Error if given a refl *)
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Algebra.sml | 106 | destVar _ = raise Error "destVar"; 111 | destSum _ = raise Error "destSum"; 116 | destProd _ = raise Error "destProd"; 125 if Map.size m <> 1 then raise Error "destExplSingle" 135 | _ => raise Error "destExplUnit"; 295 else raise Error "explSubtract*: wrong exp" 296 | NONE => raise Error "explSubtract*: no such base"; 310 NONE => raise Error "explProdRewrite" 314 fun norm _ (Var _) = raise Error "unchanged" 324 if not changed then raise Error "unchange [all...] |
H A D | Map.sig | 31 val get : ('key,'a) map -> 'key -> 'a (* raises Error *) 41 val delete : ('key,'a) map -> 'key -> ('key,'a) map (* raises Error *) 77 val nth : ('key,'a) map -> int -> 'key * 'a (* raises Error *)
|
/seL4-l4v-master/seL4/include/arch/x86/arch/machine/ |
H A D | debug.h | 105 if (getRegister(target_thread, Error) == -1) { 106 setRegister(target_thread, Error, 0);
|