diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-10 21:06:33 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-10 21:06:33 +0000 |
commit | 5e06a8ef480a68b20f94814b4b2fee1df3d192fd (patch) | |
tree | 3d9f21f0dfd8cd133a570c931542ca0d4200e43b /interp/constrextern.ml | |
parent | c76d3d5b03c45e0710f96089e0fb3abd7da67cd7 (diff) |
Amélioration afficheur de Cases pour les constr_pattern
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
Extension du traducteur de nom
Ajout notation c.(f) en v8 pour les projections de Record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r-- | interp/constrextern.ml | 322 |
1 files changed, 196 insertions, 126 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d23986def..102754384 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -118,8 +118,93 @@ let raw_string_of_ref = function | VarRef id -> "SECVAR("^(string_of_id id)^")" +(* v7->v8 translation *) + +let is_coq_root d = + let d = repr_dirpath d in d <> [] & string_of_id (list_last d) = "Coq" + +let is_module m = + let d = repr_dirpath (Lib.library_dp()) in + d <> [] & string_of_id (List.hd d) = m + +let translate_v7_string = function + (* ZArith *) + | "double_moins_un" -> "double_minus_one" + | "double_moins_deux" -> "double_minus_two" + | "entier" -> "N" + | "SUPERIEUR" -> "GREATER" + | "EGAL" -> "EQUAL" + | "INFERIEUR" -> "LESS" + | "add" -> "Padd" + | "times" when not (is_module "Mapfold") -> "Pmult" + | "true_sub" -> "Psub" + | "add_un" -> "Padd_one" + | "sub_un" -> "Psub_one" + | "sub_pos" -> "PNsub" + | "sub_neg" -> "PNsub_carry" + | "convert_add_un" -> "convert_Padd_one" + | "compare_convert_INFERIEUR" -> "compare_convert_LESS" + | "compare_convert_SUPERIEUR" -> "compare_convert_GREATER" + | "compare_convert_EGAL" -> "compare_convert_EQUAL" + | "convert_compare_INFERIEUR" -> "convert_compare_LESS" + | "convert_compare_SUPERIEUR" -> "convert_compare_GREATER" + | "convert_compare_EGAL" -> "convert_compare_EQUAL" + | "Zcompare_EGAL" -> "Zcompare_EQUAL" + | "Nul" -> "Null" + | "Un_suivi_de" -> "double_plus_one" + | "Zero_suivi_de" -> "double" + | "is_double_moins_un" -> "is_double_minus_one" + | "Zplus_sym" -> "Zplus_comm" + | "Zmult_sym" -> "Zmult_comm" + | "sub_pos_SUPERIEUR" -> "sub_pos_GREATER" + | "inject_nat" -> "INZ" + | "convert" -> "IPN" + | "anti_convert" -> "INP" + | "convert_intro" -> "IPN_inj" + | "convert_add" -> "IPN_add" + | "convert_add_carry" -> "IPN_add_carry" + | "compare_convert_O" -> "lt_O_IPN" + | "Zopp_intro" -> "Zopp_inj" + (* Arith *) + | "plus_sym" -> "plus_comm" + | "mult_sym" -> "mult_comm" + | "max_sym" -> "max_comm" + | "min_sym" -> "min_comm" + | "gt_not_sym" -> "gt_asym" + | "fact_growing" -> "fact_le" + (* Lists *) + | "idempot_rev" -> "involutive_rev" + (* Bool *) + | "orb_sym" -> "orb_comm" + | "andb_sym" -> "andb_comm" + (* Reals *) + (* redundant *) + | "Rle_sym1" -> "Rle_ge" + | "Rmin_sym" -> "Rmin_comm" + | s when String.length s >= 7 & + let s' = String.sub s 0 7 in + (s' = "unicite" or s' = "unicity") -> + "uniqueness"^(String.sub s 7 (String.length s - 7)) + (* Default *) + | x -> x + +let id_of_v7_string s = + id_of_string (if !Options.v7 then s else translate_v7_string s) + +let v7_to_v8_dir_id dir id = + if Options.do_translate() + & (is_coq_root (Lib.library_dp()) or is_coq_root dir) + then id_of_string (translate_v7_string (string_of_id id)) else id + +let v7_to_v8_id = v7_to_v8_dir_id empty_dirpath + +let shortest_qualid_of_v7_global ctx ref = + let fulldir,_ = repr_path (sp_of_global ref) in + let dir,id = repr_qualid (shortest_qualid_of_global ctx ref) in + make_qualid dir (v7_to_v8_dir_id fulldir id) + let extern_reference loc vars r = - try Qualid (loc,shortest_qualid_of_global vars r) + try Qualid (loc,shortest_qualid_of_v7_global vars r) with Not_found -> (* happens in debugger *) Ident (loc,id_of_string (raw_string_of_ref r)) @@ -127,11 +212,13 @@ let extern_reference loc vars r = (**********************************************************************) (* conversion of terms and cases patterns *) +let make_current_scope (scopt,scopes) = option_cons scopt scopes + let rec extern_cases_pattern_in_scope scopes vars 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 + match Symbols.availability_of_numeral sc (make_current_scope scopes) with | None -> raise No_match | Some key -> let loc = pattern_loc pat in @@ -153,9 +240,16 @@ let occur_name na aty = | Name id -> occur_var_constr_expr id aty | Anonymous -> false +let is_projection nargs = function + | Some r -> + (try Recordops.find_projection_nparams r + 1 = nargs + with Not_found -> false) + | None -> + false + (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) -let explicitize loc inctx impl f args = +let explicitize loc inctx impl (cf,f) args = let n = List.length args in let rec exprec q = function | a::args, imp::impl when is_status_implicit imp -> @@ -169,8 +263,9 @@ let explicitize loc inctx impl f args = | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) | [], _ -> [] in + let isproj = is_projection (List.length args) cf in let args = exprec 1 (args,impl) in - if args = [] then f else CApp (loc, f, args) + if args = [] then f else CApp (loc, (isproj, f), args) let rec skip_coercion dest_ref (f,args as app) = if !print_coercions or Options.do_translate () then app @@ -188,23 +283,23 @@ let rec skip_coercion dest_ref (f,args as app) = | None -> app with Not_found -> app -let extern_app loc inctx impl f args = +let extern_app loc inctx impl (cf,f) args = if !print_implicits & not !print_implicits_explicit_args & List.exists is_status_implicit impl then if args = [] (* maybe caused by a hidden coercion *) then CRef f - else CAppExpl (loc, f, args) + else CAppExpl (loc, (is_projection (List.length args) cf, f), args) else - explicitize loc inctx impl (CRef f) args + explicitize loc inctx impl (cf,CRef f) args let rec extern_args extern scopes env args subscopes = match args with | [] -> [] | a::args -> let argscopes, subscopes = match subscopes with - | [] -> scopes, [] - | scopt::subscopes -> option_cons scopt scopes, subscopes in + | [] -> (None,scopes), [] + | scopt::subscopes -> (scopt,scopes), subscopes in extern argscopes env a :: extern_args extern scopes env args subscopes let rec extern inctx scopes vars r = @@ -219,7 +314,7 @@ let rec extern inctx scopes vars r = with No_match -> match r with | RRef (loc,ref) -> CRef (extern_reference loc vars ref) - | RVar (loc,id) -> CRef (Ident (loc,id)) + | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id)) | REvar (loc,n) -> extern_evar loc n @@ -235,39 +330,40 @@ let rec extern inctx scopes vars r = | 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 true) scopes vars args subscopes in + let args = + extern_args (extern true) (snd scopes) vars args subscopes in extern_app loc inctx (implicits_of_global_out ref) - (extern_reference loc vars ref) + (Some ref,extern_reference loc vars ref) args | RVar (loc,id) -> (* useful for translation of inductive *) let args = List.map (extern true scopes vars) args in extern_app loc inctx (get_temporary_implicits_out id) - (Ident (loc,id)) + (None,Ident (loc,v7_to_v8_id id)) args | _ -> - explicitize loc inctx [] (extern false scopes vars f) + explicitize loc inctx [] (None,extern false scopes vars f) (List.map (extern true scopes vars) args)) | RProd (loc,Anonymous,t,c) -> (* Anonymous product are never factorized *) - CArrow (loc,extern true scopes vars t, extern true scopes vars c) + CArrow (loc,extern_type scopes vars t, extern_type scopes vars c) | RLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),extern false scopes vars t, extern inctx scopes (add_vname vars na) c) | RProd (loc,na,t,c) -> - let t = extern true scopes vars (anonymize_if_reserved na t) in + let t = extern_type scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_prod scopes (add_vname vars na) t c in CProdN (loc,[(dummy_loc,na)::idl,t],c) | RLambda (loc,na,t,c) -> - let t = extern true scopes vars (anonymize_if_reserved na t) in + let t = extern_type scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,t],c) | RCases (loc,typopt,tml,eqns) -> - let pred = option_app (extern true scopes vars) typopt in + let pred = option_app (extern_type scopes vars) typopt in let tml = List.map (extern false scopes vars) tml in let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in CCases (loc,pred,tml,eqns) @@ -276,7 +372,7 @@ let rec extern inctx scopes vars r = let bv = Array.to_list (Array.map (extern (typopt<>None) scopes vars) bv) in COrderedCase - (loc,cs,option_app (extern true scopes vars) typopt, + (loc,cs,option_app (extern_type scopes vars) typopt, extern false scopes vars tm,bv) | RRec (loc,fk,idv,tyv,bv) -> @@ -307,10 +403,12 @@ let rec extern inctx scopes vars r = | RHole (loc,e) -> CHole loc | RCast (loc,c,t) -> - CCast (loc,extern false scopes vars c,extern false scopes vars t) + CCast (loc,extern false scopes vars c,extern_type scopes vars t) | RDynamic (loc,d) -> CDynamic (loc,d) - + +and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes) + and factorize_prod scopes vars aty = function | RProd (loc,(Name id as na),ty,c) when aty = extern true scopes vars (anonymize_if_reserved na ty) @@ -333,11 +431,11 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = extern inctx scopes vars c) and extern_numeral loc scopes (sc,n) = - match Symbols.availability_of_numeral sc scopes with + match Symbols.availability_of_numeral sc (make_current_scope scopes) with | None -> raise No_match | Some key -> insert_delimiters (CNumeral (loc,n)) key -and extern_symbol scopes vars t = function +and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as rule)::rules -> let loc = Rawterm.loc t in @@ -354,31 +452,34 @@ and extern_symbol scopes vars t = function let e = match keyrule with | NotationRule (sc,ntn) -> - (match Symbols.availability_of_notation (sc,ntn) scopes with + let scopes' = option_cons tmp_scope scopes in + (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,key) -> let scopes = option_cons scopt scopes in let l = - List.map (fun (c,scl) -> + List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true - (scl@scopes) vars c) + (scopt,scl@scopes) vars c) subst in insert_delimiters (CNotation (loc,ntn,l)) key) | SynDefRule kn -> CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in if args = [] then e - else explicitize loc false [] e - (List.map (extern true scopes vars) args) + else + (* TODO: compute scopt for the extra args, in case, head is a ref *) + explicitize loc false [] (None,e) + (List.map (extern true allscopes vars) args) with - No_match -> extern_symbol scopes vars t rules + No_match -> extern_symbol allscopes vars t rules let extern_rawconstr vars c = - extern false (Symbols.current_scopes()) vars c + extern false (None,Symbols.current_scopes()) vars c let extern_cases_pattern vars p = - extern_cases_pattern_in_scope (Symbols.current_scopes()) vars p + extern_cases_pattern_in_scope (None,Symbols.current_scopes()) vars p (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -388,110 +489,79 @@ let loc = dummy_loc (* for constr and pattern, locations are lost *) let extern_constr at_top env t = let vars = vars_of_env env in let avoid = if at_top then ids_of_context env else [] in - extern (not at_top) (Symbols.current_scopes()) vars + extern (not at_top) (None,Symbols.current_scopes()) vars (Detyping.detype env avoid (names_of_rel_context env) t) (******************************************************************) (* Main translation function from pattern -> constr_expr *) -let rec extern_pattern tenv vars env = function - | PRef ref -> CRef (extern_reference loc vars ref) - - | PVar id -> CRef (Ident (loc,id)) - - | PEvar n -> extern_evar loc n - +let rec raw_of_pat tenv env = function + | PRef ref -> RRef (loc,ref) + | PVar id -> RVar (loc,id) + | PEvar n -> REvar (loc,n) | PRel n -> - CRef (Ident (loc, - try match lookup_name_of_rel n env with - | Name id -> id - | Anonymous -> - anomaly "ast_of_pattern: index to an anonymous variable" - with Not_found -> - id_of_string ("[REL "^(string_of_int n)^"]"))) - - | PMeta None -> CHole loc - - | PMeta (Some n) -> CPatVar (loc,(false,n)) - + let id = try match lookup_name_of_rel n env with + | Name id -> id + | Anonymous -> + anomaly "rawconstr_of_pattern: index to an anonymous variable" + with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in + RVar (loc,id) + | PMeta None -> RHole (loc,InternalHole) + | PMeta (Some n) -> RPatVar (loc,(false,n)) | PApp (f,args) -> - let (f,args) = - skip_coercion (function PRef r -> Some r | _ -> None) - (f,Array.to_list args) in - let args = List.map (extern_pattern tenv vars env) args in - (match f with - | PRef ref -> - extern_app loc false (implicits_of_global ref) - (extern_reference loc vars ref) - args - | _ -> - explicitize loc false [] (extern_pattern tenv vars env f) args) - + RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args) | PSoApp (n,args) -> - let args = List.map (extern_pattern tenv vars env) args in - (* [-n] is the trick to embed a so patten into a regular application *) - (* see constrintern.ml and g_constr.ml4 *) - explicitize loc false [] (CPatVar (loc,(true,n))) args - - | PProd (Anonymous,t,c) -> - (* Anonymous product are never factorized *) - CArrow (loc,extern_pattern tenv vars env t, - extern_pattern tenv vars env c) - - | PLetIn (na,t,c) -> - CLetIn (loc,(loc,na),extern_pattern tenv vars env t, - extern_pattern tenv (add_vname vars na) (na::env) c) - + RApp (loc,RPatVar (loc,(true,n)), + List.map (raw_of_pat tenv env) args) | PProd (na,t,c) -> - let t = extern_pattern tenv vars env t in - let (idl,c) = - factorize_prod_pattern tenv (add_vname vars na) (na::env) t c in - CProdN (loc,[(loc,na)::idl,t],c) - + RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c) + | PLetIn (na,t,c) -> + RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) | PLambda (na,t,c) -> - let t = extern_pattern tenv vars env t in - let (idl,c) = - factorize_lambda_pattern tenv (add_vname vars na) (na::env) t c in - CLambdaN (loc,[(loc,na)::idl,t],c) - - | PCase (cs,typopt,tm,bv) -> - let bv = Array.to_list (Array.map (extern_pattern tenv vars env) bv) in - COrderedCase - (loc,cs,option_app (extern_pattern tenv vars env) typopt, - extern_pattern tenv vars env tm,bv) - - | PFix f -> - extern true (Symbols.current_scopes()) vars - (Detyping.detype tenv [] env (mkFix f)) - - | PCoFix c -> - extern true (Symbols.current_scopes()) vars - (Detyping.detype tenv [] env (mkCoFix c)) - - | PSort s -> - let s = match s with - | RProp _ -> s - | RType (Some _) when !print_universes -> s - | RType _ -> RType None in - CSort (loc,s) - -and factorize_prod_pattern tenv vars env aty = function - | PProd (Name id as na,ty,c) - when aty = extern_pattern tenv vars env ty - & not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*) - -> let (nal,c) = - factorize_prod_pattern tenv (add_vname vars na) (na::env) aty c in - ((loc,Name id)::nal,c) - | c -> ([],extern_pattern tenv vars env c) - -and factorize_lambda_pattern tenv vars env aty = function - | PLambda (na,ty,c) - when aty = extern_pattern tenv vars env ty - & not (occur_name na aty) (* To avoid na in ty' escapes scope *) - -> let (nal,c) = - factorize_lambda_pattern tenv (add_vname vars na) (na::env) aty c - in ((loc,na)::nal,c) - | c -> ([],extern_pattern tenv vars env c) + RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) + | PCase ((_,(IfStyle|LetStyle as cs)),typopt,tm,bv) -> + ROrderedCase (loc,cs,option_app (raw_of_pat tenv env) typopt, + raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv) + | PCase ((_,cs),typopt,tm,[||]) -> + RCases (loc,option_app (raw_of_pat tenv env) typopt, + [raw_of_pat tenv env tm],[]) + | PCase ((Some ind,cs),typopt,tm,bv) -> + let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in + Detyping.detype_case false + (fun tenv _ -> raw_of_pat tenv) + (fun tenv _ -> raw_of_eqn tenv) + tenv avoid env ind cs typopt tm bv + | PCase _ -> error "Unsupported case-analysis while printing pattern" + | PFix f -> Detyping.detype tenv [] env (mkFix f) + | PCoFix c -> Detyping.detype tenv [] env (mkCoFix c) + | PSort s -> RSort (loc,s) + +and raw_of_eqn tenv env constr construct_nargs branch = + let make_pat x env b ids = + let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in + let id = next_name_away_with_default "x" x avoid in + PatVar (dummy_loc,Name id),(Name id)::env,id::ids + in + let rec buildrec ids patlist env n b = + if n=0 then + (dummy_loc, ids, + [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], + raw_of_pat tenv env b) + else + match b with + | PLambda (x,_,b) -> + let pat,new_env,new_ids = make_pat x env b ids in + buildrec new_ids (pat::patlist) new_env (n-1) b + + | PLetIn (x,_,b) -> + let pat,new_env,new_ids = make_pat x env b ids in + buildrec new_ids (pat::patlist) new_env (n-1) b + + | _ -> + error "Unsupported branch in case-analysis while printing pattern" + in + buildrec [] [] env construct_nargs branch let extern_pattern tenv env pat = - extern_pattern tenv (vars_of_env tenv) env pat + extern true (None,Symbols.current_scopes()) Idset.empty + (raw_of_pat tenv env pat) |