;;
let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- metasenv env t
+ ids_to_inner_types metasenv env 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 bs 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 ainnertype,innertype,innersort =
let cicenv = List.map (function (_,ty) -> ty) bs in
- let innertype = T.type_of_aux' metasenv cicenv tt 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 cicenv (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 =
+ if computeinnertypes then
+ Some (aux false (Some fresh_id'') bs 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 ->
| 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.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' bs s, aux' ((n, C.Decl s)::bs) 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' bs s, aux' ((n, C.Decl s)::bs) 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' bs s, aux' ((n, C.Def s)::bs) 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.Const (uri,cn) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
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 ;
+ 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.Fix (funno, funs) ->
- let names = List.map (fun (name,_,ty,_) -> C.Name name,ty) funs in
+ let names =
+ List.map (fun (name,_,ty,_) -> 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) ->
) funs
)
| C.CoFix (funno, funs) ->
- let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in
+ let names =
+ List.map (fun (name,ty,_) -> 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) ->
) funs
)
in
- aux None env t
+ aux true None env t
;;
let acic_of_cic_env metasenv env 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
+ ids_to_inner_types metasenv env t,
+ ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;
-exception Found of (Cic.name * Cic.term) list;;
+exception Found of (Cic.name * Cic.context_entry) list;;
(* get_context_of_meta meta term *)
(* returns the context of the occurrence of [meta] in [term]. *)
| 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.Prod (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+ | C.Lambda (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+ | C.LetIn (n,s,t) -> aux ctx s ; aux ((n, C.Def s)::ctx) t
| C.Appl l -> List.iter (aux ctx) l
| C.Const _ -> ()
| C.Abst _ -> assert false
let ctx' =
List.rev_map
(function (name,_,ty,bo) ->
- let res = ((*P.Definition,*) C.Name name, C.Fix (!counter,ifl)) in
+ let res = (C.Name name, C.Def (C.Fix (!counter,ifl))) in
incr counter ;
res
) ifl
let ctx' =
List.rev_map
(function (name,ty,bo) ->
- let res = ((*P.Definition,*) C.Name name, C.CoFix (!counter,ifl)) in
+ let res = (C.Name name, C.Def (C.CoFix (!counter,ifl))) in
incr counter ;
res
) ifl
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
+ acic_of_cic_env' 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 aobj =
match obj with
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
;;
projects / helm.git / blobdiff