X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8;hb=8dbc4dcef7328f3ac84f847255e9be8d47c1de6d;hp=bb00476b97b73faf25e2fed68d891855c3a06aaf;hpb=07c5372510a5abecd788aa0b500e5deaa548c9d4;p=helm.git diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index bb00476b9..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 @@ -511,6 +514,19 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = 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) -> @@ -549,10 +565,11 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = None -> None | Some (n, C.Decl t)-> Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t)) - | Some (n, C.Def (t,None)) -> + | Some (n, C.Def (t,ty)) -> Some (n, - C.Def ((eta_fix_and_unshare 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 [] @@ -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 ())