X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;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..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 ;; @@ -82,16 +85,16 @@ let fresh_id seed ids_to_terms ids_to_father_ids = let source_id_of_id id = "#source#" ^ id;; -exception NotEnoughElements;; +exception NotEnoughElements of string;; (*CSC: cut&paste da cicPp.ml *) (* get_nth l n returns the nth element of the list l if it exists or *) (* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = +let rec get_nth msg l n = match (n,l) with (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements + | (n, he::tail) when n > 1 -> get_nth msg tail (n-1) + | (_,_) -> raise (NotEnoughElements msg) ;; @@ -135,7 +138,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? *) @@ -150,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 @@ -225,7 +227,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes match tt with C.Rel n -> let id = - match get_nth context n with + match get_nth "1" context n with (Some (C.Name s,_)) -> s | _ -> "__" ^ string_of_int n in @@ -301,13 +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) -> - 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) + | 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' 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 @@ -347,8 +349,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 +370,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 +396,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 = @@ -417,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) @@ -457,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 [] @@ -477,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=true) 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 @@ -496,30 +511,43 @@ let acic_object_of_cic_object ?(eta_fix=true) 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 @@ -536,16 +564,17 @@ let acic_object_of_cic_object ?(eta_fix=true) 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 @@ -559,9 +588,9 @@ 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 ty' = eta_fix conjectures' [] ty in + (* let bo' = eta_fix conjectures' [] bo in *) + let bo' = bo in + let ty' = eta_fix_and_unshare conjectures' [] ty in (* let time2 = Sys.time () in prerr_endline @@ -619,7 +648,10 @@ let acic_object_of_cic_object ?(eta_fix=true) 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 @@ -631,7 +663,7 @@ let plain_acic_term_of_cic_term = match t with C.Rel n -> let idref,id = - match get_nth context n with + match get_nth "2" context n with idref,(Some (C.Name s,_)) -> idref,s | idref,_ -> idref,"__" ^ string_of_int n in @@ -655,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) -> @@ -683,9 +715,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 +729,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 @@ -754,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 ())