Possibilité de syntaxe conjointement à la définition des inductifs et des points-fixes; prise en compte par le traducteur

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

5 files changed, 120 insertions, 94 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d9418f58f6..11b697165c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -219,7 +219,7 @@ let interp_mutual lparams lnamearconstrs finite =
       option_app (fun df ->
         let larnames =
 	  List.rev_append lparnames 
-	    (List.map fst (fst (decompose_prod ar))) in
+	    (List.rev (List.map fst (fst (decompose_prod ar)))) in
 	(recname,larnames,df)) ntnopt)
       lnamearconstrs arityl in
   let fs = States.freeze() in
@@ -227,7 +227,7 @@ let interp_mutual lparams lnamearconstrs finite =
   try
   List.iter (option_iter (fun (recname,larnames,(df,scope)) ->
     Metasyntax.add_notation_interpretation df
-      (AVar recname,larnames) scope)) notations;
+      (AVar recname,larnames) (* no scope for tmp ntn *) scope)) notations;
   let ind_env_params = push_rel_context params ind_env in
   let mispecvec = 
     List.map2
@@ -332,33 +332,49 @@ let collect_non_rec env =
   searchrec [] 
 
 let build_recursive lnameargsardef =
-  let lrecnames = List.map (fun (f,_,_,_) -> f) lnameargsardef 
+  let lrecnames = List.map (fun ((f,_,_,_),_) -> f) lnameargsardef 
   and sigma = Evd.empty
   and env0 = Global.env()
-  and nv = Array.of_list (List.map (fun (_,n,_,_) -> n) lnameargsardef) in
+  and nv = Array.of_list (List.map (fun ((_,n,_,_),_) -> n) lnameargsardef) in
   let fs = States.freeze() in
+  (* Declare the notations for the inductive types pushed in local context*)
   let (rec_sign,arityl) = 
