diff options
| author | filliatr | 1999-09-06 15:14:57 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-06 15:14:57 +0000 |
| commit | 136cb0538a61792ed8caca9969c8052cc9b42071 (patch) | |
| tree | eb2abfbc1f5dc86fb70efd0f80f6615e49b5cdc9 | |
| parent | eec1ca7cdb14eadb6b6f671fe993e0a8b9489758 (diff) | |
un mini toplevel pour tester le noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@38 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/minicoq.ml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml new file mode 100644 index 0000000000..e4b1496a3a --- /dev/null +++ b/toplevel/minicoq.ml @@ -0,0 +1,26 @@ + +(* $Id$ *) + +open Names +open Generic + +let lookup_var id = + let rec look n = function + | [] -> VAR id + | (Name id')::_ when id = id' -> Rel n + | _::r -> look (succ n) r + in + look 1 + +let rec globalize bv = function + | VAR id -> lookup_var id bv + | DOP1 (op,c) -> DOP1 (op, globalize bv c) + | DOP2 (op,c1,c2) -> DOP2 (op, globalize bv c1, globalize bv c2) + | DOPN (op,v) -> DOPN (op, Array.map (globalize bv) v) + | DOPL (op,l) -> DOPL (op, List.map (globalize bv) l) + | DLAM (na,c) -> DLAM (na, globalize (na::bv) c) + | DLAMV (na,v) -> DLAMV (na, Array.map (globalize (na::bv)) v) + | Rel _ | DOP0 _ as c -> c + +let main () = + failwith "todo" |