1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
(* Title: elaboration.ML
Author: Joshua Chen
Basic term elaboration.
*)
structure Elab: sig
val elab: Proof.context -> cterm list -> term -> Envir.env
val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term
val elaborate: Proof.context -> cterm list -> ('a * (term * term list) list) list -> ('a * (term * term list) list) list
end = struct
(*Elaborate `tm` by solving the inference problem `tm: {}`, knowing `assums`,
which are fully elaborated, in `ctxt`. Return a substitution.*)
fun elab ctxt assums tm =
if Lib.no_vars tm
then Envir.init
else
let
val inf = Goal.init (Thm.cterm_of ctxt (Lib.typing_of_term tm))
val res = Types.check_infer (map Thm.assume assums) 1 (ctxt, inf)
val tm' =
Thm.prop_of (#2 (Seq.hd (Seq.filter_results res)))
|> Lib.dest_prop |> Lib.term_of_typing
handle TERM ("dest_typing", [t]) =>
let val typ = Logic.unprotect (Logic.strip_assums_concl t)
|> Lib.term_of_typing
in
error ("Elaboration of " ^ Syntax.string_of_term ctxt typ ^ " failed")
end
in
Seq.hd (Unify.matchers (Context.Proof ctxt) [(tm, tm')])
end
handle Option => error
("Elaboration of " ^ Syntax.string_of_term ctxt tm ^ " failed")
(*Recursively elaborate a statement \<And>x ... y. \<lbrakk>...\<rbrakk> \<Longrightarrow> P x ... y by elaborating
only the types of typing judgments (in particular, does not look at judgmental
equality statements). Could also elaborate the terms of typing judgments, but
for now we assume that these are always free variables in all the cases we're
interested in.*)
fun elab_stmt ctxt assums stmt =
let
val stmt = Lib.dest_prop stmt
fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
in
if Lib.no_vars stmt orelse Lib.is_eq stmt then
(Envir.init, stmt)
else if Lib.is_typing stmt then
let
val typ = Lib.type_of_typing stmt
val subst = elab ctxt assums typ
in (subst, subst_term subst stmt) end
else
let
fun elab' assums (x :: xs) =
let
val (env, x') = elab_stmt ctxt assums x
val assums' =
if Lib.no_vars x' then Thm.cterm_of ctxt x' :: assums else assums
in env :: elab' assums' xs end
| elab' _ [] = []
val (prems, concl) = Lib.decompose_goal ctxt stmt
val subst = fold (curry Envir.merge) (elab' assums prems) Envir.init
val prems' = map (Thm.cterm_of ctxt o subst_term subst) prems
val subst' =
if Lib.is_typing concl then
let val typ = Lib.type_of_typing concl
in Envir.merge (subst, elab ctxt (assums @ prems') typ) end
else subst
in (subst', subst_term subst' stmt) end
end
(*Apply elaboration to the list format that assumptions and goal statements are
given in*)
fun elaborate ctxt known assms =
let
fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
fun elab_fact (fact, xs) assums =
let val (subst, fact') = elab_stmt ctxt assums fact in
((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums)
end
fun elab (b, facts) assums =
let val (facts', assums') = fold_map elab_fact facts assums
in ((b, facts'), assums') end
in #1 (fold_map elab assms known) end
end
|
