author | wenzelm |
Fri, 23 May 1997 10:14:16 +0200 | |
changeset 3311 | 36e3de24137d |
parent 3302 | 404fe31fd8d2 |
child 3332 | 3921ebbd9cf0 |
permissions | -rw-r--r-- |
3302 | 1 |
(* Title: TFL/thry |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
5 |
*) |
|
6 |
||
2112 | 7 |
structure Thry : Thry_sig (* LThry_sig *) = |
8 |
struct |
|
9 |
||
10 |
structure USyntax = USyntax; |
|
11 |
||
12 |
open Mask; |
|
13 |
structure S = USyntax; |
|
14 |
||
15 |
||
16 |
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg}; |
|
17 |
||
18 |
(*--------------------------------------------------------------------------- |
|
19 |
* Matching |
|
20 |
*---------------------------------------------------------------------------*) |
|
21 |
||
22 |
local open Utils |
|
23 |
infix 3 |-> |
|
24 |
fun tybind (x,y) = TVar (x,["term"]) |-> y |
|
25 |
fun tmbind (x,y) = Var (x,type_of y) |-> y |
|
26 |
in |
|
27 |
fun match_term thry pat ob = |
|
28 |
let val tsig = #tsig(Sign.rep_sg(sign_of thry)) |
|
29 |
val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob) |
|
30 |
in (map tmbind tm_theta, map tybind ty_theta) |
|
31 |
end |
|
32 |
||
33 |
fun match_type thry pat ob = |
|
34 |
map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob))) |
|
35 |
end; |
|
36 |
||
37 |
||
38 |
(*--------------------------------------------------------------------------- |
|
39 |
* Typing |
|
40 |
*---------------------------------------------------------------------------*) |
|
41 |
||
42 |
fun typecheck thry = cterm_of (sign_of thry); |
|
43 |
||
44 |
||
45 |
||
46 |
(*---------------------------------------------------------------------------- |
|
47 |
* Making a definition. The argument "tm" looks like "f = WFREC R M". This |
|
48 |
* entrypoint is specialized for interactive use, since it closes the theory |
|
49 |
* after making the definition. This allows later interactive definitions to |
|
50 |
* refer to previous ones. The name for the new theory is automatically |
|
51 |
* generated from the name of the argument theory. |
|
52 |
*---------------------------------------------------------------------------*) |
|
3191 | 53 |
|
54 |
||
55 |
(*--------------------------------------------------------------------------- |
|
56 |
* TFL attempts to make definitions where the lhs is a variable. Isabelle |
|
57 |
* wants it to be a constant, so here we map it to a constant. Moreover, the |
|
58 |
* theory should already have the constant, so we refrain from adding the |
|
59 |
* constant to the theory. We just add the axiom and return the theory. |
|
60 |
*---------------------------------------------------------------------------*) |
|
2112 | 61 |
local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection)) |
62 |
val Const(eeq_name, ty) = eeq |
|
63 |
val prop = #2 (S.strip_type ty) |
|
64 |
in |
|
65 |
fun make_definition parent s tm = |
|
66 |
let val {lhs,rhs} = S.dest_eq tm |
|
67 |
val {Name,Ty} = S.dest_var lhs |
|
68 |
val lhs1 = S.mk_const{Name = Name, Ty = Ty} |
|
69 |
val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
70 |
val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) |
3191 | 71 |
val (_, tm', _) = Sign.infer_types (sign_of parent) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
72 |
(K None) (K None) [] true ([dtm],propT) |
3191 | 73 |
val new_thy = add_defs_i [(s,tm')] parent |
2112 | 74 |
in |
3191 | 75 |
(freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy) |
76 |
end; |
|
2112 | 77 |
end; |
78 |
||
79 |
(*--------------------------------------------------------------------------- |
|
80 |
* Utility routine. Insert into list ordered by the key (a string). If two |
|
81 |
* keys are equal, the new element replaces the old. A more efficient option |
|
82 |
* for the future is needed. In fact, having the list of datatype facts be |
|
83 |
* ordered is useless, since the lookup should never fail! |
|
84 |
*---------------------------------------------------------------------------*) |
|
85 |
fun insert (el as (x:string, _)) = |
|
86 |
let fun canfind[] = [el] |
|
87 |
| canfind(alist as ((y as (k,_))::rst)) = |
|
88 |
if (x<k) then el::alist |
|
89 |
else if (x=k) then el::rst |
|
90 |
else y::canfind rst |
|
91 |
in canfind |
|
92 |
end; |
|
93 |
||
94 |
||
95 |
(*--------------------------------------------------------------------------- |
|
96 |
* A collection of facts about datatypes |
|
97 |
*---------------------------------------------------------------------------*) |
|
98 |
val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac) |
|
99 |
val prod_record = |
|
100 |
let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] |
|
101 |
(fn s => res_inst_tac [("p",s)] PairE_lemma) |
|
102 |
fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s)) |
|
103 |
in ("*", |
|
104 |
{constructors = [const "Pair"], |
|
105 |
case_const = const "split", |
|
106 |
case_rewrites = [split RS eq_reflection], |
|
107 |
case_cong = #case_cong prod_case_thms, |
|
108 |
nchotomy = #nchotomy prod_case_thms}) |
|
109 |
end; |
|
110 |
||
111 |
(*--------------------------------------------------------------------------- |
|
112 |
* Hacks to make interactive mode work. Referring to "datatypes" directly |
|
113 |
* is temporary, I hope! |
|
114 |
*---------------------------------------------------------------------------*) |
|
115 |
val match_info = fn thy => |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
116 |
fn "*" => Some({case_const = #case_const (#2 prod_record), |
2112 | 117 |
constructors = #constructors (#2 prod_record)}) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
118 |
| "nat" => Some({case_const = #case_const (#2 nat_record), |
2112 | 119 |
constructors = #constructors (#2 nat_record)}) |
120 |
| ty => case assoc(!datatypes,ty) |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
121 |
of None => None |
2112 | 122 |
| Some{case_const,constructors, ...} => |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
123 |
Some{case_const=case_const, constructors=constructors} |
2112 | 124 |
|
125 |
val induct_info = fn thy => |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
126 |
fn "*" => Some({nchotomy = #nchotomy (#2 prod_record), |
2112 | 127 |
constructors = #constructors (#2 prod_record)}) |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
128 |
| "nat" => Some({nchotomy = #nchotomy (#2 nat_record), |
2112 | 129 |
constructors = #constructors (#2 nat_record)}) |
130 |
| ty => case assoc(!datatypes,ty) |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
131 |
of None => None |
2112 | 132 |
| Some{nchotomy,constructors, ...} => |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
133 |
Some{nchotomy=nchotomy, constructors=constructors} |
2112 | 134 |
|
135 |
val extract_info = fn thy => |
|
136 |
let val case_congs = map (#case_cong o #2) (!datatypes) |
|
137 |
val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes)) |
|
138 |
in {case_congs = #case_cong (#2 prod_record):: |
|
139 |
#case_cong (#2 nat_record)::case_congs, |
|
140 |
case_rewrites = #case_rewrites(#2 prod_record)@ |
|
141 |
#case_rewrites(#2 nat_record)@case_rewrites} |
|
142 |
end; |
|
143 |
||
144 |
end; (* Thry *) |