/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 34 | destVar (Fn _) = raise Error "destVar"; 44 | destFn (Var _) = raise Error "destFn"; 78 | destConst _ = raise Error "destConst"; 87 if Name.equal x f then (a,b) else raise Error "Term.destBinop: wrong binop" 88 | destBinop _ _ = raise Error "Term.destBinop: not a binop"; 152 | subterm (Var _) (_ :: _) = raise Error "Term.subterm: Var" 154 if h >= length tms then raise Error "Term.replace: Fn" 176 Var _ => raise Error "Term.replace: Var" 178 if h >= length tms then raise Error "Term.replace: Fn" 258 raise Error "Ter [all...] |
H A D | Rule.sig | 32 (* 2. Raises an Error exception. *) 74 (* 2. Raises an Error exception. *) 104 (* A rule takes one theorem and either deduces another or raises an Error *)
|
H A D | Thm.sml | 60 else raise Error "Thm.destUnit"; 178 handle Error err => 179 raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
|
H A D | problems2tptp.sml | 35 else raise Error ("duplicate problem name: " ^ x) 170 handle Error s => die (PROGRAM^" failed:\n" ^ s)
|
H A D | Useful.sml | 13 exception Error of string; exception 19 Error message => SOME ("Error: " ^ message) 29 | NONE => raise Bug "errorToString: not an Error exception"; 45 fun total f x = SOME (f x) handle Error _ => NONE; 214 | z _ _ _ = raise Error "zipWith: lists different lengths"; 607 else raise Error "destPrefix" 630 else raise Error "destSuffix" 710 | destLeft _ = raise Error "destLeft"; 716 | destRight _ = raise Error "destRigh [all...] |
H A D | TermNet.sml | 94 val _ = NameArity.equal f g orelse raise Error "TermNet.qv" 110 else raise Error "TermNet.qu"; 188 handle Error _ => raise Bug "TermNet.insert: should never fail"; 216 handle Error _ => raise Bug "TermNet.filter: should never fail"; 369 handle Error _ => raise Bug "TermNet.match: should never fail"; 402 handle Error _ => raise Bug "TermNet.matched: should never fail"; 435 handle Error _ => raise Bug "TermNet.unify: should never fail";
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rewrite.sml | 175 fun orderToOrient (SOME EQUAL) = raise Error "Rewrite.orient: reflexive" 246 val _ = id <> id' orelse raise Error "same theorem" 248 val _ = wellOriented ort lr orelse raise Error "orientation" 254 raise Error "order" 261 NONE => raise Error "Rewrite.rewrIdConv: no matching rewrites" 274 NONE => raise Error "incomparable" 280 if Term.equal tm r then (l,th) else raise Error "mkNeqConv: RL" 282 | SOME EQUAL => raise Error "irreflexive" 288 if Term.equal tm l then (r,th) else raise Error "mkNeqConv: LR" 351 handle Error er [all...] |
H A D | Term.sml | 34 | destVar (Fn _) = raise Error "destVar"; 44 | destFn (Var _) = raise Error "destFn"; 78 | destConst _ = raise Error "destConst"; 87 if Name.equal x f then (a,b) else raise Error "Term.destBinop: wrong binop" 88 | destBinop _ _ = raise Error "Term.destBinop: not a binop"; 152 | subterm (Var _) (_ :: _) = raise Error "Term.subterm: Var" 154 if h >= length tms then raise Error "Term.replace: Fn" 176 Var _ => raise Error "Term.replace: Var" 178 if h >= length tms then raise Error "Term.replace: Fn" 258 raise Error "Ter [all...] |
H A D | Rule.sig | 32 (* 2. Raises an Error exception. *) 74 (* 2. Raises an Error exception. *) 104 (* A rule takes one theorem and either deduces another or raises an Error *)
|
H A D | Thm.sml | 60 else raise Error "Thm.destUnit"; 178 handle Error err => 179 raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
|
H A D | problems2tptp.sml | 35 else raise Error ("duplicate problem name: " ^ x) 170 handle Error s => die (PROGRAM^" failed:\n" ^ s)
|
H A D | Useful.sml | 13 exception Error of string; exception 19 Error message => SOME ("Error: " ^ message) 29 | NONE => raise Bug "errorToString: not an Error exception"; 45 fun total f x = SOME (f x) handle Error _ => NONE; 214 | z _ _ _ = raise Error "zipWith: lists different lengths"; 607 else raise Error "destPrefix" 630 else raise Error "destSuffix" 710 | destLeft _ = raise Error "destLeft"; 716 | destRight _ = raise Error "destRigh [all...] |
H A D | TermNet.sml | 94 val _ = NameArity.equal f g orelse raise Error "TermNet.qv" 110 else raise Error "TermNet.qu"; 188 handle Error _ => raise Bug "TermNet.insert: should never fail"; 216 handle Error _ => raise Bug "TermNet.filter: should never fail"; 369 handle Error _ => raise Bug "TermNet.match: should never fail"; 402 handle Error _ => raise Bug "TermNet.matched: should never fail"; 435 handle Error _ => raise Bug "TermNet.unify: should never fail";
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | grammarLib.sml | 14 fun fail0 (m:string) e = (e, Error m) 20 Error x => (s1, Error x) 40 (((p, m), qb), Error e) => m2 ((p0, m), qb0) 132 [] => (st, Error error) 134 else (st, Error error) 178 | Error _ => ok s 271 (((_,SOME(p,m)), _), Error _) => raise Fail m 272 | (((_, NONE), _), Error s) => 334 (_, Error [all...] |
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibTerm.sml | 42 | dest_var (Fn _) = raise Error "dest_var"; 49 | dest_fn (Var _) = raise Error "dest_fn"; 66 | dest_const _ = raise Error "dest_const"; 75 if x = f then (a, b) else raise Error "dest_binop: wrong binop" 76 | dest_binop _ _ = raise Error "dest_binop: not a binop"; 83 | dest_atom _ = raise Error "dest_atom"; 90 | dest_neg _ = raise Error "dest_neg"; 495 | dest_literal _ = raise Error "dest_literal"; 568 | dest_eq _ = raise Error "dest_eq"; 625 | subterm (_ :: _) (Var _) = raise Error "subter [all...] |
H A D | mlibTptp.sml | 192 case explode s of [] => raise Error "write_cnf: empty string variable" 201 case explode s of [] => raise Error "write_cnf: empty string function" 217 | literal _ _ = raise Error "write_cnf: not in CNF"; 242 val () = assert (0 < n) (Error "write: no clauses") 248 | write _ _ = raise Error "write: not in CNF format";
|
H A D | mlibMeson.sml | 181 val no_choice = (fn () => raise Error "no_choice: always fails"); 186 handle Error _ => g ()); 194 handle Error _ => S.NIL; 361 if List.exists p (!mem) then raise Error "cache_cut: repetition" 392 val prove = partial (Error "use_unit: NONE") (U.prove (Uref.!units)) 400 use_unit units g c s handle Error _ => f a g (c o grab_unit units) s; 430 val () = assert (0 <= low) (Error "meson: impossible divide and conquer") 432 if n' <= low then s' else raise Error "meson: divide and conquer" 448 match env r g handle Error _ => unify env r g; 473 raise Error "meso [all...] |
H A D | mlibRewrite.sml | 51 | NONE => raise Error "rewrite: rewr has been rewritten away!"); 170 in assert (order (tm, term_subst sub r) = SOME GREATER) (Error "orw") 214 val () = assert (j <> i) (Error "rewrite: same theorem") 216 val () = assert (agree lr ort) (Error "rewrite: bad orientation") 222 (Error "rewrite: order violation") 231 | NONE => raise Error "rewrite: no matching rewrites") 323 (Error "valid: violates order")
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | MMUScript.sml | 38 - more detailed version of mmu_arm_next (ValueState and Error X) 409 Error e => Error e 418 Error e => Error e 425 Error e => Error e
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Map.sml | 15 exception Error = mlibUseful.Error; exception 81 val () = if l + 1 + r = size then () else raise Error "wrong size" 96 | EQUAL => raise Error "duplicate keys" 97 | GREATER => raise Error "unsorted" 111 | EQUAL => raise Error "left child has equal key" 112 | GREATER => raise Error "left child has greater priority" 119 | EQUAL => raise Error "right child has equal key" 120 | GREATER => raise Error "right child has greater priority" 134 handle Error er [all...] |
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/ |
H A D | oracleSemScript.sml | 35 | Error 54 r ��� Timeout ��� r ��� Error ��� 62 eval_with_clock sem k (sem.init_st oracle) p = (st, Error))`; 232 (r = Error ��� ~sem_s.is_result r') ��� 233 (r ��� Error ��� sem_f.get_oracle_events st = sem_s.unload r')) 338 (same_result sem_f sem_s (st, Error) s ���
|
/seL4-l4v-master/l4v/tools/haskell-translator/ |
H A D | make_spec.sh | 57 echo Error: $SKEL is not a directory.
|
/seL4-l4v-master/HOL4/tools/quote-filter/ |
H A D | quote-filter.sml | 15 (output(stdErr, "Error opening "^infn^"\n");
|
/seL4-l4v-master/seL4/src/arch/x86/ |
H A D | c_traps.c | 52 /* Error code is in Error. Pull out bit 5, which is whether it was instruction or data */ 53 vm_fault_type_t type = (NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[Error] >> 4u) & 1u; 73 handleUserLevelFault(irq, NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[Error]);
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | server_commands.scala | 89 else throw new Server.Error("Session build failed: return code " + results.rc, results_json) 111 catch { case exn: Server.Error => error(exn.message) } 139 else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
|