Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

1 files changed, 128 insertions, 59 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0ae4c2214c..c813cf71d1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -39,9 +39,6 @@ let print_arguments = ref false
 (* If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false
 
-(* This forces printing of cast nodes *)
-let print_casts = ref true
-
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
    how implicit args are printed. If on, implicit args are printed
@@ -56,6 +53,8 @@ let print_coercions = ref false
 (* This forces printing universe names of Type{.} *)
 let print_universes = ref false
 
+(* This suppresses printing of numeral and symbols *)
+let print_no_symbol = ref false
 
 let with_option o f x =
   let old = !o in o:=true;
@@ -63,10 +62,23 @@ let with_option o f x =
   with e -> o := old; raise e
 
 let with_arguments f = with_option print_arguments f
-let with_casts f = with_option print_casts f
 let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
 let with_universes f = with_option print_universes f
+let without_symbols f = with_option print_no_symbol f
+
+(**********************************************************************)
+(* Various externalisation functions *)
+
+let insert_delimiters e = function
+  | None -> e
+  | Some sc -> CDelimiters (dummy_loc,sc,e)
+
+let insert_pat_delimiters e = function
+  | None -> e
+  | Some sc -> CPatDelimiters (dummy_loc,sc,e)
+
+let loc = dummy_loc (* shorter... *)
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -90,13 +102,21 @@ let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
 let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r)
 
 (**********************************************************************)
