author | desharna |
Thu, 31 Mar 2022 18:12:38 +0200 | |
changeset 75374 | 6e8ca4959334 |
parent 74561 | 8e6c973003c8 |
permissions | -rw-r--r-- |
70364
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/soft_type_system.ML |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
2 |
Author: Alexander Krauss |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
4 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
5 |
Support for a soft-type system within the Isabelle logical framework. |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
6 |
*) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
7 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
8 |
signature SOFT_TYPE_SYSTEM = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
9 |
sig |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
10 |
type operations = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
11 |
{augment: term -> Proof.context -> Proof.context, |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
12 |
implicit_vars: Proof.context -> term -> (string * typ) list, |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
13 |
purge: theory -> term -> term} |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
14 |
val setup: operations -> theory -> theory |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
15 |
val augment: term -> Proof.context -> Proof.context |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
16 |
val implicit_vars: Proof.context -> term -> (string * typ) list |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
17 |
val global_purge: theory -> term -> term |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
18 |
val purge: Proof.context -> term -> term |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
19 |
end; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
20 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
21 |
structure Soft_Type_System: SOFT_TYPE_SYSTEM = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
22 |
struct |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
23 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
24 |
(* operations *) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
25 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
26 |
type operations = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
27 |
{ |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
28 |
(*extend the proof context by additional information present in the |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
29 |
given term, e.g. assumptions about variables*) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
30 |
augment: term -> Proof.context -> Proof.context, |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
31 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
32 |
(*variables from the term that are implicitly introduced into the |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
33 |
context via this statement*) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
34 |
implicit_vars: Proof.context -> term -> (string * typ) list, |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
35 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
36 |
(*purge soft type annotations encoded in a term*) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
37 |
purge: theory -> term -> term |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
38 |
}; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
39 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
40 |
val no_operations: operations = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
41 |
{augment = K I, |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
42 |
implicit_vars = K (K []), |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
43 |
purge = K I}; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
44 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
45 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
46 |
(* theory data *) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
47 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
48 |
structure Data = Theory_Data |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
49 |
( |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
50 |
type T = (operations * stamp) option; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
51 |
val empty = NONE; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
52 |
fun merge (data as SOME (_, s), SOME (_, s')) = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
53 |
if s = s' then data |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
54 |
else error "Cannot merge theories with different soft-type systems" |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
55 |
| merge data = merge_options data; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
56 |
); |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
57 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
58 |
fun setup operations = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
59 |
Data.map (fn data => |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
60 |
(case data of |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
61 |
NONE => SOME (operations, stamp ()) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
62 |
| SOME _ => error "Duplicate setup of soft-type system")); |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
63 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
64 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
65 |
(* get operations *) |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
66 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
67 |
fun global_operations thy = |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
68 |
(case Data.get thy of SOME (ops, _) => ops | NONE => no_operations); |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
69 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
70 |
val operations = global_operations o Proof_Context.theory_of; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
71 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
72 |
fun augment t ctxt = #augment (operations ctxt) t ctxt; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
73 |
fun implicit_vars ctxt t = #implicit_vars (operations ctxt) ctxt t; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
74 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
75 |
fun global_purge thy t = #purge (global_operations thy) thy t; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
76 |
val purge = global_purge o Proof_Context.theory_of; |
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
77 |
|
b2bedb022a75
support for a soft-type system within the Isabelle logical framework;
wenzelm
parents:
diff
changeset
|
78 |
end; |