Searched refs:strs (Results 1 - 17 of 17) sorted by relevance

/seL4-l4v-master/HOL4/examples/real-to-float/
H A DdaisyLib.sml19 val strs = String.tokens (fn c => mem c cs) str value
20 val err = el 3 strs |> stringSyntax.fromMLstring
21 val lower = el 5 strs |> stringSyntax.fromMLstring
22 val upper = el 6 strs |> stringSyntax.fromMLstring
/seL4-l4v-master/HOL4/examples/lambda/barendregt/
H A DreductionEval.sml298 val (strs, sets) = value
303 fun do_them (strs,sets) ys (w as (asl,g)) =
315 if HOLset.isEmpty strs then ALL_TAC
317 val avoid_t = mk_set (HOLset.listItems strs)
321 else if HOLset.isEmpty strs then let
327 val base = mk_set (HOLset.listItems strs)
345 do_them (HOLset.add(strs,newname_t), sets) rest
349 do_them (strs,sets) y_fvs
/seL4-l4v-master/graph-refine/
H A Dstats.py209 def strs (seconds): function in function:print_total_time
211 print 'Slowest problem: %ss (%s)' % strs (time_vals[-1])
212 print 'Total time: %ss (%s)' % strs (sum (time_vals))
H A Dgraph-refine.py267 strs = [pair.funs[pair.tags[0]] for pair in pairs if pair]
268 return ' '.join (strs)
/seL4-l4v-master/HOL4/help/src-sml/
H A DParsspec.sml57 | OPENspec strs => res
58 | INCLUDEspecs strs => res
/seL4-l4v-master/HOL4/src/postkernel/
H A DThyDataSexp.sml170 fun sterms0 (s, acc as (strs,tms)) =
173 | SharedString s => (s::strs,tms)
174 | Term tm => (strs,tm::tms)
175 | Thm th => (strs, concl th :: (hyp th @ tms))
176 | Type ty => (strs, Term.mk_var("x", ty) :: tms)
178 | KName{Thy,Name} => (Thy::Name::strs,tms)
H A DSharingTables.sml332 fun add_strings strs (SDI {strtable,idtable,tytable,tmtable,exp}) =
334 val strtable = List.foldl str1 strtable strs
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DHelp.sml107 fun show name centerline initiallySought (strs : string Vector.vector) =
109 val lines = Vector.length strs
126 else if instr s (Vector.sub(strs, (i+curr) mod lines)) then
182 let val line = Vector.sub(strs, i)
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A DexportLib.sml102 val pat = ``Call next name args strs``
107 val (strs,ty) = tm |> rand |> listSyntax.dest_list value
109 val strs = strs |> map stringSyntax.fromHOLstring value
115 in (next,name,args,strs) end
/seL4-l4v-master/HOL4/examples/lambda/basics/
H A DbinderLib.sml153 fun find_avoids (t, (strs, sets)) = let
173 (addList(strs,strings), addList(addList(sets, fv_terms), stringsets))
184 val (strs, sets) = List.foldl find_avoids (empty_tmset, empty_tmset) (w::asl) value
206 fun do_one used strs sets' (g as (asl, w)) =
231 List.foldl mk_union (mk_set (HOLset.listItems strs)) sets'
246 (HOLset.add(strs,new_t))
253 do_one empty_tmset strs sets' g
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A Dcompiler.sml268 val (th,strs) = arm_compilerLib.arm_compile (SPEC_ALL def) ind (!style)
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dautomation_lemmasScript.sml550 val strs = map (fn v => mk_var(fst (dest_var v) ^ "_" ^ s,���:string���)) vs value
551 val nums = map (fn t => ���name ^t���) strs
559 val t2 = listSyntax.mk_list(strs,���:string���)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DDEBUGGER_.sml339 fun makeStructDebugEntries (strs: structVals list, debugEnv, level, lex, mkAddr) =
353 updateState (level, mkAddr) (List.foldl loadStruct ([], debugEnv) strs)
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A Darm_compiler_demoScript.sml44 val (th,strs) = arm_compile def ind as_proc
45 (* val _ = map print (["\n\n\n"] @ strs @ ["\n\n\n"]) *)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml881 val strs = listSyntax.mk_list(map fromMLstring params,``:string``) value
882 val x1 = pairSyntax.mk_pair(strs,body)
/seL4-l4v-master/l4v/tools/haskell-translator/
H A Dlhs_pars.py545 strs = [str(bit) for bit in bits]
546 return ' '.join(strs)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DTYPECHECK_PARSETREE.sml904 val strs = List.mapPartial findStructure ptl value
969 val () = List.app copyEntries strs;

Completed in 122 milliseconds