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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
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 Glob_term
open Evarconv
open Pattern
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_glob_constr env c) ++ *)
(* str " and tycon "++ my_print_tycon env tycon ++ *)
(* str " in environment: " ++ my_print_env env); *)
let interp env isevars c tycon =
let j = pretype true tycon env isevars ([],[]) c in
let _ = isevars := Evarutil.nf_evar_map !isevars in
let evd = consider_remaining_unif_problems env !isevars in
(* let unevd = undefined_evars evd in *)
let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in
let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in
let evm = unevd' in
isevars := unevd';
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
open Vernacexpr
let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr =
Constrintern.intern_constr evd env
let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr =
Constrintern.intern_type 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, k, 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 ?(is_type=false) env isevars id bl c tycon =
let c = Topconstr.abstract_constr_expr c bl in
let tycon, imps =
match tycon with
None -> empty_tycon, None
| Some t ->
let t = Topconstr.prod_constr_expr t bl in
let t = coqintern_type !isevars env t in
let imps = Implicit_quantifiers.implicits_of_glob_constr t in
let coqt, ttyp = interp env isevars t empty_tycon in
mk_tycon coqt, Some imps
in
let c = coqintern_constr !isevars env c in
let imps = match imps with
| Some i -> i
| None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c
in
let coqc, ctyp = interp env isevars c tycon in
let evm = non_instanciated_map env isevars !isevars in
let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
evm, coqc, ty, imps
open Subtac_obligations
let subtac_proof kind hook env isevars id bl c tycon =
let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
let evm' = Subtac_utils.evars_of_term evm evm' coqt in
let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars
|
