export_helper.ml revision 6516023b9db74939c0a0f79fd6cc5bc7d9bab382
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersignature ExportHelper =
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_consts : theory -> (string * (typ * term option)) list
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val get_gen_consts : theory -> string -> (string * Datatype.info) list -> string list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_axioms : theory -> (string * term) list
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val get_gen_axioms : theory -> string -> (string * Datatype.info) list -> string list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_theorems : theory -> (string * term) list
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val get_gen_theorems : theory -> string -> (string * Datatype.info) list -> string list -> string list
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val get_datatypes : theory -> (string * Datatype.info) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val filter : string list -> (string * 'a) list -> (string * 'a) list
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstructure ExportHelper : ExportHelper =
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun mergesort _ [] = []
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | mergesort _ [x] = [x]
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | mergesort cmp_data xs = let val (ys,zs) = List.foldl (fn(i, (ys,zs)) => (zs, i::ys)) ([],[]) xs
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun merge (xs,[]) = xs
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | merge ([],xs) = xs
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | merge (x::xr,y::yr) = if (cmp_data x) <= (cmp_data y)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder then x::merge(xr,y::yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder else y::merge(x::xr,yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in merge(mergesort cmp_data ys, mergesort cmp_data zs) end
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder (* make a sorted list unique*)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder fun unique [] = []
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | unique [x] = [x]
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder | unique (x1::x2::xr) = if x1 = x2
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder then unique (x2::xr)
4d4ee5ef6601170c9d419da9fe8742c506507d11Jonathan von Schroeder else x1::(unique (x2::xr))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder (* remove xs from ys - both lists need to be sorted asc *)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove' _ _ ([],ys) = ys
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | remove' _ _ (_,[]) = []
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder | remove' cd1 cd2 (x::xr,y::yr) = if (cd1 x) < (cd2 y)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder then remove' cd1 cd2 (xr,y::yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder else if (cd2 y) < (cd1 x)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder then y::(remove' cd1 cd2 (x::xr,yr))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder else remove' cd1 cd2 (xr,yr)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove cmp_data = remove' cmp_data cmp_data
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun remove_parent_data df cmp_data T = let val d = df T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val pd = (List.foldl op@ [] (map df (Context.parents_of T)))
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in remove cmp_data (mergesort cmp_data pd,mergesort cmp_data d) end
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun full_name T name = Name_Space.full_name (Sign.naming_of T) (Binding.name name)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun prefix p s = List.map (fn x => p^s^x)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun postfix s p = List.map (fn x => x^s^p)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun l_to_intl l = List.map Int.toString (List.tl (List.rev (List.foldl (fn (_,x::xs) => (x+1)::x::xs) [0] l)))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun is_mutually_rec_type T (n,i) = (case (#alt_names i) of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (Option.isSome o (Datatype.get_info T) o (full_name T))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | NONE => false)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun check_rec T (n,v) = if is_mutually_rec_type T (n,v)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder then case String.compare (((#1 o #2 o List.hd o #descr) v),full_name T n) of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun restructure_rec_types T ts = List.foldl (fn (d,l) => case d of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (n,SOME(v)) => if check_rec T (n,v) then (n,v)::l
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | (_,NONE) => l) [] ts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_type_names T ts =
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val rec_types = List.filter (is_mutually_rec_type T) ts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val grouped_rec_names = List.map (fn x => case (#alt_names o #2) x of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder | NONE => []) rec_types
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val def_names = (List.map (Long_Name.base_name o #1 o #2) (List.concat (List.map (#descr o #2) rec_types)))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val all_rec_names = (List.concat grouped_rec_names)@def_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val constructors = List.map #1 (List.concat (List.map (#3 o #2) (List.concat (List.map (#descr o #2) ts))))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (grouped_rec_names,all_rec_names,constructors,def_names) end
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_consts T = let val consts_of = (Name_Space.dest_table (Syntax.init_pretty_global T)) o #constants o Consts.dest o Sign.consts_of
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in remove_parent_data consts_of #1 T end
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_gen_consts T name ts = let val (grouped_rec_names,all_rec_names,constructors,_) = get_type_names T ts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val rec_names = List.concat grouped_rec_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1) grouped_rec_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val simple_names = List.map List.hd (List.filter (fn x => List.length x = 1) grouped_rec_names)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in constructors@(prefix name "." (List.concat
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder[prefix "Abs" "_" rec_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "Rep" "_" rec_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x) all_rec_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.concat (List.map (fn x => let val comb = space_implode "_" x
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.concat (List.map (fn x => [x^"."^x^"_rec",
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rec_set",
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rep_set"]) simple_names),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (fn x => let val comb = space_implode "_" x
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (comb^"."^comb^"_rec_set")::
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (comb^"."^comb^"_rep_set")::(List.concat
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (fn y => [comb^"."^comb^"_rec_"^y,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder comb^"."^comb^"_rec_set_"^y,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder comb^"."^comb^"_rep_set_"^y]) (l_to_intl x))) end) mutually_rec_names)])) end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_axioms = remove_parent_data Theory.axioms_of #1
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_gen_axioms T name ts = let val (grouped_rec_names,all_rec_names,constructors,def_names) = get_type_names T ts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val rec_names = List.concat grouped_rec_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1) grouped_rec_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val simple_names = List.map List.hd (List.filter (fn x => List.length x = 1) grouped_rec_names)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (postfix "_" "def" constructors)@(prefix name "." (List.concat
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder [prefix "arity_type" "_" def_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "equal" "_" (postfix "_" "def_raw" def_names),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "type_definition" "_" rec_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x^"_def") def_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (postfix "_" "def"
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (fn x => let val comb = space_implode "_" x
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (comb^"."^comb^"_rec_set")::
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (comb^"."^comb^"_rep_set")::(List.concat
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder (fn y => [comb^"."^comb^"_rec_"^y,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder comb^"."^comb^"_rec_set_"^y,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder comb^"."^comb^"_rep_set_"^y]) (l_to_intl x))) end) mutually_rec_names)),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.concat (List.map (fn x => let val comb = space_implode "_" x
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in (List.map (fn y => comb^"."^y^"_case") x) end) grouped_rec_names),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.concat (List.map (fn x => [x^"."^x^"_rec",
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rec_set",
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder x^"."^x^"_rep_set"]) simple_names)]))])) end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val get_theorems = let fun theorems_of T = map (fn (a,b) => (a, prop_of b)) (Global_Theory.all_thms_of T)
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder in remove_parent_data theorems_of #1 end
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder fun get_gen_theorems T name ts ths = let val (grouped_rec_names,all_rec_names,constructors,def_names) = get_type_names T ts
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val rec_names = List.concat grouped_rec_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val mutually_rec_names = List.filter (fn x => List.length x > 1) grouped_rec_names
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val simple_names = List.map List.hd (List.filter (fn x => List.length x = 1) grouped_rec_names)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in prefix name "." (List.concat
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder [prefix "arity_equal" "_" def_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "arity_type" "_" def_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "type_definition" "_" rec_names,
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "equal" "_" (postfix "_" "def" def_names),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder prefix "equal" "_" (postfix "_" "def_raw" def_names),
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.map (fn x => "equal_"^x^"_inst.equal_"^x) def_names])
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.filter (String.isPrefix (name^"."^x^".")) ths) (unique (rec_names@def_names))))
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder List.filter (String.isPrefix (name^"."^(space_implode "_" x)^".")) ths) mutually_rec_names)) end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun get_datatypes T = let val tname = Context.theory_name T
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder val ts = (#log_types o Type.rep_tsig o Sign.tsig_of) T
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder val ts' = map (fn s => (String.extract (s,tl+1,NONE),Datatype.get_info T s)) (List.filter (String.isPrefix tname) ts)
6516023b9db74939c0a0f79fd6cc5bc7d9bab382Jonathan von Schroeder in restructure_rec_types T ts' end
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder fun filter rem d = remove' id #1 ((mergesort id rem),(mergesort #1 d))