Lines Matching +refs:val +refs:target
8 val result : 'a list -> ('a -> ('a,'b) r) -> 'a list * ('a,'b) r;
9 val p : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c * 'b) p;
10 val liftP : (('a,'b) p -> ('a,'c) p) -> ('a list,'b) p
12 val >> : ('a -> ('b, 'c) p) * ('c -> 'd) -> 'a -> ('b, 'd) p;
13 val >>> : ('a -> ('b,'c*'d) p) * ('d -> 'e) -> 'a -> ('b,'c*'e) p;
14 val >>= : ('a, 'b) p * ('b -> 'c) -> 'c option;
15 val getError : ('a, 'b) p -> string;
16 val return : 'a -> ('b, 'c) p -> ('b, 'c * 'a) p;
17 val initialState : 'a list -> ('a,string) p;
18 val pack : ('a, ('b * 'c) * 'd) p -> ('a, 'b * ('c * 'd)) p;
19 val expect_end : ('a, 'b) p -> ('c, 'b) p;
20 val e : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
21 val succeed : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
22 val succeedP : (('a, 'b) p -> ('a, 'b * 'c) p) ->
24 val fail : ('a, 'b) p -> ('c, 'd) p;
25 val many : (('a, 'b) p -> ('a, 'b * 'c) p) ->
27 val sepBy : (('a, 'b * 'c) p -> ('a, 'd * 'c) p) ->
30 val optional : (('a, 'b) p -> ('a, 'b * 'c) p) ->
32 val oneOf : (('a, 'b) p -> ('a, 'b * 'c) p) list ->
114 let val (ds',vs) = case many p (State (ds,v)) of
123 let val (ds',vs') =
150 val scan : string -> cmd list;
152 val test : cmd list -> (parsed_theory option * string);
184 val emptyLocalData = LocalData { assumes = [], fixes = [] };
208 target: string option,
214 target: string option,
234 eq:string,target:string option,
297 val parse_theory_head = e (content "theory") #> p name
304 val parse_theory_end = e (content "end") #> expect_end;
306 let val assumes = fn k => e k #>
310 val fixes = e (keyword "fixes") #>
322 val parse_mixfix = fn p_ =>
323 let val s2i = raw_explode #> read_int #> #1
324 val prio = fn s2i => p str_ >>> s2i
325 val prios = optional (many (prio s2i))
341 let val dt_type = e (content "datatype")
353 val consts = e (content "consts") #> many (
356 val axioms = e (content "axioms") #> many ((p name)
359 val cls = e (content "class") #> p name
368 val locale = e (content "locale") #> p name
377 val tp_synonym = e (content "type_synonym")
384 val fun_ = e (content "fun") #> p name
392 val primrec = e (content "primrec")
402 val def = e (content "definition")
417 name_tp=n,eq=e,target=t,attrs=a})
418 val notation = (oneOf [p (content "notation"),
444 t::_ => let val l' = cmd::l
445 val i' = case Token.content_of t of
466 t::_ => let val res = case Token.content_of t of
485 val parse_arity = fn _ => optional (e (keyword "(") #>
496 target=t,
506 target=t,
579 val parse_context = ((e (content "context") #> p name #>
584 val parse_instantiation = ((e (content "instantiation") #>
592 val test = initialState #> optional (p (unparse_cmd "header"))
611 val unlines : string list -> string
612 val unqualify : string -> string
614 val theory_of_string : string -> theory list -> theory
615 val theory_by_name : string -> theory
616 val name_of_theory : theory -> string
617 val axioms_of : theory -> named_term list
618 val non_image_theories : theory -> theory list
619 val thms_of : theory -> named_term list
620 val consts_of : theory -> (string * typ) list
621 val datatypes_of : theory -> ((string * typ list *
625 val functions_of : theory -> (string * typ *
629 val classes_of : theory -> (class * string list *
633 val locales_of : theory -> (string *
639 val pretty_as_str : Pretty.T -> string
640 val repr_term : theory -> term -> Pretty.T
641 val repr_typ : theory -> typ -> Pretty.T
642 val repr_name : string -> Pretty.T
643 val repr_function : theory -> (string * typ *
645 val repr_class : theory -> (class * string list *
648 val repr_locale : theory -> (string *
652 val repr_datatype : theory -> (string * typ list * (string *
654 val theory_of_exportable_data : theory -> theory
655 val get_basic_theory_data : theory -> (named_term list *
670 val get_theories : theory -> theory_data list
671 val xml_of_theories : theory_data list -> XML.tree
696 val unlines = String.concatWith (String.str (Char.chr 10))
707 val thmNum = Unsynchronized.ref 0
711 let val name = "TempTheory"^Int.toString (Unsynchronized.inc thmNum)
712 val header = Thy_Header.make ("TempTheory",Position.none) [] [] []
713 val text = unlines ["theory "^name,"begin",body,"end"]
723 val prettify_term = Logic.strip_imp_concl o remove_hol_true_prop
727 let val d = df T
728 val pd = (List.foldl op@ [] (List.map df (Context.parents_of T)))
732 val theory_by_name = Thy_Info.get_theory
733 val name_of_theory = Context.theory_name
734 val axioms_of = Theory.axioms_of
745 let val qnt = #1 (Term.dest_Const (HOLogic.all_const HOLogic.boolT))
746 val body = Term.strip_qnt_body qnt tm
747 val vars = List.map (fn (s,tp) => Var ((s,0),tp))
764 let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))
770 let val get_datatypes = (#log_types o Type.rep_tsig o Sign.tsig_of)
771 val ts = remove_parent_data get_datatypes fast_string_ord T
772 val is_mutually_rec_type = fn (_,i) => length (#descr i) >1
773 val check_rec = fn (n,v) => if is_mutually_rec_type (n,v)
775 val rec dtyp2typ = fn (descs,t) => case t of
784 val dt_desc = fn info => List.map (fn (_,(s,vs,eqs)) =>
785 let val vs' = List.map (curry dtyp2typ info) vs
786 val eqs' = List.map (fn (s,ts) =>
800 val functions_of =
801 let val get_funs = fn T =>
802 let val d = Item_Net.content (Function_Common.get_function
804 val fun_def = (fn (pats,def) => (#2 (strip_comb pats),def))
812 let val cls_suffix = "_class_def"
813 val thms = thms_of T
814 val cls_names = List.map (fn n => String.substring (n,0,String.size n-
818 let val i = AxClass.get_info T name
819 val parents' = List.concat (List.map
823 val parents = List.map (fn n => String.substring
827 val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2
832 val all_params = List.map (fn (s,t) => (Long_Name.base_name s,t))
834 val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params
835 val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))
840 let val all_locales = fn T => List.map (fn l => (#name l, #parents l))
842 val locales = Ord_List.subtract
850 let val parent_params = List.map (#1 o #1) (List.concat
853 val params = Ord_List.subtract (fn (s,((s1,_),_)) =>
858 val filter = ["_axioms.intro","_axioms_def","_def",".intro",".axioms_"]
859 val axs = List.filter ((String.isPrefix name) o #1)
861 val axioms' = List.filter
865 val axioms = List.map (fn (s,t) => (s,(HOLogic.dest_Trueprop o #2
868 val fix_consts = List.map (fn (s,t) => (s, Term.subst_Vars
871 val parse_axioms = fn v => List.map hol_forall_elim
873 val in_locale_axioms =
880 val in_loc = List.filter (fn (_,t) =>
882 val ex_loc = List.filter (fn (_,t) =>
891 let val ctxt = Config.put Printer.show_question_marks false
898 let val n = Long_Name.base_name n'
903 let val head = [Pretty.str "fun ", repr_name s, Pretty.str " :: ",
905 val body = List.map (fn (pats,tm) => Pretty.quote (Pretty.block
913 let val head = [Pretty.str "class", repr_name s]
916 val parents = List.map repr_name ps
917 val fixes' = List.map (fn (s,tp) => Pretty.block (Pretty.breaks
920 val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
932 let val head = [Pretty.str "locale", repr_name s]
935 val parents = List.map repr_name ps
936 val fixes' = List.map (fn ((s,tp),_) => Pretty.block (Pretty.breaks
939 val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
951 let val dts = List.map (fn (s,vs,eqs) =>
952 let val vs' = Pretty.enclose "(" ")"
954 val eqs' = Pretty.separate "|" (List.map
964 let val datatypes = datatypes_of T
965 val functions = functions_of T
966 val classes_Graph = String_Graph.make
968 val classes_sorted =
970 val classes = List.map
973 val locales_Graph = String_Graph.make
975 val locales_sorted =
977 val locales = List.map
987 let val T' = theory_of_exportable_data T
988 val cmp = (fn (s,(s1,_)) =>
990 val axs = Ord_List.subtract cmp
993 val thms = Ord_List.subtract cmp
996 val consts = Ord_List.subtract cmp
1002 let val Ts = T::(non_image_theories T)
1004 let val name = name_of_theory T
1005 val (axs,thms,consts) = get_basic_theory_data T
1006 val datatypes = datatypes_of T
1007 val functions = functions_of T
1008 val classes = classes_of T
1009 val locales = locales_of T
1037 let val b = case (Syntax.guess_infix (Sign.syn_of T)
1091 let val T = theory_by_name name
1092 val imports = List.map
1095 val axioms = List.map (fn (n,t) => XML.Elem
1098 val theorems = List.map (fn (n,t) => XML.Elem
1101 val consts = List.map (fn (n,tp) => XML.Elem
1104 val datatypes = List.map (xml_of_datatype T) dts
1105 val functions = List.map (xml_of_function T) fns
1106 val classes = List.map (xml_of_class T) cls
1107 val locales' = List.map (xml_of_locale T) locales