/seL4-l4v-10.1.1/isabelle/src/Pure/ML/ |
H A D | ml_lex.scala | 109 "#\"" ~ 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 D | ml_lex.scala | 109 "#\"" ~ 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 D | regexRef.sml | 2 (* /opt/hol_bir/tools/Holmake/regexpMatch.sml *)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_stepLib.sml | 758 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 D | arm_encoderLib.sml | 212 | ("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 D | selftest.sml | 45 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 D | arm_parserLib.sml | 2577 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 D | arm_rulesScript.sml | 301 ``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 D | arm_evalLib.sml | 388 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 D | json.scala | 101 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 D | json.scala | 101 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 D | Canon_Port.sml | 227 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 D | Options.sml | 19 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 D | Options.sml | 19 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 D | network.cpp | 308 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 D | ARM_proverLib.sml | 680 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 D | DeviceBase.sml | 339 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 D | quantHeuristicsScript.sml | 1204 ``!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 D | ObsCongrConv.sml | 119 val (opt, t1, t2) = args_equiv w value 121 if (opt = ``OBS_CONGR``) then
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | mungeTools.sml | 7 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 D | regAlloc.sml | 351 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 D | mlibMeson.sml | 258 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 D | TypeBase.sml | 144 fun valOf2 ty t opt = 145 case opt of
|
/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | computeLib.sml | 156 fun set_skip compset c opt = 158 in clauses.set_skip compset (Name,Thy) opt
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | rep_graph.py | 34 for opt in self.opts: 35 assert opt.kind in ['Number', 'Offset'] 96 opts = [opt for opt in opts if opt]
|