diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-28 16:10:46 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-28 16:10:46 +0000 |
commit | 4f523e7d25ed22b6e41cabf1c2bd091afc0fde7f (patch) | |
tree | 641577f5554c30485dbd0ce076002f890fbe0ef3 /plugins/extraction/modutil.ml | |
parent | 98279dced2c1e01c89d3c79cb2a9f03e5dcd82e1 (diff) |
Extraction: Richer patterns in matchs as proposed by P.N. Tollitte
The MLcase has notably changed:
- No more case_info in it, but only a type annotation
- No more "one branch for one constructor", but rather a sequence
of patterns. Earlier "full" pattern correspond to pattern Pusual.
Patterns Pwild and Prel allow to encode optimized matchs without
hacks as earlier. Other pattern situations aren't used (yet)
by extraction, but only by P.N Tollitte's code.
A MLtuple constructor has been introduced. It isn't used by
the extraction for the moment, but only but P.N. Tollitte's code.
Many pretty-print functions in ocaml.ml and other have been reorganized
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/modutil.ml')
-rw-r--r-- | plugins/extraction/modutil.ml | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index a548c7866..9e8dd8286 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -77,18 +77,26 @@ let type_iter_references do_type t = | _ -> () in iter t +let patt_iter_references do_cons p = + let rec iter = function + | Pcons (r,l) -> do_cons r; List.iter iter l + | Pusual r -> do_cons r + | Ptuple l -> List.iter iter l + | Prel _ | Pwild -> () + in iter p + let ast_iter_references do_term do_cons do_type a = let rec iter a = ast_iter iter a; match a with | MLglob r -> do_term r - | MLcons (i,r,_) -> - if lang () = Ocaml then record_iter_references do_term i.c_kind; - do_cons r - | MLcase (i,_,v) -> - if lang () = Ocaml then record_iter_references do_term i.m_kind; - Array.iter (fun (r,_,_) -> do_cons r) v - | _ -> () + | MLcons (_,r,_) -> do_cons r + | MLcase (ty,_,v) -> + type_iter_references do_type ty; + Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v + + | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ + | MLdummy | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = |