X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8;hb=8ed18544e1591dd3068e2d9095b05d0c4349209c;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..3285dcc15 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -25,19 +25,22 @@ (* $Id$ *) -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string] let string_of_sort = function | `Prop -> "Prop" | `Set -> "Set" - | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) - | `CProp -> "CProp" + | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) + | `NType s -> "Type[" ^ s ^ "]" + | `NCProp s -> "CProp[" ^ s ^ "]" + | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u) + let sort_of_sort = function | Cic.Prop -> `Prop | Cic.Set -> `Set | Cic.Type u -> `Type u - | Cic.CProp -> `CProp + | Cic.CProp u -> `CProp u (* let hashtbl_add_time = ref 0.0;; *) @@ -49,11 +52,11 @@ let xxx_add h k v = let xxx_type_of_aux' m c t = let res,_ = try - CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph with | CicTypeChecker.AssertFailure _ | CicTypeChecker.TypeCheckerFailure _ -> - Cic.Sort Cic.Prop, CicUniv.empty_ugraph + Cic.Sort Cic.Prop, CicUniv.oblivion_ugraph in res ;; @@ -149,7 +152,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes | C.Sort C.Set -> `Set | C.Sort (C.Type u) -> `Type u | C.Meta _ -> `Type (CicUniv.fresh()) - | C.Sort C.CProp -> `CProp + | C.Sort (C.CProp u) -> `CProp u | t -> prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ; assert false @@ -300,20 +303,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 +425,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 +474,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 [] @@ -489,7 +492,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=false) obj = +let acic_term_or_object_of_cic_term_or_object ?(eta_fix=false) () = let module C = Cic in let module E = Eta_fixing in let ids_to_terms = Hashtbl.create 503 in @@ -508,30 +511,43 @@ 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 + (fun context t -> + let map = function + | None -> None + | Some (n, C.Decl ty) -> Some (n, C.Decl (Unshare.unshare ty)) + | Some (n, C.Def (bo, ty)) -> + Some (n, C.Def (Unshare.unshare bo, Unshare.unshare ty)) + in + let t = Unshare.unshare t in + let context = List.map map context in + let idrefs = List.map (function _ -> gen_id seed) context in + let t = acic_term_of_cic_term_context' ~computeinnertypes:true [] context idrefs t None in + t, ids_to_inner_sorts, ids_to_inner_types + ),(function obj -> 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 +564,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 +590,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 @@ -631,7 +648,10 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = in aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, ids_to_conjectures,ids_to_hypotheses -;; +);; + +let acic_object_of_cic_object ?eta_fix = + snd (acic_term_or_object_of_cic_term_or_object ?eta_fix ()) let plain_acic_term_of_cic_term = let module C = Cic in @@ -667,10 +687,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) -> @@ -772,3 +792,6 @@ let plain_acic_object_of_cic_object obj = in C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs) ;; + +let acic_term_of_cic_term ?eta_fix = + fst (acic_term_or_object_of_cic_term_or_object ?eta_fix ())