X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=c5bbfff78b34d658e347e817d84c0857d8b0aae5;hb=08e9d02504942642a917c0d3e4b4795e65172d89;hp=89d3d00b410b10c92495716812a8b12cf2423ef9;hpb=c465c17581bf606e0330cbd89b238279c184ad35;p=helm.git diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index 89d3d00b4..c5bbfff78 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -300,20 +300,13 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes C.ALambda (fresh_id'',n, aux' context idrefs s, aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) - | C.LetIn (n,s,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 + | C.LetIn (n,s,ty,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,Some s_ty)))::context) (fresh_id''::idrefs) t) + (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty, + aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t) | C.Appl l -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -429,12 +422,21 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids Hashtbl.add ids_to_hypotheses hid binding ; incr hypotheses_seed ; match binding with - Some (n,Cic.Def (t,_)) -> - let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in - Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) - (Some hid); - (binding::context), - ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs) + Some (n,Cic.Def (t,ty)) -> + let acic = + acic_of_cic_context ~computeinnertypes context idrefs t + None in + let acic2 = + acic_of_cic_context ~computeinnertypes context idrefs ty + None + in + Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) + (Some hid); + Hashtbl.replace ids_to_father_ids + (CicUtil.id_of_annterm acic2) (Some hid); + (binding::context), + ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext), + (hid::idrefs) | Some (n,Cic.Decl t) -> let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) @@ -469,10 +471,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = None -> None | Some (n, Cic.Decl t)-> Some (n, Cic.Decl (Unshare.unshare t)) - | Some (n, Cic.Def (t,None)) -> - Some (n, Cic.Def ((Unshare.unshare t),None)) - | Some (n,Cic.Def (bo,Some ty)) -> - Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty))) + | Some (n,Cic.Def (bo,ty)) -> + Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty)) in d::canonical_context' ) canonical_context [] @@ -508,30 +508,30 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = let aconjecture_of_conjecture' = aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed in - let eta_fix metasenv context t = + let eta_fix_and_unshare metasenv context t = let t = if eta_fix then E.eta_fix metasenv context t else t in Unshare.unshare t in let aobj = match obj with C.Constant (id,Some bo,ty,params,attrs) -> - let bo' = (*eta_fix [] []*) bo in - let ty' = eta_fix [] [] ty in + let bo' = (*eta_fix_and_unshare[] [] bo*) Unshare.unshare bo in + let ty' = eta_fix_and_unshare [] [] 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 C.AConstant ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs) | C.Constant (id,None,ty,params,attrs) -> - let ty' = eta_fix [] [] ty in + let ty' = eta_fix_and_unshare [] [] ty in let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in C.AConstant ("mettereaposto",None,id,None,aty,params,attrs) | C.Variable (id,bo,ty,params,attrs) -> - let ty' = eta_fix [] [] ty in + let ty' = eta_fix_and_unshare [] [] ty in let abo = match bo with None -> None | Some bo -> - let bo' = eta_fix [] [] bo in + let bo' = eta_fix_and_unshare [] [] bo in Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty')) in let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in @@ -548,16 +548,17 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = match d with None -> None | Some (n, C.Decl t)-> - Some (n, C.Decl (eta_fix conjectures canonical_context' t)) - | Some (n, C.Def (t,None)) -> + Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t)) + | Some (n, C.Def (t,ty)) -> Some (n, - C.Def ((eta_fix conjectures canonical_context' t),None)) - | Some (_,C.Def (_,Some _)) -> assert false + C.Def + (eta_fix_and_unshare conjectures canonical_context' t, + eta_fix_and_unshare conjectures canonical_context' ty)) in d::canonical_context' ) canonical_context [] in - let term' = eta_fix conjectures canonical_context' term in + let term' = eta_fix_and_unshare conjectures canonical_context' term in (i,canonical_context',term') ) conjectures in @@ -573,7 +574,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = conjectures' in (* let bo' = eta_fix conjectures' [] bo in *) let bo' = bo in - let ty' = eta_fix conjectures' [] ty in + let ty' = eta_fix_and_unshare conjectures' [] ty in (* let time2 = Sys.time () in prerr_endline @@ -667,10 +668,10 @@ let plain_acic_term_of_cic_term = C.ALambda (fresh_id,n, aux context s, aux ((fresh_id, Some (n, C.Decl s))::context) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> C.ALetIn - (fresh_id, n, aux context s, - aux ((fresh_id, Some (n, C.Def(s,None)))::context) t) + (fresh_id, n, aux context s, aux context ty, + aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t) | C.Appl l -> C.AAppl (fresh_id, List.map (aux context) l) | C.Const (uri,exp_named_subst) ->