Searched refs:Error (Results 51 - 75 of 226) sorted by relevance

12345678910

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DTerm.sml34 | 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 DRule.sig32 (* 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 DThm.sml60 else raise Error "Thm.destUnit";
178 handle Error err =>
179 raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
H A Dproblems2tptp.sml35 else raise Error ("duplicate problem name: " ^ x)
170 handle Error s => die (PROGRAM^" failed:\n" ^ s)
H A DUseful.sml13 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 DTermNet.sml94 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 DRewrite.sml175 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 DTerm.sml34 | 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 DRule.sig32 (* 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 DThm.sml60 else raise Error "Thm.destUnit";
178 handle Error err =>
179 raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
H A Dproblems2tptp.sml35 else raise Error ("duplicate problem name: " ^ x)
170 handle Error s => die (PROGRAM^" failed:\n" ^ s)
H A DUseful.sml13 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 DTermNet.sml94 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 DgrammarLib.sml14 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 DmlibTerm.sml42 | 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 DmlibTptp.sml192 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 DmlibMeson.sml181 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 DmlibRewrite.sml51 | 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 DMMUScript.sml38 - 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 DMap.sml15 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 DoracleSemScript.sml35 | 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 Dmake_spec.sh57 echo Error: $SKEL is not a directory.
/seL4-l4v-master/HOL4/tools/quote-filter/
H A Dquote-filter.sml15 (output(stdErr, "Error opening "^infn^"\n");
/seL4-l4v-master/seL4/src/arch/x86/
H A Dc_traps.c52 /* 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 Dserver_commands.scala89 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)

Completed in 116 milliseconds

12345678910