-    try 
-      List.fold_left 
-        (fun (env,arl) (recname,_,arityc,_) -> 
-           let arity = interp_type sigma env0 arityc in
-           let _ = declare_variable recname
-	     (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
-           (Environ.push_named (recname,None,arity) env, (arity::arl)))
-        (env0,[]) lnameargsardef
-    with e ->
-      States.unfreeze fs; raise e in
+    List.fold_left 
+      (fun (env,arl) ((recname,_,arityc,_),_) -> 
+        let arity = interp_type sigma env0 arityc in
+        (Environ.push_named (recname,None,arity) env, (arity::arl)))
+      (env0,[]) lnameargsardef in
   let arityl = List.rev arityl in
+  let notations = 
+    List.map2 (fun ((recname,_,_,_),ntnopt) arityl ->
+      option_app (fun ntn ->
+        let larnames = List.map fst (fst (decompose_prod arityl)) in
+	(recname,List.rev larnames,ntn)) ntnopt)
+      lnameargsardef arityl in
+
   let recdef =
-    try 
-      List.map2
-	(fun (_,_,_,def) arity ->
-          interp_casted_constr sigma rec_sign def arity)
-        lnameargsardef arityl
-    with e ->
-      States.unfreeze fs; raise e
+
+    (* Declare local context and local notations *)
+    let fs = States.freeze() in
+    let def = 
+      try
+	List.iter (option_iter (fun (recname,larnames,(df,scope)) ->
+	  Metasyntax.add_notation_interpretation df
+	  (AVar recname,larnames) (* no scope for tmp ntn *) None)) notations;
+	List.iter2
+	  (fun recname arity -> 
+            let _ = declare_variable recname
+	      (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
+	    ()) lrecnames arityl;
+	List.map2
+	  (fun ((_,_,_,def),_) arity ->
+            interp_casted_constr sigma rec_sign def arity)
+          lnameargsardef arityl
+      with e ->
+	States.unfreeze fs; raise e in
+    States.unfreeze fs; def 
   in
-  States.unfreeze fs;
+
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in
   let recvec = 
@@ -389,7 +405,9 @@ let build_recursive lnameargsardef =
       (List.map var_subst (Array.to_list namerec))
       lnonrec 
   in
-  ()
+  List.iter (option_iter (fun (recname,names,(df,scope)) ->
+      Metasyntax.add_notation_interpretation df
+        (ARef (ConstRef (Lib.make_kn recname)),names) scope)) notations
 
 let build_corecursive lnameardef = 
   let lrecnames = List.map (fun (f,_,_) -> f) lnameardef
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 791c33d66a..4ed7a89288 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -43,7 +43,7 @@ val build_mutual : inductive_expr list -> bool -> unit
 val declare_mutual_with_eliminations :
   Entries.mutual_inductive_entry -> mutual_inductive
 
-val build_recursive : fixpoint_expr list -> unit
+val build_recursive : (fixpoint_expr * decl_notation) list -> unit
 
 val build_corecursive : cofixpoint_expr list -> unit
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1e0077373d..43785836af 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -437,35 +437,6 @@ let rec find_symbols c_current c_next c_last = function
   | Terminal s :: sl -> find_symbols c_next c_next c_last sl
   | Break n :: sl -> find_symbols c_current c_next c_last sl
 
-(*
-let rec find_symbols c_current c_next c_last = function
-  | []    -> (vars, [])
-  | String x :: sl when Lexer.is_normal_token x ->
-      Lexer.check_ident x;
-      let id = Names.id_of_string x in
-      if List.mem_assoc id vars then
-	error ("Variable "^x^" occurs more than once");
-      let prec = if sl <> [] then c_current else c_last in
-      let (vars,l) = find_symbols c_next c_next c_last sl in
-      ((id,prec)::vars, NonTerminal id :: l)
-(*
-  | "_"::sl ->
-      warning "Found '_'";
-      let prec = if List.exists is_symbols sl then c_first else c_last in
-      let (vars,l) =
-        find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in
-      let meta = create_meta new_var in
-      (vars, NonTerminal (prec, meta) :: l)
-*)
-  | String s :: sl ->
-      Lexer.check_special_token s;
-      let (vars,l) = find_symbols c_next c_next c_last sl in
-      (vars, Terminal (strip s) :: l)
-  | WhiteSpace n :: sl ->
-      let (vars,l) = find_symbols c_current c_next c_last sl in
-      (vars, Break n :: l)
-*)
-
 let make_grammar_rule n assoc typs symbols ntn =
   let prod = make_production typs symbols in
   (n,assoc,ntn,prod)
@@ -546,8 +517,7 @@ let interp_modifiers a n =
   let onlyparsing = ref false in
   let rec interp assoc level etyps = function
     | [] ->
-	let n = match level with None -> 1 | Some n -> n in
-	(assoc,n,etyps,!onlyparsing)
+	(assoc,level,etyps,!onlyparsing)
     | SetEntryType (s,typ) :: l ->
 	let id = id_of_string s in
 	if List.mem_assoc id etyps then
@@ -575,16 +545,18 @@ let interp_modifiers a n =
 
 (* Infix defaults to LEFTA (cf doc) *)
 let interp_infix_modifiers a n l =
-  let (assoc,n,t,b) = interp_modifiers a n l in
+  let (assoc,level,t,b) = interp_modifiers a n l in
   if t <> [] then
     error "explicit entry level or type unexpected in infix notation";
   let assoc = match assoc with None -> Some Gramext.LeftA | a -> a in
+  let n = match level with None -> 1 | Some n -> n in
   (assoc,n,b)
 
 (* Notation defaults to NONA *)
 let interp_notation_modifiers modl =
   let (assoc,n,t,b) = interp_modifiers None None modl in
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
+  let n = match n with None -> 1 | Some n -> n in
   (assoc,n,t,b)
 
 (* 2nd list of types has priority *)
@@ -761,54 +733,88 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,df))
 
-let add_notation local df a modifiers mv8 sc =
-  let toks = split df in
-  match toks with 
-    | [String x] when quote(strip x) = x
-	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
-        (* Means a Syntactic Definition *)
-        let ident = id_of_string (strip x) in
-	let c = snd (interp_aconstr [] a) in
-	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
-        Syntax_def.declare_syntactic_definition local ident onlyparse c
-    | _ ->
-        add_notation_in_scope local
-          df a (interp_notation_modifiers modifiers)
-          (option_app (fun (s8,ml8) ->
-            let toks8 = split s8 in 
-            let im8 = interp_notation_modifiers ml8 in
-            (toks8,im8)) mv8)
-          sc toks
-
-let check_occur l id =
-  if not (List.mem (Name id) l) then error ((string_of_id id)^"is unbound")
-
-let add_notation_interpretation df (c,l) sc =
+let add_notation_interpretation_core local vars symbs df (a,r) sc onlyparse =
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
-  let (vars,symbs) = analyse_tokens (split df) in
   let notation = make_anon_notation symbs in
   let prec = 
     try Symbols.level_of_notation notation
     with Not_found ->
       error "Parsing rule for this notation has to be previously declared" in
-  List.iter (check_occur l) vars;
   let old_pp_rule =
-    let c = match c with AVar id -> RVar (dummy_loc,id)
-      | ARef c -> RRef (dummy_loc,c)
-      | _ -> anomaly "add_notation_interpretation" in
     let typs = List.map2 
       (fun id n -> id,ETConstr (NumLevel n,InternalProd)) vars (snd prec) in
