| (_,_) -> raise NotEnoughElements
;;
-let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- ids_to_inner_types metasenv env t
+let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
+ ids_to_inner_types metasenv context t
=
let module T = CicTypeChecker in
let module C = Cic in
let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
- let rec aux computeinnertypes father bs tt =
+ let rec aux computeinnertypes father context tt =
let fresh_id'' = fresh_id' father tt in
let aux' = aux true (Some fresh_id'') in
(* First of all we compute the inner type and the inner sort *)
| _ -> assert false
in
let ainnertype,innertype,innersort =
- let cicenv = List.map (function (_,ty) -> ty) bs in
- let innertype = T.type_of_aux' metasenv cicenv tt in
- let innersort = T.type_of_aux' metasenv cicenv innertype in
+(*CSC: Here we need the algorithm for Coscoy's double type-inference *)
+(*CSC: (expected type + inferred type). Just for now we use the usual *)
+(*CSC: type-inference, but the result is very poort. As a very weak *)
+(*CSC: patch, I apply whd to the computed type. Full beta *)
+(*CSC: reduction would be a much better option. *)
+ let innertype =
+ CicReduction.whd context (T.type_of_aux' metasenv context tt)
+ in
+ let innersort = T.type_of_aux' metasenv context innertype in
let ainnertype =
if computeinnertypes then
- Some (aux false (Some fresh_id'') bs innertype)
+ Some (aux false (Some fresh_id'') context innertype)
else
None
in
match tt with
C.Rel n ->
let id =
- match get_nth bs n with
- (C.Name s,_) -> s
+ match get_nth context n with
+ (Some (C.Name s,_)) -> s
| _ -> raise NameExpected
in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
| C.Var uri ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
C.AVar (fresh_id'', uri)
- | C.Meta n ->
+ | C.Meta (n,l) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.AMeta (fresh_id'', n)
+ C.AMeta (fresh_id'', n,
+ (List.map
+ (function None -> None | Some t -> Some (aux' context t)) l))
| C.Sort s -> C.ASort (fresh_id'', s)
| C.Implicit -> C.AImplicit (fresh_id'')
| C.Cast (v,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
- C.ACast (fresh_id'', aux' bs v, aux' bs t)
+ C.ACast (fresh_id'', aux' context v, aux' context t)
| C.Prod (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id''
(string_of_sort innertype) ;
- C.AProd (fresh_id'', n, aux' bs s, aux' ((n,s)::bs) t)
+ C.AProd
+ (fresh_id'', n, aux' context s,
+ aux' ((Some (n, C.Decl s))::context) t)
| C.Lambda (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
if not father_is_lambda then
add_inner_type fresh_id''
end ;
- C.ALambda (fresh_id'',n, aux' bs s, aux' ((n,s)::bs) t)
+ C.ALambda
+ (fresh_id'',n, aux' context s,
+ aux' ((Some (n, C.Decl s)::context)) t)
| C.LetIn (n,s,t) ->
-(*CSC: Nell'environment debbo poter avere anche dichiarazioni! ;-(
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t)
-*) assert false
+ C.ALetIn
+ (fresh_id'', n, aux' context s,
+ aux' ((Some (n, C.Def s))::context) t)
| C.Appl l ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
- C.AAppl (fresh_id'', List.map (aux' bs) l)
+ C.AAppl (fresh_id'', List.map (aux' context) l)
| C.Const (uri,cn) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
C.AConst (fresh_id'', uri, cn)
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
- C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
- aux' bs term, List.map (aux' bs) patterns)
+ C.AMutCase (fresh_id'', uri, cn, tyno, aux' context outty,
+ aux' context term, List.map (aux' context) patterns)
| C.Fix (funno, funs) ->
- let names = List.map (fun (name,_,ty,_) -> C.Name name,ty) funs in
+ let tys =
+ List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+ in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.AFix (fresh_id'', funno,
List.map
(fun (name, indidx, ty, bo) ->
- (name, indidx, aux' bs ty, aux' (names@bs) bo)
+ (name, indidx, aux' context ty, aux' (tys@context) bo)
) funs
)
| C.CoFix (funno, funs) ->
- let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in
+ let tys =
+ List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.ACoFix (fresh_id'', funno,
List.map
(fun (name, ty, bo) ->
- (name, aux' bs ty, aux' (names@bs) bo)
+ (name, aux' context ty, aux' (tys@context) bo)
) funs
)
in
- aux true None env t
+ aux true None context t
;;
-let acic_of_cic_env metasenv env t =
+let acic_of_cic_context metasenv context t =
let ids_to_terms = Hashtbl.create 503 in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
let seed = ref 0 in
- acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- ids_to_inner_types metasenv env t,
+ acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
+ ids_to_inner_types metasenv context t,
ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;
-exception Found of (Cic.name * Cic.term) list;;
-
-(* get_context_of_meta meta term *)
-(* returns the context of the occurrence of [meta] in [term]. *)
-(* Warning: if [meta] occurs not linearly in [term], the context *)
-(* of one "random" occurrence is returned. *)
-let get_context_of_meta meta term =
- let module C = Cic in
- let rec aux ctx =
- function
- C.Rel _
- | C.Var _ -> ()
- | C.Meta i when meta = i -> raise (Found ctx)
- | C.Meta _
- | C.Sort _
- | C.Implicit -> ()
- | C.Cast (te,ty) -> aux ctx te ; aux ctx ty
- | C.Prod (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
- | C.Lambda (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
- | C.LetIn (n,s,t) ->
- aux ctx s ; assert false (* aux ([P.Definition,n,s]::ctx) t *)
- | C.Appl l -> List.iter (aux ctx) l
- | C.Const _ -> ()
- | C.Abst _ -> assert false
- | C.MutInd _
- | C.MutConstruct _ -> ()
- | C.MutCase (_,_,_,outt,t,pl) ->
- aux ctx outt ; aux ctx t; List.iter (aux ctx) pl
- | C.Fix (_,ifl) ->
- let counter = ref 0 in
- let ctx' =
- List.rev_map
- (function (name,_,ty,bo) ->
- let res = ((*P.Definition,*) C.Name name, C.Fix (!counter,ifl)) in
- incr counter ;
- res
- ) ifl
- @ ctx
- in
- List.iter (function (_,_,ty,bo) -> aux ctx ty ; aux ctx' bo) ifl
- | C.CoFix (_,ifl) ->
- let counter = ref 0 in
- let ctx' =
- List.rev_map
- (function (name,ty,bo) ->
- let res = ((*P.Definition,*) C.Name name, C.CoFix (!counter,ifl)) in
- incr counter ;
- res
- ) ifl
- @ ctx
- in
- List.iter (function (_,ty,bo) -> aux ctx ty ; aux ctx' bo) ifl
- in
- try
- aux [] term ;
- assert false (* No occurrences found. *)
- with
- Found context -> context
-;;
-
-exception NotImplemented;;
+exception Found of (Cic.name * Cic.context_entry) list;;
let acic_object_of_cic_object obj =
let module C = Cic in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
+ let ids_to_conjectures = Hashtbl.create 11 in
+ let ids_to_hypotheses = Hashtbl.create 127 in
+ let hypotheses_seed = ref 0 in
+ let conjectures_seed = ref 0 in
let seed = ref 0 in
- let acic_term_of_cic_term_env' =
- acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
+ let acic_term_of_cic_term_context' =
+ acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
ids_to_inner_types in
- let acic_term_of_cic_term' = acic_term_of_cic_term_env' [] [] in
+ let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] in
let aobj =
match obj with
C.Definition (id,bo,ty,params) ->
| C.CurrentProof (id,conjectures,bo,ty) ->
let aconjectures =
List.map
- (function (i,term) ->
- let context = get_context_of_meta i bo in
- let aterm = acic_term_of_cic_term_env' conjectures context term in
- (i, aterm))
- conjectures in
- let abo = acic_term_of_cic_term_env' conjectures [] bo in
- let aty = acic_term_of_cic_term_env' conjectures [] ty in
+ (function (i,canonical_context,term) as conjecture ->
+ let cid = "c" ^ string_of_int !conjectures_seed in
+ Hashtbl.add ids_to_conjectures cid conjecture ;
+ incr conjectures_seed ;
+ let acanonical_context =
+ let rec aux =
+ function
+ [] -> []
+ | hyp::tl ->
+ let hid = "h" ^ string_of_int !hypotheses_seed in
+ Hashtbl.add ids_to_hypotheses hid hyp ;
+ incr hypotheses_seed ;
+ match hyp with
+ (Some (n,C.Decl t)) ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ (hid,Some (n,C.ADecl at))::(aux tl)
+ | (Some (n,C.Def t)) ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ (hid,Some (n,C.ADef at))::(aux tl)
+ | None -> (hid,None)::(aux tl)
+ in
+ aux canonical_context
+ in
+ let aterm =
+ acic_term_of_cic_term_context' conjectures canonical_context term
+ in
+ (cid,i,acanonical_context,aterm)
+ ) conjectures in
+ let abo = acic_term_of_cic_term_context' conjectures [] bo in
+ let aty = acic_term_of_cic_term_context' conjectures [] ty in
C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
| C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
in
- aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types
+ aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
+ ids_to_conjectures,ids_to_hypotheses
;;
projects / helm.git / blobdiff