aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/recordobj.ml
blob: 6457fb5389206e258550ba40336a90d21bd74f29 (plain)
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