-(* conversion of patterns                                             *)
-
-let rec extern_cases_pattern = function   (* loc is thrown away for printing *)
-  | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
-  | PatVar (loc,Anonymous) -> CPatAtom (loc, None) 
-  | PatCstr(loc,cstrsp,args,na) ->
-      let args = List.map extern_cases_pattern args in
+(* conversion of terms and cases patterns                             *)
+
+let rec extern_cases_pattern_in_scope scopes pat =
+  try 
+    if !print_no_symbol then raise No_match;
+    let (sc,n) = Symbols.uninterp_cases_numeral pat in
+    match Symbols.availability_of_numeral sc scopes with
+    | None -> raise No_match
+    | Some scopt -> insert_pat_delimiters (CPatNumeral (loc,n)) scopt
+  with No_match ->
+  match pat with
+  | PatVar (_,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
+  | PatVar (_,Anonymous) -> CPatAtom (loc, None) 
+  | PatCstr(_,cstrsp,args,na) ->
+      let args = List.map (extern_cases_pattern_in_scope scopes) args in
       let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in
       (match na with
 	| Name id -> CPatAlias (loc,p,id)
@@ -140,14 +160,31 @@ let rec skip_coercion dest_ref (f,args as app) =
     with Not_found -> app
 
 let extern_app impl f args =
-  if !print_implicits & not !print_implicits_explicit_args then 
+  if (!print_implicits & not !print_implicits_explicit_args) then 
     CAppExpl (dummy_loc, f, args)
   else
     explicitize impl (CRef f) args
 
-let loc = dummy_loc
+let rec extern_args extern scopes args subscopes =
+  match args with
+    | [] -> []
+    | a::args ->
+	let argscopes, subscopes = match subscopes with
+	  | [] -> scopes, []
+	  | scopt::subscopes -> option_cons scopt scopes, subscopes in
+	extern argscopes a :: extern_args extern scopes args subscopes
+
+let rec extern scopes r =
+  try 
+    if !print_no_symbol then raise No_match;
+    extern_numeral scopes r (Symbols.uninterp_numeral r)
+  with No_match ->
+
+  try 
+    if !print_no_symbol then raise No_match;
+    extern_symbol scopes r (Symbols.uninterp_notations r)
+  with No_match -> match r with
 
-let rec extern = function
   | RRef (_,ref) -> CRef (extern_ref ref)
 
   | RVar (_,id) -> CRef (Ident (loc,id))
@@ -159,51 +196,55 @@ let rec extern = function
   | RApp (_,f,args) ->
       let (f,args) =
 	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
-      let args = List.map extern args in
       (match f with
 	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
 	 | RRef (loc,ref) ->
+	     let subscopes = Symbols.find_arguments_scope ref in
+	     let args = extern_args extern scopes args subscopes in
 	     extern_app (implicits_of_global ref) (extern_ref ref) args
-	 | _       -> explicitize [] (extern f) args)
+	 | _       -> 
+	     explicitize [] (extern scopes f) (List.map (extern scopes) args))
 
   | RProd (_,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
-      CArrow (loc,extern t,extern c)
+      CArrow (loc,extern scopes t,extern scopes c)
 
   | RLetIn (_,na,t,c) ->
-      CLetIn (loc,(loc,na),extern t,extern c)
+      CLetIn (loc,(loc,na),extern scopes t,extern scopes c)
 
   | RProd (_,na,t,c) ->
-      let t = extern t in
-      let (idl,c) = factorize_prod t c in
+      let t = extern scopes t in
+      let (idl,c) = factorize_prod scopes t c in
       CProdN (loc,[(loc,na)::idl,t],c)
 
   | RLambda (_,na,t,c) ->
-      let t = extern t in
-      let (idl,c) = factorize_lambda t c in
+      let t = extern scopes t in
+      let (idl,c) = factorize_lambda scopes t c in
       CLambdaN (loc,[(loc,na)::idl,t],c)
 
   | RCases (_,typopt,tml,eqns) ->
-      let pred = option_app extern typopt in
-      let tml = List.map extern tml in
-      let eqns = List.map extern_eqn eqns in 
+      let pred = option_app (extern scopes) typopt in
+      let tml = List.map (extern scopes) tml in
+      let eqns = List.map (extern_eqn scopes) eqns in 
       CCases (loc,pred,tml,eqns)
 	
   | ROrderedCase (_,cs,typopt,tm,bv) ->
-      let bv = Array.to_list (Array.map extern bv) in
-      COrderedCase (loc,cs,option_app extern typopt,extern tm,bv)
+      let bv = Array.to_list (Array.map (extern scopes) bv) in
+      COrderedCase
+	(loc,cs,option_app (extern scopes) typopt,extern scopes tm,bv)
 
   | RRec (_,fk,idv,tyv,bv) ->
       (match fk with
 	 | RFix (nv,n) ->
 	     let listdecl = 
-	       Array.mapi
-		 (fun i fi -> (fi,nv.(i),extern tyv.(i),extern bv.(i))) idv
+	       Array.mapi (fun i fi ->
+		 (fi,nv.(i),extern scopes tyv.(i),extern scopes bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
 	 | RCoFix n -> 
 	     let listdecl =
-               Array.mapi (fun i fi -> (fi,extern tyv.(i),extern bv.(i))) idv
+               Array.mapi (fun i fi ->
+		 (fi,extern scopes tyv.(i),extern scopes bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
@@ -216,46 +257,71 @@ let rec extern = function
 
   | RHole (_,e) -> CHole loc
 
-  | RCast (_,c,t) -> CCast (loc,extern c,extern t)
+  | RCast (_,c,t) -> CCast (loc,extern scopes c,extern scopes t)
 
   | RDynamic (_,d) -> CDynamic (loc,d)
 	
-and factorize_prod aty = function
+and factorize_prod scopes aty = function
   | RProd (_,Name id,ty,c)
-      when aty = extern ty
-	& not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*)
-	-> let (nal,c) = factorize_prod aty c in ((loc,Name id)::nal,c)
-  | c -> ([],extern c)
+      when aty = extern scopes ty
+	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
+	-> let (nal,c) = factorize_prod scopes aty c in ((loc,Name id)::nal,c)
+  | c -> ([],extern scopes c)
 
-and factorize_lambda aty = function
+and factorize_lambda scopes aty = function
   | RLambda (_,na,ty,c)
-      when aty = extern ty
+      when aty = extern scopes ty
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-	-> let (nal,c) = factorize_lambda aty c in ((loc,na)::nal,c)
-  | c -> ([],extern c)
-
-and extern_eqn (loc,ids,pl,c) =
-  (loc,List.map extern_cases_pattern pl,extern c)
-(*
-and extern_numerals r =
-  on_numeral (fun p ->
-    match filter p r with
-      | Some f 
-
-and extern_symbols r =
-*)
-
-let extern_rawconstr = extern
+	-> let (nal,c) = factorize_lambda scopes aty c in ((loc,na)::nal,c)
+  | c -> ([],extern scopes c)
+
+and extern_eqn scopes (loc,ids,pl,c) =
+  (loc,List.map (extern_cases_pattern_in_scope scopes) pl,extern scopes c)
+
+and extern_numeral scopes t (sc,n) =
+  match Symbols.availability_of_numeral sc scopes with
+    | None -> raise No_match
+    | Some scopt -> insert_delimiters (CNumeral (loc,n)) scopt
+
+and extern_symbol scopes t = function
+  | [] -> raise No_match
+  | (sc,ntn,pat,n as rule)::rules ->
+      try
+	(* Adjusts to the number of arguments expected by the notation *)
+	let (t,args) = match t,n with
+	  | RApp (_,f,args), Some n when List.length args > n ->
+	      let args1, args2 = list_chop n args in
+	      RApp (loc,f,args1), args2
+	  | _ -> t,[] in
+	(* Try matching ... *)
+	let subst = match_aconstr t pat in
+	(* Try availability of interpretation ... *)
+	(match Symbols.availability_of_notation (sc,ntn) scopes with
+          (* Uninterpretation is not allowed in current context *)
+	  | None -> raise No_match
+          (* Uninterpretation is allowed in current context *)
+	  | Some scopt ->
+	      let scopes = option_cons scopt scopes in
+	      let l = List.map (fun (id,c) -> (id,extern scopes c)) subst in
+	      let e = insert_delimiters (CNotation (loc,ntn,l)) scopt in
+	      if args = [] then e 
+	      else explicitize [] e (List.map (extern scopes) args))
+      with
+	  No_match -> extern_symbol scopes t rules
+
+let extern_rawconstr = 
+  extern (Symbols.current_scopes())
+
+let extern_cases_pattern = 
+  extern_cases_pattern_in_scope (Symbols.current_scopes())
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
        
 let extern_constr at_top env t =
-  let t' =
-    if !print_casts then t
-    else Reductionops.local_strong strip_outer_cast t in
   let avoid = if at_top then ids_of_context env else [] in
-  extern (Detyping.detype env avoid (names_of_rel_context env) t')
+  extern (Symbols.current_scopes())
+    (Detyping.detype env avoid (names_of_rel_context env) t)
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -319,9 +385,12 @@ let rec extern_pattern tenv env = function
 	(loc,cs,option_app (extern_pattern tenv env) typopt,
 	 extern_pattern tenv env tm,bv)
 
-  | PFix f -> extern (Detyping.detype tenv [] env (mkFix f))
+  | PFix f ->
+      extern (Symbols.current_scopes()) (Detyping.detype tenv [] env (mkFix f))
 
-  | PCoFix c -> extern (Detyping.detype tenv [] env (mkCoFix c))
+  | PCoFix c ->
+      extern (Symbols.current_scopes())
+        (Detyping.detype tenv [] env (mkCoFix c))
 
   | PSort s ->
       let s = match s with