mise en place commandes minicoq

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

13 files changed, 192 insertions, 58 deletions

diff --git a/.depend b/.depend
index dca30597ab..3f98e2e092 100644
--- a/.depend
+++ b/.depend
@@ -32,7 +32,7 @@ lib/util.cmi: lib/pp.cmi
 library/libobject.cmi: kernel/names.cmi 
 library/summary.cmi: kernel/names.cmi 
 parsing/g_minicoq.cmi: /usr/local/lib/camlp4/grammar.cmi kernel/names.cmi \
-    kernel/term.cmi 
+    lib/pp.cmi kernel/term.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
@@ -149,11 +149,13 @@ library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
-toplevel/minicoq.cmo: parsing/g_minicoq.cmi kernel/generic.cmi \
-    /usr/local/lib/camlp4/grammar.cmi kernel/names.cmi \
-    /usr/local/lib/camlp4/stdpp.cmi 
-toplevel/minicoq.cmx: parsing/g_minicoq.cmi kernel/generic.cmx \
-    /usr/local/lib/camlp4/grammar.cmi kernel/names.cmx \
-    /usr/local/lib/camlp4/stdpp.cmi 
+toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
+    kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi kernel/inductive.cmi \
+    kernel/names.cmi lib/pp.cmi /usr/local/lib/camlp4/stdpp.cmi \
+    kernel/typing.cmi lib/util.cmi 
+toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
+    kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi kernel/inductive.cmx \
+    kernel/names.cmx lib/pp.cmx /usr/local/lib/camlp4/stdpp.cmi \
+    kernel/typing.cmx lib/util.cmx 
 parsing/g_minicoq.cmo: parsing/g_minicoq.cmi 
 parsing/g_minicoq.cmx: parsing/g_minicoq.cmi 
