and context_entry = (* A declaration or definition *)
Decl of term
- | Def of term
+ | Def of term * term option (* body, type (if known) *)
and hypothesis =
(name * context_entry) option (* None means no more accessible *)
and annhypothesis =
id * (name * anncontext_entry) option (* None means no more accessible *)
-and anncontext = annhypothesis list;;
+and anncontext = annhypothesis list
+;;
List.map
(function
_,Some (n,(C.ADef at)) ->
- Some (n,(C.Def (deannotate_term at)))
+ Some (n,(C.Def ((deannotate_term at),None)))
| _,Some (n,(C.ADecl at)) ->
Some (n,(C.Decl (deannotate_term at)))
| _,None -> None
* http://cs.unibo.it/helm/.
*)
+let hashtbl_add_time = ref 0.0;;
+
+let xxx_add h k v =
+ let t1 = Sys.time () in
+ Hashtbl.add h k v ;
+ let t2 = Sys.time () in
+ hashtbl_add_time := !hashtbl_add_time +. t2 -. t1
+;;
+
+let number_new_type_of_aux' = ref 0;;
+let type_of_aux'_add_time = ref 0.0;;
+
+let xxx_type_of_aux' m c t =
+ let t1 = Sys.time () in
+ let res = TypeInference.type_of_aux' m c t in
+ let t2 = Sys.time () in
+ type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
+ res
+;;
+
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 = gen_id seed in
- Hashtbl.add ids_to_father_ids res father ;
- Hashtbl.add ids_to_terms res t ;
+ xxx_add ids_to_father_ids res father ;
+ xxx_add ids_to_terms res t ;
res
;;
ids_to_inner_types metasenv context idrefs 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
-prerr_endline "*************** INIZIO DOUBLE TYPE INFERENCE ************";
+ let time1 = Sys.time () in
let terms_to_types =
D.double_type_of metasenv context t expectedty
in
-prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
+ let time2 = Sys.time () in
+ prerr_endline
+ ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
let rec aux computeinnertypes father context idrefs tt =
let fresh_id'' = fresh_id' father tt in
(*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
(*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. *)
+(*CSC: solo per testare i tempi *)
+(*XXXXXXX *)
+ try
+(* *)
let {D.synthesized = synthesized; D.expected = expected} =
if computeinnertypes then
D.CicHash.find terms_to_types tt
(* We are already in an inner-type and Coscoy's double *)
(* type inference algorithm has not been applied. *)
{D.synthesized =
- CicReduction.whd context (T.type_of_aux' metasenv context tt) ;
+(***CSC: patch per provare i tempi
+ CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
+Cic.Sort Cic.Type ;
D.expected = None}
in
- let innersort = T.type_of_aux' metasenv context synthesized in
+ incr number_new_type_of_aux' ;
+ let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
let ainnertypes,expected_available =
if computeinnertypes then
let annexpected,expected_available =
None,false
in
ainnertypes,synthesized, string_of_sort innersort, expected_available
+(*XXXXXXXX *)
+ with
+ Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *)
+ (* CSC: Type or Set? I can not tell *)
+ None,Cic.Sort Cic.Type,"Type",false
+(* *)
in
let add_inner_type id =
match ainnertypes with
None -> ()
- | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes
+ | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
in
match tt with
C.Rel n ->
(Some (C.Name s,_)) -> s
| _ -> raise NameExpected
in
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
| C.Var (uri,exp_named_subst) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
let exp_named_subst' =
let (_,canonical_context,_) =
List.find (function (m,_,_) -> n = m) metasenv
in
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
C.AMeta (fresh_id'', n,
| 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 ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
| C.Prod (n,s,t) ->
- Hashtbl.add ids_to_inner_sorts fresh_id''
+ xxx_add ids_to_inner_sorts fresh_id''
(string_of_sort innertype) ;
- let sourcetype = T.type_of_aux' metasenv context s in
- Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+ let sourcetype = xxx_type_of_aux' metasenv context s in
+ xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
(string_of_sort sourcetype) ;
let n' =
match n with
C.Anonymous -> n
| C.Name n' ->
- if D.does_not_occur 1 t then
+ if TypeInference.does_not_occur 1 t then
C.Anonymous
else
C.Name n'
(fresh_id'', n', aux' context idrefs s,
aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
| C.Lambda (n,s,t) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- let sourcetype = T.type_of_aux' metasenv context s in
- Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
+ let sourcetype = xxx_type_of_aux' metasenv context s in
+ xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
(string_of_sort sourcetype) ;
if innersort = "Prop" then
begin
(fresh_id'',n, aux' context idrefs s,
aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
| C.LetIn (n,s,t) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.ALetIn
(fresh_id'', n, aux' context idrefs s,
- aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t)
+ aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
| C.Appl l ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_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 idrefs) l)
| C.Const (uri,exp_named_subst) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
let exp_named_subst' =
in
C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
| C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
let exp_named_subst' =
in
C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
| C.MutCase (uri, tyno, outty, term, patterns) ->
- Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
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 ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.AFix (fresh_id'', funno,
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 ;
+ xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.ACoFix (fresh_id'', funno,
) fresh_idrefs funs
)
in
- aux true None context idrefs t
+ let timea = Sys.time () in
+ let res = aux true None context idrefs t in
+ let timeb = Sys.time () in
+ prerr_endline
+ ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
+ res
;;
let acic_of_cic_context metasenv context idrefs t =
C.AVariable
("mettereaposto",id,abo,aty, params)
| C.CurrentProof (id,conjectures,bo,ty,params) ->
-prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ;
let conjectures' =
List.map
(function (i,canonical_context,term) ->
(function
None -> None
| Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
- | Some (n, C.Def t) -> Some (n, C.Def (E.eta_fix conjectures t))
+ | Some (n, C.Def (t,None)) ->
+ Some (n, C.Def ((E.eta_fix conjectures t),None))
+ | Some (_,C.Def (_,Some _)) -> assert false
) canonical_context
in
let term' = E.eta_fix conjectures term in
(i,canonical_context',term')
) conjectures
in
-prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ;
let aconjectures =
List.map
(function (i,canonical_context,term) as conjecture ->
let cid = "c" ^ string_of_int !conjectures_seed in
- Hashtbl.add ids_to_conjectures cid conjecture ;
+ xxx_add ids_to_conjectures cid conjecture ;
incr conjectures_seed ;
let idrefs',revacanonical_context =
let rec aux context idrefs =
| hyp::tl ->
let hid = "h" ^ string_of_int !hypotheses_seed in
let new_idrefs = hid::idrefs in
- Hashtbl.add ids_to_hypotheses hid hyp ;
+ xxx_add ids_to_hypotheses hid hyp ;
incr hypotheses_seed ;
match hyp with
(Some (n,C.Decl t)) ->
conjectures context idrefs t None
in
final_idrefs,(hid,Some (n,C.ADecl at))::atl
- | (Some (n,C.Def t)) ->
+ | (Some (n,C.Def (t,_))) ->
let final_idrefs,atl =
aux (hyp::context) new_idrefs tl in
let at =
in
(cid,i,(List.rev revacanonical_context),aterm)
) conjectures' in
-prerr_endline "*********** INIZIO ETA FIXING PROVA **********";
+ let time1 = Sys.time () in
let bo' = E.eta_fix conjectures' bo in
let ty' = E.eta_fix conjectures' ty in
-prerr_endline "*********** INIZIO CIC ==> ACIC PROVA **********";
+ let time2 = Sys.time () in
+ prerr_endline
+ ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
+ hashtbl_add_time := 0.0 ;
+ type_of_aux'_add_time := 0.0 ;
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
+ let time3 = Sys.time () in
+ prerr_endline
+ ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
+ prerr_endline
+ ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
+ prerr_endline
+ ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ;
+ prerr_endline
+ ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
+ prerr_endline
+ ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
C.ACurrentProof
("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
| C.InductiveDefinition (tys,params,paramsno) ->
exception RferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let prerr_endline _ = ();;
+
(*
let rec fix_lambdas_wrt_type ty te =
let module C = Cic in
let eta_fix metasenv t =
let rec eta_fix' context t =
- prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
- flush stderr ;
+ (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
+ flush stderr ; *)
let module C = Cic in
let module S = CicSubstitution in
match t with
(n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
| C.LetIn (n,s,t) ->
C.LetIn
- (n, eta_fix' context s, eta_fix' ((Some (n,(C.Def s)))::context) t)
+ (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
| C.Appl l as appl ->
let l' = List.map (eta_fix' context) l
in
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
- let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
- if not (CicReduction.are_convertible [] appl result) then
- (prerr_endline ("prima :" ^(CicPp.ppterm appl));
- prerr_endline ("dopo :" ^(CicPp.ppterm result)));
- result
+ fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
| _ -> C.Appl l' )
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (fun (_,t) -> t) constructors
else
let term_type =
- CicTypeChecker.type_of_aux' metasenv context term in
+ TypeInference.type_of_aux' metasenv context term in
(match term_type with
C.Appl (hd::params) ->
List.map (fun (_,t) -> clean_up t params) constructors
let patterns2 =
List.map2 fix_lambdas_wrt_type
constructor_types patterns in
- let dopo =
- C.MutCase (uri, tyno, outty',term',patterns2) in
- if not (CicReduction.are_convertible [] prima dopo) then
- (prerr_endline ("prima :" ^(CicPp.ppterm prima));
- prerr_endline ("dopo :" ^(CicPp.ppterm dopo)));
- dopo
+ C.MutCase (uri, tyno, outty',term',patterns2)
| C.Fix (funno, funs) ->
let fun_types =
List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in
List.fold_right
(fun (n, context, t) i ->
let conjectures',name_context =
- List.fold_right
- (fun context_entry (i,name_context) ->
- (match context_entry with
- Some (n,C.Decl at) ->
+ List.fold_right
+ (fun context_entry (i,name_context) ->
+ (match context_entry with
+ Some (n,C.Decl at) ->
(separate i) ^
- string_of_name n ^ ":" ^ pp at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def at) ->
+ string_of_name n ^ ":" ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,None)) ->
(separate i) ^
- string_of_name n ^ ":= " ^ pp at name_context ^ " ",
- (Some n)::name_context
+ string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+ (Some n)::name_context
| None ->
- (separate i) ^ "_ :? _ ", None::name_context)
- ) context ("",[])
+ (separate i) ^ "_ :? _ ", None::name_context
+ | _ -> assert false)
+ ) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
pp t name_context ^ "\n" ^ i
match List.nth context (n - 1 - k) with
None -> assert false
| Some (_,C.Decl _) -> None
- | Some (_,C.Def x) -> Some (S.lift (n - k) x)
+ | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
end
with
_ -> None
) true l1 l2
| (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+ aux context s1 s2 &&
+ aux ((Some (name1, (C.Decl s1)))::context) t1 t2
| (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
- aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+ aux context s1 s2 &&
+ aux ((Some (name1, (C.Decl s1)))::context) t1 t2
| (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
- aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
+ aux context s1 s2 &&
+ aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2
| (C.Appl l1, C.Appl l2) ->
(try
List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true
C.Rel n as t ->
(match List.nth context (n-1) with
Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_, C.Def bo) -> whdaux l (S.lift n bo)
+ | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)
| C.Var (uri,exp_named_subst) as t ->
) true l1 l2
| (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+ aux context s1 s2 &&
+ aux ((Some (name1, (C.Decl s1)))::context) t1 t2
| (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
- aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+ aux context s1 s2 &&
+ aux ((Some (name1, (C.Decl s1)))::context) t1 t2
| (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
- aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
+ aux context s1 s2 &&
+ aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2
| (C.Appl l1, C.Appl l2) ->
(try
List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true
does_not_occur context n nn te && does_not_occur context n nn ty
| C.Prod (name,so,dest) ->
does_not_occur context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+ does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ dest
| C.Lambda (name,so,dest) ->
does_not_occur context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+ does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ dest
| C.LetIn (name,so,dest) ->
does_not_occur context n nn so &&
- does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
+ does_not_occur ((Some (name,(C.Def (so,None))))::context)
+ (n + 1) (nn + 1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
| C.Var (_,exp_named_subst)
(fun x i ->
i &&
weakly_positive
- ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
+ ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+ x
) cl' true
| t -> does_not_occur context n nn t
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.LetIn (name,so,ta) ->
check_is_really_smaller_arg context n nn kl x safes so &&
- check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
+ check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Appl (he::_) ->
(*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
match CicEnvironment.get_obj uri with
C.InductiveDefinition (tl,_,paramsno) ->
let tys =
- List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
+ List.map
+ (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
in
let (_,isinductive,_,cl) = List.nth tl i in
let cl' =
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
- List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+ List.map (fun (n,_,ty,_) ->
+ Some(Cic.Name n,(Cic.Decl ty))) tl
in
let cl' =
List.map
| C.Rel n ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
- | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
+ | Some (_,C.Def (bo,_)) ->
+ guarded_by_destructors context n nn kl x safes bo
| None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
)
| C.Meta _
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.LetIn (name,so,ta) ->
guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Def so)))::context)
+ guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
let k = List.nth kl (m - n - 1) in
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
- List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+ List.map (fun (n,_,ty,_) ->
+ Some(Cic.Name n,(Cic.Decl ty))) tl
in
let cl' =
List.map
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
- List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+ List.map
+ (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
in
let cl' =
List.map
[] -> true
| he::tl ->
analyse_branch context so he &&
- analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
- de tl
+ analyse_instantiated_type
+ ((Some (name,(C.Decl so)))::context) de tl
end
| C.Lambda _
| C.LetIn _ ->
let n_plus_len = n + len
and nn_plus_len = nn + len
(*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
- and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+ and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,_,ty,bo) i ->
i && does_not_occur context n nn ty &&
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def t))::tl ->
- (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (Some (n,C.Def (t,None)))::tl ->
+ (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
+ | (Some (n,C.Def (_,Some _)))::_ -> assert false
in
aux 1 canonical_context
in
let res =
match (t,ct) with
_,None -> true
- | Some t,Some (_,C.Def ct) ->
+ | Some t,Some (_,C.Def (ct,_)) ->
R.are_convertible context t ct
| Some t,Some (_,C.Decl ct) ->
R.are_convertible context (type_of_aux' metasenv context t) ct
(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)
- | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty
+ | Some (_,C.Def (bo,None)) ->
+ prerr_endline "##### CASO DA INVESTIGARE E CAPIRE" ;
+ type_of_aux context (S.lift n bo)
+ | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
with
_ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term"))
)
C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let _ = type_of_aux context s in
+ let ty = type_of_aux context s in
(* The type of a LetIn is a LetIn. Extremely slow since the computed
LetIn is later reduced and maybe also re-checked.
(C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
(CicSubstitution.subst s
- (type_of_aux ((Some (n,(C.Def s)))::context) t))
+ (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
| 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 in
match i with
Some (n,Cic.Decl t) ->
print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
- | Some (n,Cic.Def t) ->
+ | Some (n,Cic.Def (t,None)) ->
print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
| None ->
"_ ?= _\n", None::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
in
output^newoutput,context'
) ctx ("",[])
Hashtbl.add ids_to_hypotheses hid binding ;
incr hypotheses_seed ;
match binding with
- (Some (n,(Cic.Def t as b)) as entry)
+ (Some (n,(Cic.Def (t,None) as b)) as entry)
| (Some (n,(Cic.Decl t as b)) as entry) ->
let acic = acic_of_cic_context context idrefs t None in
[< s ;
| None ->
(* Invariant: "" is never looked up *)
[< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context ([<>],[],[])
)
in
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t,subst,metasenv
- | Some (_,C.Def bo) ->
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
+ | Some (_,C.Def (bo,None)) ->
+ prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
type_of_aux subst metasenv context (S.lift n bo)
| None -> raise RelToHiddenHypothesis
with
C.Prod (n,s,type2),subst'''',metasenv''''
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let _,subst',metasenv' = type_of_aux subst metasenv context s in
+ let ty,subst',metasenv' = type_of_aux subst metasenv context s in
let inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
+ type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
in
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def t))::tl ->
- (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (Some (n,C.Def (t,None)))::tl ->
+ (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
+ | (Some (_,C.Def (_,Some _)))::_ -> assert false
in
aux 1 canonical_context
in
(fun (subst,metasenv) t ct ->
match (t,ct) with
_,None -> subst,metasenv
- | Some t,Some (_,C.Def ct) ->
+ | Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
with _ -> raise MetasenvInconsistency)
let restrict to_be_restricted =
let rec erase i n =
function
- [] -> []
- | _::tl when List.mem (n,i) to_be_restricted ->
- None::(erase (i+1) n tl)
+ [] -> []
+ | _::tl when List.mem (n,i) to_be_restricted ->
+ None::(erase (i+1) n tl)
| he::tl -> he::(erase (i+1) n tl) in
let rec aux =
function
- [] -> []
- | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
+ [] -> []
+ | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
aux
;;
C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
(*CSC: deliftato la regola per il LetIn *)
else
- (match List.nth context (m-k-1) with
- Some (_,C.Def t) -> deliftaux k (S.lift m t)
- | Some (_,C.Decl t) ->
+ (match List.nth context (m-k-1) with
+ Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t)
+ | Some (_,C.Decl t) ->
(* It may augment to_be_restricted *)
ignore (deliftaux k (S.lift m t)) ;
C.Rel ((position (m-k) l) + k)
- | None -> raise RelToHiddenHypothesis)
+ | None -> raise RelToHiddenHypothesis)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
(* First possibility: restriction *)
(* Second possibility: unification *)
(* Third possibility: convertibility *)
- R.are_convertible context t1' t2'
+ R.are_convertible context t1' t2'
) true ln lm
in
if ok then subst,metasenv else raise UnificationFailed
| (C.Meta (n,l), t)
| (t, C.Meta (n,l)) ->
let subst',metasenv' =
- try
- let oldt = (List.assoc n subst) in
- let lifted_oldt = S.lift_meta l oldt in
- fo_unif_subst subst context metasenv lifted_oldt t
- with Not_found ->
- let t',metasenv' = delift context metasenv l t in
- (n, t')::subst, metasenv'
+ try
+ let oldt = (List.assoc n subst) in
+ let lifted_oldt = S.lift_meta l oldt in
+ fo_unif_subst subst context metasenv lifted_oldt t
+ with Not_found ->
+ let t',metasenv' = delift context metasenv l t in
+ (n, t')::subst, metasenv'
in
- let (_,_,meta_type) =
- List.find (function (m,_,_) -> m=n) metasenv' in
- let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
- fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+ let (_,_,meta_type) =
+ List.find (function (m,_,_) -> m=n) metasenv' in
+ let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
+ fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
| (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
| (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
if UriManager.eq uri1 uri2 then
in
fo_unif_l subst' metasenv' (l1,l2)
in
- fo_unif_l subst metasenv (lr1, lr2)
+ fo_unif_l subst metasenv (lr1, lr2)
| (C.Const _, _)
| (_, C.Const _)
| (C.MutInd _, _)
let subst', metasenv' =
fo_unif_subst subst context metasenv outt1 outt2 in
let subst'',metasenv'' =
- fo_unif_subst subst' context metasenv' t1 t2 in
+ fo_unif_subst subst' context metasenv' t1 t2 in
List.fold_left2
- (function (subst,metasenv) ->
+ (function (subst,metasenv) ->
fo_unif_subst subst context metasenv
) (subst'',metasenv'') pl1 pl2
| (C.Fix _, _)
let restrict canonical_context m k l =
let rec erase i =
function
- [] -> []
- | None::tl -> None::(erase (i+1) tl)
- | he::tl ->
- let i' = (List.nth l (i-1)) in
- if i' <= k
- then he::(erase (i+1) tl) (* local variable *)
- else
- let acc =
- (try List.nth canonical_context (i'-k-1)
- with Failure _ -> None) in
- if acc = None
- then None::(erase (i+1) tl)
- else he::(erase (i+1) tl) in
+ [] -> []
+ | None::tl -> None::(erase (i+1) tl)
+ | he::tl ->
+ let i' = (List.nth l (i-1)) in
+ if i' <= k
+ then he::(erase (i+1) tl) (* local variable *)
+ else
+ let acc =
+ (try List.nth canonical_context (i'-k-1)
+ with Failure _ -> None) in
+ if acc = None
+ then None::(erase (i+1) tl)
+ else he::(erase (i+1) tl) in
let rec aux =
function
- [] -> []
- | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
- | hd::tl -> hd::(aux tl)
+ [] -> []
+ | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
+ | hd::tl -> hd::(aux tl)
in
aux
;;
| C.Sort _ -> metasenv
| C.Implicit -> metasenv
| C.Cast (te,ty) ->
- let metasenv' = aux metasenv k te in
- aux metasenv' k ty
+ let metasenv' = aux metasenv k te in
+ aux metasenv' k ty
| C.Prod (_,s,t)
| C.Lambda (_,s,t)
| C.LetIn (_,s,t) ->
- let metasenv' = aux metasenv k s in
- aux metasenv' (k+1) t
+ let metasenv' = aux metasenv k s in
+ aux metasenv' (k+1) t
| C.Appl l ->
- List.fold_left
- (function metasenv -> aux metasenv k) metasenv l
+ List.fold_left
+ (function metasenv -> aux metasenv k) metasenv l
| C.Const _
| C.MutInd _
| C.MutConstruct _ -> metasenv
| C.MutCase (_,_,_,outty,t,pl) ->
- let metasenv' = aux metasenv k outty in
- let metasenv'' = aux metasenv' k t in
- List.fold_left
- (function metasenv -> aux metasenv k) metasenv'' pl
+ let metasenv' = aux metasenv k outty in
+ let metasenv'' = aux metasenv' k t in
+ List.fold_left
+ (function metasenv -> aux metasenv k) metasenv'' pl
| C.Fix (i, fl) ->
let len = List.length fl in
List.fold_left
(fun metasenv f ->
- let (_,_,ty,bo) = f in
- let metasenv' = aux metasenv k ty in
- aux metasenv' (k+len) bo
+ let (_,_,ty,bo) = f in
+ let metasenv' = aux metasenv k ty in
+ aux metasenv' (k+len) bo
) metasenv fl
| C.CoFix (i, fl) ->
- let len = List.length fl in
+ let len = List.length fl in
List.fold_left
(fun metasenv f ->
- let (_,ty,bo) = f in
- let metasenv' = aux metasenv k ty in
- aux metasenv' (k+len) bo
+ let (_,ty,bo) = f in
+ let metasenv' = aux metasenv k ty in
+ aux metasenv' (k+len) bo
) metasenv fl
in aux metasenv 0
;;
C.Rel _ as t -> t,metasenv
| C.Var _ as t -> t,metasenv
| C.Meta (i,l) ->
- (try
+ (try
S.lift_meta l (List.assoc i !unwinded), metasenv
with Not_found ->
if List.mem i !frozen then raise OccurCheck
else
let saved_frozen = !frozen in
- frozen := i::!frozen ;
+ frozen := i::!frozen ;
let res =
try
- let t = List.assoc i subst in
+ let t = List.assoc i subst in
let t',metasenv' = um_aux metasenv t in
- let _,metasenv'' =
+ let _,metasenv'' =
let (_,canonical_context,_) =
List.find (function (m,_,_) -> m=i) metasenv
in
(* not constrained variable, i.e. free in subst*)
let l',metasenv' =
List.fold_right
- (fun t (tl,metasenv) ->
+ (fun t (tl,metasenv) ->
match t with
None -> None::tl,metasenv
| Some t ->
- let t',metasenv' = um_aux metasenv t in
- (Some t')::tl, metasenv'
- ) l ([],metasenv)
+ let t',metasenv' = um_aux metasenv t in
+ (Some t')::tl, metasenv'
+ ) l ([],metasenv)
in
C.Meta (i,l'), metasenv'
in
| C.Appl (he::tl) ->
let tl',metasenv' =
List.fold_right
- (fun t (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- t'::tl, metasenv'
- ) tl ([],metasenv)
+ (fun t (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ t'::tl, metasenv'
+ ) tl ([],metasenv)
in
begin
match um_aux metasenv' he with
| C.Const (uri,exp_named_subst) ->
let exp_named_subst', metasenv' =
List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
+ (fun (uri,t) (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ (uri,t')::tl, metasenv'
+ ) exp_named_subst ([],metasenv)
in
C.Const (uri,exp_named_subst'),metasenv'
| C.MutInd (uri,typeno,exp_named_subst) ->
let exp_named_subst', metasenv' =
List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
+ (fun (uri,t) (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ (uri,t')::tl, metasenv'
+ ) exp_named_subst ([],metasenv)
in
C.MutInd (uri,typeno,exp_named_subst'),metasenv'
| C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
let exp_named_subst', metasenv' =
List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
+ (fun (uri,t) (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ (uri,t')::tl, metasenv'
+ ) exp_named_subst ([],metasenv)
in
C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
| C.MutCase (sp,i,outty,t,pl) ->
let t',metasenv'' = um_aux metasenv' t in
let pl',metasenv''' =
List.fold_right
- (fun p (pl,metasenv) ->
- let p',metasenv' = um_aux metasenv p in
- p'::pl, metasenv'
- ) pl ([],metasenv'')
+ (fun p (pl,metasenv) ->
+ let p',metasenv' = um_aux metasenv p in
+ p'::pl, metasenv'
+ ) pl ([],metasenv'')
in
C.MutCase (sp, i, outty', t', pl'),metasenv'''
| C.Fix (i, fl) ->
let liftedfl,metasenv' =
List.fold_right
(fun (name, i, ty, bo) (fl,metasenv) ->
- let ty',metasenv' = um_aux metasenv ty in
- let bo',metasenv'' = um_aux metasenv' bo in
- (name, i, ty', bo')::fl,metasenv''
- ) fl ([],metasenv)
+ let ty',metasenv' = um_aux metasenv ty in
+ let bo',metasenv'' = um_aux metasenv' bo in
+ (name, i, ty', bo')::fl,metasenv''
+ ) fl ([],metasenv)
in
C.Fix (i, liftedfl),metasenv'
| C.CoFix (i, fl) ->
let liftedfl,metasenv' =
List.fold_right
(fun (name, ty, bo) (fl,metasenv) ->
- let ty',metasenv' = um_aux metasenv ty in
- let bo',metasenv'' = um_aux metasenv' bo in
- (name, ty', bo')::fl,metasenv''
- ) fl ([],metasenv)
+ let ty',metasenv' = um_aux metasenv ty in
+ let bo',metasenv'' = um_aux metasenv' bo in
+ (name, ty', bo')::fl,metasenv''
+ ) fl ([],metasenv)
in
C.CoFix (i, liftedfl),metasenv'
in
[] -> []
| Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
CicSubstitution.lift n a))] @ superlift next (n+1)
- | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
- CicSubstitution.lift n a))] @ superlift next (n+1)
+ | Some(name,Cic.Def(a,None))::next -> [Some(name,Cic.Def((
+ CicSubstitution.lift n a),None))] @ superlift next (n+1)
+ | Some(name,Cic.Def(a,Some ty))::next -> [Some(name,Cic.Def((
+ CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1)
| _::next -> superlift next (n+1) (*?? ??*)
;;
(context',ty,C.Lambda(n',s,bo))
| C.LetIn (n,s,t) ->
let (context',ty,bo) =
- collect_context ((Some (n,(C.Def s)))::context) t
+ collect_context ((Some (n,(C.Def (s,None))))::context) t
in
(context',ty,C.LetIn(n,s,bo))
| _ as t ->
match entry with
Some (n,Cic.Decl s) ->
Some (n,Cic.Decl (subst_in canonical_context' s))
- | Some (n,Cic.Def s) ->
- Some (n,Cic.Def (subst_in canonical_context' s))
+ | Some (n,Cic.Def (s,None)) ->
+ Some (n,Cic.Def ((subst_in canonical_context' s),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
in
entry'::canonical_context'
) canonical_context []
let fresh_name =
mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in
let context_for_newmeta =
- (Some (fresh_name,C.Def term))::context in
+ (Some (fresh_name,C.Def (term,None)))::context in
let irl =
identity_relocation_list_for_metavariable context_for_newmeta in
let newmetaty = CicSubstitution.lift 1 ty in
let context' =
List.map
(function
- Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
+ Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None))
| Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context
in
let metasenv' =
List.map
(function
Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
+ | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context
in
i,canonical_context',(subst_in ty)
(function
None -> None
| Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
- | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t))
+ | Some (i,Cic.Def (t,None)) ->
+ Some (i,Cic.Def ((subst_in t),None))
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context
in
(m,canonical_context',subst_in ty)::i
C.Rel n as t ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
+ | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)
| C.Var (uri,exp_named_subst) ->
C.Rel n as t ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def bo) ->
+ | Some (_,C.Def (bo,_)) ->
try_delta_expansion l t (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)
let module C = Cic in
match hyp with
None -> assert false
+ | Some (_, C.Def (_, Some _)) -> assert false
| Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
- | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
+ | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
let curi,metasenv,pbo,pty = proof in
let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let string_of_name =
cleared_entry::context
| None -> None::context
| Some (n,C.Decl t)
- | Some (n,C.Def t) ->
+ | Some (n,C.Def (t,None)) ->
let _ =
try
CicTypeChecker.type_of_aux' metasenv context t
)
in
entry::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context []
in
let _ =
match entry with
t when t == hyp_to_clear -> None::context
| None -> None::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
| Some (n,C.Decl t)
- | Some (n,C.Def t) ->
+ | Some (n,C.Def (t,None)) ->
let _ =
try
CicTypeChecker.type_of_aux' metasenv context t
List.fold_right
(fun entry context ->
match entry with
- Some (name,Cic.Def t) ->
- (Some (name,Cic.Def (replace context t)))::context
+ Some (name,Cic.Def (t,None)) ->
+ (Some (name,Cic.Def ((replace context t),None)))::context
| Some (name,Cic.Decl t) ->
(Some (name,Cic.Decl (replace context t)))::context
| None -> None::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context []
else
context
List.map
(function
Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
- | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t))
+ | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context
else
context
(match hd with
(Some (_, C.Decl t)) when
(R.are_convertible context (S.lift n t) ty) -> n
- | (Some (_, C.Def t)) when
+ | (Some (_, C.Def (_,Some ty'))) when
+ (R.are_convertible context ty' ty) -> n
+ | (Some (_, C.Def (t,None))) when
(R.are_convertible context
(CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
| _ -> find (n+1) tl
projects / helm.git / commitdiff