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
|
(* Title: elaboration.ML
Author: Joshua Chen
Basic elaboration.
*)
structure Elab: sig
val elab: Proof.context -> cterm list -> term -> Envir.env
val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term
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
end
|