| (_,_) -> raise NotEnoughElements
;;
-let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- 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 father bs tt =
+ let rec aux computeinnertypes father context tt =
let fresh_id'' = fresh_id' father tt in
- let aux' = aux (Some fresh_id'') in
+ let aux' = aux true (Some fresh_id'') in
(* First of all we compute the inner type and the inner sort *)
(* of the term. They may be useful in what follows. *)
(*CSC: This is a very inefficient way of computing inner types *)
| C.Sort C.Type -> "Type"
| _ -> assert false
in
- let 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
- innertype, string_of_sort innersort
+ let ainnertype,innertype,innersort =
+(*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'') context innertype)
+ else
+ None
+ in
+ ainnertype, innertype, string_of_sort innersort
+ in
+ let add_inner_type id =
+ match ainnertype with
+ None -> ()
+ | Some ainnertype -> Hashtbl.add ids_to_inner_types id ainnertype
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 ;
- C.ACast (fresh_id'', aux' bs v, aux' bs t)
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
+ 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 ;
- C.ALambda (fresh_id'',n, aux' bs s, aux' ((n,s)::bs) t)
+ if innersort = "Prop" then
+ begin
+ let father_is_lambda =
+ match father with
+ None -> false
+ | Some father' ->
+ match Hashtbl.find ids_to_terms father' with
+ C.Lambda _ -> true
+ | _ -> false
+ in
+ if not father_is_lambda then
+ add_inner_type fresh_id''
+ end ;
+ 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 ;
- C.AAppl (fresh_id'', List.map (aux' bs) l)
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
+ 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)
C.AMutConstruct (fresh_id'', uri, cn, tyno, consno)
| C.MutCase (uri, cn, tyno, outty, term, patterns) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
- aux' bs term, List.map (aux' bs) patterns)
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
+ 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 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
- metasenv env t,
- ids_to_terms, ids_to_father_ids, ids_to_inner_sorts
+ 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 Found of (Cic.name * Cic.context_entry) list;;
exception NotImplemented;;
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
- let acic_term_of_cic_term_env' =
- acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts in
- let acic_term_of_cic_term' = acic_term_of_cic_term_env' [] [] in
+ 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_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) ->
+ let acanonical_context =
+ let rec aux =
+ function
+ [] -> []
+ | (Some (n,C.Decl t))::tl ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ Some (n,C.ADecl at)::(aux tl)
+ | (Some (n,C.Def t))::tl ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ Some (n,C.ADef at)::(aux tl)
+ | None::tl -> None::(aux tl)
+ in
+ aux canonical_context
+ in
+ let aterm =
+ acic_term_of_cic_term_context' conjectures canonical_context term
+ in
+ (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
+ aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types
;;