diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-21 11:31:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-21 11:31:57 +0000 |
| commit | e3696e15775c44990018d1d4aea01c9bf662cd73 (patch) | |
| tree | 6f14fb168ffe95ef0dd25984a99e0678f53bd89e /plugins/extraction/scheme.ml | |
| parent | b1ae368ec3228f7340076ba0d3bc465f79ed44fa (diff) | |
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/scheme.ml')
| -rw-r--r-- | plugins/extraction/scheme.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index eb7562609..77c8e944e 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -85,7 +85,7 @@ let rec pp_expr env args = ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> apply (pp_global Term r) - | MLcons (i,r,args') -> + | MLcons (info,r,args') -> assert (args=[]); let st = str "`" ++ @@ -93,7 +93,7 @@ let rec pp_expr env args = (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in - if i = Coinductive then paren (str "delay " ++ st) else st + if info.c_kind = Coinductive then paren (str "delay " ++ st) else st | MLcase (_,t,pv) when is_custom_match pv -> let mkfun (_,ids,e) = if ids <> [] then named_lams (List.rev ids) e @@ -102,9 +102,9 @@ let rec pp_expr env args = hov 2 (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv ++ pp_expr env [] t) - | MLcase ((i,_),t, pv) -> + | MLcase (info,t, pv) -> let e = - if i <> Coinductive then pp_expr env [] t + if info.m_kind <> Coinductive 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))) @@ -121,7 +121,7 @@ let rec pp_expr env args = | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") and pp_cons_args env = function - | MLcons (i,r,args) when i<>Coinductive -> + | MLcons (info,r,args) when info.c_kind<>Coinductive -> paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) |