Searched refs:locs (Results 1 - 18 of 18) sorted by relevance

/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DExportTree.sml57 and PTreferences(exp: bool, locs: location list): ptProperties = cast(0w10, exp, locs)
111 fun mapLocationProps locs =
118 List.map prop locs
124 fun definingLocationProps locs =
130 List.foldl prop [] locs
H A DSIGNATURES.sml956 fun checkAndEnter (enter, lookup, kind, locs) (s: string, v) =
966 errorNear (lex, true, fn n => displaySigs(str, n), getDecLoc(locs v),
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Ddate.scala56 def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
59 if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Ddate.scala56 def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
59 if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A DGraphLangScript.sml191 (exec_next locs (IF guard n1 n2) s t w call =
192 if guard s then exec_next locs n1 s t w call
193 else exec_next locs n2 s t w call) /\
194 (exec_next locs (ASM assert update jmp) s t w call =
198 (exec_next locs (CALL assert update name jmp) s t w call =
201 locs name <> NONE /\
202 check_jump (Jump (THE (locs name))) t w /\
352 IMPL_INST code locs (Inst n assert next) =
355 assert s /\ exec_next locs next s t w call ==>
363 ``IMPL_INST code locs (Ins
[all...]
H A Dfunc_decompileLib.sml81 val lemma = prove(``LIST_IMPL_INST ^code locs []``,
151 val pat = ``locs (name:string) = SOME (w:word32)``
167 val lemma = prove(``EVERY (func_ok ^code locs) []``,
174 val th = th |> Q.INST [`locs`|->`fs_locs ^funcs`]
H A Dcond_cleanLib.sml10 val pat = ``IMPL_INST code locs (Inst ^loc assert next)``
H A Dgraph_specsLib.sml273 val goal = ``(locs ^name = SOME ^pc2) ==> IMPL_INST ^(mk_code_term c) locs ^i``
316 val goal = ``IMPL_INST ^(mk_code_term c) locs ^i``
359 val goal = ``IMPL_INST ^(mk_code_term c) locs ^i``
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DlocationScript.sml9 locs = Locs locn locn
H A DpegLib.sml28 ,``:('a,'b,'locs)parsetree``
H A DpegexecScript.sml16 | returnTo of ('atok # locs) list => 'cvalue option list => kont
39 ('atok # locs) list => 'cvalue option list =>
43 ('atok # locs) list => 'cvalue option list
44 | Result of (('atok # locs) list # 'cvalue) option
H A DgrammarScript.sml34 parsetree = Lf (('a,'b) symbol # 'locs)
35 | Nd ('b inf # 'locs) (parsetree list)
H A DpegScript.sml16 | any of (('a # locs) -> 'c)
17 | tok of ('a -> bool) => (('a # locs) -> 'c)
H A DsimpleSexpParseScript.sml618 (Q.ISPEC`sexpPEG`(Q.GEN`G`(Q.ISPEC`��(c,l:locs). SX_SYM[c]`(Q.GEN`a`peg_eval_list_tok_every_imp))))))
/seL4-l4v-10.1.1/HOL4/polyml/libpolymain/
H A DMakefile.in417 locs=`for p in $$list; do echo $$p; done | \
420 test -z "$$locs" || { \
421 echo rm -f $${locs}; \
422 rm -f $${locs}; \
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A DMakefile.in649 locs=`for p in $$list; do echo $$p; done | \
652 test -z "$$locs" || { \
653 echo rm -f $${locs}; \
654 rm -f $${locs}; \
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A DMakefile.in763 locs=`for p in $$list; do echo $$p; done | \
766 test -z "$$locs" || { \
767 echo rm -f $${locs}; \
768 rm -f $${locs}; \
798 locs=`for p in $$list; do echo $$p; done | \
801 test -z "$$locs" || { \
802 echo rm -f $${locs}; \
803 rm -f $${locs}; \
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DCODEGEN_PARSETREE.sml210 | getDeclLoc (_ :: locs) = getDeclLoc locs

Completed in 140 milliseconds