From e1c8e5ca2e8cdb03b090b6c049e417f3c7be50f3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 5 Jan 2006 12:26:08 +0000 Subject: Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la suppression des coercions permet aussi d'afficher un nombre, on choisit l'affichage qui n'introduit pas de délimiteurs si possible (exemple: avec 'Zpos 2', si Zpos est une coercion, on peut effacer la coercion et afficher 2 dans le type positive, ou bien garder la coercion afficher 'Zpos 2' comme 2 dans Z; dans certains cas - cf 4CT - il n'y a pas d'afficheur qui gère la coercion et il faut la retirer avant d'appliquer l'afficheur de nombre le plus interne) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7796 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.ml | 33 ++++++++++++++++++++++++--------- 1 file changed, 24 insertions(+), 9 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ffd598cd1..006d9bc2f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -582,19 +582,39 @@ let rec share_fix_binders n rbl ty def = share_fix_binders (n-1) ((na,None,t0)::rbl) b m | _ -> List.rev rbl, ty, def +(**********************************************************************) +(* mapping rawterms to numerals (in presence of coercions, choose the *) +(* one with no delimiter if possible) *) + +let extern_possible_prim_token scopes r = + try + let (sc,n) = uninterp_prim_token r in + match availability_of_prim_token sc (make_current_scopes scopes) with + | None -> None + | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key) + with No_match -> + None + +let extern_optimal_prim_token scopes r r' = + let c = extern_possible_prim_token scopes r in + let c' = if r==r' then None else extern_possible_prim_token scopes r' in + match c,c' with + | Some n, (Some (CDelimiters _) | None) | _, Some n -> n + | _ -> raise No_match + (**********************************************************************) (* mapping rawterms to constr_expr *) let rec extern inctx scopes vars r = - let r = remove_coercions inctx r in + let r' = remove_coercions inctx r in try if !Options.raw_print or !print_no_symbol then raise No_match; - extern_prim_token (loc_of_rawconstr r) scopes (uninterp_prim_token r) + extern_optimal_prim_token scopes r r' with No_match -> try if !Options.raw_print or !print_no_symbol then raise No_match; - extern_symbol scopes vars r (uninterp_notations r) - with No_match -> match r with + extern_symbol scopes vars r' (uninterp_notations r') + with No_match -> match r' with | RRef (loc,ref) -> extern_global loc (implicits_of_global ref) (extern_reference loc vars ref) @@ -763,11 +783,6 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, extern inctx scopes vars c) -and extern_prim_token loc scopes (sc,p) = - match availability_of_prim_token sc (make_current_scopes scopes) with - | None -> raise No_match - | Some key -> insert_delimiters (CPrim (loc,p)) key - and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> -- cgit v1.2.3