Searched refs:opt (Results 51 - 75 of 109) sorted by relevance

12345

/seL4-l4v-10.1.1/isabelle/src/Pure/ML/
H A Dml_lex.scala109 "#\"" ~ opt(str) ^^ { case x ~ Some(y) => x + y case x ~ None => x }
213 val sign = opt("~") ^^ { case Some(x) => x case None => "" }
226 decint ~ opt("/" ~ dec) ^^ { case x ~ None => x case x ~ Some(y ~ z) => x + y + z }
229 (decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ML/
H A Dml_lex.scala109 "#\"" ~ opt(str) ^^ { case x ~ Some(y) => x + y case x ~ None => x }
213 val sign = opt("~") ^^ { case Some(x) => x case None => "" }
226 decint ~ opt("/" ~ dec) ^^ { case x ~ None => x case x ~ Some(y ~ z) => x + y + z }
229 (decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/lib/
H A DregexRef.sml2 (* /opt/hol_bir/tools/Holmake/regexpMatch.sml *)
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_stepLib.sml758 fun make_arm_state_and_pre the_state (opt:options) instr =
760 val arch = #arch opt
761 val thumb = #thumb opt
762 val thumbee = #thumbee opt
763 val endian = #endian opt
777 val IT = wordsSyntax.mk_wordii (if T2 then #itblock opt else 0,8)
779 val M = mode_to_term (#mode opt)
801 val (flags_fupd,flags_pre) = set_flags the_state cond (#pass opt)
807 val npass = if #pass opt then F else T
1073 fun process_opt opt
1193 val opt = process_options options value
[all...]
H A Darm_encoderLib.sml212 | ("Hint_debug", [opt]) => [(PC,4),(opt,0)]
426 | ("Data_Memory_Barrier", [opt]) =>
428 [(``0b010101111111111100000101w:word24``,4), (opt,0)]
429 | ("Data_Synchronization_Barrier", [opt]) =>
431 [(``0b010101111111111100000100w:word24``,4), (opt,0)]
432 | ("Instruction_Synchronization_Barrier", [opt]) =>
434 [(``0b010101111111111100000110w:word24``,4), (opt,0)]
1244 | ("Data_Memory_Barrier", [opt]) =>
1245 [(``0b1001110111111100011110101w:25 word``,4), (opt,
[all...]
H A Dselftest.sml45 fun step opt instr =
51 case arm_step_updates opt opc
56 fun validate_arm_step opt (instr,upds) =
59 val cmp = (updates_to_set (step opt instr), updates_to_set upds)
H A Darm_parserLib.sml2577 fn (opt,indx,unpriv,rt,rn) =>
2596 case opt of
2616 case opt
2648 case opt
2659 fn opt =>
2668 (fn _ => arm_parse_mode3_offset (opt,true,F,rt,rn))
2672 (fn _ => arm_parse_mode3_offset (opt,false,F,rt,rn))
2676 case opt of
2684 case opt
2696 assertT (isSome opt andals
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A Darm_rulesScript.sml301 ``enc (instruction$LDR c b opt Rd Rn Op2)``);
304 ``enc (instruction$STR c b opt Rd Rn Op2)``);
310 ``enc (instruction$LDM c s opt Rd list)``);
313 ``enc (instruction$STM c s opt Rd list)``);
502 (IS_DT_SHIFT_IMMEDIATE offset) opt.Pre opt.Up Rn
509 ``enc (instruction$LDR c b opt Rd Rn offset)``);
513 ``enc (instruction$STR c b opt Rd Rn offset)``);
518 ``enc (instruction$LDR c b opt Rd Rn offset)``));
523 ``enc (instruction$STR c b opt R
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/
H A Darm_evalLib.sml388 fun mk_config_map opt s =
397 val _ = Lib.mem lr opt orelse
537 fun output_program opt t =
538 case opt
551 let val opt =
569 case opt
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Djson.scala101 opt("-") ~ number_body ~ opt(letter) ^^ {
108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Djson.scala101 opt("-") ~ number_body ~ opt(letter) ^^ {
108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^
/seL4-l4v-10.1.1/HOL4/src/meson/src/
H A DCanon_Port.sml227 local fun STRIP conv tm opt =
228 let val (vlist,M) = strip_binder opt tm
229 in GEN_ABS opt vlist (conv M)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DOptions.sml19 type opt = {switches : string list, arguments : string list, type
112 val basicOptions : opt list =
131 footer : string, options : opt list};
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DOptions.sml19 type opt = {switches : string list, arguments : string list, type
112 val basicOptions : opt list =
131 footer : string, options : opt list};
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dnetwork.cpp308 static Handle setSocketOption(TaskData *taskData, Handle args, int level, int opt);
309 static Handle getSocketOption(TaskData *taskData, Handle args, int level, int opt);
310 static Handle getSocketInt(TaskData *taskData, Handle args, int level, int opt);
1314 static Handle setSocketOption(TaskData *taskData, Handle args, int level, int opt) argument
1319 if (setsockopt(strm->device.sock, level, opt,
1326 static Handle getSocketOption(TaskData *taskData, Handle args, int level, int opt) argument
1332 if (getsockopt(strm->device.sock, level, opt,
1339 static Handle getSocketInt(TaskData *taskData, Handle args, int level, int opt) argument
1345 if (getsockopt(strm->device.sock, level, opt,
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A DARM_proverLib.sml680 fn (opt,body,flag,src_inv,trg_inv,uargs,pthms) =>
709 map (fn (opt, body) =>
710 prove_case_body (opt, body,true,src_inv,trg_inv,uargs,pthms)) cases
711 val (opt , body) = hd(List.rev(case_options)) value
725 let val proved_cases = map (fn (opt, body) =>
726 prove_case_body (opt, body,false,src_inv, trg_inv,uargs,pthms)) case_options
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DDeviceBase.sml339 fun getOpt opt conv v =
340 if IntInf.andb(fields, opt) = 0 then NONE else SOME(conv v)
456 | setOpt opt conv (SOME v) = (fields := IntInf.orb(!fields, opt); conv v)
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsScript.sml1204 ``!opt. (SOME (THE opt) = opt) <=> IS_SOME opt``,
1208 ``!opt. (opt = SOME (THE opt)) <=> IS_SOME opt``,
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DObsCongrConv.sml119 val (opt, t1, t2) = args_equiv w value
121 if (opt = ``OBS_CONGR``) then
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A DmungeTools.sml7 datatype opt = Turnstile | Case | TT | Def | SpacedDef | TypeOf | TermThm type
205 end where type elem = opt = struct
206 type elem = opt
415 fun foldthis (opt, acc) =
416 case opt of
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DregAlloc.sml351 let val opt = value
356 val (thing,_) = valOf opt
560 val opt = List.find (fn x => is_mem x andalso value
562 val tmp_m = valOf opt
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibMeson.sml258 fun mk_contrapositives chosen opt sos th =
266 fun f (a,c) = c |-> {asms = opt a, c = c, thm = th, asmn = length a}
274 val opt = if 1 <= sort_literals then sort_lits else I value
275 fun f sos (th,l) = mk_contrapositives chosen opt sos th @ l
/seL4-l4v-10.1.1/HOL4/src/1/
H A DTypeBase.sml144 fun valOf2 ty t opt =
145 case opt of
/seL4-l4v-10.1.1/HOL4/src/compute/src/
H A DcomputeLib.sml156 fun set_skip compset c opt =
158 in clauses.set_skip compset (Name,Thy) opt
/seL4-l4v-10.1.1/graph-refine/
H A Drep_graph.py34 for opt in self.opts:
35 assert opt.kind in ['Number', 'Offset']
96 opts = [opt for opt in opts if opt]

Completed in 174 milliseconds

12345