From 136cb0538a61792ed8caca9969c8052cc9b42071 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Sep 1999 15:14:57 +0000
Subject: 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
---
 toplevel/minicoq.ml | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 toplevel/minicoq.ml

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"
-- 
cgit v1.2.3