(* $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;; *)
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
;;
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)
;;
| 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
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
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
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
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
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)
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 []
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
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
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
= 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
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
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
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) ->
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
) 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
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 ())
projects / helm.git / blobdiff