- minicoq : definition inductifs; syntaxe a->b

 - kernel : bug Typing/one_inductive (il fallait chercher l'arite typée dans
     l'environnement avec lookup_rel et non lookup_var)


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

6 files changed, 96 insertions, 33 deletions

diff --git a/.depend b/.depend
index 3f98e2e09..1d9de53a7 100644
--- a/.depend
+++ b/.depend
@@ -152,10 +152,10 @@ parsing/lexer.cmx: lib/util.cmx parsing/lexer.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 
+    kernel/term.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 
+    kernel/term.cmx 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/typeops.ml b/kernel/typeops.ml
index 325d9fff3..afc79925f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -28,12 +28,11 @@ let j_val = j_val_only
 let j_val_cast j = mkCast j.uj_val j.uj_type
 
 let typed_type_of_judgment env j =
-  match whd_betadeltaiota env j.uj_type with
-    | DOP0(Sort s) -> { body = j.uj_val; typ = s }
-    | _ -> error_not_type CCI env j.uj_val
+  match whd_betadeltaiota env j.uj_kind with
+    | DOP0(Sort s) -> { body = j.uj_type; typ = s }
+    | _ -> error_not_type CCI env j.uj_type
 
-(* same function, but with a different error message *)
-let assumption_of_judgement env j =
+let assumption_of_judgment env j =
   match whd_betadeltaiota env j.uj_type with
     | DOP0(Sort s) -> { body = j.uj_val; typ = s }
     | _ -> error_assumption CCI env j.uj_val
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 5ddb8031e..b02e37b1d 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -15,8 +15,12 @@ val make_judge : constr -> typed_type -> unsafe_judgment
 
 val j_val_only : unsafe_judgment -> constr
 
+(* If [j] is the judgement $c:t:s$, then [typed_type_of_judgment env j]
+   constructs the typed type $t:s$, while [assumption_of_judgement env j]
+   cosntructs the type type $c:t$, checking that $t$ is a sort. *)
+
 val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
-val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type
+val assumption_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
 
 val relative : 'a unsafe_env -> int -> unsafe_judgment
 
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 13a809b03..03c160e1b 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -117,7 +117,7 @@ let rec execute mf env cstr =
 	    
     | IsLambda (name,c1,c2) -> 
         let (j,u1) = execute mf env c1 in
-        let var = assumption_of_judgement env j in
+        let var = assumption_of_judgment env j in
 	let env1 = push_rel (name,var) (set_universes u1 env) in
         let (j',u2) = execute mf env1 c2 in 
 	let env2 = set_universes u2 env1 in
@@ -125,7 +125,7 @@ let rec execute mf env cstr =
 	  
     | IsProd (name,c1,c2) ->
         let (j,u1) = execute mf env c1 in
-        let var = assumption_of_judgement env j in
+        let var = assumption_of_judgment env j in
 	let env1 = push_rel (name,var) (set_universes u1 env) in
         let (j',u2) = execute mf env1 c2 in
 	let env2 = set_universes u2 env1 in
@@ -143,7 +143,7 @@ let rec execute mf env cstr =
 and execute_fix mf env lar lfi vdef =
   let (larj,u1) = execute_array mf env lar in
   let env1 = set_universes u1 env in
-  let lara = Array.map (assumption_of_judgement env1) larj in
+  let lara = Array.map (assumption_of_judgment env1) larj in
   let nlara = 
     List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
   let env2 = 
@@ -170,7 +170,7 @@ and execute_list mf env = function
 
 let execute_type mf env constr = 
   let (j,_) = execute mf env constr in
-  typed_type_of_judgment env j
+  assumption_of_judgment env j
 
 
 (* Exported machines.  First safe machines, with no general fixpoint
@@ -262,7 +262,7 @@ let lookup_meta = lookup_meta
 let push_rel_or_var push (id,c) env =
   let (j,u) = safe_machine env c in
   let env' = set_universes u env in
-  let var = assumption_of_judgement env' j in
+  let var = assumption_of_judgment env' j in
   push (id,var) env'
 
 let push_var nvar env = push_rel_or_var push_var nvar env
@@ -290,7 +290,7 @@ let add_constant sp ce env =
 	  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
+		env'', assumption_of_judgment env'' jt
 	    | NotConvertible -> 
 		error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
@@ -335,7 +335,7 @@ let rec for_all_prods p env c =
 	 for_all_prods p env' c)
     | DOP2(Prod, b, DLAM(name,c)) -> 
 	let (jb,u) = unsafe_machine env b in
-	let var = assumption_of_judgement env jb in
+	let var = assumption_of_judgment env jb in
 	(p var) &&
 	(let env' = Environ.push_rel (name,var) (set_universes u env) in
 	 for_all_prods p env' c)
@@ -378,7 +378,7 @@ let is_unit env_par nparams ar spec =
 	(let (_,c') = decompose_prod_n nparams c in logic_constr env_par c')
     | _ -> false
 
-let type_one_inductive env_ar env_par nparams (id,ar,cnames,spec) =
+let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
   let (lna,vc) = decomp_all_DLAMV_name spec in
   let (env',(issmall,jlc)) = 
     List.fold_left 
@@ -390,7 +390,7 @@ let type_one_inductive env_ar env_par nparams (id,ar,cnames,spec) =
   let castlc = List.map cast_of_judgment jlc in
   let spec' = put_DLAMSV lna (Array.of_list castlc) in
   let isunit = is_unit env_par nparams ar spec in
-  let (_,tyar) = lookup_var id env' in
+  let (_,tyar) = lookup_rel (ninds+1-i) env' in
   (env', (id,tyar,cnames,issmall,isunit,spec'))
 
 let add_mind sp mie env =
@@ -399,17 +399,20 @@ let add_mind sp mie env =
   let params = mind_extract_and_check_params mie in
   let nparams = mie.mind_entry_nparams in
   mind_check_lc params mie;
+  let ninds = List.length mie.mind_entry_inds in
   let types_sign = 
     List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
   in
   let env_arities = push_rels types_sign env in
   let env_params = push_rels params env_arities in
-  let env_arities',inds =
+  let env_arities',_,inds =
     List.fold_left 
-      (fun (env,inds) ind -> 
-	 let (env',ind') = type_one_inductive env env_params nparams ind in
-	 (env',ind'::inds))
-      (env_arities,[]) mie.mind_entry_inds
+      (fun (env,i,inds) ind -> 
+	 let (env',ind') = 
+	   type_one_inductive i env env_params nparams ninds ind 
+	 in
+	 (env',succ i,ind'::inds))
+      (env_arities,1,[]) mie.mind_entry_inds
   in
   let kind = kind_of_path sp in
   let mib = 
diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
index 9cd01fdd0..ccf22ce44 100644
--- a/parsing/g_minicoq.g4
+++ b/parsing/g_minicoq.g4
@@ -27,6 +27,9 @@ let gram = Grammar.create lexer
 
 let term = Grammar.Entry.create gram "term"
 let name = Grammar.Entry.create gram "name"
+let nametype = Grammar.Entry.create gram "nametype"
+let inductive = Grammar.Entry.create gram "inductive"
+let constructor = Grammar.Entry.create gram "constructor"
 let command = Grammar.Entry.create gram "command"
 
 let new_univ =
@@ -37,12 +40,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)
+  name: 
+  [ [ id = IDENT -> Name (id_of_string id)
     | "_" -> Anonymous
   ] ];
-  term: [ 
-    [ id = IDENT -> 
+  nametype: 
+  [ [ id = IDENT; ":"; t = term -> (id_of_string id, t) 
+  ] ];
+  term: 
+  [ [ id = IDENT -> 
 	VAR (id_of_string id) 
     | IDENT "Rel"; n = INT ->
 	Rel (int_of_string n)
@@ -64,6 +70,8 @@ EXTEND
 	DOP2 (Lambda, t, DLAM (na, c))
     | "("; na = name; ":"; t = term; ")"; c = term ->
 	DOP2 (Prod, t, DLAM (na, c))
+    | c1 = term; "->"; c2 = term ->
+	DOP2 (Prod, c1, DLAM (Anonymous, c2))
     | "("; id = IDENT; cl = LIST1 term; ")" ->
 	let c = VAR (id_of_string id) in
 	DOPN (AppL, Array.of_list (c::cl))
@@ -78,8 +86,8 @@ EXTEND
       bl = LIST0 term; "end" ->
 	DOPN (MutCase None, Array.of_list (p :: c :: bl))
   ] ];
-  command: [ 
-    [ "Definition"; id = IDENT; ":="; c = term; "." ->
+  command: 
+  [ [ "Definition"; id = IDENT; ":="; c = term; "." ->
 	Definition (id_of_string id, None, c)
     | "Definition"; id = IDENT; ":"; t = term; ":="; c = term; "." ->
 	Definition (id_of_string id, Some t, c)
@@ -87,10 +95,19 @@ EXTEND
 	Parameter (id_of_string id, t)
     | "Variable"; id = IDENT; ":"; t = term; "." ->
 	Variable (id_of_string id, t)
+    | "Inductive"; "["; params = LIST0 nametype SEP ";"; "]"; 
+      inds = LIST1 inductive SEP "with" ->
+	Inductive (params, inds)
     | IDENT "Check"; c = term; "." ->
 	Check c
     | EOI -> raise End_of_file
   ] ];
+  inductive: 
+  [ [ id = IDENT; ":"; ar = term; ":="; constrs = LIST0 constructor SEP "|" ->
+        (id_of_string id,ar,constrs)
+  ] ];
+  constructor:
+  [ [ id = IDENT; ":"; c = term -> (id_of_string id,c) ] ];
 END
 
 (* Pretty-print. *)
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 8dee09d69..6eb89dab6 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -5,6 +5,7 @@ open Pp
 open Util
 open Names
 open Generic
+open Term
 open Constant
 open Inductive
 open Typing
@@ -56,19 +57,52 @@ let variable id t =
   mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 
 		  'sPC; 'sTR"is declared"; 'fNL >])
 
+let inductive par inds =
+  let nparams = List.length par in
+  let bvpar = List.rev (List.map (fun (id,_) -> Name id) par) in
+  let name_inds = List.map (fun (id,_,_) -> Name id) inds in
+  let bv = bvpar @  List.rev name_inds in
+  let par = List.map (fun (id,c) -> (Name id, globalize [] c)) par in
+  let one_inductive (id,ar,cl) =
+    let cv = Array.of_list (List.map snd cl) in
+    let cv = Array.map (fun c -> prod_it (globalize bv c) par) cv in
+    let c = put_DLAMSV name_inds cv in
+    (id, prod_it (globalize bvpar ar) par, List.map fst cl, c)
+  in
+  let inds = List.map one_inductive inds in
+  let mie = { 
+    mind_entry_nparams = nparams;
+    mind_entry_finite = true;
+    mind_entry_inds = inds }
+  in
+  let sp = let (id,_,_,_) = List.hd inds in make_path [] id CCI in
+  env := add_mind sp mie !env;
+  mSGNL (hOV 0 [< 'sTR"inductive type(s) are 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
+  | Inductive (par,inds) -> inductive par inds
 
-let main () =
+let parse_file f =
+  let c = open_in f in
+  let cs = Stream.of_channel c in
+  try
+    while true do
+      let c = Grammar.Entry.parse command cs in execute c
+    done
+  with 
+    | End_of_file | Stdpp.Exc_located (_, End_of_file) -> close_in c; exit 0
+    | exn -> close_in c; raise exn
+      
+let top () =
   let cs = Stream.of_channel stdin in
   while true do
     try
-      let c = Grammar.Entry.parse command cs in
-      execute c
+      let c = Grammar.Entry.parse command cs in execute c
     with 
       | End_of_file | Stdpp.Exc_located (_, End_of_file) -> 
 	  exit 0
@@ -78,5 +112,11 @@ let main () =
 	  mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >]
   done
 
-let _ = Printexc.catch main ()
+let main () =
+  if Array.length Sys.argv = 1 then
+    parse_file "test"
+  else
+    if Sys.argv.(1) = "-top" then top () else parse_file (Sys.argv.(1))
+
+let _ = Printexc.print main ()