Les Objdef introduisent une convertibilité avec les projections dans le test de conversion de Evarconv

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1291 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 86 insertions, 0 deletions

diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
new file mode 100755
index 000000000..5e54d1ffa
--- /dev/null
+++ b/toplevel/recordobj.ml
@@ -0,0 +1,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 
+	       ((NAM_Constant spi,cte_of_constr ci),v,lt,params,l_ui)) comp
+    | _ -> objdef_err ref
+                 
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
new file mode 100755
index 000000000..3a16613ed
--- /dev/null
+++ b/toplevel/recordobj.mli
@@ -0,0 +1,6 @@
+
+(* $Id$ *)
+
+open Term
+
+val objdef_declare : global_reference -> unit