- completely new version of "functional inversion" using inversion on

  inductive  

- bug  correction in  "Functional  scheme" and  "functional inversion": the
  function are now parsed as references and not indent

- adding a zeta normalization function in rawtermops to zeta normalize
  graph constructions (not used for now)

- Bug correction  in generation of  functional principle types  (if an
  arguments of the function has a type which is a sort)
  
- adding a new persistent table for functional induction informations
  (graph,...)  

- new  save mechanism  for functional  induction principles  (reuse of
  proofs when possible)

- Minor bug correction in proof of principle.

- Distinguishing building_principles (that is  save them) and making then
  (just construct their proof term)



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

1 files changed, 60 insertions, 0 deletions

diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index c6406468a7..96b0e1eb7b 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -539,3 +539,63 @@ let ids_of_pat =
   in
   ids_of_pat Idset.empty 
   
+
+
+
+
+let zeta_normalize = 
+  let rec zeta_normalize_term rt = 
+    match rt with 
+      | RRef _ -> rt 
+      | RVar _ -> rt 
+      | REvar _ -> rt 
+      | RPatVar _ -> rt 
+      | RApp(loc,rt',rtl) -> 
+	  RApp(loc,
+	       zeta_normalize_term rt',
+	       List.map zeta_normalize_term rtl
+	      )
+      | RLambda(loc,name,t,b) -> 
+	  RLambda(loc,
+		  name,
+		  zeta_normalize_term t,
+		  zeta_normalize_term b
+		 )
+      | RProd(loc,name,t,b) -> 
+	  RProd(loc,
+		name, 		  
+		zeta_normalize_term t,
+		zeta_normalize_term b
+		 )
+      | RLetIn(_,Name id,def,b) -> 
+	  zeta_normalize_term (replace_var_by_term id def b)
+      | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
+      | RLetTuple(loc,nal,(na,rto),def,b) -> 
+	  RLetTuple(loc,
+		    nal,
+		    (na,option_map zeta_normalize_term rto),
+		    zeta_normalize_term def,
+		    zeta_normalize_term b
+		   )
+      | RCases(loc,infos,el,brl) -> 
+	  RCases(loc,
+		 infos,
+		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, 
+		 List.map zeta_normalize_br brl
+		)
+      | RIf(loc,b,(na,e_option),lhs,rhs) -> 
+	  RIf(loc, zeta_normalize_term b,
+	      (na,option_map zeta_normalize_term e_option),
+	      zeta_normalize_term lhs,
+	      zeta_normalize_term rhs
+	     )
+      | RRec _ -> raise (UserError("",str "Not handled RRec"))
+      | RSort _ -> rt 
+      | RHole _ -> rt 
+      | RCast(loc,b,k,t) -> 
+	  RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+      | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+  and zeta_normalize_br (loc,idl,patl,res) = 
+    (loc,idl,patl,zeta_normalize_term res)
+  in
+  zeta_normalize_term