(* $Id$ *) open Pp open Util open Univ open Names open Generic open Term open Inductive open Sign open Declare open Impargs open Coqast open Ast open Rawterm (* In this file, we translate constr to ast, in order to print constr *) (**********************************************************************) (* conversion of references *) let ids_of_ctxt cl = List.map (function | VAR id -> id | Rel n -> warning "ids_of_ctxt: rel"; id_of_string ("REL "^(string_of_int n)) | _-> anomaly"ids_of_ctxt") (Array.to_list cl) let ast_of_ident id = nvar (string_of_id id) let ast_of_constructor (((sp,tyi),n),ids) = ope("MUTCONSTRUCT", (path_section dummy_loc sp)::(num tyi)::(num n) ::(List.map ast_of_ident ids)) let ast_of_mutind ((sp,tyi),ids) = ope("MUTIND", (path_section dummy_loc sp)::(num tyi)::(List.map ast_of_ident ids)) let ast_of_ref = function | RConst (sp,idl) -> ope("CONST", (path_section dummy_loc sp)::(List.map ast_of_ident idl)) | RAbst (sp) -> ope("ABST", (path_section dummy_loc sp) ::(List.map ast_of_ident (* on triche *) [])) | RInd (ind,idl) -> ast_of_mutind(ind,idl) | RConstruct (cstr,idl) -> ast_of_constructor (cstr,idl) | RVar id -> nvar (string_of_id id) | REVar (ev,idl) -> ope("EVAR", (num ev)::(List.map ast_of_ident idl)) | RMeta n -> ope("META",[num n]) (**********************************************************************) (* conversion of patterns *) let rec ast_of_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) -> ope("PATTCONSTRUCT", (ast_of_constructor cstr)::List.map ast_of_pattern args) | PatAs(loc,id,p) -> ope("PATTAS",[nvar (string_of_id id); ast_of_pattern p]) (* Nouvelle version de renommage des variables (DEC 98) *) (* This is the algorithm to display distinct bound variables - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste des noms à éviter - Règle 2 : c'est la dépendance qui décide si on affiche ou pas Exemple : si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b) mais f et f0 contribue à la liste des variables à éviter (en supposant que les noms f et f0 ne sont pas déjà pris) Intérêt : noms homogènes dans un but avant et après Intro *) type used_idents = identifier list (* let concrete_name (lo,l as ll) n c = if n = Anonymous then if dependent (Rel 1) c then anomaly "Anonymous should be non dependent" else (None,ll) else let l' = match lo with None -> l | Some l0 -> l0@l in let fresh_id = next_name_away n l' in let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in (idopt, (lo,fresh_id::l)) *) let occur_id env id0 c = let rec occur n = function | VAR id -> id=id0 | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) | DOPN (Abst sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) | DOPN (MutInd _, cl) as t -> (basename (mind_path t) = id0) or (array_exists (occur n) cl) | DOPN (MutConstruct _, cl) as t -> (basename (mind_path t) = id0) or (array_exists (occur n) cl) | DOPN(_,cl) -> array_exists (occur n) cl | DOP1(_,c) -> occur n c | DOP2(_,c1,c2) -> (occur n c1) or (occur n c2) | DOPL(_,cl) -> List.exists (occur n) cl | DLAM(_,c) -> occur (n+1) c | DLAMV(_,v) -> array_exists (occur (n+1)) v | Rel p -> p>n & (try (fst (lookup_rel (p-n) env) = Name id0) with Not_found -> false) (* Unbound indice : may happen in debug *) | DOP0 _ -> false in occur 1 c let next_name_not_occuring name l env t = let rec next id = if List.mem id l or occur_id env id t then next (lift_ident id) else id in match name with | Name id -> next id | Anonymous -> id_of_string "_" let concrete_name l env n c = if n = Anonymous then begin if dependent (Rel 1) c then anomaly "Anonymous should be non dependent"; (None,l) end else let fresh_id = next_name_not_occuring n l env c in let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in (idopt, fresh_id::l) (* Returns the list of global variables and constants in a term *) let global_vars_and_consts t = let rec collect acc = function | VAR id -> id::acc | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl) | DOPN (Abst sp,cl) -> (basename sp)::(Array.fold_left collect acc cl) | DOPN (MutInd _, cl) as t -> (basename (mind_path t))::(Array.fold_left collect acc cl) | DOPN (MutConstruct _, cl) as t -> (basename (mind_path t))::(Array.fold_left collect acc cl) | DOPN(_,cl) -> Array.fold_left collect acc cl | DOP1(_,c) -> collect acc c | DOP2(_,c1,c2) -> collect (collect acc c1) c2 | DOPL(_,cl) -> List.fold_left collect acc cl | DLAM(_,c) -> collect acc c | DLAMV(_,v) -> Array.fold_left collect acc v | _ -> acc in list_uniquize (collect [] t) let used_of = global_vars_and_consts let ids_of_env = Sign.ids_of_env (****************************************************************************) (* Tools for printing of Cases *) (* These functions implement a light form of Termenv.mind_specif_of_mind *) (* specially for handle Cases printing; they respect arities but not typing *) let indsp_of_id id = let (oper,_) = try let sp = Nametab.sp_of_id CCI id in global_operator sp id with Not_found -> error ("Cannot find reference "^(string_of_id id)) in match oper with | MutInd(sp,tyi) -> (sp,tyi) | _ -> errorlabstrm "indsp_of_id" [< 'sTR ((string_of_id id)^" is not an inductive type") >] let mind_specif_of_mind_light (sp,tyi) = let mib = Global.lookup_mind sp in (mib,mind_nth_type_packet mib tyi) let rec remove_indtypes = function | (1, DLAMV(_,cl)) -> cl | (n, DLAM (_,c)) -> remove_indtypes (n-1, c) | _ -> anomaly "remove_indtypes: bad list of constructors" let rec remove_params n t = if n = 0 then t else match t with | DOP2(Prod,_,DLAM(_,c)) -> remove_params (n-1) c | DOP2(Cast,c,_) -> remove_params n c | _ -> anomaly "remove_params : insufficiently quantified" let rec get_params = function | DOP2(Prod,_,DLAM(x,c)) -> x::(get_params c) | DOP2(Cast,c,_) -> get_params c | _ -> [] let lc_of_lmis (mib,mip) = let lc = remove_indtypes (mib.mind_ntypes,mip.mind_lc) in Array.map (remove_params mib.mind_nparams) lc let sp_of_spi ((sp,_) as spi) = let (_,mip) = mind_specif_of_mind_light spi in let (pa,_,k) = repr_path sp in make_path pa (mip.mind_typename) k (* Parameterization of the translation from constr to ast *) (* Tables for Cases printing under a "if" form, a "let" form, *) let isomorphic_to_bool lc = let lcparams = Array.map get_params lc in Array.length lcparams = 2 & lcparams.(0) = [] & lcparams.(1) = [] let isomorphic_to_tuple lc = (Array.length lc = 1) module PrintingCasesMake = functor (Test : sig val test : constr array -> bool val error_message : string val member_message : identifier -> bool -> string val field : string val title : string end) -> struct type t = section_path * int let encode = indsp_of_id let check indsp = if not (Test.test (lc_of_lmis (mind_specif_of_mind_light indsp))) then errorlabstrm "check_encode" [< 'sTR Test.error_message >] let decode = sp_of_spi let key = Goptions.SecondaryTable ("Printing",Test.field) let title = Test.title let member_message = Test.member_message let synchronous = true end module PrintingCasesIf = PrintingCasesMake (struct let test = isomorphic_to_bool let error_message = "This type cannot be seen as a boolean type" let field = "If" let title = "Types leading to pretty-printing of Cases using a `if' form: " let member_message id = function | true -> "Cases on elements of " ^ (string_of_id id) ^ " are printed using a `if' form" | false -> "Cases on elements of " ^ (string_of_id id) ^ " are not printed using `if' form" end) module PrintingCasesLet = PrintingCasesMake (struct let test = isomorphic_to_tuple let error_message = "This type cannot be seen as a tuple type" let field = "Let" let title = "Types leading to a pretty-printing of Cases using a `let' form:" let member_message id = function | true -> "Cases on elements of " ^ (string_of_id id) ^ " are printed using a `let' form" | false -> "Cases on elements of " ^ (string_of_id id) ^ " are not printed using a `let' form" end) module PrintingIf = Goptions.MakeTable(PrintingCasesIf) module PrintingLet = Goptions.MakeTable(PrintingCasesLet) (* Options for printing or not wildcard and synthetisable types *) open Goptions let wildcard_value = ref true let force_wildcard () = !wildcard_value let _ = declare_async_bool_option { optasyncname = "the forced wildcard option"; optasynckey = SecondaryTable ("Printing","Wildcard"); optasyncread = force_wildcard; optasyncwrite = (fun v -> wildcard_value := v) } let synth_type_value = ref true let synthetize_type () = !synth_type_value let _ = declare_async_bool_option { optasyncname = "the synthesisablity"; optasynckey = SecondaryTable ("Printing","Synth"); optasyncread = synthetize_type; optasyncwrite = (fun v -> synth_type_value := v) } (* Printing of implicit *) let print_implicits = ref false (**************************************************) (* The main translation function is bdize_depcast *) (* pour les implicites *) (* l est ordonne'ee (croissant), ne garder que les elements <= n *) let filter_until n l = let rec aux = function | [] -> [] | i::l -> if i > n then [] else i::(aux l) in aux l (* l est ordonne'e (de'croissant), n>=max(l), diviser l en deux listes, la 2eme est la plus longue se'quence commencant par n, la 1ere contient les autres elements *) let rec div_implicits n = function | [] -> [],[] | i::l -> if i = n then let l1,l2=(div_implicits (n-1) l) in l1,i::l2 else i::l,[] let bdize_app c al = let impl = match c with | DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp | DOPN(Const sp,_) -> constant_implicits_list sp | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *) | _ -> [] in if impl = [] then ope("APPLIST", al) else if !print_implicits then ope("APPLIST", ope("XTRA",[str "!";List.hd al])::List.tl al) else let largs = List.length al - 1 in let impl = List.rev (filter_until largs impl) in let impl1,impl2=div_implicits largs impl in let al1 = Array.of_list al in List.iter (fun i -> al1.(i) <- ope("XTRA", [str "!"; str "EX"; num i; al1.(i)])) impl2; List.iter (fun i -> al1.(i) <- ope("XTRA",[str "!"; num i; al1.(i)])) impl1; al1.(0) <- ope("XTRA",[str "!"; al1.(0)]); ope("APPLIST",Array.to_list al1) type optioncast = WithCast | WithoutCast (* [reference_tree p] pre-computes the variables and de bruijn occurring in a term to avoid a O(n2) factor when computing dependent each time *) type ref_tree = NODE of (int list * identifier list) * ref_tree list let combine l = let rec combine_rec = function | [] -> [],[] | NODE ((a,b),_)::l -> let a',b' = combine_rec l in (list_union a a',list_union b b') in NODE (combine_rec l,l) let rec reference_tree p = function | VAR id -> NODE (([],[id]),[]) | Rel n -> NODE (([n-p],[]),[]) | DOP0 op -> NODE (([],[]),[]) | DOP1(op,c) -> reference_tree p c | DOP2(op,c1,c2) -> combine [reference_tree p c1;reference_tree p c2] | DOPN(op,cl) -> combine (List.map (reference_tree p) (Array.to_list cl)) | DOPL(op,cl) -> combine (List.map (reference_tree p) cl) | DLAM(na,c) -> reference_tree (p+1) c | DLAMV(na,cl) -> combine (List.map (reference_tree (p+1))(Array.to_list cl)) (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) let computable p k = (* We first remove as many lambda as the arity, then we look if it remains a lambda for a dependent elimination. This function works for normal eta-expanded term. For non eta-expanded or non-normal terms, it may affirm the pred is synthetisable because of an undetected ultimate dependent variable in the second clause, or else, it may affirms the pred non synthetisable because of a non normal term in the fourth clause. A solution could be to store, in the MutCase, the eta-expanded normal form of pred to decide if it depends on its variables Lorsque le prédicat est dépendant de manière certaine, on ne déclare pas le prédicat synthétisable (même si la variable dépendante ne l'est pas effectivement) parce que sinon on perd la réciprocité de la synthèse (qui, lui, engendrera un prédicat non dépendant) *) let rec striprec = function | (0,DOP2(Lambda,_,DLAM(_,d))) -> false | (0,d ) -> noccur_bet 1 k d | (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d) | _ -> false in striprec (k,p) (* Main translation function from constr -> ast *) let old_bdize_depcast opcast at_top env t = let init_avoid = if at_top then ids_of_env env else [] in let rec bdrec avoid env t = match collapse_appl t with (* Not well-formed constructions *) | DLAM(na,c) -> (match concrete_name avoid env na c with | (Some id,avoid') -> slam(Some (string_of_id id), bdrec avoid' (add_rel (Name id,()) env) c) | (None,avoid') -> slam(None,bdrec avoid' env (pop c))) | DLAMV(na,cl) -> if not(array_exists (dependent (Rel 1)) cl) then slam(None,ope("V$",array_map_to_list (fun c -> bdrec avoid env (pop c)) cl)) else let id = next_name_away na avoid in slam(Some (string_of_id id), ope("V$", array_map_to_list (bdrec (id::avoid) (add_rel (Name id,()) env)) cl)) (* Well-formed constructions *) | regular_constr -> (match kind_of_term regular_constr with | IsRel n -> (try match fst(lookup_rel n env) with | Name id -> nvar (string_of_id id) | Anonymous -> raise Not_found with Not_found -> ope("REL",[num n])) (* TODO: Change this to subtract the current depth *) | IsMeta n -> ope("META",[num n]) | IsVar id -> nvar (string_of_id id) | IsXtra s -> ope("XTRA",[str s]) | IsSort s -> (match s with | Prop Null -> ope("PROP",[]) | Prop Pos -> ope("SET",[]) | Type u -> ope("TYPE", [path_section dummy_loc u.u_sp; num u.u_num])) | IsCast (c1,c2) -> if opcast=WithoutCast then bdrec avoid env c1 else ope("CAST",[bdrec avoid env c1;bdrec avoid env c2]) | IsProd (Anonymous,ty,c) -> (* Anonymous product are never factorized *) ope("PROD",[bdrec [] env ty; slam(None,bdrec avoid env (pop c))]) | IsProd (Name _ as na,ty,c) -> let (n,a) = factorize_binder 1 avoid env Prod na ty c in (* PROD et PRODLIST doivent être distingués à cause du cas non dépendant, pour isoler l'implication; peut-être un constructeur ARROW serait-il plus justifié ? *) let oper = if n=1 then "PROD" else "PRODLIST" in ope(oper,[bdrec [] env ty;a]) | IsLambda (na,ty,c) -> let (_,a) = factorize_binder 1 avoid env Lambda na ty c in (* LAMBDA et LAMBDALIST se comportent pareil *) ope("LAMBDALIST",[bdrec [] env ty;a]) | IsAppL (f,args) -> bdize_app f (List.map (bdrec avoid env) (f::args)) | IsConst (sp,cl) -> ope("CONST",((path_section dummy_loc sp):: (array_map_to_list (bdrec avoid env) cl))) | IsEvar (ev,cl) -> ope("EVAR",((num ev):: (array_map_to_list (bdrec avoid env) cl))) | IsAbst (sp,cl) -> ope("ABST",((path_section dummy_loc sp):: (array_map_to_list (bdrec avoid env) cl))) | IsMutInd (sp,tyi,cl) -> ope("MUTIND",((path_section dummy_loc sp)::(num tyi):: (array_map_to_list (bdrec avoid env) cl))) | IsMutConstruct (sp,tyi,n,cl) -> ope("MUTCONSTRUCT", ((path_section dummy_loc sp)::(num tyi)::(num n):: (array_map_to_list (bdrec avoid env) cl))) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = bdrec avoid env c in begin match annot with | None -> (* Pas d'annotation --> affichage avec vieux Case *) let pred = bdrec avoid env p in let bl' = array_map_to_list (bdrec avoid env) bl in ope("MUTCASE",pred::tomatch::bl') | Some indsp -> let (mib,mip as lmis) = mind_specif_of_mind_light indsp in let lc = lc_of_lmis lmis in let lcparams = Array.map get_params lc in let k = (nb_prod mip.mind_arity.body) - mib.mind_nparams in let pred = if synth_type & computable p k & lcparams <> [||] then (str "SYNTH") else bdrec avoid env p in if PrintingIf.active indsp then ope("FORCEIF", [ pred; tomatch; bdrec avoid env bl.(0); bdrec avoid env bl.(1) ]) else let idconstructs = mip.mind_consnames in let asttomatch = ope("TOMATCH", [tomatch]) in let eqnv = array_map3 (bdize_eqn avoid env) idconstructs lcparams bl in let eqnl = Array.to_list eqnv in let tag = if PrintingLet.active indsp then "FORCELET" else "MULTCASE" in ope(tag,pred::asttomatch::eqnl) end | IsFix (nv,n,cl,lfn,vt) -> let lfi = List.map (fun na -> next_name_away na avoid) lfn in let def_env = List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in let def_avoid = lfi@avoid in let f = List.nth lfi n in let rec split_lambda binds env avoid = function | (0, t) -> (binds,bdrec avoid env t) | (n, DOP2(Cast,t,_)) -> split_lambda binds env avoid (n,t) | (n, DOP2(Lambda,t,DLAM(na,b))) -> let ast = bdrec avoid env t in let id = next_name_away na avoid in let ast_of_bind = ope("BINDER",[ast;nvar (string_of_id id)]) in let new_env = add_rel (Name id,()) env in split_lambda (ast_of_bind::binds) new_env (id::avoid) (n-1,b) | _ -> error "split_lambda" in let rec split_product env avoid = function | (0, t) -> bdrec avoid env t | (n, DOP2(Cast,t,_)) -> split_product env avoid (n,t) | (n, DOP2(Prod,t,DLAM(na,b))) -> let ast = bdrec avoid env t in let id = next_name_away na avoid in let new_env = add_rel (Name id,()) env in split_product new_env (id::avoid) (n-1,b) | _ -> error "split_product" in let listdecl = list_map_i (fun i fi -> let (lparams,ast_of_def) = split_lambda [] def_env def_avoid (nv.(i)+1,vt.(i)) in let ast_of_typ = split_product env avoid (nv.(i)+1,cl.(i)) in ope("FDECL", [nvar (string_of_id fi); ope ("BINDERS",List.rev lparams); ast_of_typ; ast_of_def ])) 0 lfi in ope("FIX", (nvar (string_of_id f))::listdecl) | IsCoFix (n,cl,lfn,vt) -> let lfi = List.map (fun na -> next_name_away na avoid) lfn in let def_env = List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in let def_avoid = lfi@avoid in let f = List.nth lfi n in let listdecl = list_map_i (fun i fi -> ope("CFDECL", [nvar (string_of_id fi); bdrec avoid env cl.(i); bdrec def_avoid def_env vt.(i)])) 0 lfi in ope("COFIX", (nvar (string_of_id f))::listdecl)) and bdize_eqn avoid env constructid construct_params branch = let print_underscore = force_wildcard () in let cnvar = nvar (string_of_id constructid) in let rec buildrec nvarlist avoid env = function _::l, DOP2(Lambda,_,DLAM(x,b)) -> let x'= if not print_underscore or (dependent (Rel 1) b) then x else Anonymous in let id = next_name_away x' avoid in let new_env = (add_rel (Name id,()) env) in let new_avoid = id::avoid in let new_nvarlist = (nvar (string_of_id id))::nvarlist in buildrec new_nvarlist new_avoid new_env (l,b) | l , DOP2(Cast,b,_) (* Oui, il y a parfois des cast *) -> buildrec nvarlist avoid env (l,b) | x::l, b (* eta-expansion : n'arrivera plus lorsque tous les termes seront construits à partir de la syntaxe Cases *) -> (* nommage de la nouvelle variable *) let id = next_name_away_with_default "x" x avoid in let new_nvarlist = (nvar (string_of_id id))::nvarlist in let new_env = (add_rel (Name id,()) env) in let new_avoid = id::avoid in let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in buildrec new_nvarlist new_avoid new_env (l,new_b) | [] , b -> let pattern = if nvarlist = [] then cnvar else ope ("PATTCONSTRUCT", cnvar::(List.rev nvarlist)) in let action = bdrec avoid env b in ope("EQN", [action; pattern]) in buildrec [] avoid env (construct_params,branch) and factorize_binder n avoid env oper na ty c = let (env2, avoid2,na2) = match concrete_name avoid env na c with (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) | (None,l') -> add_rel (Anonymous,()) env, l', None in let (p,body) = match c with DOP2(oper',ty',DLAM(na',c')) when (oper = oper') & eq_constr (lift 1 ty) ty' & not (na' = Anonymous & oper = Prod) -> factorize_binder (n+1) avoid2 env2 oper na' ty' c' | _ -> (n,bdrec avoid2 env2 c) in (p,slam(na2, body)) in bdrec init_avoid env t let lookup_name_as_renamed env t s = let rec lookup avoid env n = function DOP2(Prod,_,DLAM(name,c')) -> (match concrete_name avoid env name c' with (Some id,avoid') -> if id=s then (Some n) else lookup avoid' (add_rel (Name id,()) env) (n+1) c' | (None,avoid') -> lookup avoid' env (n+1) (pop c')) | DOP2(Cast,c,_) -> lookup avoid env n c | _ -> None in lookup (ids_of_env env) env 1 t let lookup_index_as_renamed t n = let rec lookup n d = function DOP2(Prod,_,DLAM(name,c')) -> (match concrete_name [] (gLOB nil_sign) name c' with (Some _,_) -> lookup n (d+1) c' | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c') | DOP2(Cast,c,_) -> lookup n d c | _ -> None in lookup n 1 t (* Until V6.2.4, similar names were allowed in hypothesis and quantified variables of a goal. *) (* $Id$ *) exception StillDLAM let rec detype t = match collapse_appl t with (* Not well-formed constructions *) | DLAM _ | DLAMV _ -> raise StillDLAM (* Well-formed constructions *) | regular_constr -> (match kind_of_term regular_constr with | IsRel n -> RRel (dummy_loc,n) | IsMeta n -> RRef (dummy_loc,RMeta n) | IsVar id -> RRef (dummy_loc,RVar id) | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr" (* ope("XTRA",((str s):: pl@(List.map detype cl)))*) | IsSort (Prop c) -> RSort (dummy_loc,RProp c) | IsSort (Type _) -> RSort (dummy_loc,RType) | IsCast (c1,c2) -> RCast(dummy_loc,detype c1,detype c2) | IsProd (na,ty,c) -> RBinder (dummy_loc,BProd,na,detype ty,detype c) | IsLambda (na,ty,c) -> RBinder (dummy_loc,BLambda,na,detype ty,detype c) | IsAppL (f,args) -> RApp (dummy_loc,detype f,List.map detype args) | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl)) | IsEvar (ev,cl) -> RRef (dummy_loc,REVar (ev,ids_of_ctxt cl)) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" | IsMutInd (sp,tyi,cl) -> RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl)) | IsMutConstruct (sp,tyi,n,cl) -> RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl)) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype c in begin match annot with | None -> (* Pas d'annotation --> affichage avec vieux Case *) warning "Printing in old Case syntax"; ROldCase (dummy_loc,false,Some (detype p), tomatch,Array.map detype bl) | Some indsp -> let (mib,mip as lmis) = mind_specif_of_mind_light indsp in let lc = lc_of_lmis lmis in let lcparams = Array.map get_params lc in let k = (nb_prod mip.mind_arity.body) - mib.mind_nparams in let pred = if synth_type & computable p k & lcparams <> [||] then None else Some (detype p) in let constructs = Array.init (Array.length mip.mind_consnames) (fun i -> ((indsp,i),[] (* on triche *))) in let eqnv = array_map3 bdize_eqn constructs lcparams bl in let eqnl = Array.to_list eqnv in let tag = if PrintingLet.active indsp then PrintLet else if PrintingIf.active indsp then PrintIf else PrintCases in RCases (dummy_loc,tag,pred,[tomatch],eqnl) end | IsFix (nv,n,cl,lfn,vt) -> let l = Array.of_list (List.map (function Name id -> id | Anonymous -> anomaly"detype") lfn) in RRec(dummy_loc,RFix (nv,n),l,Array.map detype cl, Array.map detype vt) | IsCoFix (n,cl,lfn,vt) -> let l = Array.of_list (List.map (function Name id -> id | Anonymous -> anomaly"detype") lfn) in RRec(dummy_loc,RCofix n,l,Array.map detype cl, Array.map detype vt)) and bdize_eqn constr_id construct_params branch = let avoid = global_vars_and_consts branch in let make_pat x avoid b = if not (force_wildcard ()) or (dependent (Rel 1) b) then let id = next_name_away x avoid in (PatVar (dummy_loc,Name id)),id::avoid,id else PatVar (dummy_loc,Anonymous),avoid,id_of_string "_" in let rec buildrec idl patlist avoid = function | _::l, DOP2(Lambda,_,DLAM(x,b)) -> let pat,new_avoid,id = make_pat x avoid b in buildrec (id::idl) (pat::patlist) new_avoid (l,b) | l , DOP2(Cast,b,_) -> (* Oui, il y a parfois des cast *) buildrec idl patlist avoid (l,b) | x::l, b -> (* eta-expansion : n'arrivera plus lorsque tous les termes seront construits à partir de la syntaxe Cases *) (* nommage de la nouvelle variable *) let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in let pat,new_avoid,id = make_pat x avoid new_b in buildrec (id::idl) (pat::patlist) new_avoid (l,new_b) | [] , rhs -> (idl, [PatCstr(dummy_loc, constr_id, List.rev patlist)], detype rhs) in buildrec [] [] avoid (construct_params,branch) let implicit_of_ref = function | RConstruct (cstrid,_) -> constructor_implicits_list cstrid | RInd (indid,_) -> inductive_implicits_list indid | RConst (sp,_) -> constant_implicits_list sp | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *) | _ -> [] let ast_of_app impl f args = if impl = [] then ope("APPLIST", f::args) else if !print_implicits then ope("APPLISTEXPL", (f::args)) else let largs = List.length args in let impl = List.rev (filter_until largs impl) in let impl1,impl2=div_implicits largs impl in let al1 = Array.of_list args in List.iter (fun i -> al1.(i) <- ope("EXPL", [str "EX"; num i; al1.(i)])) impl2; List.iter (fun i -> al1.(i) <- ope("EXPL",[num i; al1.(i)])) impl1; (* On laisse les implicites, à charge du PP de ne pas les imprimer *) ope("APPLISTEXPL",f::(Array.to_list al1)) let rec ast_of_raw avoid env = function | RRef (_,ref) -> ast_of_ref ref | RRel (_,n) -> (try match fst (lookup_rel n env) with | Name id -> ast_of_ident id | Anonymous -> anomaly "ast_of_raw: index to an anonymous variable" with Not_found -> ope("REL",[num (n - List.length (get_rels env))])) | RApp (_,f,args) -> let astf = ast_of_raw avoid env f in let astargs = List.map (ast_of_raw avoid env ) args in (match f with | RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs | _ -> ast_of_app [] astf astargs) | RBinder (_,BProd,Anonymous,t,c) -> (* Anonymous product are never factorized *) ope("PROD",[ast_of_raw avoid env t; slam(None,ast_of_raw avoid (add_rel (Anonymous,()) env) c)]) | RBinder (_,bk,na,t,c) -> let (n,a) = factorize_binder 1 avoid env bk na t c in let tag = match bk with (* LAMBDA et LAMBDALIST se comportent pareil *) | BLambda -> "LAMBDALIST" (* PROD et PRODLIST doivent être distingués à cause du cas *) (* non dépendant, pour isoler l'implication; peut-être un *) (* constructeur ARROW serait-il plus justifié ? *) | BProd -> if n=1 then "PROD" else "PROLIST" in ope(tag,[ast_of_raw [] env t;a]) | RCases (_,printinfo,typopt,tml,eqns) -> let pred = ast_of_rawopt avoid env typopt in let tag = match printinfo with | PrintIf -> "FORCEIF" | PrintLet -> "FORCELET" | PrintCases -> "MULTCASE" in let asttomatch = ope("TOMATCH", List.map (ast_of_raw avoid env) tml) in let asteqns = List.map (ast_of_eqn avoid env) eqns in ope(tag,pred::asttomatch::asteqns) | ROldCase (_,isrec,typopt,tm,bv) -> warning "Old Case syntax"; ope("MUTCASE",(ast_of_rawopt avoid env typopt) ::(ast_of_raw avoid env tm) ::(Array.to_list (Array.map (ast_of_raw avoid env) bv))) | RRec (_,fk,idv,tyv,bv) -> let lfi = Array.map (fun id -> next_ident_away id avoid) idv in let alfi = Array.map ast_of_ident lfi in let def_avoid = (Array.to_list lfi)@avoid in let def_env = List.fold_left (fun env id -> add_rel (Name id,()) env) env (Array.to_list lfi) in (match fk with | RFix (nv,n) -> let rec split_lambda binds avoid env = function | (0, t) -> (binds,ast_of_raw avoid env t) | (n, RBinder(_,BLambda,na,t,b)) -> let ast = ast_of_raw avoid env t in let id = next_name_away na avoid in let bind = ope("BINDER",[ast;ast_of_ident id]) in split_lambda (bind::binds) (id::avoid) (add_rel (na,()) env) (n-1,b) | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in let rec split_product avoid env = function | (0, t) -> ast_of_raw avoid env t | (n, RBinder(_,BProd,na,t,b)) -> let id = next_name_away na avoid in split_product (id::avoid) (add_rel (na,()) env) (n-1,b) | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in let listdecl = Array.mapi (fun i fi -> let (lparams,astdef) = split_lambda [] avoid def_env (nv.(i)+1,bv.(i)) in let asttyp = split_product avoid env (nv.(i)+1,tyv.(i)) in ope("FDECL", [fi; ope ("BINDERS",List.rev lparams); asttyp; astdef])) alfi in ope("FIX", alfi.(n)::(Array.to_list listdecl)) | RCofix n -> let listdecl = Array.mapi (fun i fi -> ope("CFDECL", [fi; ast_of_raw avoid env tyv.(i); ast_of_raw def_avoid def_env bv.(i)])) alfi in ope("COFIX", alfi.(n)::(Array.to_list listdecl))) | RSort (_,s) -> (match s with | RProp Null -> ope("PROP",[]) | RProp Pos -> ope("SET",[]) | RType -> ope("TYPE",[])) | RHole _ -> ope("ISEVAR",[]) | RCast (_,c,t) -> ope("CAST",[ast_of_raw avoid env c;ast_of_raw avoid env t]) and ast_of_eqn avoid env (idl,pl,c) = let new_env = List.fold_left (fun env id -> add_rel (Name id,()) env) env idl in let rhs = ast_of_raw avoid new_env c in ope("EQN", rhs::(List.map ast_of_pattern pl)) and ast_of_rawopt avoid env = function | None -> (str "SYNTH") | Some p -> ast_of_raw avoid env p and factorize_binder n avoid env oper na ty c = let (env2, avoid2,na2) = match weak_concrete_name avoid env na c with | (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) | (None,l') -> add_rel (Anonymous,()) env, l', None in let (p,body) = match c with RBinder(_,oper',na',ty',c') when (oper = oper') & (ast_of_raw avoid env ty) = (ast_of_raw avoid (add_rel (na,()) env) ty') & not (na' = Anonymous & oper = BProd) -> factorize_binder (n+1) avoid2 env2 oper na' ty' c' | _ -> (n,ast_of_raw avoid2 env2 c) in (p,slam(na2, body)) (* A brancher sur le vrai concrete_name *) and weak_concrete_name avoid env na c = match na with | Anonymous -> (None,avoid) | Name id -> (Some id,avoid) let bdize_no_casts at_top env t = try let avoid = if at_top then ids_of_env env else [] in ast_of_raw avoid env (detype t) with StillDLAM -> old_bdize_depcast WithoutCast at_top env t (* En attendant que strong aille dans term.ml *) let rec strong whdfun t = match whdfun t with | DOP0 _ as t -> t (* Cas ad hoc *) | DOP1(oper,c) -> DOP1(oper,strong whdfun c) | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2) | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl) | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl) | DLAM(na,c) -> DLAM(na,strong whdfun c) | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c) | VAR _ as t -> t | Rel _ as t -> t let bdize at_top env t = bdize_no_casts at_top env (strong strip_outer_cast t) let ast_of_rawconstr = ast_of_raw []