let ids_to_hypotheses = Hashtbl.create 23 in
let hypotheses_seed = ref 0 in
let seed = ref 1 in (* 'i0' is used for the whole sequent *)
+ let sequent =
+ let i,canonical_context,term = sequent in
+ let canonical_context' =
+ List.fold_right
+ (fun d canonical_context' ->
+ let d =
+ match d with
+ 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 (_,Cic.Def (_,Some _)) -> assert false
+ in
+ d::canonical_context'
+ ) canonical_context []
+ in
+ let term' = Unshare.unshare term in
+ (i,canonical_context',term')
+ in
let (metano,acontext,agoal) =
aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_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 =
- if eta_fix then E.eta_fix metasenv context t else t
- in
+ 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 canonical_context' =
List.fold_right
(fun d canonical_context' ->
- let d' =
+ let d =
match d with
None -> None
| Some (n, C.Decl t)->
| Some (_,C.Def (_,Some _)) -> assert false
in
d::canonical_context'
- ) [] canonical_context
+ ) canonical_context []
in
let term' = eta_fix conjectures canonical_context' term in
(i,canonical_context',term')
= aconjecture_of_conjecture' conjectures conjecture in
(cid,i,acanonical_context,aterm))
conjectures' in
-(* let idrefs',revacanonical_context =
- let rec aux context idrefs =
- function
- [] -> idrefs,[]
- | hyp::tl ->
- let hid = "h" ^ string_of_int !hypotheses_seed in
- let new_idrefs = hid::idrefs in
- xxx_add ids_to_hypotheses hid hyp ;
- incr hypotheses_seed ;
- match hyp with
- (Some (n,C.Decl t)) ->
- let final_idrefs,atl =
- aux (hyp::context) new_idrefs tl in
- let at =
- acic_term_of_cic_term_context'
- conjectures context idrefs t None
- in
- final_idrefs,(hid,Some (n,C.ADecl at))::atl
- | (Some (n,C.Def (t,_))) ->
- let final_idrefs,atl =
- aux (hyp::context) new_idrefs tl in
- let at =
- acic_term_of_cic_term_context'
- conjectures context idrefs t None
- in
- final_idrefs,(hid,Some (n,C.ADef at))::atl
- | None ->
- let final_idrefs,atl =
- aux (hyp::context) new_idrefs tl
- in
- final_idrefs,(hid,None)::atl
- in
- aux [] [] (List.rev canonical_context)
- in
- let aterm =
- acic_term_of_cic_term_context' conjectures
- canonical_context idrefs' term None
- in
- (cid,i,(List.rev revacanonical_context),aterm)
- ) conjectures' in *)
(* let time1 = Sys.time () in *)
let bo' = eta_fix conjectures' [] bo in
let ty' = eta_fix conjectures' [] ty in
C.ACurrentProof
("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
| C.InductiveDefinition (tys,params,paramsno,attrs) ->
+ let tys =
+ List.map
+ (fun (name,i,arity,cl) ->
+ (name,i,Unshare.unshare arity,
+ List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
let context =
List.map
- (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
+ (fun (name,_,arity,_) ->
+ Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
let idrefs = List.map (function _ -> gen_id seed) tys in
let atys =
List.map2
aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
ids_to_conjectures,ids_to_hypotheses
;;
-
-