doubleTypeInference.cmx: doubleTypeInference.cmi
cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi
cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi
+cic2Xml.cmo: cic2acic.cmi
+cic2Xml.cmx: cic2acic.cmx
logicalOperations.cmo: proofEngine.cmo
logicalOperations.cmx: proofEngine.cmx
sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo
all: gTopLevel
opt: gTopLevel.opt
-DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \
+DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml \
doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
- cic2acic.mli logicalOperations.ml sequentPp.ml mquery.mli \
- mquery.ml gTopLevel.ml
+ cic2Xml.ml cic2acic.mli logicalOperations.ml sequentPp.ml \
+ mquery.mli mquery.ml gTopLevel.ml
TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \
- cic2Xml.cmo doubleTypeInference.cmo cic2acic.cmo \
+ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \
logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo
depend:
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_empty "CONST"
["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
- | C.AAbst (id,uri) -> raise NotImplemented
| C.AMutInd (id,uri,_,i) ->
X.xml_empty "MUTIND"
["uri", (U.string_of_uri uri) ;
;;
let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+ let module C2A = Cic2acic in
let module X = Xml in
X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
(Hashtbl.fold
- (fun id ty x ->
+ (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
[< x ;
X.xml_nempty "TYPE" ["of",id]
- (print_term curi ids_to_inner_sorts ty)
+ [< print_term curi ids_to_inner_sorts synty ;
+ match expty with
+ None -> [<>]
+ | Some expty' -> print_term curi ids_to_inner_sorts expty'
+ >]
>]
) ids_to_inner_types [<>]
)
exception NotImplemented;;
+type anntypes =
+ {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
+;;
+
let fresh_id seed ids_to_terms ids_to_father_ids =
fun father t ->
let res = "i" ^ string_of_int !seed in
;;
let 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_inner_types metasenv context t expectedty
=
+ let module D = DoubleTypeInference in
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 terms_to_types = DoubleTypeInference.double_type_of metasenv context t in
- let rec aux computeinnertypes father context tt =
- let fresh_id'' = fresh_id' father tt in
- (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
- let aux' = aux computeinnertypes (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 *)
- (*CSC: and inner sorts: very deep terms have their types/sorts *)
- (*CSC: computed again and again. *)
- let string_of_sort =
- function
- C.Sort C.Prop -> "Prop"
- | C.Sort C.Set -> "Set"
- | C.Sort C.Type -> "Type"
- | _ -> assert false
- in
- let ainnertype,innertype,innersort =
+ let terms_to_types =
+ D.double_type_of metasenv context t expectedty
+ in
+ let rec aux computeinnertypes father context tt =
+ let fresh_id'' = fresh_id' father tt in
+ (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
+ let aux' = aux computeinnertypes (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 *)
+ (*CSC: and inner sorts: very deep terms have their types/sorts *)
+ (*CSC: computed again and again. *)
+ let string_of_sort =
+ function
+ C.Sort C.Prop -> "Prop"
+ | C.Sort C.Set -> "Set"
+ | C.Sort C.Type -> "Type"
+ | _ -> assert false
+ in
+ let ainnertypes,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 poor. 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 =
+ let {D.synthesized = synthesized; D.expected = expected} =
if computeinnertypes then
- let {DoubleTypeInference.synthesized = synthesized} =
- DoubleTypeInference.CicHash.find terms_to_types tt
- in
- synthesized
+ D.CicHash.find terms_to_types tt
else
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
- CicReduction.whd context (T.type_of_aux' metasenv context tt)
+ {D.synthesized =
+ CicReduction.whd context (T.type_of_aux' metasenv context tt) ;
+ D.expected = None}
in
- let innersort = T.type_of_aux' metasenv context innertype in
- let ainnertype =
+ let innersort = T.type_of_aux' metasenv context synthesized in
+ let ainnertypes =
if computeinnertypes then
- Some (aux false (Some fresh_id'') context innertype)
+ Some
+ {annsynthesized =
+ aux false (Some fresh_id'') context synthesized ;
+ annexpected =
+ match expected with
+ None -> None
+ | Some expectedty' ->
+ Some (aux false (Some fresh_id'') context expectedty')
+ }
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 context n with
- (Some (C.Name s,_)) -> s
- | _ -> raise NameExpected
- in
+ ainnertypes, synthesized, string_of_sort innersort
+ in
+ let add_inner_type id =
+ match ainnertypes with
+ None -> ()
+ | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes
+ in
+ match tt with
+ C.Rel n ->
+ let id =
+ match get_nth context n with
+ (Some (C.Name s,_)) -> s
+ | _ -> raise NameExpected
+ in
+ Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ C.ARel (fresh_id'', n, id)
+ | C.Var uri ->
+ Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ C.AVar (fresh_id'', uri)
+ | C.Meta (n,l) ->
+ Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ 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' 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' 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
+ 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) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.ARel (fresh_id'', n, id)
- | C.Var uri ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.AVar (fresh_id'', uri)
- | C.Meta (n,l) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- 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' context v, aux' context t)
- | C.Prod (n,s,t) ->
- Hashtbl.add ids_to_inner_sorts fresh_id''
- (string_of_sort innertype) ;
- C.AProd
+ C.ALetIn
(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
- begin
- let father_is_lambda =
- match father with
- None -> false
- | Some father' ->
- match Hashtbl.find ids_to_terms father' with
- C.Lambda _ -> true
- | _ -> false
+ 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' context) l)
+ | C.Const (uri,cn) ->
+ Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ C.AConst (fresh_id'', uri, cn)
+ | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno)
+ | C.MutConstruct (uri,cn,tyno,consno) ->
+ 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' context outty,
+ aux' context term, List.map (aux' context) patterns)
+ | C.Fix (funno, funs) ->
+ let tys =
+ List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
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) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- 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' context) l)
- | C.Const (uri,cn) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.AConst (fresh_id'', uri, cn)
- | C.Abst _ -> raise NotImplemented
- | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno)
- | C.MutConstruct (uri,cn,tyno,consno) ->
- 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' context outty,
- aux' context term, List.map (aux' context) patterns)
- | C.Fix (funno, funs) ->
- 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' context ty, aux' (tys@context) bo)
- ) funs
- )
- | C.CoFix (funno, funs) ->
- 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' context ty, aux' (tys@context) bo)
- ) funs
- )
- in
- aux true None context t
+ 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' context ty, aux' (tys@context) bo)
+ ) funs
+ )
+ | C.CoFix (funno, funs) ->
+ 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' context ty, aux' (tys@context) bo)
+ ) funs
+ )
+ in
+ aux true None context t
;;
let acic_of_cic_context metasenv context t =
let aobj =
match obj with
C.Definition (id,bo,ty,params) ->
- let abo = acic_term_of_cic_term' bo in
- let aty = acic_term_of_cic_term' ty
- in
+ let abo = acic_term_of_cic_term' bo (Some ty) in
+ let aty = acic_term_of_cic_term' ty None in
C.ADefinition ("mettereaposto",id,abo,aty,(Cic.Actual params))
| C.Axiom (id,ty,params) -> raise NotImplemented
| C.Variable (id,bo,ty) -> raise NotImplemented
match hyp with
(Some (n,C.Decl t)) ->
let at =
- acic_term_of_cic_term_context' conjectures tl t
+ acic_term_of_cic_term_context' conjectures tl t None
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
+ acic_term_of_cic_term_context' conjectures tl t None
in
(hid,Some (n,C.ADef at))::(aux tl)
| None -> (hid,None)::(aux tl)
aux canonical_context
in
let aterm =
- acic_term_of_cic_term_context' conjectures canonical_context term
+ acic_term_of_cic_term_context' conjectures canonical_context
+ term None
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
+ let abo = acic_term_of_cic_term_context' conjectures [] bo (Some ty) in
+ let aty = acic_term_of_cic_term_context' conjectures [] ty None in
C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
| C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
in
exception NotEnoughElements
exception NameExpected
+type anntypes =
+ {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
+;;
+
val acic_of_cic_context' :
int ref -> (* seed *)
(Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *)
(Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *)
- (Cic.id, Cic.annterm) Hashtbl.t -> (* ids_to_inner_types *)
+ (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *)
Cic.metasenv -> (* metasenv *)
Cic.context -> (* context *)
Cic.term -> (* term *)
+ Cic.term option -> (* expected type *)
Cic.annterm (* annotated term *)
val acic_object_of_cic_object :
(Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
(Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *)
- (Cic.id, Cic.annterm) Hashtbl.t * (* ids_to_inner_types *)
+ (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *)
(Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *)
(Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)
exception ListTooShort;;
exception RelToHiddenHypothesis;;
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+type types = {synthesized : Cic.term ; expected : Cic.term option};;
+
+(*CSC: potrebbe creare applicazioni di applicazioni *)
+(*CSC: ora non e' piu' head, ma completa!!! *)
+let rec head_beta_reduce =
+ let module S = CicSubstitution in
+ let module C = Cic in
+ function
+ C.Rel _
+ | C.Var _ as t -> t
+ | C.Meta (n,l) ->
+ C.Meta (n,
+ List.map
+ (function None -> None | Some t -> Some (head_beta_reduce t)) l
+ )
+ | C.Sort _ as t -> t
+ | C.Implicit -> assert false
+ | C.Cast (te,ty) ->
+ C.Cast (head_beta_reduce te, head_beta_reduce ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
+ let he' = S.subst he t in
+ if tl = [] then
+ head_beta_reduce he'
+ else
+ head_beta_reduce (C.Appl (he'::tl))
+ | C.Appl l ->
+ C.Appl (List.map head_beta_reduce l)
+ | C.Const _ as t -> t
+ | C.MutInd _
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cno,i,outt,t,pl) ->
+ C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
+ List.map head_beta_reduce pl)
+ | C.Fix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,i,ty,bo) ->
+ name,i,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.Fix (i,fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,ty,bo) ->
+ name,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.CoFix (i,fl')
+;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant), *)
+(* distinction between fake dependent products *)
+(* and non-dependent products, alfa-conversion *)
+(*CSC: must alfa-conversion be considered or not? *)
+let syntactic_equality t t' =
+ let module C = Cic in
+ let rec syntactic_equality t t' =
+ if t = t' then true
+ else
+ match t, t' with
+ C.Rel _, C.Rel _
+ | C.Var _, C.Var _
+ | C.Meta _, C.Meta _
+ | C.Sort _, C.Sort _
+ | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ | C.Cast (te,ty), C.Cast (te',ty') ->
+ syntactic_equality te te' &&
+ syntactic_equality ty ty'
+ | C.Prod (_,s,t), C.Prod (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Appl l, C.Appl l' ->
+ List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
+ | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
+ | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
+ UriManager.eq uri uri' && i = i'
+ | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
+ UriManager.eq uri uri' && i = i' && j = j'
+ | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ UriManager.eq sp sp' && i = i' &&
+ syntactic_equality outt outt' &&
+ syntactic_equality t t' &&
+ List.fold_left2
+ (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+ | C.Fix (i,fl), C.Fix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+ b && i = i' &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | C.CoFix (i,fl), C.CoFix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (_,ty,bo) (_,ty',bo') ->
+ b &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | _,_ -> false
+ in
+ try
+ syntactic_equality t t'
+ with
+ _ -> false
+;;
let rec split l n =
match (l,n) with
;;
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-let rec type_of_aux' subterms_to_types metasenv context t =
+let rec type_of_aux' subterms_to_types metasenv context t expectedty =
(* Coscoy's double type-inference algorithm *)
(* It computes the inner-types of every subterm of [t], *)
(* even when they are not needed to compute the types *)
(* of other terms. *)
- let rec type_of_aux context t =
+ let rec type_of_aux context t expectedty =
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t
- | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
+ | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
| None -> raise RelToHiddenHypothesis
with
_ -> raise (NotWellTyped "Not a close term")
(* Let's visit all the subterms that will not be visited later *)
let _ =
List.iter
- (function None -> () | Some t -> ignore (type_of_aux context t)) l
+ (function
+ None -> ()
+ | Some t -> ignore (type_of_aux context t None)
+ ) l
in
let (_,canonical_context,ty) =
List.find (function (m,_,_) -> n = m) metasenv
| C.Implicit -> raise (Impossible 21)
| C.Cast (te,ty) ->
(* Let's visit all the subterms that will not be visited later *)
- let _ = type_of_aux context te in
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
+ let _ = type_of_aux context ty None in
(* Checks suppressed *)
ty
| C.Prod (name,s,t) ->
- let sort1 = type_of_aux context s
- and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
+ let sort1 = type_of_aux context s None
+ and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
sort_of_prod context (name,s) (sort1,sort2)
| C.Lambda (n,s,t) ->
(* Let's visit all the subterms that will not be visited later *)
- let _ = type_of_aux context s in
- let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
- (* Checks suppressed *)
- C.Prod (n,s,type2)
+ let _ = type_of_aux context s None in
+ let expected_target_type =
+ match expectedty with
+ None -> None
+ | Some expectedty' ->
+ let ty =
+ match R.whd context expectedty' with
+ C.Prod (_,_,expected_target_type) ->
+ head_beta_reduce expected_target_type
+ | _ -> assert false
+ in
+ Some ty
+ in
+ let type2 =
+ type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
+ in
+ (* Checks suppressed *)
+ C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
+(*CSC: What are the right expected types for the source and *)
+(*CSC: target of a LetIn? None used. *)
(* Let's visit all the subterms that will not be visited later *)
- let _ = type_of_aux context s in
+ let _ = type_of_aux context s None in
(* Checks suppressed *)
- C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
+ C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he
- and tlbody_and_type =
- List.map (fun x -> (x, type_of_aux context x)) tl
+ let hetype = type_of_aux context he None in
+ let tlbody_and_type =
+ let rec aux =
+ function
+ _,[] -> []
+ | C.Prod (n,s,t),he::tl ->
+ (he, type_of_aux context he (Some (head_beta_reduce s)))::
+ (aux (R.whd context (S.subst he t), tl))
+ | _ -> assert false
+ in
+ aux (R.whd context hetype, tl)
in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
| C.Const (uri,cookingsno) ->
cooked_type_of_constant uri cookingsno
- | C.Abst _ -> raise (Impossible 22)
| C.MutInd (uri,cookingsno,i) ->
cooked_type_of_mutual_inductive_defs uri cookingsno i
| C.MutConstruct (uri,cookingsno,i,j) ->
let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
cty
| C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
- (* Let's visit all the subterms that will not be visited later *)
- let _ = List.map (type_of_aux context) pl in
- let outsort = type_of_aux context outtype in
- let (need_dummy, k) =
- let rec guess_args context t =
- match CicReduction.whd context t with
- C.Sort _ -> (true, 0)
- | C.Prod (name, s, t) ->
- let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
- if n = 0 then
- (* last prod before sort *)
- match CicReduction.whd context s with
- (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
- C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
- (false, 1)
- | C.Appl ((C.MutInd (uri',_,i')) :: _)
- when U.eq uri' uri && i' = i -> (false, 1)
- | _ -> (true, 1)
- else
- (b, n + 1)
- | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
- in
- (*CSC whd non serve dopo type_of_aux ? *)
- let (b, k) = guess_args context outsort in
- if not b then (b, k - 1) else (b, k)
+ let outsort = type_of_aux context outtype None in
+ let (need_dummy, k) =
+ let rec guess_args context t =
+ match CicReduction.whd context t with
+ C.Sort _ -> (true, 0)
+ | C.Prod (name, s, t) ->
+ let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
+ if n = 0 then
+ (* last prod before sort *)
+ match CicReduction.whd context s with
+ (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
+ C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
+ (false, 1)
+ | C.Appl ((C.MutInd (uri',_,i')) :: _)
+ when U.eq uri' uri && i' = i -> (false, 1)
+ | _ -> (true, 1)
+ else
+ (b, n + 1)
+ | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
in
- let (_, arguments) =
- match R.whd context (type_of_aux context term) with
- (*CSC manca il caso dei CAST *)
- C.MutInd (uri',_,i') ->
- (* Checks suppressed *)
- [],[]
- | C.Appl (C.MutInd (uri',_,i') :: tl) ->
- split tl (List.length tl - k)
- | _ ->
- raise (NotWellTyped "MutCase: the term is not an inductive one")
+ let (b, k) = guess_args context outsort in
+ if not b then (b, k - 1) else (b, k)
+ in
+ let (parameters, arguments) =
+ let type_of_term =
+ CicTypeChecker.type_of_aux' metasenv context term
in
- (* Checks suppressed *)
- if not need_dummy then
- C.Appl ((outtype::arguments)@[term])
- else if arguments = [] then
- outtype
- else
- C.Appl (outtype::arguments)
+ match
+ R.whd context (type_of_aux context term
+ (Some (head_beta_reduce type_of_term)))
+ with
+ (*CSC manca il caso dei CAST *)
+ C.MutInd (uri',_,i') ->
+ (* Checks suppressed *)
+ [],[]
+ | C.Appl (C.MutInd (uri',_,i') :: tl) ->
+ split tl (List.length tl - k)
+ | _ ->
+ raise (NotWellTyped "MutCase: the term is not an inductive one")
+ in
+ (* Checks suppressed *)
+ (* Let's visit all the subterms that will not be visited later *)
+ let (cl,parsno) =
+ match CicEnvironment.get_cooked_obj uri cookingsno with
+ C.InductiveDefinition (tl,_,parsno) ->
+ let (_,_,_,cl) = List.nth tl i in (cl,parsno)
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ in
+ let _ =
+ List.fold_left
+ (fun j (p,(_,c,_)) ->
+ let cons =
+ if parameters = [] then
+ (C.MutConstruct (uri,cookingsno,i,j))
+ else
+ (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
+ in
+ let expectedtype =
+ type_of_branch context parsno need_dummy outtype cons
+ (CicTypeChecker.type_of_aux' metasenv context cons)
+ in
+ ignore (type_of_aux context p
+ (Some (head_beta_reduce expectedtype))) ;
+ j+1
+ ) 1 (List.combine pl cl)
+ in
+ if not need_dummy then
+ C.Appl ((outtype::arguments)@[term])
+ else if arguments = [] then
+ outtype
+ else
+ C.Appl (outtype::arguments)
| C.Fix (i,fl) ->
(* Let's visit all the subterms that will not be visited later *)
let context' =
List.rev
(List.map
(fun (n,_,ty,_) ->
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context ty None in
(Some (C.Name n,(C.Decl ty)))
) fl
) @
in
let _ =
List.iter
- (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
+ (fun (_,_,ty,bo) ->
+ let expectedty =
+ head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+ in
+ ignore (type_of_aux context' bo (Some expectedty))
+ ) fl
in
(* Checks suppressed *)
let (_,_,ty,_) = List.nth fl i in
List.rev
(List.map
(fun (n,ty,_) ->
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context ty None in
(Some (C.Name n,(C.Decl ty)))
) fl
) @
in
let _ =
List.iter
- (fun (_,_,bo) -> ignore (type_of_aux context' bo))
+ (fun (_,ty,bo) ->
+ let expectedty =
+ head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+ in
+ ignore (type_of_aux context' bo (Some expectedty))
+ ) fl
in
(* Checks suppressed *)
let (_,ty,_) = List.nth fl i in
ty
in
- (*CSC: Is whd the right thing to do? Or should full beta *)
- (*CSC: reduction be more appropriate? *)
-(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
-(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
- let synthesized' = CicReduction.whd context synthesized in
- CicHash.add subterms_to_types t
- {synthesized = synthesized' ; expected = Cic.Implicit} ;
- synthesized'
+ let synthesized' = head_beta_reduce synthesized in
+ let types,res =
+ match expectedty with
+ None ->
+ (* No expected type *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | Some ty when syntactic_equality synthesized' ty ->
+ (* The expected type is synthactically equal to *)
+ (* the synthesized type. Let's forget it. *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | Some expectedty' ->
+prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
+prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
+ {synthesized = synthesized' ; expected = Some expectedty'},
+ expectedty'
+ in
+ CicHash.add subterms_to_types t types ;
+ res
and sort_of_prod context (name,s) (t1, t2) =
let module C = Cic in
| _ -> raise (NotWellTyped "Appl: wrong Prod-type")
)
+and type_of_branch context argsno need_dummy outtype term constype =
+ let module C = Cic in
+ let module R = CicReduction in
+ match R.whd context constype with
+ C.MutInd (_,_,_) ->
+ if need_dummy then
+ outtype
+ else
+ C.Appl [outtype ; term]
+ | C.Appl (C.MutInd (_,_,_)::tl) ->
+ let (_,arguments) = split tl argsno
+ in
+ if need_dummy && arguments = [] then
+ outtype
+ else
+ C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
+ | C.Prod (name,so,de) ->
+ let term' =
+ match CicSubstitution.lift 1 term with
+ C.Appl l -> C.Appl (l@[C.Rel 1])
+ | t -> C.Appl [t ; C.Rel 1]
+ in
+ C.Prod (C.Anonimous,so,type_of_branch
+ ((Some (name,(C.Decl so)))::context) argsno need_dummy
+ (CicSubstitution.lift 1 outtype) term' de)
+ | _ -> raise (Impossible 20)
+
in
- type_of_aux context t
+ type_of_aux context t expectedty
;;
-let double_type_of metasenv context t =
+let double_type_of metasenv context t expectedty =
let subterms_to_types = CicHash.create 503 in
- ignore (type_of_aux' subterms_to_types metasenv context t) ;
+ ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
subterms_to_types
;;
exception ListTooShort
exception RelToHiddenHypothesis
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+type types = {synthesized : Cic.term ; expected : Cic.term option};;
module CicHash :
sig
- type key = Cic.term
- and 'a t
- val find : 'a t -> key -> 'a
+ type 'a t
+ val find : 'a t -> Cic.term -> 'a
end
+;;
val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
"/public/sacerdot/currentproof</h1>")
;;
+(* Used to typecheck the loaded proofs *)
+let typecheck_loaded_proof metasenv bo ty =
+ let module T = CicTypeChecker in
+ (*CSC: bisogna controllare anche il metasenv!!! *)
+ ignore (T.type_of_aux' metasenv [] ty) ;
+ ignore (T.type_of_aux' metasenv [] bo)
+;;
+
let load rendering_window () =
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let output = (rendering_window#output : GMathView.math_view) in
let uri = UriManager.uri_of_string "cic:/dummy.con" in
match CicParser.obj_of_xml "/public/sacerdot/currentproof" uri with
Cic.CurrentProof (_,metasenv,bo,ty) ->
+ typecheck_loaded_proof metasenv bo ty ;
ProofEngine.proof :=
Some (uri, metasenv, bo, ty) ;
ProofEngine.goal :=
| C.LetIn _ -> []
| C.Appl _
| C.Const _ -> []
- | C.Abst _ -> assert false
| C.MutInd _
| C.MutConstruct _
| C.MutCase _ -> []
| Meta (i, _) -> l
| Sort s -> l
| Implicit -> l
- | Abst u -> l
| Var u -> inspect_uri main l u None None v
| Const (u, i) -> inspect_uri main l u None None v
| MutInd (u, i, t) -> inspect_uri main l u (Some t) None v
| C.LetIn (_,s,t) -> (aux s) @ (aux t)
| C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
| C.Const _
- | C.Abst _
| C.MutInd _
| C.MutConstruct _ -> []
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
| C.Appl l -> C.Appl (List.map (aux n) l)
| C.Const _ as t -> t
- | C.Abst _ -> assert false
| C.MutInd _
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| _ ->raise NotTheRightEliminatorShape
in
find_head he,fargs
+ | C.Meta (emeta,_) -> emeta,[]
(* *)
| _ -> raise NotTheRightEliminatorShape
in
| C.Appl l, C.Appl l' ->
List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
| C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
- | C.Abst _, C.Abst _ -> assert false
| C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
UriManager.eq uri uri' && i = i'
| C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
(C.Appl l')::tl -> C.Appl (l'@tl)
| l' -> C.Appl l')
| C.Const _ as t -> t
- | C.Abst _ as t -> t
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| C.CurrentProof (_,_,body,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
- | C.Abst _ as t -> t (*CSC l should be empty ????? *)
| C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
eat_first (num_to_eat,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Abst _ | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
| C.CurrentProof (_,_,body,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
- | C.Abst _ as t -> t (*CSC l should be empty ????? *)
| C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
eat_first (num_to_eat,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Abst _ | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
match binding with
(Some (n,(Cic.Def t as b)) as entry)
| (Some (n,(Cic.Decl t as b)) as entry) ->
- let acic = acic_of_cic_context context t in
+ let acic = acic_of_cic_context context t None in
[< s ;
X.xml_nempty
(match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
) context ([<>],[])
)
in
- let acic = acic_of_cic_context context goal in
+ let acic = acic_of_cic_context context goal None in
X.xml_nempty "Sequent" ["no",string_of_int metano]
[< final_s ;
Xml.xml_nempty "Goal" []
projects / helm.git / commitdiff