diff --git a/kernel/constant.ml b/kernel/constant.ml
index 9699d68a75..ba932b7885 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -18,7 +18,7 @@ type recipe =
 
 type constant_entry = {
   const_entry_body : constr;
-  const_entry_type : constr }
+  const_entry_type : constr option }
 
 type constant_body = {
   const_kind : path_kind;
diff --git a/kernel/constant.mli b/kernel/constant.mli
index bc3d1a4e3d..d8aeb7670e 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -17,7 +17,7 @@ type recipe =
 
 type constant_entry = {
   const_entry_body : constr;
-  const_entry_type : constr }
+  const_entry_type : constr option }
 
 type constant_body = {
   const_kind : path_kind;
diff --git a/kernel/term.ml b/kernel/term.ml
index a166250234..3871f6ce17 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -150,8 +150,10 @@ let mkMutInd sp i l = (DOPN (MutInd (sp,i), l))
 let mkMutConstruct sp i j l =  (DOPN ((MutConstruct ((sp,i),j),l))) 
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkMutCase ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] (Array.of_list ac))
-let mkMutCaseA ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] ac)
+let mkMutCase ci p c ac = 
+  DOPN (MutCase ci, Array.append [|p;c|] (Array.of_list ac))
+let mkMutCaseA ci p c ac = 
+  DOPN (MutCase ci, Array.append [|p;c|] ac)
 
 (* If recindxs = [|i1,...in|] 
       typarray = [|t1,...tn|]
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7e81618654..325d9fff37 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -32,6 +32,7 @@ let typed_type_of_judgment env j =
     | DOP0(Sort s) -> { body = j.uj_val; typ = s }
     | _ -> error_not_type CCI env j.uj_val
 
+(* same function, but with a different error message *)
 let assumption_of_judgement env j =
   match whd_betadeltaiota env j.uj_type with
     | DOP0(Sort s) -> { body = j.uj_val; typ = s }
diff --git a/kernel/typing.ml b/kernel/typing.ml
index e69c846658..13a809b034 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -18,22 +18,9 @@ open Indtypes
 
 type judgment = unsafe_judgment
 
-(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
-
-let tjudge_of_cast env = function
-  | DOP2 (Cast, b, t) ->
-      (match whd_betadeltaiota env t with
-	 | DOP0 (Sort s) -> {body=b; typ=s}
-	 | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]"
-	 | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]")
-  | _ -> anomaly "Not casted (tjudge_of_cast)"
-	
-let tjudge_of_judge env j =
-  { body = j.uj_val;
-    typ = match whd_betadeltaiota env j.uj_type with
-      (* Nécessaire pour ZFC *)
-      | DOP0 (Sort s) -> s
-      | _ -> anomaly "Not a type (tjudge_ofjudge)" }
+let j_val j = j.uj_val
+let j_type j = j.uj_type
+let j_kind j = j.uj_kind
 
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
@@ -293,20 +280,28 @@ let push_rels vars env =
 let add_constant sp ce env =
   let (jb,u) = safe_machine env ce.const_entry_body in
   let env' = set_universes u env in
-  let (jt,u') = safe_machine env ce.const_entry_type in
-  let env'' = set_universes u' env' in
-  match conv env'' jb.uj_type jt.uj_val with
-    | Convertible u'' -> 
-	let cb = { 
-	  const_kind = kind_of_path sp;
-	  const_body = Some (ref (Cooked ce.const_entry_body));
-	  const_type = typed_type_of_judgment env'' jt;
-	  const_hyps = get_globals (context env);
-	  const_opaque = false } 
-	in
-	add_constant sp cb (set_universes u'' env'')
-    | NotConvertible -> 
-	error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+  let (env'',ty) = 
+    match ce.const_entry_type with
+      | None -> 
+	  env', typed_type_of_judgment env' jb
+      | Some ty -> 
+	  let (jt,u') = safe_machine env ty in
+	  let env'' = set_universes u' env' in
+	  match conv env'' jb.uj_type jt.uj_val with
+	    | Convertible u'' -> 
+		let env'' = set_universes u'' env' in
+		env'', typed_type_of_judgment env'' jt
+	    | NotConvertible -> 
+		error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+  in
+  let cb = { 
+    const_kind = kind_of_path sp;
+    const_body = Some (ref (Cooked ce.const_entry_body));
+    const_type = ty;
+    const_hyps = get_globals (context env);
+    const_opaque = false } 
+  in
+  add_constant sp cb env''
 
 let type_from_judgment env j =
   match whd_betadeltaiota env j.uj_kind with
diff --git a/kernel/typing.mli b/kernel/typing.mli
index ec3ca5d7d9..d9d410c542 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -45,6 +45,10 @@ val lookup_meta : int -> 'a environment -> constr
 
 type judgment
 
+val j_val : judgment -> constr
+val j_type : judgment -> constr
+val j_kind : judgment -> constr
+
 val safe_machine : 'a environment -> constr -> judgment * universes
 val safe_machine_type : 'a environment -> constr -> typed_type
 
diff --git a/lib/util.ml b/lib/util.ml
index fb50d1e4e5..deb810cdd1 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -259,6 +259,12 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset = Set.Make(struct type t = int let compare = compare end)
 
+let option_app f = function
+  | None -> None
+  | Some x -> Some (f x)
+
+(* Time stamps. *)
+
 type time_stamp = float
 
 let get_time_stamp () = Unix.time()
diff --git a/lib/util.mli b/lib/util.mli
index 98296264f9..0ef34a8418 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,6 +72,10 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
+val option_app : ('a -> 'b) -> 'a option -> 'b option
+
+(*s Time stamps. *)
+
 type time_stamp
 
 val get_time_stamp : unit -> time_stamp
diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
index 4f8e145719..9cd01fdd0d 100644
--- a/parsing/g_minicoq.g4
+++ b/parsing/g_minicoq.g4
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Names
 open Univ
 open Generic
@@ -25,6 +26,7 @@ type command =
 let gram = Grammar.create lexer
 
 let term = Grammar.Entry.create gram "term"
+let name = Grammar.Entry.create gram "name"
 let command = Grammar.Entry.create gram "command"
 
 let new_univ =
@@ -35,9 +37,15 @@ let new_univ =
 let path_of_string s = make_path [] (id_of_string s) CCI
 
 EXTEND
+  name: [ 
+    [ id = IDENT -> Name (id_of_string id)
+    | "_" -> Anonymous
+  ] ];
   term: [ 
     [ id = IDENT -> 
 	VAR (id_of_string id) 
+    | IDENT "Rel"; n = INT ->
+	Rel (int_of_string n)
     | "Set" ->
 	DOP0 (Sort (Prop Pos))
     | "Prop" ->
@@ -52,10 +60,23 @@ EXTEND
     | IDENT "Construct"; id = IDENT; n = INT; i = INT ->
 	let n = int_of_string n and i = int_of_string i in
 	DOPN (MutConstruct ((path_of_string id, n), i), [||])
-    | "["; id = IDENT; ":"; t = term; "]"; c = term ->
-	DOP2 (Lambda, t, DLAM (Name (id_of_string id), c))
-    | "("; id = IDENT; ":"; t = term; ")"; c = term ->
-	DOP2 (Prod, t, DLAM (Name (id_of_string id), c))
+    | "["; na = name; ":"; t = term; "]"; c = term ->
+	DOP2 (Lambda, t, DLAM (na, c))
+    | "("; na = name; ":"; t = term; ")"; c = term ->
+	DOP2 (Prod, t, DLAM (na, c))
+    | "("; id = IDENT; cl = LIST1 term; ")" ->
+	let c = VAR (id_of_string id) in
+	DOPN (AppL, Array.of_list (c::cl))
+    | "("; cl = LIST1 term; ")" ->
+	begin match cl with
+	  | [c] -> c
+	  | _ -> DOPN (AppL, Array.of_list cl)
+	end
+    | "("; c = term; "::"; t = term; ")" ->
+	DOP2 (Cast, c, t)
+    | "<"; p = term; ">"; IDENT "Case"; c = term; "of"; 
+      bl = LIST0 term; "end" ->
+	DOPN (MutCase None, Array.of_list (p :: c :: bl))
   ] ];
   command: [ 
     [ "Definition"; id = IDENT; ":="; c = term; "." ->
@@ -72,3 +93,59 @@ EXTEND
   ] ];
 END
 
+(* Pretty-print. *)
+
+let print_univers = ref false
+let print_casts = ref false
+
+let print_type u =
+  let sp = u.u_sp and num = u.u_num in
+  [< 'sTR "Type";
+     if !print_univers then 
+       [< 'sTR "("; print_id (basename sp); 'sPC; 'iNT num >] 
+     else 
+       [< >] 
+  >]
+  
+let print_name = function
+  | Anonymous -> [< 'sTR "_" >]
+  | Name id -> print_id id
+
+let print_rel bv n = print_name (List.nth bv (pred n))
+
+let rename bv = function
+  | Anonymous -> Anonymous
+  | Name id as na -> 
+      let idl = 
+	List.fold_left 
+	  (fun l n -> match n with Name x -> x::l | _ -> l) [] bv 
+      in
+      if List.mem na bv then Name (next_ident_away id idl) else na
+
+let rec pp bv = function
+  | DOP0 (Sort (Prop Pos)) -> [< 'sTR "Set" >]
+  | DOP0 (Sort (Prop Null)) -> [< 'sTR "Prop" >]
+  | DOP0 (Sort (Type u)) -> print_type u
+  | DOP2 (Lambda, t, DLAM(na, c)) ->
+      [< 'sTR"["; print_name na; 'sTR":"; pp bv t; 'sTR"]"; pp (na::bv) c >]
+  | DOP2 (Prod, t, DLAM(na, c)) ->
+      [< 'sTR"("; print_name na; 'sTR":"; pp bv t; 'sTR")"; pp (na::bv) c >]
+  | DOP2 (Cast, c, t) ->
+      if !print_casts then 
+	[< 'sTR"("; pp bv c; 'sTR"::"; pp bv t; 'sTR")" >]
+      else
+	pp bv c
+  | DOPN (AppL, cv) ->
+      [< >]
+  | DOPN (Const sp, _) ->
+      [< 'sTR"Const "; print_id (basename sp) >]
+  | DOPN (MutInd (sp,i), _) ->
+      [< 'sTR"Ind "; print_id (basename sp); 'sTR" "; 'iNT i >]
+  | DOPN (MutConstruct ((sp,i),j), _) ->
+      [< 'sTR"Construct "; print_id (basename sp); 'sTR" "; 'iNT i; 
+	 'sTR" "; 'iNT j >]
+  | VAR id -> print_id id
+  | Rel n -> print_rel bv n
+  | _ -> [< 'sTR"<???>" >]
+
+let pr_term = pp []
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index ef47c4f894..77dbb5c712 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -1,4 +1,5 @@
 
+open Pp
 open Names
 open Term
 
@@ -15,3 +16,4 @@ type command =
 
 val command : command Grammar.Entry.e
 
+val pr_term : constr -> std_ppcmds
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 08ec04091b..181c50a77c 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -63,7 +63,7 @@ let firstchar =
 let identchar = 
   ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let symbolchar =
-  ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~']
+  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' '=' '?' '@' '^' '|' '~']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
 let oct_literal = '0' ['o' 'O'] ['0'-'7']+
@@ -77,13 +77,13 @@ rule token = parse
 	if is_keyword s then ("",s) else ("IDENT",s) }
   | decimal_literal | hex_literal | oct_literal | bin_literal
       { ("INT", Lexing.lexeme lexbuf) }
-  | ":=" { ("COLONEQUAL","") }
-  | ":"  { ("COLON","") }
-  | "."  { ("DOT","") }
+  | "(" | ")" | "[" | "]" | "{" | "}" | "<" | ">" | "." | "_" 
+      { ("", Lexing.lexeme lexbuf) }
   | symbolchar+
-      { ("SPECIAL", Lexing.lexeme lexbuf) }
+      { ("", Lexing.lexeme lexbuf) }
   | '`' [^'`']* '`'
-      { ("QUOTED", Lexing.lexeme lexbuf) }
+      { let s = Lexing.lexeme lexbuf in
+	("QUOTED", String.sub s 1 (String.length s - 2)) }
   | "\""
       { Buffer.reset string_buffer;
         let string_start = Lexing.lexeme_start lexbuf in
@@ -99,7 +99,7 @@ rule token = parse
       { ("EOI","") }
 
 and comment = parse
-    "(*"
+  | "(*"
       { comment_depth := succ !comment_depth; comment lexbuf }
   | "*)"
       { comment_depth := pred !comment_depth;
@@ -124,7 +124,7 @@ and comment = parse
       { comment lexbuf }
 
 and string = parse
-    '"'
+  | '"'
       { () }
   | '\\' ("\010" | "\013" | "\013\010") [' ' '\009'] *
       { string lexbuf }
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 ()