From 6248703e9f479d4c3edfcf227908ffd9d2dd7adc Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 Jul 2003 15:42:19 +0000 Subject: [PATCH] Few modif in eta-fixing. --- helm/ocaml/cic_omdoc/cic2content.ml | 37 ++++-- helm/ocaml/cic_omdoc/contentPp.ml | 12 +- helm/ocaml/cic_omdoc/contentPp.mli | 2 + helm/ocaml/cic_omdoc/eta_fixing.ml | 171 +++++++++++++++++++--------- 4 files changed, 157 insertions(+), 65 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 21b39fe65..0933dbc4b 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -257,10 +257,10 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = }; } else - { K.proof_name = None ; + { K.proof_name = inner_proof.K.proof_name; K.proof_id = gen_id seed; K.proof_context = [] ; - K.proof_apply_context = [inner_proof]; + K.proof_apply_context = [{inner_proof with K.proof_name = None}]; K.proof_conclude = { K.conclude_id = gen_id seed; K.conclude_aref = id; @@ -436,15 +436,27 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in + (match name_of n with + Some "w" -> prerr_endline ("build_def: " ^ sort ); + | _ -> ()); if sort = "Prop" then - `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + (prerr_endline ("entro"); + let p = + (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + in + (match p.K.proof_name with + Some "w" -> prerr_endline ("TUTTO BENE:"); + | Some s -> prerr_endline ("mi chiamo " ^ s); + | _ -> prerr_endline ("ho perso il nome");); + prerr_endline ("esco"); `Proof p;) else + (prerr_endline ("siamo qui???"); `Definition { K.def_name = name_of n; K.def_id = gen_id seed; K.def_aref = id; K.def_term = t - } + }) with Not_found -> assert false @@ -500,7 +512,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = else raise Not_a_proof | C.ALetIn (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = "Prop" then let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then @@ -686,6 +698,10 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = with Not_found -> -1) in if n<0 then raise NotApplicable else + let method_name = + if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then + "Exists" + else "ByInduction" in let prefix = String.sub uri_str 0 n in let ind_str = (prefix ^ ".ind") in let ind_uri = UriManager.uri_of_string ind_str in @@ -700,7 +716,10 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = if n = 0 then ([],l) else let p,a = split (n-1) (List.tl l) in ((List.hd l::p),a) in - let params_and_IP,tail_args = split (noparams+1) args in + let params_and_IP,tail_args = split (noparams+1) args in + if method_name = "Exists" then + (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args)); + prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args))); let constructors = (match inductive_types with [(_,_,_,l)] -> l @@ -767,14 +786,14 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = hdarg::(build_method_args (tlc,tla)) | _ -> assert false in build_method_args (constructors1,args_for_cases) in - { K.proof_name = None; + { K.proof_name = name; K.proof_id = gen_id seed; K.proof_context = []; K.proof_apply_context = serialize seed subproofs; K.proof_conclude = { K.conclude_id = gen_id seed; K.conclude_aref = id; - K.conclude_method = "ByInduction"; + K.conclude_method = method_name; K.conclude_args = K.Aux (string_of_int no_constructors) ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP)) @@ -819,7 +838,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = else K.Term a in hd::(ma_aux (n-1) tl) in (ma_aux 3 args) in - { K.proof_name = None; + { K.proof_name = name; K.proof_id = gen_id seed; K.proof_context = []; K.proof_apply_context = serialize seed subproofs; diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml index 58ba4873b..3967c6216 100644 --- a/helm/ocaml/cic_omdoc/contentPp.ml +++ b/helm/ocaml/cic_omdoc/contentPp.ml @@ -139,7 +139,17 @@ and parg indent = | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!") ;; -let print_proof p = pproof p 0; +let print_proof p = pproof p 0;; + +let print_obj (_,_,_,obj) = + match obj with + `Decl (_,decl) -> + pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element) + | `Def (_,_,def) -> + pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element) + | `Joint _ as jo -> pcontext_element 0 jo +;; + diff --git a/helm/ocaml/cic_omdoc/contentPp.mli b/helm/ocaml/cic_omdoc/contentPp.mli index 85ce238f3..a160ab1ff 100644 --- a/helm/ocaml/cic_omdoc/contentPp.mli +++ b/helm/ocaml/cic_omdoc/contentPp.mli @@ -25,4 +25,6 @@ val print_proof: Cic.annterm Content.proof -> unit +val print_obj: Cic.annterm Content.cobj -> unit +val parg: int -> Cic.annterm Content.arg ->unit diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index c3b84b605..8407f8357 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -27,83 +27,138 @@ exception ReferenceToVariable;; exception RferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +(* let rec fix_lambdas_wrt_type ty te = let module C = Cic in let module S = CicSubstitution in -(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); - flush stderr ; *) - (* cast e altra porcheria ???? *) +(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *) + match ty with + C.Prod (_,_,ty') -> + (match CicReduction.whd [] te with + C.Lambda (n,s,te') -> + C.Lambda (n,s,fix_lambdas_wrt_type ty' te') + | t -> + let rec get_sources = + function + C.Prod (_,s,ty) -> s::(get_sources ty) + | _ -> [] in + let sources = get_sources ty in + let no_sources = List.length sources in + let rec mk_rels n shift = + if n = 0 then [] + else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in + let t' = S.lift no_sources t in + let t2 = + match t' with + C.Appl l -> + C.LetIn + (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1))) + | _ -> + C.Appl (t'::(mk_rels no_sources 0)) in + List.fold_right + (fun source t -> C.Lambda (C.Name "y",source,t)) + sources t2) + | _ -> te +;; *) + +let rec fix_lambdas_wrt_type ty te = + let module C = Cic in + let module S = CicSubstitution in +(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *) + match ty,te with + C.Prod (_,_,ty'), C.Lambda (n,s,te') -> + C.Lambda (n,s,fix_lambdas_wrt_type ty' te') + | C.Prod (_,s,ty'), t -> + let rec get_sources = + function + C.Prod (_,s,ty) -> s::(get_sources ty) + | _ -> [] in + let sources = get_sources ty in + let no_sources = List.length sources in + let rec mk_rels n shift = + if n = 0 then [] + else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in + let t' = S.lift no_sources t in + let t2 = + match t' with + C.Appl l -> + C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1))) + | _ -> C.Appl (t'::(mk_rels no_sources 0)) in + List.fold_right + (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2 + | _, _ -> te +;; + +(* +let rec fix_lambdas_wrt_type ty te = + let module C = Cic in + let module S = CicSubstitution in +(* prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *) match ty,te with C.Prod (_,_,ty'), C.Lambda (n,s,te') -> C.Lambda (n,s,fix_lambdas_wrt_type ty' te') + | C.Prod (_,s,ty'), ((C.Appl (C.Const _ ::_)) as t) -> + (* const have a fixed arity *) + (* prerr_endline ("******** fl - eta expansion 0: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *) + let t' = S.lift 1 t in + C.Lambda (C.Name "x",s, + C.LetIn + (C.Name "H", fix_lambdas_wrt_type ty' t', + C.Appl [C.Rel 1;C.Rel 2])) | C.Prod (_,s,ty'), C.Appl l -> - prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); - flush stderr ; + (* prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *) let l' = List.map (S.lift 1) l in C.Lambda (C.Name "x",s, fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1]))) | C.Prod (_,s,ty'), _ -> - prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); + (* prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *) flush stderr ; let te' = S.lift 1 te in C.Lambda (C.Name "x",s, fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1])) | _, _ -> te -;; +;;*) let fix_according_to_type ty hd tl = let module C = Cic in let module S = CicSubstitution in - let rec aux ty tl res = - (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); - flush stderr ; *) - match ty with - C.Rel _ - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit -> + let rec count_prods = + function + C.Prod (_,_,t) -> 1 + (count_prods t) + | _ -> 0 in + let expected_arity = count_prods ty in + let rec aux n ty tl res = + if n = 0 then (match tl with [] -> C.Appl res - | _ -> - prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); - flush stderr ; - C.LetIn - (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) - | C.Cast (v,t) -> aux v tl res - | C.Prod (n,s,t) -> - (match tl with - [] -> - prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); - flush stderr ; - let res' = List.map (S.lift 1) res - in + | _ -> + match res with + [] -> assert false + | [a] -> C.Appl (a::tl) + | _ -> + (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *) + C.LetIn + (C.Name "H", + C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) + else + let name,source,target = + (match ty with + C.Prod (C.Name _ as n,s,t) -> n,s,t + | C.Prod (C.Anonymous, s,t) -> C.Name "z",s,t + | _ -> (* prods number may only increase for substitution *) + assert false) in + match tl with + [] -> + (* prerr_endline ("******* too few args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *) + let res' = List.map (S.lift 1) res in C.Lambda - (C.Name "x", (* Andrea: to do: generate a fresh name *) - s, - aux t [] (res'@[C.Rel 1])) + (name, source, aux (n-1) target [] (res'@[C.Rel 1])) | hd::tl' -> - let hd' = fix_lambdas_wrt_type s hd - in - aux (S.subst hd' t) tl' (res@[hd'])) - | C.Lambda _ -> assert false - | C.LetIn (n,s,t) -> aux (S.subst s t) tl res - | C.Appl _ - | C.Const _ - | C.MutInd _ - | C.MutConstruct _ - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> (* ???? *) - (match tl with - [] -> C.Appl res - | _ -> (* Andrea: to do: generate a fresh name *) - C.LetIn - (C.Name "H", - C.Appl res, - C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) - in - aux ty tl [hd] + let hd' = fix_lambdas_wrt_type source hd in + (* (prerr_endline ("++++++prima :" ^(CicPp.ppterm hd)); + prerr_endline ("++++++dopo :" ^(CicPp.ppterm hd'))); *) + aux (n-1) (S.subst hd' target) tl' (res@[hd']) in + aux expected_arity ty tl [hd] ;; let eta_fix metasenv t = @@ -139,7 +194,7 @@ let eta_fix metasenv t = | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t) | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t) | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t) - | C.Appl l -> + | C.Appl l as appl -> let l' = List.map eta_fix' l in (match l' with @@ -152,7 +207,11 @@ let eta_fix metasenv t = | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) in - fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' + let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in + if not (CicReduction.are_convertible [] appl result) then + (prerr_endline ("prima :" ^(CicPp.ppterm appl)); + prerr_endline ("dopo :" ^(CicPp.ppterm result))); + result | _ -> C.Appl l' ) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -189,3 +248,5 @@ let eta_fix metasenv t = eta_fix' t ;; + + -- 2.39.2