aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/recordobj.ml
blob: a5556e6e619e75d942a1ad7c15f7cc4d7b7ea707 (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
76
77
78
79
80

(* $Id$ *)

open Util
open Pp
open Names
open Term
open Instantiate
open Lib
open Declare
open Recordops
open Classops

(*****  object definition ******)
 
let typ_lams_of t = 
  let rec aux acc c = match kind_of_term c with
    | IsLambda (x,c1,c2) -> aux (c1::acc) c2
    | IsCast (c,_) -> aux acc c
    | t -> acc,t
  in aux [] t

let objdef_err ref =
  errorlabstrm "object_declare"
    [< Printer.pr_global ref; 'sTR" is not a structure object" >]

let trait t =
  match kind_of_term t with
    | IsApp (f,args) ->
	if (match kind_of_term f with  
              | IsConst _ | IsMutInd _ | IsVar _ | IsMutConstruct _ -> true    
	      | _ -> false)
	then (f,Array.to_list args)
        else raise Not_found
    | IsConst _ | IsMutInd _ | IsVar _ | IsMutConstruct _ -> t,[]
    | _ -> raise Not_found

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 Evd.empty env ref in
  let vc =
    match kind_of_term v with
      | IsConst (sp,l as cst) ->
	  (match constant_opt_value env cst with
	     | Some vc -> vc
	     | None -> objdef_err ref)
      | _ -> objdef_err ref in
  let lt,t = decompose_lam vc in
  let lt = List.rev (List.map snd lt) in
  match kind_of_term t with 
    | IsApp (f,args) ->
	let { s_PARAM = p; s_PROJ = lpj } = 
        (try (find_structure
		(match kind_of_term f with
                   | IsMutConstruct ((indsp,1),_) -> indsp
		   | _ -> objdef_err ref))
         with _ -> 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 sp ->
		     try (sp, trait t)::l
                     with Not_found -> l)
            [] lps in
        add_anonymous_leaf (inObjDef1 sp);
        List.iter 
	  (fun (spi,(ci,l_ui)) -> 
	     add_new_objdef 
	       ((ConstRef spi,cte_of_constr ci),v,lt,params,l_ui)) comp
    | _ -> objdef_err ref