Boyer_Moore/shells.ml

   1 (******************************************************************************)
   2 (* FILE          : shells.ml                                                  *)
   3 (* DESCRIPTION   : Vague approximation in ML to Boyer-Moore "shell" principle *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 8th May 1991                                               *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : R.J.Boulton                                                *)
  12 (* DATE          : 12th October 1992                                          *)
  13 (*                                                                            *)
  14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  15 (* DATE          : July 2009                                                  *)
  16 (******************************************************************************)
  17
  18 (*----------------------------------------------------------------------------*)
  19 (* ML datatype for holding information about a recursive logical type.        *)
  20 (*----------------------------------------------------------------------------*)
  21
  22 type constructor_info =
  23    string *               (* Constructor name   *)
  24    hol_type list *        (* Argument types     *)
  25    (string * thm) list;;   (* Accessor functions *)
  26
  27
  28 type shell_info =
  29    {arg_types : hol_type list;     (* Argument types for type constructor *)
  30     constructors :
  31        constructor_info list;      (* Constructors for the type           *)
  32     axiom : thm;                   (* Type axiom                          *)
  33     induct : thm;                  (* Induction theorem                   *)
  34     cases : thm;                   (* Cases theorem                       *)
  35     distinct : thm list;           (* Constructors distinct               *)
  36     one_one : thm list;            (* Constructors one-one                *)
  37     struct_conv : conv -> conv};;
  38
  39 type shell = Shell of string * shell_info;;
  40
  41 (*----------------------------------------------------------------------------*)
  42 (* Reference variable holding the currently defined system shells.            *)
  43 (*----------------------------------------------------------------------------*)
  44
  45 let system_shells = ref ([]:shell list);;
  46
  47 (*----------------------------------------------------------------------------*)
  48 (* Function to find the details of a named shell from a list of shells.       *)
  49 (*----------------------------------------------------------------------------*)
  50
  51 let rec shell_info (shl:shell list) name =
  52    if (shl = [])
  53    then failwith "shell_info"
  54    else match (hd shl) with Shell (sh_name,info) ->
  55             (if (sh_name = name)
  56                then info
  57                else shell_info (tl shl) name);;
  58
  59 (*----------------------------------------------------------------------------*)
  60 (* Function to find the details of a named shell from the shells currently    *)
  61 (* defined in the system.                                                     *)
  62 (*----------------------------------------------------------------------------*)
  63
  64 let sys_shell_info name = shell_info !system_shells name;;
  65
  66 (*----------------------------------------------------------------------------*)
  67 (* Functions to extract the components of shell information.                  *)
  68 (*----------------------------------------------------------------------------*)
  69 let shell_constructors info = info.constructors;;
  70 let shell_accessor_thms info =
  71   ((map snd) o flat o (map  thd3) o shell_constructors) info;;
  72 let shell_arg_types info = info.arg_types;;
  73
  74 (*
  75 let shell_arg_types info = fst info
  76 and shell_constructors info = (fst o snd) info
  77 and shell_axiom info = (fst o snd o snd) info
  78 and shell_induct info = (fst o snd o snd o snd) info
  79 and shell_cases info = (fst o snd o snd o snd o snd) info
  80 and shell_distinct info = (fst o snd o snd o snd o snd o snd) info
  81 and shell_one_one info = (fst o snd o snd o snd o snd o snd o snd) info
  82 and shell_struct_conv info = (snd o snd o snd o snd o snd o snd o snd) info;;
  83 *)
  84
  85 (*----------------------------------------------------------------------------*)
  86 (* Function to extract details of a named constructor from shell information. *)
  87 (*----------------------------------------------------------------------------*)
  88
  89 let shell_constructor name (info:shell_info) =
  90    let rec shell_constructor' name triples =
  91       if (triples = [])
  92       then failwith "shell_constructor"
  93       else let (con_name,arg_types,accessors) = (hd triples)
  94       in if (con_name = name)
  95            then (arg_types,accessors)
  96            else shell_constructor' name (tl triples)
  97    in shell_constructor' name (info.constructors);;
  98
  99 (*----------------------------------------------------------------------------*)
 100 (* Functions to extract the argument types and the accessor functions for a   *)
 101 (* particular constructor. The source is a set of shell information.          *)
 102 (*----------------------------------------------------------------------------*)
 103
 104 let shell_constructor_arg_types name info =
 105    fst (shell_constructor name info)
 106 and shell_constructor_accessors name info =
 107    snd (shell_constructor name info);;
 108
 109 (*----------------------------------------------------------------------------*)
 110 (* shells : void -> string list                                               *)
 111 (*                                                                            *)
 112 (* Function to compute the names of the currently defined system shells.      *)
 113 (*----------------------------------------------------------------------------*)
 114
 115 let shells () =
 116    let rec shells' shl =
 117       if (shl = [])
 118       then []
 119       else match (hd shl) with (Shell (name,_)) -> (name::(shells' (tl shl)))
 120    in shells' !system_shells;;
 121
 122 (*----------------------------------------------------------------------------*)
 123 (* all_constructors : void -> string list                                     *)
 124 (*                                                                            *)
 125 (* Returns a list of all the shell constructors (and bottom values) available *)
 126 (* in the system.                                                             *)
 127 (*----------------------------------------------------------------------------*)
 128
 129 let all_constructors () =
 130  flat (map (map fst3 o shell_constructors o sys_shell_info) (shells ()));;
 131
 132 (*----------------------------------------------------------------------------*)
 133 (* all_accessors : void -> string list                                        *)
 134 (*                                                                            *)
 135 (* Returns a list of all the shell accessors available in the system.         *)
 136 (*----------------------------------------------------------------------------*)
 137
 138 let all_accessors () =
 139    flat (map (flat o map (map fst o thd3) o shell_constructors o
 140               sys_shell_info) (shells ()));;
 141
 142 let all_accessor_thms () =
 143   flat (map (shell_accessor_thms o sys_shell_info) (shells ()));;
 144
 145 (*----------------------------------------------------------------------------*)
 146 (* `Shell' for natural numbers.                                               *)
 147 (*----------------------------------------------------------------------------*)
 148
 149 let num_shell =
 150      let axiom = num_Axiom
 151          and induct = num_INDUCTION
 152          and cases = num_CASES
 153          and distinct = [NOT_SUC]
 154          and one_one = [SUC_INJ]
 155 (*         and pre = PRE *)
 156      in  Shell
 157             ("num",
 158              {arg_types = [];
 159               constructors =
 160                  [("0",[],[]);("SUC",[`:num`],[("PRE",CONJUNCT2 PRE)])];
 161               axiom = axiom;
 162               induct = induct;
 163               cases = cases;
 164               distinct = distinct;
 165               one_one = one_one;
 166               struct_conv = ONE_STEP_RECTY_EQ_CONV
 167                                (induct,distinct,one_one)});;
 168
 169 (*----------------------------------------------------------------------------*)
 170 (* `Shell' for lists.                                                         *)
 171 (*----------------------------------------------------------------------------*)
 172
 173 let list_shell =
 174    let axiom = new_axiom `!x f. ?!fn1. (fn1 [] = x) /\ (!h t. fn1 (CONS h t) = f (fn1 t) h t)`
 175 (* |- !x f. ?!fn1. (fn1 [] = x) /\ (!h t. fn1 (CONS h t) = f (fn1 t) h t) *)
 176        and induct = list_INDUCT
 177        and cases = list_CASES
 178        and distinct = [NOT_CONS_NIL]
 179        and one_one = [CONS_11]
 180    in  Shell
 181           ("list",
 182            {arg_types = [`:'a`];
 183             constructors =
 184                [("NIL",[],[]);
 185                 ("CONS",
 186                  [`:'a`;`:('a)list`],[("HD",HD);("TL",TL)])];
 187             axiom = axiom;
 188             induct = induct;
 189             cases = cases;
 190             distinct = distinct;
 191             one_one = one_one;
 192             struct_conv = ONE_STEP_RECTY_EQ_CONV
 193                              (induct,distinct,one_one)});;
 194
 195 (*----------------------------------------------------------------------------*)
 196 (* Set-up the system shell to reflect the basic HOL system.                   *)
 197 (*----------------------------------------------------------------------------*)
 198
 199 system_shells := [list_shell;num_shell];;
 200
 201 (*----------------------------------------------------------------------------*)
 202 (* define_shell : string -> string -> (string # string list) list -> void     *)
 203 (*                                                                            *)
 204 (* Function for defining a new HOL type together with accessor functions, and *)
 205 (* making a new Boyer-Moore shell from these definitions. If the type already *)
 206 (* exists the function attempts to load the corresponding theorems from the   *)
 207 (* current theory hierarchy and use them to make the shell.                   *)
 208 (*                                                                            *)
 209 (* The first two arguments correspond to the arguments taken by `define_type' *)
 210 (* and the third argument defines the accessor functions. This is a list of   *)
 211 (* constructor names each with names of accessors. The function assumes that  *)
 212 (* there are no accessors for a constructor that doesn't appear in the list,  *)
 213 (* so it is not necessary to include an entry for a nullary constructor. For  *)
 214 (* other constructors there must be one accessor name for each argument and   *)
 215 (* they should be given in the correct order. The function ignores any item   *)
 216 (* in the list with a constructor name that does not belong to the type.      *)
 217 (*                                                                            *)
 218 (* The constructor and accessor names must all be distinct and must not be    *)
 219 (* the names of existing constants.                                           *)
 220 (*                                                                            *)
 221 (* Example:                                                                   *)
 222 (*                                                                            *)
 223 (*    define_shell `sexp` `sexp = Nil | Atom * | Cons sexp sexp`              *)
 224 (*       [(`Atom`,[`Tok`]);(`Cons`,[`Car`;`Cdr`])];;                          *)
 225 (*                                                                            *)
 226 (* This results in the following theorems being stored in the current theory  *)
 227 (* (or these are the theorems the function would expect to find in the theory *)
 228 (* hierarchy if the type already exists):                                     *)
 229 (*                                                                            *)
 230 (*    sexp               (type axiom)                                         *)
 231 (*    sexp_Induct        (induction theorem)                                  *)
 232 (*    sexp_one_one       (injectivity of constructors)                        *)
 233 (*    sexp_distinct      (distinctness of constructors)                       *)
 234 (*    sexp_cases         (cases theorem)                                      *)
 235 (*                                                                            *)
 236 (* The following definitions for the accessor functions are also stored:      *)
 237 (*                                                                            *)
 238 (*    Tok                |- !x. Tok(Atom x) = x                               *)
 239 (*    Car                |- !s1 s2. Car(Cons s1 s2) = s1                      *)
 240 (*    Cdr                |- !s1 s2. Cdr(Cons s1 s2) = s2                      *)
 241 (*                                                                            *)
 242 (* In certain cases the distinctness or injectivity theorems may not exist,   *)
 243 (* when nothing is saved for them.                                            *)
 244 (*                                                                            *)
 245 (* Finally, a new Boyer-Moore shell is added based on the definitions and     *)
 246 (* theorems.                                                                  *)
 247 (*----------------------------------------------------------------------------*)
 248 (*
 249 let define_shell name syntax accessors =
 250    let find_theory s =
 251       letrec f s l =
 252          if (null l)
 253          then failwith `find_theory`
 254          else if can (theorem (hd l)) s
 255               then hd l
 256               else f s (tl l)
 257       in f s (ancestry ())
 258    in
 259    let mk_def_eq (name,comb,arg) =
 260       let ty = mk_type(`fun`,[type_of comb;type_of arg])
 261       in  mk_eq(mk_comb(mk_var(name,ty),comb),arg)
 262    in
 263    let define_accessor axiom (name,tm) =
 264       (name,new_recursive_definition false axiom name tm)
 265    in
 266    let define_accessors axiom (comb,specs) =
 267       map (\(name,arg). define_accessor axiom (name,mk_def_eq (name,comb,arg)))
 268           specs
 269    in
 270    if (mem name (shells ()))
 271    then failwith `define_shell -- shell already exists`
 272    else
 273    let defined = is_type name
 274    in  let theory =
 275           if defined
 276           then (find_theory name ?
 277                 failwith (`define_shell -- no axiom found for type ` ^ name))
 278           else current_theory ()
 279    in  let name_Axiom =
 280           if defined
 281           then theorem theory name
 282           else define_type name syntax
 283    in  let name_Induct =
 284           if defined
 285           then theorem theory (name ^ `_Induct`)
 286           else save_thm((name ^ `_Induct`),prove_induction_thm name_Axiom)
 287        and name_one_ones =
 288           if defined
 289           then (CONJUNCTS (theorem theory (name ^ `_one_one`))
 290                 ?\s if (can prove_constructors_one_one name_Axiom)
 291                     then failwith s
 292                     else [])
 293           else ((CONJUNCTS o save_thm)
 294                    ((name ^ `_one_one`),prove_constructors_one_one name_Axiom)
 295                 ? [])
 296        and name_distincts =
 297           if defined
 298           then (CONJUNCTS (theorem theory (name ^ `_distinct`))
 299                 ?\s if (can prove_constructors_distinct name_Axiom)
 300                     then failwith s
 301                     else [])
 302           else ((CONJUNCTS o save_thm)
 303                   ((name ^ `_distinct`),prove_constructors_distinct name_Axiom)
 304                 ? [])
 305    in  let name_cases =
 306           if defined
 307           then theorem theory (name ^ `_cases`)
 308           else save_thm((name ^ `_cases`),prove_cases_thm name_Induct)
 309    in  let ty = (type_of o fst o dest_forall o concl) name_cases
 310    in  let ty_args = snd (dest_type ty)
 311    in  let cases = (disjuncts o snd o dest_forall o concl) name_cases
 312    in  let combs = map (rhs o snd o strip_exists) cases
 313    in  let constrs_and_args = map (((fst o dest_const) # I) o strip_comb) combs
 314    in  let (constrs,arg_types) =
 315           split (map (I # (map type_of)) constrs_and_args)
 316    in  let acc_specs =
 317           map (\(c,args). combine((snd (assoc c accessors) ? []),args)
 318                   ? failwith
 319                        (`define_shell -- ` ^
 320                         `incorrect number of accessors for constructor ` ^ c))
 321               constrs_and_args
 322    in  let acc_defs =
 323           if defined
 324           then map (map ((\acc. (acc,definition theory acc)) o fst)) acc_specs
 325           else map (define_accessors name_Axiom) (combine (combs,acc_specs))
 326    in  let name_shell =
 327           Shell (name,ty_args,combine(constrs,combine(arg_types,acc_defs)),
 328                  name_Axiom,name_Induct,name_cases,
 329                  name_distincts,name_one_ones,
 330                  ONE_STEP_RECTY_EQ_CONV
 331                     (name_Induct,name_distincts,name_one_ones))
 332    in  do (system_shells := name_shell.system_shells);;
 333 *)