-    let r = RApp (dummy_loc, c,
-    List.map (function Name id when List.mem id vars -> RVar (dummy_loc,id)
-      | _ -> RHole (dummy_loc,QuestionMark)) l) in
     Some (make_old_pp_rule (fst prec) symbs typs r notation scope vars) in
-  let a = AApp (c,List.map (function Name id when List.mem id vars -> AVar id | 
-_ -> AHole QuestionMark) l) in
+  Lib.add_anonymous_leaf
+    (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,df))
+
+let check_occur l id =
+  if not (List.mem (Name id) l) then error ((string_of_id id)^"is unbound")
+
+let add_notation_interpretation df (c,l) sc =
+  let (vars,symbs) = analyse_tokens (split df) in
+  List.iter (check_occur l) vars;
+  let a_for_old =
+    let c = match c with AVar id -> RVar (dummy_loc,id)
+      | ARef c -> RRef (dummy_loc,c)
+      | _ -> anomaly "add_notation_interpretation" in
+    RApp (dummy_loc, c,
+      List.map (function
+	| Name id when List.mem id vars -> RVar (dummy_loc,id)
+	| _ -> RHole (dummy_loc,QuestionMark)) l) in
+  let a = AApp (c,List.map (function 
+    | Name id when List.mem id vars -> AVar id
+    | _ -> AHole QuestionMark) l) in
   let la = List.map (fun id -> id,[]) vars in
   let onlyparse = false in
   let local = false in
-  Lib.add_anonymous_leaf
-    (inNotation(local,old_pp_rule,notation,scope,(la,a),onlyparse,df))
+  add_notation_interpretation_core local vars symbs df ((la,a),a_for_old) sc
+    onlyparse
+
+let add_notation local df c modifiers mv8 sc =
+  let toks = split df in
+  match toks with 
+    | [String x] when quote(strip x) = x
+	(* This is an ident that can be qualified: a syntactic definition *)
+	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
+        (* Means a Syntactic Definition *)
+        let ident = id_of_string (strip x) in
+	let c = snd (interp_aconstr [] c) in
+	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
+        Syntax_def.declare_syntactic_definition local ident onlyparse c
+    | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
+	(* This is a ident to be declared as a rule *)
+        add_notation_in_scope local df c (None,0,[],modifiers=[SetOnlyParsing])
+          (option_app (fun (s8,ml8) ->
+	    let toks8 = split s8 in 
+	    let im8 = interp_notation_modifiers ml8 in
+	    (toks8,im8)) mv8)
+        sc toks
+    | _ ->
+	let (assoc,lev,typs,onlyparse) = interp_modifiers None None modifiers
+	in
+	match lev with
+	  | None->
+	      if modifiers <> [] & modifiers <> [SetOnlyParsing] then
+		error "Parsing rule for this notation includes no level"
+	      else
+	        (* Declare only interpretation *)
+		let (vars,symbs) = analyse_tokens toks in
+		let onlyparse = modifiers = [SetOnlyParsing] in
+		let a = interp_aconstr vars c in
+		let a_for_old = interp_rawconstr_gen
+		  false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in
+		add_notation_interpretation_core local vars symbs df
+		  (a,a_for_old) sc onlyparse
+	  | Some n ->
+	    (* Declare both syntax and interpretation *)
+	    let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
+	    let mods = (assoc,n,typs,onlyparse)	in
+            add_notation_in_scope local df c mods
+              (option_app (fun (s8,ml8) ->
+		let toks8 = split s8 in 
+		let im8 = interp_notation_modifiers ml8 in
+		(toks8,im8)) mv8)
+              sc toks
 
 (* TODO add boxes information in the expression *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index dea54e58a2..b52af04f3a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -140,13 +140,15 @@ let rec vernac_com interpfun (loc,com) =
              Options.v7_only := true;
              if !translate_file then msg (pr_comments !comments)
          | _ ->
+	     let fs = States.freeze () in
              if !translate_file then
                msgnl
 		 (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end())
              else
-	       msgnl
+	       (msgnl
                  (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++
-                         pr_vernac com ++ sep_end())));
+                         pr_vernac com ++ sep_end()));
+		 States.unfreeze fs));
        Constrintern.set_temporary_implicits_in [];
        Constrextern.set_temporary_implicits_out [];
        comments := None;
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b68fe70225..7388137720 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -177,7 +177,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list
-  | VernacFixpoint of fixpoint_expr list
+  | VernacFixpoint of (fixpoint_expr * decl_notation) list
   | VernacCoFixpoint of cofixpoint_expr list
   | VernacScheme of (identifier * bool * reference * sort_expr) list