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