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
|
(************************************************************************)
(* 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$ *)
open Util
open Pp
open Names
open Libnames
open Nameops
open Term
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 (id_of_global 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
let comp' = List.map (fun (refi,c,argj) ->
(refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp in
add_canonical_structure (sp, comp')
let add_object_hook _ = objdef_declare
|
