1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11signature SPEC_GRAPH =
12sig
13
14datatype spec_type =
15    Definition | Constructor |  Case | Locale
16
17type entry = {name : string, def_name: string option, spec_type : spec_type}
18
19val get_graph: theory -> ((entry Int_Graph.T) * (string * typ -> Int_Graph.key option))
20
21val encode_graph: entry Int_Graph.T XML.Encode.T
22
23val decode_graph : entry Int_Graph.T XML.Decode.T
24
25
26end
27
28structure Spec_Graph : SPEC_GRAPH =
29struct
30
31datatype spec_type =
32  Definition | Constructor |  Case | Locale
33
34type entry = {name : string, def_name: string option, spec_type : spec_type}
35
36
37fun could_match (Ts, Us) =
38  Option.isSome (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
39
40
41fun get_graph thy =
42let
43  val defs = Theory.defs_of thy
44  val consts = Sign.consts_of thy
45  val {restricts,reducts} = Defs.dest (Theory.defs_of thy)
46
47  fun body_of (nm,args) =
48    let
49      val specs = Defs.specifications_of defs nm
50      val spec_of = find_first (fn {def,description,pos,lhs,rhs} => lhs = args) specs
51    in
52      the spec_of
53      |> (fn s => (#rhs s,#def s))
54  end
55
56fun add_general nm ls =
57let
58  val c = Consts.the_const consts nm
59  val args = Consts.typargs consts c
60in
61  if null args orelse exists (fn (args',_) =>
62      could_match (args',args)) ls
63  then ls else (ls @ [(args,([],NONE))])
64end
65
66val reduct_tab = map (fn ((nm,args),_) => (nm,(args,(body_of (nm,args))))) reducts
67  |> Symtab.make_list
68  |> Symtab.map add_general
69
70
71val id_reduct_tab =
72  fold_map (fn entry => fn id => ((id,entry),id + 1)) (Symtab.dest_list reduct_tab) 0
73  |> fst
74  |> map (fn (id,(nm,entry)) => (nm,(id,entry)))
75  |> Symtab.make_list
76
77fun id_of (nm,args) = case Symtab.lookup id_reduct_tab nm of SOME e =>
78    get_first (fn (id,(args',_)) => if could_match (args',args) then SOME id else NONE) e
79  | NONE => NONE
80
81fun mk_graph_entry (nm,(id,(args,(body,def)))) =
82let
83
84  val T = Consts.the_constraint consts nm
85
86  val case_suffixes = ["_case","_rec","_rec_set","_rep_set","_update","_Tuple_Iso"]
87
88  val spec_type = case (Datatype.info_of_constr thy (nm,T)) of
89      SOME _ => Constructor
90    | NONE => if Locale.defined thy nm then Locale else
91       if exists (fn n => String.isSuffix n nm) case_suffixes then Case else Definition
92
93  fun clean_def_name nm = if String.isSuffix "_raw" nm then (unsuffix "_raw" nm) else nm
94
95  val entry = {name = nm, def_name = Option.map clean_def_name def, spec_type = spec_type}
96in
97  ((id,entry),map_filter id_of body)
98end
99
100val raw_graph = map mk_graph_entry (Symtab.dest_list id_reduct_tab)
101
102val graph = Int_Graph.make raw_graph
103
104fun lookup_const (nm,T) =
105  let
106    val specs = Symtab.lookup id_reduct_tab nm
107    val args = Consts.typargs consts (nm,T)
108  in
109    Option.map (get_first (fn (id,(args',_)) => if could_match (args',args) then SOME id else NONE)) specs
110    |> Option.join
111  end
112
113in
114  (graph,lookup_const)
115end
116
117local
118  open XML.Encode
119
120fun spec_type_tostring spec_type = case spec_type of
121  Definition => "Definition"
122 | Constructor => "Constructor"
123 | Locale => "Locale"
124 | Case => "Case"
125
126
127in
128
129fun encode_entry (e as {name, def_name, spec_type} : entry) =
130  (triple string (option string) string) (name,def_name,spec_type_tostring spec_type)
131
132val encode_graph = Int_Graph.encode XML.Encode.int encode_entry
133
134
135end
136
137local
138  open XML.Decode
139
140fun spec_type_fromstring str = case str of
141  "Definition" => Definition
142 | "Constructor" => Constructor
143 | "Locale" => Locale
144 | "Case" => Case
145 | _ => error "Unknown spec type"
146
147fun triple_to_entry (name,def_name,spec_type) = ({name = name, def_name = def_name,
148  spec_type = spec_type_fromstring spec_type} : entry)
149
150in
151
152val decode_entry  =
153  (triple string (option string) string)
154
155fun decode_graph body = Int_Graph.decode XML.Decode.int decode_entry body
156|> Int_Graph.map (fn _ => triple_to_entry)
157
158end
159
160end
161
162