From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 plugins/extraction/scheme.ml | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

(limited to 'plugins/extraction/scheme.ml')

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 1f04ca59..21507655 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s Production of Scheme syntax. *)
 
 open Pp
@@ -87,7 +85,7 @@ let rec pp_expr env args =
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r ->
 	apply (pp_global Term r)
-    | MLcons (info,r,args') ->
+    | MLcons (_,r,args') ->
 	assert (args=[]);
 	let st =
 	  str "`" ++
@@ -95,9 +93,12 @@ let rec pp_expr env args =
 		 (if args' = [] then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
-	if info.c_kind = Coinductive then paren (str "delay " ++ st) else st
+	if is_coinductive r then paren (str "delay " ++ st) else st
+    | MLtuple _ -> error "Cannot handle tuples in Scheme yet."
+    | MLcase (_,_,pv) when not (is_regular_match pv) ->
+	error "Cannot handle general patterns in Scheme yet."
     | MLcase (_,t,pv) when is_custom_match pv ->
-	let mkfun (_,ids,e) =
+	let mkfun (ids,_,e) =
 	  if ids <> [] then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
@@ -107,9 +108,9 @@ let rec pp_expr env args =
 		(str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
 		 ++ pp_expr env [] t)))
-     | MLcase (info,t, pv) ->
-	let e =
-	  if info.m_kind <> Coinductive then pp_expr env [] t
+    | MLcase (typ,t, pv) ->
+        let e =
+	  if not (is_coinductive_type typ) then pp_expr env [] t
 	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
 	in
 	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
@@ -126,14 +127,18 @@ let rec pp_expr env args =
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
 
 and pp_cons_args env = function
-  | MLcons (info,r,args) when info.c_kind<>Coinductive ->
+  | MLcons (_,r,args) when is_coinductive r ->
       paren (pp_global Cons r ++
 	     (if args = [] then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
 
-
-and pp_one_pat env (r,ids,t) =
+and pp_one_pat env (ids,p,t) =
+  let r = match p with
+    | Pusual r -> r
+    | Pcons (r,l) -> r (* cf. the check [is_regular_match] above *)
+    | _ -> assert false
+  in
   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
   let args =
     if ids = [] then mt ()
-- 
cgit v1.2.3