diff options
| -rw-r--r-- | interp/constrextern.ml | 9 | ||||
| -rw-r--r-- | interp/constrextern.mli | 4 | ||||
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 14 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 42 |
6 files changed, 58 insertions, 23 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a094e17ab8..472b636a8f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -67,6 +67,13 @@ let with_universes f = Options.with_option print_universes f let without_symbols f = Options.with_option print_no_symbol f let with_meta_as_hole f = Options.with_option print_meta_as_hole f +(* For the translator *) +let temporary_implicits_out = ref [] +let set_temporary_implicits_out l = temporary_implicits_out := l +let get_temporary_implicits_out id = + try List.assoc id !temporary_implicits_out + with Not_found -> [] + (**********************************************************************) (* Various externalisation functions *) @@ -230,7 +237,7 @@ let rec extern inctx scopes vars r = args | RVar (loc,id) -> (* useful for translation of inductive *) let args = List.map (extern true scopes vars) args in - extern_app loc (implicits_of_global_out (VarRef id)) + extern_app loc (get_temporary_implicits_out id) (Ident (loc,id)) args | _ -> diff --git a/interp/constrextern.mli b/interp/constrextern.mli index b2dd833aaf..cb58ca58ee 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -61,3 +61,7 @@ val without_symbols : ('a -> 'b) -> 'a -> 'b (* This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b + +(* For v8 translation *) +val set_temporary_implicits_out : + (identifier * Impargs.implicits_list) list -> unit diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 641ccf7fc5..ffed01a34e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -32,6 +32,10 @@ let for_grammar f x = interning_grammar := false; a +(* For the translator *) +let temporary_implicits_in = ref [] +let set_temporary_implicits_in l = temporary_implicits_in := l + (**********************************************************************) (* Internalisation errors *) @@ -183,7 +187,9 @@ let intern_reference env lvar = function (* Extra allowance for grammars *) if !interning_grammar then begin set_var_scope loc id env lvar; - RVar (loc,id), [], [] + RVar (loc,id), + (try List.assoc id !temporary_implicits_in with Not_found -> []), + [] end else raise e diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 99e7d68bbc..b135caf505 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -93,3 +93,7 @@ val interp_aconstr : identifier list -> constr_expr -> interpretation (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b + +(* For v8 translation *) +val set_temporary_implicits_in : + (identifier * Impargs.implicits_list) list -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 5da98da625..9016aa9893 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -140,21 +140,15 @@ let rec vernac_com interpfun (loc,com) = Options.v7_only := true; if !translate_file then msgnl (pr_comments !comments) | _ -> - let protect = match com with (* Pour gérer les implicites *) - | VernacFixpoint _ | VernacInductive _ -> - fun f x -> - (let fs = States.freeze () in - try let e = f x in States.unfreeze fs; e - with e -> States.unfreeze fs; raise e) - | _ -> fun f -> f in if !translate_file then msgnl - (pr_comments !comments ++ hov 0 (protect pr_vernac com) ++ - sep_end) + (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end) else msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ - protect pr_vernac com ++ sep_end))); + pr_vernac com ++ sep_end))); + Constrintern.set_temporary_implicits_in []; + Constrextern.set_temporary_implicits_out []; comments := None; Format.set_formatter_out_channel stdout); interp com; diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index bd6648bb4a..30fc771e54 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -515,15 +515,26 @@ let rec pr_vernac = function (Termops.push_rel_assum (Name id,p) env, (Name id,None,p)::params)) (env0,[]) lparams in - List.iter + let impls = List.map (fun (recname, _,arityc,_) -> let arity = Constrintern.interp_type sigma env_params arityc in let fullarity = - Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in - if Impargs.is_implicit_args_out() - then - Impargs.set_var_implicits recname - (Impargs.compute_implicits false env_params fullarity)) l; + Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) + in + let impl_in = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env_params fullarity + else [] in + let impl_out = + if Impargs.is_implicit_args_out() + then Impargs.compute_implicits true env_params fullarity + else [] in + (recname,impl_in,impl_out)) l in + let impls_in = List.map (fun (id,a,_) -> (id,a)) impls in + let impls_out = List.map (fun (id,_,a) -> (id,a)) impls in + Constrintern.set_temporary_implicits_in impls_in; + Constrextern.set_temporary_implicits_out impls_out; + (* Fin calcul implicites *) let pr_constructor (coe,(id,c)) = @@ -547,13 +558,22 @@ let rec pr_vernac = function (* Copie simplifiée de command.ml pour recalculer les implicites *) let sigma = Evd.empty and env0 = Global.env() in - List.iter + let impls = List.map (fun (recname,_,arityc,_) -> let arity = Constrintern.interp_type sigma env0 arityc in - let _ = Declare.declare_variable recname - (Lib.cwd(),Declare.SectionLocalAssum arity, - Decl_kinds.IsAssumption Decl_kinds.Definitional) in ()) - recs; + let impl_in = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env0 arity + else [] in + let impl_out = + if Impargs.is_implicit_args_out() + then Impargs.compute_implicits true env0 arity + else [] in + (recname,impl_in,impl_out)) recs in + let impls_in = List.map (fun (id,a,_) -> (id,a)) impls in + let impls_out = List.map (fun (id,_,a) -> (id,a)) impls in + Constrintern.set_temporary_implicits_in impls_in; + Constrextern.set_temporary_implicits_out impls_out; let pr_onerec = function | (id,n,type_0,def0) -> |