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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn
open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Eterm
module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)
open Pretyping
let _ = Pretyping.allow_anonymous_refs := true
type recursion_info = {
arg_name: name;
arg_type: types; (* A *)
args_after : rel_context;
wf_relation: constr; (* R : A -> A -> Prop *)
wf_proof: constr; (* : well_founded R *)
f_type: types; (* f: A -> Set *)
f_fulltype: types; (* Type with argument and wf proof product first *)
}
let my_print_rec_info env t =
str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
str "Full type: " ++ my_print_constr env t.f_fulltype
(* trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
(* str " and tycon "++ my_print_tycon env tycon ++ *)
(* str " in environment: " ++ my_print_env env); *)
let merge_evms x y =
Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y
let interp env isevars c tycon =
let j = pretype tycon env isevars ([],[]) c in
let evm = evars_of !isevars in
nf_evar evm j.uj_val, nf_evar evm j.uj_type
let find_with_index x l =
let rec aux i = function
(y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl
| [] -> raise Not_found
in aux 0 l
let list_split_at index l =
let rec aux i acc = function
hd :: tl when i = index -> (List.rev acc), tl
| hd :: tl -> aux (succ i) (hd :: acc) tl
| [] -> failwith "list_split_at: Invalid argument"
in aux 0 [] l
open Vernacexpr
let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env
let env_with_binders env isevars l =
let rec aux ((env, rels) as acc) = function
Topconstr.LocalRawDef ((loc, name), def) :: tl ->
let rawdef = coqintern_constr !isevars env def in
let coqdef, deftyp = interp env isevars rawdef empty_tycon in
let reldecl = (name, Some coqdef, deftyp) in
aux (push_rel reldecl env, reldecl :: rels) tl
| Topconstr.LocalRawAssum (bl, typ) :: tl ->
let rawtyp = coqintern_type !isevars env typ in
let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
let acc =
List.fold_left (fun (env, rels) (loc, name) ->
let reldecl = (name, None, coqtyp) in
(push_rel reldecl env,
reldecl :: rels))
(env, rels) bl
in aux acc tl
| [] -> acc
in aux (env, []) l
let subtac_process env isevars id l c tycon =
let c = Command.abstract_constr_expr c l in
(* let env_binders, binders_rel = env_with_binders env isevars l in *)
let tycon =
match tycon with
None -> empty_tycon
| Some t ->
let t = Command.generalize_constr_expr t l in
let t = coqintern_type !isevars env t in
let coqt, ttyp = interp env isevars t empty_tycon in
mk_tycon coqt
in
let c = coqintern_constr !isevars env c in
let coqc, ctyp = interp env isevars c tycon in
(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
(* str "Coq type: " ++ my_print_constr env ctyp) *)
(* with _ -> () *)
(* in *)
(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *)
(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *)
(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
(* in *)
let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
(* Evd.pr_evar_map evm) *)
(* with _ -> () *)
(* in *)
let evm = non_instanciated_map env isevars (evars_of !isevars) in
(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
evm, fullcoqc, fullctyp
open Subtac_obligations
let subtac_proof env isevars id l c tycon =
let nc = named_context env in
let nc_len = named_context_length nc in
let evm, coqc, coqt = subtac_process env isevars id l c tycon in
let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
add_definition id def coqt evars
|
