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