Lines Matching +refs:val +refs:output
147 val cmd_theory : (Token.T list * Thy_Header.header) parser
148 val cmd_header : string parser
149 val thy_body : (Token.T list * TheoryData.thy_body) parser
150 val init_thy : Path.T -> (Token.T list * Thy_Header.header) ->
158 val hide = curry Hide;
160 let val (v,toks') = f toks
161 val consumed_toks = List.take(toks,List.length toks-
172 val unparse_verbatim = unparse_kind Token.Verbatim;
173 val not_command = Parse.group (fn () => "non-command token")
181 val cmd_theory = preserve_toks (Parse.command_name "theory"
185 val cmd_header = Parse.command_name "header" |-- unparse_verbatim;
187 val opt_mode =
189 let val mode_spec = (@{keyword "output"} >> K ("", false)) ||
191 (@{keyword "output"} >> K false) true;
194 val trans_line = (* line 157 *)
195 let val trans_pat = (* line 147 *)
209 val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
217 val parse_theorem = Parse.opt_target --
224 val mk_thy_body = List.map (fn (s,p) => Parse.command_name s |-- p);
248 val proof_prefix = Scan.repeat (Scan.first
252 val unparse_tokens = (List.map (List.map Token.unparse)
255 val proof = Parse.!!! ((proof_prefix -- Scan.first
262 val simple_thy_body' = first' (mk_thy_body [
294 let val p = Parse.opt_target -- Parse.type_args --
314 let val opt_unchecked_overloaded =
483 let val opt_thm_name' : (bool * Attrib.binding) parser =
487 val spec' : (bool * (Attrib.binding * string)) parser =
490 val alt_specs' : (bool * (Attrib.binding * string)) list parser =
491 let val unexpected = Scan.ahead
499 let val dest_decl : (bool * binding option * string) parser =
509 val cons_decl = Parse.binding --
512 val domain_decl = (Parse.type_args_constrained --
516 val domains_decl =
526 let val (cmd,toks'') = take_suffix Token.is_command toks'
531 val diagnostic_commands = ["pretty_setmargin","help","print_commands",
540 val toplevel_commands = ["cd","pwd","use_thy","remove_thy",
545 val simple_thy_body = simple_thy_body' ||
551 val locale_val =
575 (let val class_val = (* Pure/Isar/isar_syn.ML line 458 *)
579 val p = Parse.binding -- Scan.optional (@{keyword "="}
591 (let val p = Scan.repeat1 (Parse.name --| (* line 493 *)
602 val thy_body = simple_thy_body || rec_thy_body;
605 let val master_dir = Thy_Load.get_master_path ()
606 val spans = (*map (resolve_files master_dir)*)
608 val elements = Thy_Syntax.parse_elements spans
610 val immediate = not (Goal.future_enabled ())
613 val (result, st') = Toplevel.proof_result immediate
615 val pos' = Toplevel.pos_of (List.last (tr :: trs))
621 val (results, (end_state, end_pos)) = fold_map element_result
625 let val t = read (K
626 (let val {name = (name, _), imports, uses, ...} = header
627 val _ = Thy_Header.define_keywords header
628 val _ = Present.init_theory name
629 val master_dir = dir
630 val parents = List.map (Thy_Info.get_theory o #1) imports
638 val scan : Path.T -> Token.T list;
639 val dbg : Token.T list -> (Token.kind * string) list
644 val thy : Token.T list -> thy
645 val read_sort : Toplevel.state -> (string * Position.T) option
647 val read_typ : Toplevel.state -> (string * Position.T) option
649 val read_term : Proof_Context.mode -> Toplevel.state ->
651 val read_prop : Toplevel.state -> (string * Position.T) option ->
653 val read_class : Toplevel.state -> (string * Position.T) option ->
655 val inferred_param : string -> Toplevel.state ->
657 val pretty_tokens : unit -> unit
665 val format_type_mixfix : string -> Mixfix.mixfix ->
667 val format_const_mixfix : Toplevel.state -> string -> Mixfix.mixfix ->
687 val dbg = List.map (fn t => (Token.kind_of t,Token.content_of t));
688 val thy = Scan.catch (Scan.option cmd_header -- cmd_theory
693 let val ctxt = Named_Target.context_cmd (the_default
697 let val ctxt' = Named_Target.context_cmd (the_default
699 val ctxt = Proof_Context.set_mode mode ctxt'
701 val read_typ = do_read Syntax.read_typ Proof_Context.mode_default;
702 val read_term = do_read Syntax.read_term;
703 val read_prop = do_read Syntax.read_prop Proof_Context.mode_default;
704 val read_class = do_read Proof_Context.read_class
736 val (bsyms, xsyms') = xsyms_to_syms xsyms;
737 val (syms, xsyms'') = xsyms_to_syms xsyms';
759 let val (Syntax_Ext.Syn_Ext {xprods=p,...}) =
766 let val (Syntax_Ext.Syn_Ext {xprods=p,...}) =
799 val xml_of_theory : (string -> unit) -> string -> XML.tree list
800 val get_non_image_parents : theory -> theory list
815 val xml_of_import = attr "name" #1 #> xml' "Import" [];
816 val xml_of_keyword = variant "xml_of_keyword" PolyML.makestring
821 val xml_of_expr = variant "xml_of_expr" PolyML.makestring
825 val unqualified = Binding.qualified_name #> Binding.name_of;
828 let val btoks = List.map #1 body |> flat
829 val blen = List.length btoks
830 val len = List.length t
841 val attr_of_target =
848 let val b' = Binding.print b
850 val attr_of_binding = attr "name" string_of_binding;
862 xml "String" (a "val" s) [],
900 (let val name = string_of_binding b
901 val tp = Parser.inferred_param name state target
923 let val (skips, raw_spec) = ListPair.unzip eqs
924 val (fixes, spec) = fst (Specification.read_spec f
926 val get_tms = (fn (lhs,rhs) => (strip_cfun lhs,rhs)) o
928 val get_imps = map HOLogic.dest_Trueprop o
930 val tms = map ((fn x => (get_imps x,get_tms x)) o
932 val tms' = ListPair.zip (skips,tms)
933 val fn_eqs = List.foldl (fn (eq,t) =>
934 let val (b,(imps,((c::vs),def_tm))) = eq
935 val (name,tp) = dest_Free c
936 val old = Symtab.lookup t name
944 val fns = List.foldl (fn (((b,_),mx),t) =>
948 let val b = unqualified k
949 val SOME(mx) = Symtab.lookup fns b
950 val equations' = List.map (fn (b,imps,vs,tm) =>
951 let val imps' = xml "Premises" [] (List.map
957 val elem = xml "FixrecFun" (a "name" b)
963 let val eqs' = List.map (fn ((b,l),tm) =>
964 let val _ = if Attrib.is_empty_binding (b,l)
972 val fn_eqs = List.foldl (fn (eq,t) =>
973 let val ((c,vs),def_tm) = eq
974 val (name,tp) = dest_Const c
975 val old = Symtab.lookup t name
983 val fns = List.foldl (fn ((b,_,mx),t) =>
987 let val b = unqualified k
988 val SOME(mx) = Symtab.lookup fns b
989 val equations' = List.map (fn (vs,tm) =>
992 val elem = xml "Fun" (a "name" b)
1006 let val t' = Parser.read_term
1009 val ts' = List.map (Parser.read_term
1026 let val (elem,state') = variant "xml_of_body" PolyML.makestring [
1028 let val l' = List.map (fn ((name,tm),args) =>
1029 let val tm' = Parser.read_prop state NONE tm
1030 val (c,def_tm) = Logic.dest_equals tm'
1031 val (cname',tp) = dest_Const c
1032 val cname = unqualified cname'
1033 val args' = List.map (Args.pretty_src
1040 val attrs = (if unchecked then a "unchecked" "" else [])
1044 let val vars' = List.map (fn (name,sort) => case sort of
1048 val tm' = Parser.read_term Proof_Context.mode_default
1050 val morphisms' = case morphisms of
1054 val mx' = xml_of_type_mixfix (string_of_binding tp)
1063 let val ([name],args',sort) = Class.read_multi_arity
1065 val args = List.map #2 args'
1066 val (begin_,end_) = extract_context toks body
1067 val s1 = trans state begin_
1068 val ((s2,_),b_elems) =
1070 val s3 = trans s2 end_
1075 let val s1 = trans state toks
1076 val (attrs,elems) = case head of
1078 let val (names,args',sort) =
1081 val args = List.map #2 args'
1082 val vars = xml "Vars" [] (List.map (fn s =>
1094 let val s1 = trans state toks
1101 let val (begin_,end_) = extract_context toks body
1102 val s1 = trans state begin_
1103 val ((s2,_),b_elems) =
1105 val s3 = trans s2 end_
1106 val parents' = variant "xml_of_body_elem (Locale)"
1109 val name' = attr_of_binding name
1110 val target = SOME (string_of_binding name,Position.none)
1111 val ctxt' = xml "Ctxt" []
1116 let val (begin_,end_) = extract_context toks body
1117 val s1 = trans state begin_
1118 val ((s2,_),b_elems) =
1120 val s3 = trans s2 end_
1121 val target = SOME (string_of_binding name,Position.none)
1122 val parents' = List.map (attr "name"
1127 val name' = attr_of_binding name
1128 val ctxt' = xml "Ctxt" []
1134 let val s1 = trans state toks
1135 val typ' = Parser.read_typ state target typ
1137 val name' = attr_of_binding name
1138 val target' = attr_of_target target
1139 val mx' = xml_of_type_mixfix (string_of_binding name)
1141 val vars' = xml "Vars" [] (List.map
1147 let val s1 = trans state toks
1148 val dts' = List.map
1154 let val cname = string_of_binding c
1155 val tps = List.map
1157 val tp = (tps ---> Type
1164 val is_c = not (String.isSubstring " " cname)
1165 val attrs = if is_c then attr_of_binding c
1167 val elems' = List.map XML_Syntax.xml_of_type
1170 val elems = if is_c then (xml_of_mixfix s1
1181 let val tp' = Parser.read_typ state NONE tp
1182 val name' = string_of_binding name
1183 val mx' = xml_of_mixfix state name' (SOME tp') mx
1193 let val result = case (args,strs) of
1195 let val s1 = trans state toks
1196 val ctxt' = xml "Ctxt" []
1205 let val s1 = trans state toks
1206 val _ = case binding of
1210 val ((_,[(_,tm')]),_) =
1213 val tm'' = HOLogic.dest_Trueprop tm'
1215 val (((name',tp),vs),def_tm) = tm'' |>
1221 val mx' = case name of
1230 let val s1 = trans state toks
1231 val elems = split_equations s1 target f a
1235 let val s1 = trans state toks
1236 val elems = split_equations s1 target f a
1239 let val s1 = trans state toks
1240 val elems = split_fixrec_equations s1 target f a
1243 let val s1 = trans state toks
1244 val dts' = List.map (fn (((vs,name),mx), cs) =>
1245 let val vars = List.map (fn (a,s) =>
1249 val mx' = xml_of_type_mixfix (string_of_binding
1251 val cs' = List.map (fn ((c,args),mx1) =>
1252 let val t = string_of_binding c |>
1275 let val _ = v ("Reading "^file'^"\n")
1276 val file = file' |> Path.explode |> Path.expand |>
1278 val dir = Path.dir file
1279 val tname = Path.explode file' |> Path.base |>
1281 val (Thy {header,args=(th,h),body}) =
1283 val _ = v ("Loading parents of theory "^tname^"\n")
1284 val thys = map (fn (i,_) => (Thy_Info.get_theory i; [])
1286 let val full = Path.explode i |>
1291 val imports = List.map xml_of_import (#imports h)
1292 val keywords = List.map xml_of_keyword (#keywords h)
1293 val uses = List.map xml_of_use (#uses h)
1294 val name = attr "name" #1 (#name h)
1295 val header' = attr_of_option "header" "header" I header
1296 val (s,t) = ParserHelper.init_thy dir (th,h)
1297 val _ = v ("Exporting theory "^tname^"\n")
1298 val (s',body'') = xml_of_body (s,t) body
1299 val _ = Toplevel.command (Toplevel.exit
1303 val body' = [body'' |> List.rev |> xml "Body" []]