mise en place commandes minicoq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@42 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 46 insertions, 5 deletions

diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 79be85fadc..8dee09d697 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -1,8 +1,14 @@
 
 (* $Id$ *)
 
+open Pp
+open Util
 open Names
 open Generic
+open Constant
+open Inductive
+open Typing
+open G_minicoq
 
 let lookup_var id =
   let rec look n = function
@@ -22,19 +28,54 @@ let rec globalize bv = function
   | DLAMV (na,v) -> DLAMV (na, Array.map (globalize (na::bv)) v)
   | Rel _ | DOP0 _ as c -> c
 
+let (env : unit environment ref) = ref empty_environment
+
+let check c = 
+  let c = globalize [] c in
+  let (j,u) = safe_machine !env c in
+  mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 (pr_term (j_type j)); 'fNL >])
+
+let definition id ty c =
+  let c = globalize [] c in
+  let ty = option_app (globalize []) ty in
+  let ce = { const_entry_body = c; const_entry_type = ty } in
+  let sp = make_path [] id CCI in
+  env := add_constant sp ce !env;
+  mSGNL (hOV 0 [< print_id id; 'sPC; 'sTR"is defined"; 'fNL >])
+
+let parameter id t =
+  let t = globalize [] t in
+  let sp = make_path [] id CCI in
+  env := add_parameter sp t !env;
+  mSGNL (hOV 0 [< 'sTR"parameter"; 'sPC; print_id id; 
+		  'sPC; 'sTR"is declared"; 'fNL >])
+
+let variable id t =
+  let t = globalize [] t in
+  env := push_var (id,t) !env;
+  mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 
+		  'sPC; 'sTR"is declared"; 'fNL >])
+
+let execute = function
+  | Check c -> check c
+  | Definition (id, ty, c) -> definition id ty c
+  | Parameter (id, t) -> parameter id t
+  | Variable (id, t) -> variable id t
+  | _ -> Printf.printf "not yet implemented\n"; flush stdout
+
 let main () =
   let cs = Stream.of_channel stdin in
   while true do
     try
-      let c = Grammar.Entry.parse G_minicoq.command cs in
-      Printf.printf "ok\n"; flush stdout
+      let c = Grammar.Entry.parse command cs in
+      execute c
     with 
       | End_of_file | Stdpp.Exc_located (_, End_of_file) -> 
 	  exit 0
-      | Stdpp.Exc_located (_,e) ->
-	  Printf.printf "error: %s\n" (Printexc.to_string e); flush stdout
+      | Stdpp.Exc_located (_,exn) ->
+	  mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >]
       | exn -> 
-	  Printf.printf "error: %s\n" (Printexc.to_string exn); flush stdout
+	  mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >]
   done
 
 let _ = Printexc.catch main ()