From 05bc5277f0d8e7c0519cb5e9dbffc7bea80d1bd3 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Fri, 24 Nov 2006 19:08:00 +0000
Subject: Functional graph merging deals with letins.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9404 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/rawtermops.ml | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'contrib/funind/rawtermops.ml')

diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index ed46ec72d0..6b9a5b5df4 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -32,9 +32,27 @@ let raw_decompose_prod =
   in
   raw_decompose_prod []
 
+let raw_decompose_prod_or_letin = 
+  let rec raw_decompose_prod args = function 
+  | RProd(_,n,t,b) -> 
+      raw_decompose_prod ((n,None,Some t)::args) b 
+  | RLetIn(_,n,t,b) -> 
+      raw_decompose_prod ((n,Some t,None)::args) b 
+  | rt -> args,rt
+  in
+  raw_decompose_prod []
+
 let raw_compose_prod = 
   List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
 
+let raw_compose_prod_or_letin = 
+  List.fold_left (
+      fun concl decl -> 
+	match decl with 
+	  | (n,None,Some t) -> mkRProd(n,t,concl)
+	  | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl)
+	  | _ -> assert false)
+
 let raw_decompose_prod_n n = 
   let rec raw_decompose_prod i args c = 
     if i<=0 then args,c
@@ -47,6 +65,20 @@ let raw_decompose_prod_n n =
   raw_decompose_prod n []
 
 
+let raw_decompose_prod_or_letin_n n = 
+  let rec raw_decompose_prod i args c = 
+    if i<=0 then args,c
+    else
+      match c with
+	| RProd(_,n,t,b) -> 
+	    raw_decompose_prod (i-1) ((n,None,Some t)::args) b 
+	| RLetIn(_,n,t,b) -> 
+	    raw_decompose_prod (i-1) ((n,Some t,None)::args) b 
+	| rt -> args,rt
+  in
+  raw_decompose_prod n []
+
+
 let raw_decompose_app = 
   let rec decompose_rapp acc rt =
 (*     msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
-- 
cgit v1.2.3