From 17b904b53e9cdd09c03d59ff94205d84a44c81b8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 8 Jan 2006 17:13:27 +0000
Subject: Fonctions de conversion rawconstr <-> cases_pattern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7816 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/rawterm.ml  | 33 +++++++++++++++++++++++++++++++++
 pretyping/rawterm.mli | 13 +++++++++++++
 2 files changed, 46 insertions(+)

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index a75f6165f6..d06395b09d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -205,6 +205,39 @@ let loc_of_rawconstr = function
   | RCast (loc,_,_,_) -> loc
   | RDynamic (loc,_) -> loc
 
+(**********************************************************************)
+(* Conversion from rawconstr to cases pattern, if possible            *)
+
+let rec cases_pattern_of_rawconstr na = function
+  | RVar (loc,id) when na<>Anonymous ->
+      (* Unable to manage the presence of both an alias and a variable *)
+      raise Not_found
+  | RVar (loc,id) -> PatVar (loc,Name id)
+  | RHole (loc,_) -> PatVar (loc,na)
+  | RRef (loc,ConstructRef cstr) ->
+      PatCstr (loc,cstr,[],na)
+  | RApp (loc,RRef (_,ConstructRef cstr),l) ->
+      PatCstr (loc,cstr,List.map (cases_pattern_of_rawconstr Anonymous) l,na)
+  | _ -> raise Not_found
+
+(* Turn a closed cases pattern into a rawconstr *)
+let rec rawconstr_of_closed_cases_pattern_aux = function
+  | PatCstr (loc,cstr,[],Anonymous) ->
+      RRef (loc,ConstructRef cstr)
+  | PatCstr (loc,cstr,l,Anonymous) ->
+      let ref = RRef (loc,ConstructRef cstr) in
+      RApp (loc,ref, List.map rawconstr_of_closed_cases_pattern_aux l)
+  | _ -> raise Not_found
+
+let rawconstr_of_closed_cases_pattern = function
+  | PatCstr (loc,cstr,l,na) ->
+      na,rawconstr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
+  | _ ->
+      raise Not_found
+
+(**********************************************************************)
+(* Reduction expressions                                              *)
+
 type 'a raw_red_flag = {
   rBeta : bool;
   rIota : bool;
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 014739fcb7..11b43ddfcc 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -96,6 +96,19 @@ val occur_rawconstr : identifier -> rawconstr -> bool
 
 val loc_of_rawconstr : rawconstr -> loc
 
+(**********************************************************************)
+(* Conversion from rawconstr to cases pattern, if possible            *)
+
+(* Take the current alias as parameter, raise Not_found if *)
+(* translation is impossible *)
+
+val cases_pattern_of_rawconstr : name -> rawconstr -> cases_pattern
+
+val rawconstr_of_closed_cases_pattern : cases_pattern -> name * rawconstr
+
+(**********************************************************************)
+(* Reduction expressions                                              *)
+
 type 'a raw_red_flag = {
   rBeta : bool;
   rIota : bool;
-- 
cgit v1.2.3