diff options
Diffstat (limited to 'plugins/extraction/scheme.ml')
| -rw-r--r-- | plugins/extraction/scheme.ml | 29 |
1 files changed, 17 insertions, 12 deletions
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 () |