Searched refs:loc (Results 1 - 25 of 65) sorted by relevance

123

/seL4-l4v-master/HOL4/src/tactictoe/src/
H A DtttLearn.sig7 type loc = mlTacticData.loc type
19 ((goal * goal list) * (loc * call)) -> (loc * call)
H A DtttLearn.sml121 ((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 DmlTacticData.sig8 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 DmlNearestNeighbor.sig9 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 DmlTacticData.sml20 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 DmlNearestNeighbor.sml95 val (loc,call) = lookup gn value
96 val _ = rl := (loc,call) :: (!rl)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DExportTree.sml49 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 Dtypecheck_error.sml26 fun mkExn (tc, loc) =
27 mk_HOL_ERRloc "Preterm" "type-analysis" loc (errorMsg tc)
H A Dbase_tokens.sml23 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 DParse_supportENV.sml15 loc : locn.locn, fv : bool,
H A Dqbuf.sml67 fun maybe l = case locopt of NONE => l | SOME loc => loc
/seL4-l4v-master/HOL4/src/prekernel/
H A Dlocn.sml76 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 Dcond_cleanLib.sml9 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 DAsynt.sml35 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 Dcache.c96 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 Dcache.c113 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 Dcache.c113 int loc = LOC(clid); local
116 for (l = 0; l < loc; l++) {
/seL4-l4v-master/l4v/tools/autocorres/tools/stats/
H A Dsummary.py31 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 Dparmonadsyntax.sml45 | 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 Dmonadsyntax.sml140 | 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 DmarkerSyntax.sml130 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 Dtheories_dockable.scala105 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 Dpretty_tooltip.scala65 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 Dtheories_dockable.scala105 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 DmungeTools.sml258 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 ^ " " ^

Completed in 198 milliseconds

123