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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Pp
open Names
open Term
open Instantiate
open Lib
open Declare
open Recordops
open Classops
open Nametab
(***** object definition ******)
let typ_lams_of t =
let rec aux acc c = match kind_of_term c with
| Lambda (x,c1,c2) -> aux (c1::acc) c2
| Cast (c,_) -> aux acc c
| t -> acc,t
in aux [] t
let objdef_err ref =
errorlabstrm "object_declare"
[< pr_id (Termops.id_of_global (Global.env()) ref);
'sTR" is not a structure object" >]
let objdef_declare ref =
let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
let env = Global.env () in
let v = constr_of_reference ref in
let vc = match Environ.constant_opt_value env sp with
| Some vc -> vc
| None -> objdef_err ref in
let lt,t = decompose_lam vc in
let lt = List.rev (List.map snd lt) in
let f,args = match kind_of_term t with
| App (f,args) -> f,args
| _ -> objdef_err ref in
let { s_PARAM = p; s_PROJ = lpj } =
try (find_structure
(match kind_of_term f with
| Construct (indsp,1) -> indsp
| _ -> objdef_err ref))
with Not_found -> objdef_err ref in
let params, projs =
try list_chop p (Array.to_list args)
with _ -> objdef_err ref in
let lps =
try List.combine lpj projs
with _ -> objdef_err ref in
let comp =
List.fold_left
(fun l (spopt,t) -> (* comp=components *)
match spopt with
| None -> l
| Some proji_sp ->
let c, args = decompose_app t in
try (ConstRef proji_sp, reference_of_constr c, args) :: l
with Not_found -> l)
[] lps in
add_anonymous_leaf (inObjDef1 sp);
List.iter
(fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj))
comp
|
