X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=98b14298274542288534df848c3bedf4303fa78d;hb=ac1f50b898154dc3d74aa8fa2fff212a7d3a235c;hp=e1c964c76073ac21388a1abf79ee9968c0c45e23;hpb=6a4cf39f4ad37545b33db31f3610d960375ce2a5;p=helm.git diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index e1c964c76..98b142982 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -135,7 +135,6 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes prerr_endline ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ; *) - let time = ref 0. in let rec aux computeinnertypes father context idrefs tt = let fresh_id'' = fresh_id' father tt in (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) @@ -302,12 +301,19 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes (fresh_id'',n, aux' context idrefs s, aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) | C.LetIn (n,s,t) -> - xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = `Prop then - add_inner_type fresh_id'' ; - C.ALetIn - (fresh_id'', n, aux' context idrefs s, - aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t) + let s_ty = + try + (cic_CicHash_find terms_to_types s).D.synthesized + with + Not_found -> + cicReduction_whd context (xxx_type_of_aux' metasenv context s); + in + xxx_add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = `Prop then + add_inner_type fresh_id'' ; + C.ALetIn + (fresh_id'', n, aux' context idrefs s, + aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t) | C.Appl l -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -347,8 +353,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes let fresh_idrefs = List.map (function _ -> gen_id seed) funs in let new_idrefs = List.rev fresh_idrefs @ idrefs in - let tys = - List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -364,8 +374,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes let fresh_idrefs = List.map (function _ -> gen_id seed) funs in let new_idrefs = List.rev fresh_idrefs @ idrefs in - let tys = - List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -386,9 +400,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ; res *) - let res = aux global_computeinnertypes None context idrefs t in - prerr_endline (">>>> aux : " ^ string_of_float !time); - res + aux global_computeinnertypes None context idrefs t ;; let acic_of_cic_context ~computeinnertypes metasenv context idrefs t = @@ -477,7 +489,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)) ;; -let acic_object_of_cic_object ?(eta_fix=true) obj = +let acic_object_of_cic_object ?(eta_fix=false) obj = let module C = Cic in let module E = Eta_fixing in let ids_to_terms = Hashtbl.create 503 in @@ -502,7 +514,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = let aobj = match obj with C.Constant (id,Some bo,ty,params,attrs) -> - let bo' = eta_fix [] [] bo in + let bo' = (*eta_fix [] []*) bo in let ty' = eta_fix [] [] ty in let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in @@ -559,8 +571,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = = aconjecture_of_conjecture' conjectures conjecture in (cid,i,acanonical_context,aterm)) conjectures' in -(* let time1 = Sys.time () in *) - let bo' = eta_fix conjectures' [] bo in + (* let bo' = eta_fix conjectures' [] bo in *) + let bo' = bo in let ty' = eta_fix conjectures' [] ty in (* let time2 = Sys.time () in @@ -683,9 +695,12 @@ let plain_acic_term_of_cic_term = C.AMutCase (fresh_id, uri, tyno, aux context outty, aux context term, List.map (aux context) patterns) | C.Fix (funno, funs) -> - let tys = - List.map - (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types, + len+1 + ) ([],0) funs in C.AFix (fresh_id, funno, List.map2 @@ -694,9 +709,12 @@ let plain_acic_term_of_cic_term = ) tys funs ) | C.CoFix (funno, funs) -> - let tys = - List.map (fun (name,ty,_) -> - mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types, + len+1 + ) ([],0) funs in C.ACoFix (fresh_id, funno, List.map2