diff options
author | 2001-02-07 10:02:40 +0000 | |
---|---|---|
committer | 2001-02-07 10:02:40 +0000 | |
commit | 78384438637eb9ce2f11f61bafc59f17c5f933da (patch) | |
tree | f1968f737066e0e736f01b5fd4c8c9c5bccacdfc /parsing | |
parent | 9c662cf9e8f4065ab354dc9c55c3e819f0db1fbe (diff) |
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/astterm.ml | 5 | ||||
-rw-r--r-- | parsing/g_natsyntax.ml | 6 | ||||
-rw-r--r-- | parsing/pretty.ml | 1 | ||||
-rw-r--r-- | parsing/termast.ml | 83 | ||||
-rw-r--r-- | parsing/termast.mli | 2 |
5 files changed, 49 insertions, 48 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 6f2385392..d96107755 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -179,15 +179,14 @@ let ast_to_global loc c = | ("CONST", [sp]) -> let ref = ConstRef (ast_to_sp sp) in RRef (loc, ref), implicits_of_global ref - | ("EVAR", [(Num (_,ev))]) -> - let ref = EvarRef ev in - RRef (loc, ref), implicits_of_global ref | ("MUTIND", [sp;Num(_,tyi)]) -> let ref = IndRef (ast_to_sp sp, tyi) in RRef (loc, ref), implicits_of_global ref | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) -> let ref = ConstructRef ((ast_to_sp sp,ti),n) in RRef (loc, ref), implicits_of_global ref + | ("EVAR", [(Num (_,ev))]) -> + REvar (loc, ev), [] | ("SYNCONST", [sp]) -> Syntax_def.search_syntactic_definition (ast_to_sp sp), [] | _ -> anomaly_loc (loc,"ast_to_global", diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index ca5033a20..41f6f1818 100644 --- a/parsing/g_natsyntax.ml +++ b/parsing/g_natsyntax.ml @@ -15,9 +15,9 @@ open Termast exception Non_closed_number -let ast_O = ast_of_ref ast_of_rawconstr glob_O -let ast_S = ast_of_ref ast_of_rawconstr glob_S -let ast_myvar = ast_of_ref ast_of_rawconstr glob_My_special_variable_nat +let ast_O = ast_of_ref glob_O +let ast_S = ast_of_ref glob_S +let ast_myvar = ast_of_ref glob_My_special_variable_nat (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) let nat_of_int n dloc = diff --git a/parsing/pretty.ml b/parsing/pretty.ml index eb6b20719..2577ef9be 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -329,7 +329,6 @@ let print_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef ((sp,_),_) -> print_inductive sp | VarRef sp -> print_section_variable sp - | EvarRef n -> [< 'sTR "?"; 'iNT n; 'fNL >] with Not_found -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in diff --git a/parsing/termast.ml b/parsing/termast.ml index 3d72f4adc..0a7a73966 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -74,35 +74,23 @@ let stringopt_of_name = function | Name id -> Some (string_of_id id) | Anonymous -> None -let ast_of_constant_ref pr (sp,ids) = - let a = ope("CONST", [path_section dummy_loc sp]) in - if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids)) - else a +let ast_of_constant_ref sp = + ope("CONST", [path_section dummy_loc sp]) -let ast_of_existential_ref pr (ev,ids) = - let a = ope("EVAR", [num ev]) in - if !print_arguments or !print_evar_arguments then - ope("INSTANCE",a::(array_map_to_list pr ids)) - else a +let ast_of_existential_ref ev = + ope("EVAR", [num ev]) -let ast_of_constructor_ref pr (((sp,tyi),n) as cstr_sp,ids) = - let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in - if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids)) - else a +let ast_of_constructor_ref ((sp,tyi),n) = + ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) -let ast_of_inductive_ref pr ((sp,tyi) as ind_sp,ids) = - let a = ope("MUTIND", [path_section dummy_loc sp; num tyi]) in - if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids)) - else a +let ast_of_inductive_ref (sp,tyi) = + ope("MUTIND", [path_section dummy_loc sp; num tyi]) -let ast_of_ref pr r = - (* TODO gérer le ctxt *) - let ctxt = [||] in match r with - | ConstRef sp -> ast_of_constant_ref pr (sp,ctxt) - | IndRef sp -> ast_of_inductive_ref pr (sp,ctxt) - | ConstructRef sp -> ast_of_constructor_ref pr (sp,ctxt) +let ast_of_ref = function + | ConstRef sp -> ast_of_constant_ref sp + | IndRef sp -> ast_of_inductive_ref sp + | ConstructRef sp -> ast_of_constructor_ref sp | VarRef sp -> ast_of_ident (basename sp) - | EvarRef ev -> ast_of_existential_ref pr (ev,ctxt) let ast_of_qualid p = let dir, s = repr_qualid p in @@ -112,21 +100,18 @@ let ast_of_qualid p = (**********************************************************************) (* conversion of patterns *) -let adapt (cstr_sp,ctxt) = (cstr_sp,Array.of_list ctxt) - let rec ast_of_cases_pattern = function (* loc is thrown away for printing *) | PatVar (loc,Name id) -> nvar (string_of_id id) | PatVar (loc,Anonymous) -> nvar "_" - | PatCstr(loc,cstr,args,Name id) -> + | PatCstr(loc,(cstrsp,_),args,Name id) -> let args = List.map ast_of_cases_pattern args in ope("PATTAS", [nvar (string_of_id id); - ope("PATTCONSTRUCT", - (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)]) - | PatCstr(loc,cstr,args,Anonymous) -> + ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)]) + | PatCstr(loc,(cstrsp,_),args,Anonymous) -> ope("PATTCONSTRUCT", - (ast_of_constructor_ref ast_of_ident (adapt cstr)):: - List.map ast_of_cases_pattern args) + (ast_of_constructor_ref cstrsp) + :: List.map ast_of_cases_pattern args) let ast_dependent na aty = match na with @@ -188,8 +173,9 @@ let ast_of_app impl f args = *) let rec ast_of_raw = function - | RRef (_,ref) -> ast_of_ref ast_of_raw ref + | RRef (_,ref) -> ast_of_ref ref | RVar (_,id) -> ast_of_ident id + | REvar (_,n) -> ast_of_existential_ref n | RMeta (_,n) -> ope("META",[num n]) | RApp (_,f,args) -> let (f,args) = @@ -197,8 +183,7 @@ let rec ast_of_raw = function let astf = ast_of_raw f in let astargs = List.map ast_of_raw args in (match f with - | RRef (_,(EvarRef _ as ref)) -> - ast_of_ref ast_of_raw ref (* we drop args *) + | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *) | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs | RVar (_,id) -> @@ -317,19 +302,37 @@ let ast_of_constr at_top env t = ast_of_raw (Detyping.detype avoid (names_of_rel_context env) t') -let ast_of_constant env = ast_of_constant_ref (ast_of_constr false env) +let ast_of_constant env (sp,ids) = + let a = ast_of_constant_ref sp in + if !print_arguments then + ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) + else a -let ast_of_existential env = ast_of_existential_ref (ast_of_constr false env) +let ast_of_existential env (ev,ids) = + let a = ast_of_existential_ref ev in + if !print_arguments or !print_evar_arguments then + ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) + else a -let ast_of_inductive env = ast_of_inductive_ref (ast_of_constr false env) +let ast_of_constructor env (cstr_sp,ids) = + let a = ast_of_constructor_ref cstr_sp in + if !print_arguments then + ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) + else a -let ast_of_constructor env = ast_of_constructor_ref (ast_of_constr false env) +let ast_of_inductive env (ind_sp,ids) = + let a = ast_of_inductive_ref ind_sp in + if !print_arguments then + ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids)) + else a let rec ast_of_pattern env = function - | PRef ref -> ast_of_ref (fun c -> ast_of_raw (Detyping.detype [] env c)) ref + | PRef ref -> ast_of_ref ref | PVar id -> ast_of_ident id + | PEvar n -> ast_of_existential_ref n + | PRel n -> (try match lookup_name_of_rel n env with | Name id -> ast_of_ident id diff --git a/parsing/termast.mli b/parsing/termast.mli index 4b689ead0..1d6ee2208 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -26,7 +26,7 @@ val ast_of_constant : env -> constant -> Coqast.t val ast_of_existential : env -> existential -> Coqast.t val ast_of_constructor : env -> constructor -> Coqast.t val ast_of_inductive : env -> inductive -> Coqast.t -val ast_of_ref : ('a -> Coqast.t) -> global_reference -> Coqast.t +val ast_of_ref : global_reference -> Coqast.t val ast_of_qualid : qualid -> Coqast.t (* For debugging *) |