/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttLearn.sig | 7 type loc = mlTacticData.loc type 19 ((goal * goal list) * (loc * call)) -> (loc * call)
|
H A D | tttLearn.sml | 121 ((g,gl), icall as (loc,{stac,ogl,fea})) = 141 SOME newstac => (loc, {stac = newstac, ogl = ogl, fea = fea})
|
/seL4-l4v-master/HOL4/src/AI/machine_learning/ |
H A D | mlTacticData.sig | 8 type loc = string * int * int type 10 val loc_compare : loc * loc -> order 14 calld : (loc,call) Redblackmap.dict, 21 val export_calls : string -> (loc * call) list -> unit 22 val import_calls : string -> (loc * call) list 30 val ttt_update_tacdata : ((loc * call) * tacdata) -> tacdata
|
H A D | mlNearestNeighbor.sig | 9 type loc = mlTacticData.loc type 24 val callknn: symweight * (loc * call) afea -> int -> fea -> (loc * call) list 25 val add_calldep: (loc,call) Redblackmap.dict -> int -> 26 (loc * call) list -> (loc * call) list
|
H A D | mlTacticData.sml | 20 type loc = string * int * int type 51 fun call_to_string (loc,{stac,ogl,fea}) = 52 [loc_to_string loc, stac, ilts ogl, ilts fea] 141 fun ttt_update_tacdata ((loc,call),{calld,taccov,symfreq}) = 143 calld = dadd loc call calld,
|
H A D | mlNearestNeighbor.sml | 95 val (loc,call) = lookup gn value 96 val _ = rl := (loc,call) :: (!rl)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | ExportTree.sml | 49 and PTdeclaredAt(loc: location): ptProperties = cast(0w2, loc) 53 and PTopenedAt(loc: location): ptProperties = cast(0w6, loc) 59 and PTstructureAt(loc: location): ptProperties = cast(0w12, loc) 113 fun prop (DeclaredAt loc) = PTdeclaredAt loc 114 | prop (OpenedAt loc) = PTopenedAt loc [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | typecheck_error.sml | 26 fun mkExn (tc, loc) = 27 mk_HOL_ERRloc "Preterm" "type-analysis" loc (errorMsg tc)
|
H A D | base_tokens.sml | 23 fun check p exnstring (s,loc) = let 29 else raise LEX_ERR (exnstring ^ ": " ^ s, loc) 81 fun parse_fraction (s, loc) = 85 loc) 94 loc)
|
H A D | Parse_supportENV.sml | 15 loc : locn.locn, fv : bool,
|
H A D | qbuf.sml | 67 fun maybe l = case locopt of NONE => l | SOME loc => loc
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | locn.sml | 76 fun toShortString loc = let 85 case loc of 87 | Loc_None => "<no loc>" 89 | Loc_Near loc => "~" ^ toShortString loc 109 fun near (loc as Loc_Near _) = loc 110 | near loc = Loc_Near loc
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | cond_cleanLib.sml | 9 fun find_inst_for loc insts = let 10 val pat = ``IMPL_INST code locs (Inst ^loc assert next)`` 50 fun report_optimisation branch loc old_dest new_dest = let 52 int_to_hex loc ^ "` can target `" ^ 78 val loc = th |> concl |> rand |> dest_Inst |> #1 |> rand value 80 val _ = report_optimisation "Else" loc old_dest new_dest 97 val loc = th |> concl |> rand |> dest_Inst |> #1 |> rand value 99 val _ = report_optimisation "Then" loc old_dest new_dest
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Asynt.sml | 35 fun mkIdInfo (loc, qualid) withOp = 37 info = { idLoc=loc, withOp=withOp }} 55 val loc = xxLR (hd ts) (last ts) value 57 (loc, RECty (mkTupleRow ts))
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/64/ |
H A D | cache.c | 96 int loc = LOC(clid); local 98 for (int l = 0; l < loc; l++) {
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv7-a/ |
H A D | cache.c | 113 int loc = LOC(clid); local 116 for (l = 0; l < loc; l++) {
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/32/ |
H A D | cache.c | 113 int loc = LOC(clid); local 116 for (l = 0; l < loc; l++) {
|
/seL4-l4v-master/l4v/tools/autocorres/tools/stats/ |
H A D | summary.py | 31 loc = intc(fetch_match(data, "([0-9]+) input line")) variable 52 print(" {project:<20} & {loc:>7} & {functions:>4} & "
|
/seL4-l4v-master/HOL4/src/monad/ |
H A D | parmonadsyntax.sml | 45 | QIDENT(loc,_,_) => 46 raise mk_HOL_ERRloc "Absyn" "to_vstruct" loc 50 | TYPED (loc, a0, pty) => VTYPED(loc, to_vstruct a0, pty) 121 | IDENT(loc,s) => if s = monad_emptyseq_special then 122 raise mk_HOL_ERRloc "monadsyntax" "clean_do" loc 137 IDENT(loc,s) => if s = monad_emptyseq_special then NONE
|
H A D | monadsyntax.sml | 140 | QIDENT(loc,_,_) => 141 raise mk_HOL_ERRloc "Absyn" "to_vstruct" loc 145 | TYPED (loc, a0, pty) => VTYPED(loc, to_vstruct a0, pty) 225 | IDENT(loc,s) => if s = monad_emptyseq_special then 226 raise mk_HOL_ERRloc "monadsyntax" "clean_do" loc 241 IDENT(loc,s) => if s = monad_emptyseq_special then NONE
|
/seL4-l4v-master/HOL4/src/marker/ |
H A D | markerSyntax.sml | 130 fun using_var loc = mk_var(using_encode loc, Type.ind) 131 fun mk_usingl loc = using_def |> SPEC (using_var loc) |> EQT_ELIM
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | theories_dockable.scala | 105 case Some((loc, size)) => 106 loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && 107 loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
|
H A D | pretty_tooltip.scala | 65 val loc = SwingUtilities.convertPoint(parent, location, layered) 66 val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | theories_dockable.scala | 105 case Some((loc, size)) => 106 loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && 107 loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | mungeTools.sml | 258 fun mkinst loc opts tm = let 267 else (warn (loc, "Type substitution mal-formed"); die "") 269 (warn (loc, "Type substitution mal-formed"); die "") 312 fun do_thminsts loc opts th = let 313 val (insts, tytheta, theta) = mkinst loc opts (concl th) 321 fun do_tminsts loc opts tm = let 322 val (insts, tytheta, theta) = mkinst loc opts tm 466 val parse_start = " (*#loc "^ Int.toString argline ^ " " ^
|