and Defs. This is a back-porting from the new generation kernel.
TODO:
a) debug some failing examples (paramodulation)
b) port the code by Ferruccio
c) do something for Coq files (that are now rejected)
| C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
| C.Cast (te,ty) -> (occur uri te)
| C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
- | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
+ | C.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t)
| C.Appl l ->
List.fold_left
(fun b a ->
| C.AProd (id,_,_,_) -> id
| C.ACast (id,_,_) -> id
| C.ALambda (id,_,_,_) -> id
- | C.ALetIn (id,_,_,_) -> id
+ | C.ALetIn (id,_,_,_,_) -> id
| C.AAppl (id,_) -> id
| C.AConst (id,_,_) -> id
| C.AMutInd (id,_,_,_) -> id
ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
true;
with Not_found -> false)
- | C.ALetIn (id,_,_,_) ->
+ | C.ALetIn (id,_,_,_,_) ->
(try
ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
true;
}
;;
-let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
+let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types =
let module C2A = Cic2acic in
let module C = Cic in
let module K = Content in
(match inner_proof.K.proof_conclude.K.conclude_conclusion with
None -> None
| Some t ->
- if is_intro then Some (C.AProd ("gen"^id,n,s,t))
- else Some (C.ALetIn ("gen"^id,n,s,t)))
+ match ty with
+ None -> Some (C.AProd ("gen"^id,n,s,t))
+ | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t)))
};
}
;;
and
-build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types =
+build_def_item seed context metasenv id n t ty ~ids_to_inner_sorts ~ids_to_inner_types =
let module K = Content in
try
let sort = Hashtbl.find ids_to_inner_sorts id in
{ K.def_name = name_of n;
K.def_id = gen_id definition_prefix seed;
K.def_aref = id;
- K.def_term = t
+ K.def_term = t;
+ K.def_type = ty
}
with
Not_found -> assert false
proof'.K.proof_context
}
in
- generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
+ generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types
else
raise Not_a_proof
- | C.ALetIn (id,n,s,t) ->
+ | C.ALetIn (id,n,s,ty,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
- let proof = (* XXX TIPAMI!!! *)
- aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t
+ let proof =
+ aux
+ ((Some (n,
+ Cic.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::context) t
in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
{ proof' with
K.proof_name = None;
K.proof_context =
- ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts
+ ((build_def_item seed context metasenv (get_id s) n s ty ids_to_inner_sorts
ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
::proof'.K.proof_context;
}
in
- generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
+ generate_intros_let_tac seed id n s (Some ty) proof'' name ~ids_to_inner_types
else
raise Not_a_proof
| C.AAppl (id,li) ->
K.dec_aref = get_id t;
K.dec_type = t
})
- | (id,Some (name,Cic.ADef t)) ->
+ | (id,Some (name,Cic.ADef (t,ty))) ->
Some
(* We should call build_def_item, but we have not computed *)
(* the inner-types ==> we always produce a declaration *)
{ K.def_name = name_of name;
K.def_id = gen_id definition_prefix seed;
K.def_aref = get_id t;
- K.def_term = t
+ K.def_term = t;
+ K.def_type = ty
})
) context
in
K.dec_aref = get_id t;
K.dec_type = t
})
- | (id,Some (name,Cic.ADef t)) ->
+ | (id,Some (name,Cic.ADef (t,ty))) ->
Some
(* We should call build_def_item, but we have not computed *)
(* the inner-types ==> we always produce a declaration *)
{ K.def_name = name_of name;
K.def_id = id;
K.def_aref = get_id t;
- K.def_term = t
+ K.def_term = t;
+ K.def_type = ty
})
) context
in
`Def (K.Const,ty,
build_def_item
seed [] (Deannotate.deannotate_conjectures conjectures)
- (get_id bo) (C.Name n) bo
+ (get_id bo) (C.Name n) bo ty
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AConstant (_,_,n,Some bo,ty,params,_) ->
(gen_id object_prefix seed, params, None,
`Def (K.Const,ty,
- build_def_item seed [] [] (get_id bo) (C.Name n) bo
+ build_def_item seed [] [] (get_id bo) (C.Name n) bo ty
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AConstant (id,_,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,
| C.AVariable (_,n,Some bo,ty,params,_) ->
(gen_id object_prefix seed, params, None,
`Def (K.Var,ty,
- build_def_item seed [] [] (get_id bo) (C.Name n) bo
+ build_def_item seed [] [] (get_id bo) (C.Name n) bo ty
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AVariable (id,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,
(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(pp_patterns patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
- | Ast.LetIn (var, t1, t2) ->
- sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1)
+ | Ast.LetIn ((var,t2), t1, t3) ->
+ let t2 = match t2 with None -> Ast.Implicit | Some t -> t in
+ sprintf "let %s : %s \\def %s in %s" (pp_term var)
(pp_term ~pp_parens:true t2)
+ (pp_term ~pp_parens:true t1)
+ (pp_term ~pp_parens:true t3)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
| [] -> (*assert false*) Ast.Implicit
| Ast.Case (term, indtype, typ, patterns) ->
Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns)
| Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
- | Ast.LetIn (var, t1, t2) ->
- Ast.LetIn (aux_capture_variable var, k t1, k t2)
+ | Ast.LetIn (var, t1, t3) ->
+ Ast.LetIn (aux_capture_variable var, k t1, k t3)
| Ast.LetRec (kind, definitions, term) ->
let definitions =
List.map
aux term ;
aux_opt outty_opt ;
List.iter aux_branch patterns
- | Ast.LetIn (_, t1, t2) ->
+ | Ast.LetIn (_, t1, t3) ->
aux t1 ;
- aux t2
+ aux t3
| Ast.LetRec (_, definitions, body) ->
List.iter aux_definition definitions ;
aux body
{ def_name : string option;
def_id : id ;
def_aref : string ;
- def_term : 'term
+ def_term : 'term ;
+ def_type : 'term
}
;;
{ def_name : string option;
def_id : id ;
def_aref : string ;
- def_term : 'term
+ def_term : 'term ;
+ def_type : 'term
}
;;
| None ->
C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
| `Proof p ->
+ let ty =
+ match p.Con.proof_conclude.Con.conclude_conclusion with
+ None -> (*Cic.Implicit None*) assert false
+ | Some ty -> deannotate ty
+ in
(match p.Con.proof_name with
Some s ->
- C.LetIn (C.Name s, proof2cic premise_env p, target)
+ C.LetIn (C.Name s, proof2cic premise_env p, ty , target)
| None ->
- C.LetIn (C.Anonymous, proof2cic premise_env p, target))
+ C.LetIn (C.Anonymous, proof2cic premise_env p, ty, target))
| `Definition d ->
(match d.Con.def_name with
Some s ->
- C.LetIn (C.Name s, proof2cic premise_env p, target)
+ C.LetIn (C.Name s, proof2cic premise_env p, deannotate d.Con.def_type, target)
| None ->
- C.LetIn (C.Anonymous, proof2cic premise_env p, target))
+ C.LetIn (C.Anonymous, proof2cic premise_env p, deannotate d.Con.def_type, target))
| `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
(match target with
C.Rel n ->
| _ -> assert false)
| Some (`Definition d) ->
(match d with
- {K.def_name = Some n ; K.def_term = t} ->
- Some (Cic.Name n, Cic.Def ((deannotate t),None))
+ {K.def_name = Some n ; K.def_term = t ; K.def_type = ty} ->
+ Some (Cic.Name n, Cic.Def (deannotate t,deannotate ty))
| _ -> assert false)
| Some (`Proof d) ->
(match d with
{K.proof_name = Some n } ->
Some (Cic.Name n,
- Cic.Def ((proof2cic deannotate d),None))
+ Cic.Def ((proof2cic deannotate d),assert false))
| _ -> assert false)
) canonical_context
in
| Cic.ALambda (id,n,s,t) ->
idref id (Ast.Binder (`Lambda,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
- | Cic.ALetIn (id,n,s,t) ->
- idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+ | Cic.ALetIn (id,n,s,ty,t) ->
+ idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, Some (k ty)),
k s, k t))
| Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
in
st, C.Decl (H.cic ity), rqv
| None ->
- st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)]
+ (*CSC: here we need the type of v *)
+ st, C.Def (H.cic v, assert false), [T.LetIn (intro, v, dtext)]
in
let entry = Some (name, hyp) in
let qt = proc_proof (next (add st entry intro)) t in
in
match t with
| C.ALambda (_, name, w, t) -> proc_lambda st name w t
- | C.ALetIn (_, name, v, t) as what -> proc_letin (f st) what name v t
+ | C.ALetIn (_, name, v, ty, t) as what -> assert false (*proc_letin (f st) what name v t*)
| C.ARel _ as what -> proc_rel (f st) what
| C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
| C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
| C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
| C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
| C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
- | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
+ | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t)
| C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
| C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
in
| Invalid_argument _ -> assert false
in
let mk_decl n v = Some (n, C.Decl v) in
- let mk_def n v = Some (n, C.Def (v, None)) in
- let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
- let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
+ let mk_def n v ty = Some (n, C.Def (v, ty)) in
+ let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in
+ let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in
let rec ann_xns c (uri, t) = uri, ann_term c t
and ann_ms c = function
| None -> None
| C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
| C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
| C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
- | C.LetIn (n, s, t) -> C.ALetIn (id, n, ann_term c s, ann_term (mk_def n s :: c) t)
+ | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t)
| C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
| C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
in
| C.ALambda (id, _, s, t) ->
let s, t = gen_term k s, gen_term (succ k) t in
if is_meta [s; t] then meta id else C.ALambda (id, anon, s, t)
- | C.ALetIn (id, _, s, t) ->
- let s, t = gen_term k s, gen_term (succ k) t in
- if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, t)
+ | C.ALetIn (id, _, s, ty, t) ->
+ let s, ty, t = gen_term k s, gen_term k ty, gen_term (succ k) t in
+ if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, ty, t)
| C.AFix (id, i, fl) -> C.AFix (id, i, List.map (gen_fix (List.length fl) k) fl)
| C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (gen_cofix (List.length fl) k) fl)
in
else
hd, names, v
in
- let p = C.LetIn (n, v, p) in
- let it = C.LetIn (n, v, it) in
- let et = C.LetIn (n, v, et) in
+ let p = C.LetIn (n, v, assert false, p) in
+ let it = C.LetIn (n, v, assert false, it) in
+ let et = C.LetIn (n, v, assert false, et) in
aux (hd :: c) names p it et tl
| Some (C.Anonymous as n, C.Decl v) as hd :: tl ->
let p = C.Lambda (n, meta, p) in
let et = C.Lambda (n, meta, et) in
aux (hd :: c) names p it et tl
| Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
- let p = C.LetIn (n, meta, p) in
- let it = C.LetIn (n, meta, it) in
- let et = C.LetIn (n, meta, et) in
+ let p = C.LetIn (n, meta, assert false, p) in
+ let it = C.LetIn (n, meta, assert false, it) in
+ let et = C.LetIn (n, meta, assert false, et) in
aux (hd :: c) names p it et tl
| None :: tl -> assert false
in
let get_fix_decl (sname, i, w, v) = sname, w in
let get_cofix_decl (sname, w, v) = sname, w in
let rec bc c = function
- | C.LetIn (name, v, t) ->
+ | C.LetIn (name, v, ty, t) ->
let name = mk_fresh_name c name in
- let entry = Some (name, C.Def (v, None)) in
- let v, t = bc c v, bc (entry :: c) t in
- C.LetIn (name, v, t)
+ let entry = Some (name, C.Def (v, ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.LetIn (name, v, ty, t)
| C.Lambda (name, w, t) ->
let name = mk_fresh_name c name in
let entry = Some (name, C.Decl w) in
let get_fix_decl (id, sname, i, w, v) = sname, cic w in
let get_cofix_decl (id, sname, w, v) = sname, cic w in
let rec bc c = function
- | C.ALetIn (id, name, v, t) ->
+ | C.ALetIn (id, name, v, ty, t) ->
let name = mk_fresh_name c name in
- let entry = Some (name, C.Def (cic v, None)) in
- let v, t = bc c v, bc (entry :: c) t in
- C.ALetIn (id, name, v, t)
+ let entry = Some (name, C.Def (cic v, cic ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.ALetIn (id, name, v, ty, t)
| C.ALambda (id, name, w, t) ->
let name = mk_fresh_name c name in
let entry = Some (name, C.Decl (cic w)) in
let define v =
let name = C.Name defined_premise in
- C.LetIn (name, v, C.Rel 1)
+ (*CSC: here we need the type of v *)
+ C.LetIn (name, v, assert false, C.Rel 1)
let clear_absts m =
let rec aux k n = function
let rec opt1_letin g es c name v t =
let name = H.mk_fresh_name c name in
- let entry = Some (name, C.Def (v, None)) in
+ (*CSC: here we need the type of v *)
+ let entry = Some (name, C.Def (v, assert false)) in
let g t =
if DTI.does_not_occur 1 t then begin
let x = S.lift (-1) t in
HLog.warn "Optimizer: remove 1"; opt1_proof g true c x
end else
let g = function
- | C.LetIn (nname, vv, tt) when H.is_proof c v ->
- let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
+ | C.LetIn (nname, vv, tyty, tt) when H.is_proof c v ->
+ (*CSC: here we need the type of v *)
+ let x = C.LetIn (nname, vv, tyty,
+ C.LetIn (name, tt, assert false, S.lift_from 2 1 t)) in
HLog.warn "Optimizer: swap 1"; opt1_proof g true c x
| v when H.is_proof c v && H.is_atomic v ->
let x = S.subst v t in
HLog.warn "Optimizer: remove 5"; opt1_proof g true c x
| v ->
- g (C.LetIn (name, v, t))
+ (*CSC: here we need the type of v *)
+ g (C.LetIn (name, v, assert false, t))
in
if es then opt1_term g es c v else g v
in
and opt1_appl g es c t vs =
let g vs =
let g = function
- | C.LetIn (mame, vv, tt) ->
+ | C.LetIn (mame, vv, tyty, tt) ->
let vs = List.map (S.lift 1) vs in
- let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in
+ let x = C.LetIn (mame, vv, tyty, C.Appl (tt :: vs)) in
HLog.warn "Optimizer: swap 2"; opt1_proof g true c x
| C.Lambda (name, ww, tt) ->
let v, vs = List.hd vs, List.tl vs in
- let x = C.Appl (C.LetIn (name, v, tt) :: vs) in
+ (*CSC: here we need the type of v *)
+ let x = C.Appl (C.LetIn (name, v, assert false, tt) :: vs) in
HLog.warn "Optimizer: remove 2"; opt1_proof g true c x
| C.Appl vvs ->
let x = C.Appl (vvs @ vs) in
aux false [] (vs, classes)
*) in
let rec aux h prev = function
- | C.LetIn (name, vv, tt) :: vs ->
+ | C.LetIn (name, vv, tyty, tt) :: vs ->
let t = S.lift 1 t in
let prev = List.map (S.lift 1) prev in
let vs = List.map (S.lift 1) vs in
let y = C.Appl (t :: List.rev prev @ tt :: vs) in
- let x = C.LetIn (name, vv, y) in
+ (*CSC: here we need the type of vv *)
+ let x = C.LetIn (name, vv, assert false, y) in
HLog.warn "Optimizer: swap 3"; opt1_proof g true c x
| v :: vs -> aux h (v :: prev) vs
| [] -> h ()
and opt1_other g es c t = g t
and opt1_proof g es c = function
- | C.LetIn (name, v, t) -> opt1_letin g es c name v t
+ (*CSC: what to do now that we have also ty? *)
+ | C.LetIn (name, v, ty, t) -> assert false (*opt1_letin g es c name v t*)
| C.Lambda (name, w, t) -> opt1_lambda g es c name w t
| C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs)
| C.Appl [t] -> opt1_proof g es c t
g (absts t)
let rec opt2_letin g c name v t =
- let entry = Some (name, C.Def (v, None)) in
+ (*CSC: here we need the type of v *)
+ let entry = Some (name, C.Def (v, assert false)) in
let g t =
- let g v = g (C.LetIn (name, v, t)) in
+ (*CSC: here we need the type of v *)
+ let g v = g (C.LetIn (name, v, assert false, t)) in
opt2_term g c v
in
opt2_proof g (entry :: c) t
end else g t
and opt2_proof g c = function
- | C.LetIn (name, v, t) -> opt2_letin g c name v t
+ (*CSC: what to do now that we have also ty? *)
+ | C.LetIn (name, v, ty, t) -> assert false (*opt2_letin g c name v t*)
| C.Lambda (name, w, t) -> opt2_lambda g c name w t
| C.Appl (t :: vs) -> opt2_appl g c t vs
| t -> opt2_other g c t
| Cast of term * term (* value, type *)
| Prod of name * term * term (* binder, source, target *)
| Lambda of name * term * term (* binder, source, target *)
- | LetIn of name * term * term (* binder, term, target *)
+ | LetIn of name * term * term * term (* binder, term, type, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * (* uri, *)
term explicit_named_substitution (* explicit named subst. *)
| ACast of id * annterm * annterm (* value, type *)
| AProd of id * name * annterm * annterm (* binder, source, target *)
| ALambda of id * name * annterm * annterm (* binder, source, target *)
- | ALetIn of id * name * annterm * annterm (* binder, term, target *)
+ | ALetIn of id * name * annterm * annterm * annterm (* binder, term, type, target *)
| AAppl of id * annterm list (* arguments *)
| AConst of id * UriManager.uri * (* uri, *)
annterm explicit_named_substitution (* explicit named subst. *)
and context_entry = (* A declaration or definition *)
Decl of term
- | Def of term * term option (* body, type (if known) *)
+ | Def of term * term (* body, type *)
and hypothesis =
(name * context_entry) option (* None means no more accessible *)
and anncontext_entry = (* A declaration or definition *)
ADecl of annterm
- | ADef of annterm
+ | ADef of annterm * annterm
and annhypothesis =
id * (name * anncontext_entry) option (* None means no more accessible *)
in
List.fold_left map g ss
| C.Cast (t1, t2) -> aux d (aux d g t2) t1
- | C.LetIn (_, t1, t2)
| C.Lambda (_, t1, t2)
| C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+ | C.LetIn (_, t1, ty, t2) ->
+ aux d (aux d (aux (succ d) g t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux d (aux d (List.fold_left (aux d) g ss) t2) t1
| C.Fix (_, ss) ->
in
List.fold_left map g ss
| C.Cast (t1, t2) -> aux (aux g t2) t1
- | C.LetIn (_, t1, t2)
| C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+ | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+ | C.LetIn (_, t1, ty, t2) -> aux (aux (aux g t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux (aux (List.fold_left aux g ss) t2) t1
| C.Fix (_, ss) ->
in
List.fold_left map (succ n) ss
| C.Cast (t1, t2)
- | C.LetIn (_, t1, t2)
| C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
+ | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
+ | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux (aux (List.fold_left aux (succ n) ss) t2) t1
| C.Fix (_, ss) ->
(* id, name, type, body *)
| Constructor of string * Cic.annterm (* name, type *)
| Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
- | Def of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
+ | Def of Cic.id * Cic.name * Cic.annterm * Cic.annterm (* id, binder, source, type *)
| Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
(* id, name, ind. index, type, body *)
| Inductive_type of string * string * bool * Cic.annterm *
| Constructor (name, _) -> "Constructor " ^ name
| Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
| Decl (id, _, _) -> sprintf "Decl (id=%s)" id
- | Def (id, _, _) -> sprintf "Def (id=%s)" id
+ | Def (id, _, _, _) -> sprintf "Def (id=%s)" id
| Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
| Inductive_type (id, name, _, _, _) ->
sprintf "Inductive_type %s (id=%s)" name id
| ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "def" -> (* same as "decl" above *)
+ let ty = pop_cic ctxt in
let source = pop_cic ctxt in
push ctxt
(match pop_tag_attrs ctxt with
| ["binder", binder; "id", id]
| ["binder", binder; "id", id; "sort", _] ->
- Def (id, Cic.Name binder, source)
+ Def (id, Cic.Name binder, source, ty)
| ["id", id]
- | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
+ | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty)
| _ -> attribute_error ())
| "arity" (* transparent elements (i.e. which contain a CIC) *)
| "body"
| "LETIN" ->
let target = pop_cic ctxt in
let rec add_def target = function
- | Def (id, binder, source) :: tl ->
- add_def (Cic.ALetIn (id, binder, source, target)) tl
+ | Def (id, binder, source, ty) :: tl ->
+ add_def (Cic.ALetIn (id, binder, source, ty, target)) tl
| tl ->
ctxt.stack <- tl;
target
| C.Cast (te,ty) -> is_closed k te && is_closed k ty
| C.Prod (name,so,dest) -> is_closed k so && is_closed (k+1) dest
| C.Lambda (_,so,dest) -> is_closed k so && is_closed (k+1) dest
- | C.LetIn (_,so,dest) -> is_closed k so && is_closed (k+1) dest
+ | C.LetIn (_,so,ty,dest) ->
+ is_closed k so && is_closed k ty && is_closed (k+1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && is_closed k x) l true
| C.Var (_,exp_named_subst)
| C.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty
| C.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest
| C.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
- | C.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest
+ | C.LetIn (_,so,ty,dest) ->
+ is_meta_closed so &&
+ is_meta_closed ty &&
+ is_meta_closed dest
| C.Appl l ->
not (List.exists (fun x -> not (is_meta_closed x)) l)
| C.Var (_,exp_named_subst)
| C.ACast (id,_,_)
| C.AProd (id,_,_,_)
| C.ALambda (id,_,_,_)
- | C.ALetIn (id,_,_,_)
+ | C.ALetIn (id,_,_,_,_)
| C.AAppl (id,_)
| C.AConst (id,_,_)
| C.AMutInd (id,_,_,_)
| C.Cast (te,ty) -> C.Cast (rehash_term te, rehash_term ty)
| C.Prod (n,s,t) -> C.Prod (n, rehash_term s, rehash_term t)
| C.Lambda (n,s,t) -> C.Lambda (n, rehash_term s, rehash_term t)
- | C.LetIn (n,s,t) -> C.LetIn (n, rehash_term s, rehash_term t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, rehash_term s, rehash_term ty, rehash_term t)
| C.Appl l -> C.Appl (List.map rehash_term l)
| C.Const (uri,exp_named_subst) ->
let uri' = recons uri in
| Some (name,C.Decl t) ->
Some (name,C.Decl (rehash_term t))
| Some (name,C.Def (bo,ty)) ->
- let ty' =
- match ty with
- None -> None
- | Some ty'' -> Some (rehash_term ty'')
- in
- Some (name,C.Def (rehash_term bo, ty'))) hyps,
+ Some (name,C.Def (rehash_term bo, rehash_term ty))) hyps,
rehash_term ty))
conjs
in
List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
| C.Cast (s, t)
| C.Prod (_, s, t)
- | C.Lambda (_, s, t)
- | C.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+ | C.Lambda (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+ | C.LetIn (_, s, ty, t) ->
+ (metas_of_term s) @ (metas_of_term ty) @ (metas_of_term t)
| C.Appl l -> List.flatten (List.map metas_of_term l)
| C.MutCase (uri, i, s, t, l) ->
(metas_of_term s) @ (metas_of_term t) @
S.empty ens
| C.Cast (s, t)
| C.Prod (_, s, t)
- | C.Lambda (_, s, t)
- | C.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t)
+ | C.Lambda (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t)
+ | C.LetIn (_, s, ty, t) ->
+ S.union (metas_of_term_set s)
+ (S.union (metas_of_term_set ty) (metas_of_term_set t))
| C.Appl l ->
List.fold_left
(fun s t -> S.union s (metas_of_term_set t))
aux s s' && aux t t'
| C.Lambda (_,s,t), C.Lambda (_,s',t') ->
aux s s' && aux t t'
- | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
- aux s s' && aux t t'
+ | C.LetIn (_,s,ty,t), C.LetIn(_,s',ty',t') ->
+ aux s s' && aux ty ty' && aux t t'
| C.Appl l, C.Appl l' when List.length l = List.length l' ->
(try
List.fold_left2
| C.MutConstruct (_, _, _, xnss)
| C.MutInd (_, _, xnss) -> sober_xnss g xnss
| C.Meta (_, xss) -> sober_xss g xss
- | C.LetIn (_, v, t)
| C.Lambda (_, v, t)
| C.Prod (_, v, t)
| C.Cast (t, v) -> sober_term (sober_term g t) v
+ | C.LetIn (_, v, ty, t) -> sober_term
+ (sober_term (sober_term g t) ty) v
| C.Appl []
| C.Appl [_] -> fun b -> false
| C.Appl ts -> sober_terms g ts
C.Prod (name, deannotate_term so, deannotate_term ta)
| C.ALambda (_,name,so,ta) ->
C.Lambda (name, deannotate_term so, deannotate_term ta)
- | C.ALetIn (_,name,so,ta) ->
- C.LetIn (name, deannotate_term so, deannotate_term ta)
+ | C.ALetIn (_,name,so,ty,ta) ->
+ C.LetIn (name, deannotate_term so, deannotate_term ty, deannotate_term ta)
| C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
| C.AConst (_,uri,exp_named_subst) ->
let deann_exp_named_subst =
let context =
List.map
(function
- | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None)))
+ | _,Some (n,(C.ADef (ate,aty))) ->
+ Some(n,(C.Def(deannotate_term ate,deannotate_term aty)))
| _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at)))
| _,None -> None)
acontext
| C.Cast (te,ty) -> C.Cast (unshare te, unshare ty)
| C.Prod (n,s,t) -> C.Prod (n, unshare s, unshare t)
| C.Lambda (n,s,t) -> C.Lambda (n, unshare s, unshare t)
- | C.LetIn (n,s,t) -> C.LetIn (n, unshare s, unshare t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, unshare s, unshare ty, unshare t)
| C.Appl l -> C.Appl (List.map unshare l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
) [< >] lambdas ;
X.xml_nempty "target" [] (aux t)
>]
- | C.ALetIn (xid,C.Anonymous,s,t) ->
+ | C.ALetIn (xid,C.Anonymous,s,ty,t) ->
assert false
- | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+ | C.ALetIn (last_id,C.Name _,_,_,_) as letins ->
let rec eat_letins =
function
- C.ALetIn (id,n,s,t) ->
+ C.ALetIn (id,n,s,ty,t) ->
let letins,t' = eat_letins t in
- (id,n,s)::letins,t'
+ (id,n,s,ty)::letins,t'
| t -> [],t
in
let letins,t = eat_letins letins in
let sort = find_sort "sort" last_id in
X.xml_nempty "LETIN" sort
[< List.fold_left
- (fun i (id,binder,s) ->
+ (fun i (id,binder,s,ty) ->
let sort = find_sort "sort" id in
let attrs =
sort @ ((None,"id",id)::
C.Anonymous -> []
| C.Name b -> [None,"binder",b])
in
- [< i ; X.xml_nempty "def" attrs (aux s) >]
+ [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >]
) [< >] letins ;
X.xml_nempty "target" [] (aux t)
>]
[None,"id",hid;None,"name",n']
| C.Anonymous -> [None,"id",hid])
(print_term ?ids_to_inner_sorts t)
- | Some (n,C.ADef t) ->
+ | Some (n,C.ADef (t,_)) ->
X.xml_nempty "Def"
(match n with
C.Name n' ->
C.ALambda
(fresh_id'',n, aux' context idrefs s,
aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
- | C.LetIn (n,s,t) ->
- let s_ty =
- try
- (cic_CicHash_find terms_to_types s).D.synthesized
- with
- Not_found ->
- cicReduction_whd context (xxx_type_of_aux' metasenv context s);
- in
+ | C.LetIn (n,s,ty,t) ->
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,Some s_ty)))::context) (fresh_id''::idrefs) t)
+ (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty,
+ aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t)
| C.Appl l ->
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = `Prop then
Hashtbl.add ids_to_hypotheses hid binding ;
incr hypotheses_seed ;
match binding with
- Some (n,Cic.Def (t,_)) ->
- let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
- Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
- (Some hid);
- (binding::context),
- ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
+ Some (n,Cic.Def (t,ty)) ->
+ let acic =
+ acic_of_cic_context ~computeinnertypes context idrefs t
+ None in
+ let acic2 =
+ acic_of_cic_context ~computeinnertypes context idrefs ty
+ None
+ in
+ Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
+ (Some hid);
+ Hashtbl.replace ids_to_father_ids
+ (CicUtil.id_of_annterm acic2) (Some hid);
+ (binding::context),
+ ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext),
+ (hid::idrefs)
| Some (n,Cic.Decl t) ->
let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
None -> None
| Some (n, Cic.Decl t)->
Some (n, Cic.Decl (Unshare.unshare t))
- | Some (n, Cic.Def (t,None)) ->
- Some (n, Cic.Def ((Unshare.unshare t),None))
- | Some (n,Cic.Def (bo,Some ty)) ->
- Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
+ | Some (n,Cic.Def (bo,ty)) ->
+ Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty))
in
d::canonical_context'
) canonical_context []
None -> None
| Some (n, C.Decl t)->
Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t))
- | Some (n, C.Def (t,None)) ->
+ | Some (n, C.Def (t,ty)) ->
Some (n,
- C.Def ((eta_fix_and_unshare conjectures canonical_context' t),None))
- | Some (_,C.Def (_,Some _)) -> assert false
+ C.Def
+ (eta_fix_and_unshare conjectures canonical_context' t,
+ eta_fix_and_unshare conjectures canonical_context' ty))
in
d::canonical_context'
) canonical_context []
C.ALambda
(fresh_id,n, aux context s,
aux ((fresh_id, Some (n, C.Decl s))::context) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.ALetIn
- (fresh_id, n, aux context s,
- aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+ (fresh_id, n, aux context s, aux context ty,
+ aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t)
| C.Appl l ->
C.AAppl (fresh_id, List.map (aux context) l)
| C.Const (uri,exp_named_subst) ->
| C.Lambda (name,so,dest) ->
does_not_occur n so &&
does_not_occur (n + 1) dest
- | C.LetIn (name,so,dest) ->
+ | C.LetIn (name,so,ty,dest) ->
does_not_occur n so &&
- does_not_occur (n + 1) dest
+ does_not_occur n ty &&
+ does_not_occur (n + 1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur n x) l true
| C.Var (_,exp_named_subst)
C.Prod (n, beta_reduce s, beta_reduce t)
| C.Lambda (n,s,t) ->
C.Lambda (n, beta_reduce s, beta_reduce t)
- | C.LetIn (n,s,t) ->
- C.LetIn (n, beta_reduce s, beta_reduce t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t)
| C.Appl ((C.Lambda (name,s,t))::he::tl) ->
let he' = S.subst he t in
if tl = [] then
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t
- | Some (_,C.Def (_,Some ty)) -> S.lift n ty
- | Some (_,C.Def (bo,None)) ->
- type_of_aux context (S.lift n bo) expectedty
- | None -> raise RelToHiddenHypothesis
+ | Some (_,C.Def (_,ty)) -> S.lift n ty
+ | None -> raise RelToHiddenHypothesis
with
_ -> raise (NotWellTyped "Not a close term")
)
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
- (aux (i+1) tl)
+ | (Some (n,C.Def (t,ty)))::tl ->
+ (Some (n,
+ C.Def
+ ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t))))::
+ (aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (_,C.Def (_,Some _)))::_ -> assert false
in
aux 1 canonical_context
in
in
(* Checks suppressed *)
C.Prod (n,s,type2)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,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 ty = type_of_aux context s None in
+ let _ = type_of_aux context ty None in
+ let _ = type_of_aux context s (Some ty) in
let t_typ =
(* Checks suppressed *)
- type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
+ type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
in (* CicSubstitution.subst s t_typ *)
if does_not_occur 1 t_typ then
(* since [Rel 1] does not occur in typ, substituting any term *)
(* in place of [Rel 1] is equivalent to delifting once *)
CicSubstitution.subst (C.Implicit None) t_typ
else
- C.LetIn (n,s,t_typ)
+ C.LetIn (n,s,ty,t_typ)
| C.Appl (he::tl) when List.length tl > 0 ->
(*
let expected_hetype =
in
let rec check uris_and_types subst =
match uris_and_types,subst with
- _,[] -> []
+ _,[] -> ()
| (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
ignore (type_of_aux context t (Some ty)) ;
let tytl' =
let t2 =
match t' with
C.Appl l ->
- C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+ C.LetIn (C.Name "w",t',assert false,
+ C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
| _ -> C.Appl (t'::(mk_rels no_sources 0)) in
List.fold_right
(fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
(* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
C.LetIn
(C.Name "H",
- C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+ C.Appl res,
+ assert false,
+ C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
else
let name,source,target =
(match ty with
| C.Lambda (n,s,t) ->
C.Lambda
(n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
+ (n,eta_fix' context s,eta_fix' context ty,
+ eta_fix' ((Some (n,(C.Def (s,ty))))::context) t)
| C.Appl [] -> assert false
| C.Appl (he::tl) ->
let tl' = List.map (eta_fix' context) tl in
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
- let cic_def =
+ let cic_typ =
match typ with
- | None -> cic_def
- | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+ | None -> Cic.Implicit (Some `Type)
+ | Some t -> aux ~localize loc context t
in
let cic_body = aux ~localize loc (cic_name :: context) body in
- Cic.LetIn (cic_name, cic_def, cic_body)
+ Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
| CicNotationPt.LetRec (kind, defs, body) ->
let context' =
List.fold_left
Cic.CoFix (n,coinductiveFuns)
in
let counter = ref ~-1 in
- let build_term funs (var,_,_,_) t =
+ let build_term funs (var,_,ty,_) t =
incr counter;
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+ Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
in
(match cic_body with
`AvoidLetInNoAppl n ->
| `Type ->
"(function " ^ ppname b ^ " -> " ^
pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
- | C.LetIn (b,s,t) ->
+ | C.LetIn (b,s,ty,t) ->
(match analyze_term context s with
`Type
- | `Proof ->
- let ty,_ =
- CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph
- in
- pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context)
+ | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
| `Term ->
- let ty,_ =
- CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph
- in
- "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
- pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")")
+ "(let " ^ ppname b ^ " : " ^ pp ~in_type:true ty context ^
+ " = " ^ pp ~in_type:false s context ^ " in " ^
+ pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
| C.Appl (he::tl) when in_type ->
let hes = pp ~in_type he context in
let stl = String.concat "," (clean_args_for_ty context tl) in
pp ~in_type:true ~metasenv:conjectures
at name_context ^ " ",
context_entry::name_context
- | Some (n,C.Def (at,None)) ->
+ | Some (n,C.Def (at,aty)) ->
(separate i) ^
- ppname n ^ ":= " ^ pp ~in_type:false
+ ppname n ^ ":" ^
+ pp ~in_type:true ~metasenv:conjectures
+ aty name_context ^
+ ":= " ^ pp ~in_type:false
~metasenv:conjectures at name_context ^ " ",
context_entry::name_context
| None ->
- (separate i) ^ "_ :? _ ", context_entry::name_context
- | _ -> assert false)
+ (separate i) ^ "_ :? _ ", context_entry::name_context)
) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
| C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty)
| C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t)
| C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t)
- | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
+ | C.LetIn (n,s,_,t) -> CicSubstitution.subst (letin_nf s) t
| C.Appl l -> C.Appl (List.map letin_nf l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
| C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
- | C.LetIn (b,s,t) ->
- " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
+ | C.LetIn (b,s,ty,t) ->
+ " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
(pp ?metasenv t name_context), (Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
- (match ty with
- None -> "_"
- | Some ty -> pp ?metasenv ty name_context)
+ (pp ?metasenv ty name_context)
(pp ?metasenv bo name_context), (Some n)::name_context
| None ->
Printf.sprintf "%s_ :? _" (separate i), None::name_context
(fun context_entry (i,name_context) ->
(match context_entry with
Some (n,C.Decl at) ->
- (separate i) ^
- ppname n ^ ":" ^
- pp ~metasenv:conjectures at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def (at,None)) ->
- (separate i) ^
- ppname n ^ ":= " ^ pp ~metasenv:conjectures
- at name_context ^ " ",
- (Some n)::name_context
- | None ->
- (separate i) ^ "_ :? _ ", None::name_context
- | _ -> assert false)
+ (separate i) ^
+ ppname n ^ ":" ^
+ pp ~metasenv:conjectures at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,aty)) ->
+ (separate i) ^
+ ppname n ^ ": " ^
+ pp ~metasenv:conjectures aty name_context ^
+ ":= " ^ pp ~metasenv:conjectures
+ at name_context ^ " ",
+ (Some n)::name_context
+ | None ->
+ (separate i) ^ "_ :? _ ", None::name_context)
) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
| Cic.Name name -> remove_prefix name string_name in
let l_string_name = check_rec ctx string_name so in
check_rec (name::ctx) l_string_name dest
- | Cic.LetIn (name,so,dest) ->
+ | Cic.LetIn (name,so,_,dest) ->
let string_name = check_rec ctx string_name so in
check_rec (name::ctx) string_name dest
| Cic.Appl l ->
| C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
| C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t)
| C.Appl l -> C.Appl (List.map (unwind_aux m) l)
| C.Const (uri,exp_named_subst) ->
let params =
| (_, _, _, C.Lambda _, []) as config -> config
| (k, e, ens, C.Lambda (_,_,t), p::s) ->
reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
- | (k, e, ens, C.LetIn (_,m,t), s) ->
+ | (k, e, ens, C.LetIn (_,m,_,t), s) ->
let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
reduce (k+1, m'::e, ens, t, s)
| (_, _, _, C.Appl [], _) -> assert false
t1 t2 ugraph'
else
false,ugraph
- | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+ | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) ->
let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
if b' then
- aux test_equality_only
- ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
+ let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in
+ if b' then
+ aux test_equality_only
+ ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph'
+ else
+ false,ugraph
else
false,ugraph
| (C.Appl l1, C.Appl l2) ->
| C.Lambda (n,s,t) ->
let s' = aux ctx s in
C.Lambda (n, s', aux ((decl n s')::ctx) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,_,t) ->
(* the term is already in weak head normal form *)
assert false
| C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
| C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (liftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k) tl in
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k) tl in
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
does_not_occur ~subst context n nn so &&
does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
dest
- | C.LetIn (name,so,dest) ->
+ | C.LetIn (name,so,ty,dest) ->
does_not_occur ~subst context n nn so &&
- does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context)
- (n + 1) (nn + 1) dest
+ does_not_occur ~subst context n nn ty &&
+ does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
+ (n + 1) (nn + 1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
| C.Var (_,exp_named_subst)
check_is_really_smaller_arg ~subst context n nn kl x safes so &&
check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.LetIn (name,so,ta) ->
+ | C.LetIn (name,so,ty,ta) ->
check_is_really_smaller_arg ~subst context n nn kl x safes so &&
- check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
+ check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
+ check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::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 *)
guarded_by_destructors ~subst context n nn kl x safes so &&
guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.LetIn (name,so,ta) ->
+ | C.LetIn (name,so,ty,ta) ->
guarded_by_destructors ~subst context n nn kl x safes so &&
- guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
+ guarded_by_destructors ~subst context n nn kl x safes ty &&
+ guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::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
if not (List.length tl > k) then false
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
+ | (Some (n,C.Def (t,ty)))::tl ->
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl)
in
aux 1 canonical_context
in
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t,ugraph
- | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
- | Some (_,C.Def (bo,None)) ->
- debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
- type_of_aux ~logger context (S.lift n bo) ugraph
+ | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph
| None -> raise
(TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
with
type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
in
(C.Prod (n,s,type2)),ugraph2
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
(* only to check if s is well-typed *)
- let ty,ugraph1 = type_of_aux ~logger context s ugraph in
+ let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+ let b,ugraph1 =
+ R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+ in
+ if not b then
+ raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ "The type of %s is %s but it is expected to be %s"
+ (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty))))
+ else
(* 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))
Moreover the inferred type is closer to the expected one. *)
let ty1,ugraph2 =
type_of_aux ~logger
- ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
+ ((Some (n,(C.Def (s,ty))))::context) t ugraph1
in
(CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
| C.Appl (he::tl) when List.length tl > 0 ->
| C.Cast (v,t) -> C.Cast (aux v, aux t)
| C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
| C.Lambda (b,s,t) -> C.Lambda (b,aux s, aux t)
- | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
+ | C.LetIn (b,s,ty,t) -> C.LetIn (b,aux s, aux ty, aux t)
| C.Appl li -> C.Appl (List.map aux li)
| C.MutCase (uri,n1,ty,te,patterns) ->
C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
(* warning: on appl we should beta reduce before the recursive call
| Cic.Lambda _ -> assert false
*)
- | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
+ | Cic.LetIn (_,s,_,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
| Cic.Appl [] -> assert false
| Cic.Appl (he::_) -> guess_a_name context he
| Cic.Const (uri,_)
| _ -> n in
let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
Cic.Lambda (n',s',t')
- | Cic.LetIn (n,s,t) ->
+ | Cic.LetIn (n,s,ty,t) ->
let s' = mk_fresh_names ~subst metasenv context s in
+ let ty' = mk_fresh_names ~subst metasenv context ty in
let n' =
match n with
Cic.Anonymous -> Cic.Anonymous
| Cic.Name "matita_dummy" ->
mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
| _ -> n in
- let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
- Cic.LetIn (n',s',t')
+ let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',ty'))::context) t in
+ Cic.LetIn (n',s',ty',t')
| Cic.Appl l ->
Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
| Cic.Const (uri,exp_named_subst) ->
let s',rels1 = aux k s in
let t',rels2 = aux (k+1) t in
C.Lambda (n, s', t'), rels1@rels2
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
let s',rels1 = aux k s in
- let t',rels2 = aux (k+1) t in
- let rels = rels1 @ rels2 in
- if List.mem k rels2 then
- C.LetIn (n, s', t'), rels
+ let ty',rels2 = aux k ty in
+ let t',rels3 = aux (k+1) t in
+ let rels = rels1 @ rels2 @ rels3 in
+ if List.mem k rels3 then
+ C.LetIn (n, s', ty', t'), rels
else
(* (C.Rel 1) is just a dummy term; any term would fit *)
CicSubstitution.subst (C.Rel 1) t', rels
| C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
| C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
| C.Appl (hd :: tl) -> appl_fun um_aux hd tl
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let t' = apply_subst subst t in
Some (n, Cic.Decl t') :: context
| Some (n, Cic.Def (t, ty)) ->
- let ty' =
- match ty with
- | None -> None
- | Some ty -> Some (apply_subst subst ty)
- in
+ let ty' = apply_subst subst ty in
let t' = apply_subst subst t in
Some (n, Cic.Def (t', ty')) :: context
| None -> None :: context)
(Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
- (match ty with
- None -> "_"
- | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context)
+ (ppterm_in_name_context ~metasenv subst ty name_context)
(ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
| None ->
sprintf "%s_ :? _" (separate i), None::name_context
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
- | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
+ | C.LetIn (name,so,ty,dest) ->
+ C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
| C.Appl l -> C.Appl (List.map (aux k) l)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
force_does_not_occur subst to_be_restricted bo
in
let more_to_be_restricted, ty' =
- match ty with
- | None -> more_to_be_restricted, None
- | Some ty ->
- let more_to_be_restricted', ty' =
- force_does_not_occur subst to_be_restricted ty
- in
- more_to_be_restricted @ more_to_be_restricted',
- Some ty'
+ let more_to_be_restricted', ty' =
+ force_does_not_occur subst to_be_restricted ty
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ ty'
in
more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
in
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
| C.Appl l -> C.Appl (List.map (deliftaux k) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
let s',subst,metasenv = liftaux subst metasenv k s in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
C.Lambda (n,s',t'),subst,metasenv
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
let s',subst,metasenv = liftaux subst metasenv k s in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
let t',subst,metasenv = liftaux subst metasenv (k+1) t in
- C.LetIn (n,s',t'),subst,metasenv
+ C.LetIn (n,s',ty',t'),subst,metasenv
| C.Appl l ->
let l',subst,metasenv =
List.fold_right
match List.nth context (n - 1) with
Some (_,C.Decl ty) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,Some ty)) ->
+ | Some (_,C.Def (_,ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (bo,None)) ->
- let ty,ugraph =
- (* if it is in the context it must be already well-typed*)
- CicTypeChecker.type_of_aux' ~subst metasenv context
- (S.lift n bo) ugraph
- in
- t,ty,subst,metasenv,ugraph
| None ->
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
in
C.Lambda (n,s',t'),C.Prod (n,s',type2),
subst'',metasenv'',ugraph2
- | C.LetIn (n,s,t) ->
- (* only to check if s is well-typed *)
- let s',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
+ | C.LetIn (n,s,ty,t) ->
+ (* only to check if s is well-typed *)
+ let s',ty',subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph in
+ let ty,_,subst',metasenv',ugraph1 =
+ type_of_aux subst' metasenv' context ty ugraph1 in
+ let subst',metasenv',ugraph1 =
+ try
+ fo_unif_subst subst' context metasenv'
+ ty ty' ugraph1
+ with
+ exn ->
+ enrich localization_tbl s' exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
+ context))
+ in
+ let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
let t',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),
+ C.LetIn (n,s',ty,t'),
CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,
- C.Def ((S.subst_meta l (S.lift i t)),
- Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ | (Some (n,C.Def (t,ty)))::tl ->
+ (Some
+ (n,
+ C.Def
+ (S.subst_meta l (S.lift i t),
+ S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
| Some (n, Cic.Def (bo,ty)) ->
let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' =
- match ty with
- None -> None
- | Some ty ->
- Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
in
Some (n, Cic.Def (bo',ty'))
) context
| C.Lambda (name,so,dest) ->
let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.LetIn (name,so,dest) ->
- let _,ty,metasenv,ugraph =
- pack_coercions := false;
- type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
- pack_coercions := true;
- let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
- C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.LetIn (name,so,ty,dest) ->
+ let ctx' = Some (name,(C.Def (so,ty)))::ctx in
+ C.LetIn
+ (name, merge_coercions ctx so, merge_coercions ctx ty,
+ merge_coercions ctx' dest)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
find_image_aux (what,with_what)
in
let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
- let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+ let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
let rec substaux k ctx what t =
try
S.lift (k-1) (find_image ctx what t)
| C.Lambda (n,s,t) ->
C.Lambda
(n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+ (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k ctx what) tl in
in
(* TASSI: sure this is in serial? *)
subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
- | C.LetIn (nn,s,t) ->
+ | C.LetIn (nn,s,ty,t) ->
let subst,metasenv,s',ugraph1 =
aux metasenv subst n context s ugraph in
+ let subst,metasenv,ty',ugraph1 =
+ aux metasenv subst n context ty ugraph in
let subst,metasenv,t',ugraph2 =
- aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
ugraph1
in
(* TASSI: sure this is in serial? *)
- subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
+ subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
| C.Appl l ->
let subst,metasenv,revl',ugraph1 =
List.fold_left
in
fo_unif_subst test_equality_only
subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
- | (C.LetIn (_,s1,t1), t2)
- | (t2, C.LetIn (_,s1,t1)) ->
+ | (C.LetIn (_,s1,ty1,t1), t2)
+ | (t2, C.LetIn (_,s1,ty1,t1)) ->
fo_unif_subst
test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
| (C.Appl l1, C.Appl l2) ->
hvbox false true [
keyword "let"; space;
hvbox false true [
- aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
+ aux_var var; space;
+ builtin_symbol "\\def"; break; top_pos (k s) ];
break; space; keyword "in" ];
break;
k t ])
| Ast.Case (term, indty, outty_opt, patterns) ->
Ast.Case (aux env term, indty, aux_opt env outty_opt,
List.map (aux_branch env) patterns)
- | Ast.LetIn (var, t1, t2) ->
- Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
+ | Ast.LetIn (var, t1, t3) ->
+ Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
| Ast.LetRec (kind, definitions, body) ->
Ast.LetRec (kind, List.map (aux_definition env) definitions,
aux env body)
merge n (inspect_conclusion n s) (inspect_conclusion n t)
| Cic.Lambda (_, s, t) ->
merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.LetIn (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
+ | Cic.LetIn (_, s, ty, t) ->
+ merge n (inspect_conclusion n s)
+ (merge n (inspect_conclusion n ty) (inspect_conclusion n t))
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
add_root (n-1) u l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
Some uri, SetSet.empty
| Cic.Cast (t, _) -> inspect_term n t
| Cic.Prod (_, _, t) -> inspect_term n t
- | Cic.LetIn (_, _, t) -> inspect_term n t
+ | Cic.LetIn (_, _, _, t) -> inspect_term n t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
let childunion = inspect_children (n-1) l in
Some u, childunion
UriManagerSet.union (signature_concl s) (signature_concl t)
| Cic.Lambda (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
- | Cic.LetIn (_, s, t) ->
- UriManagerSet.union (signature_concl s) (signature_concl t)
+ | Cic.LetIn (_, s, ty, t) ->
+ UriManagerSet.union (signature_concl s)
+ (UriManagerSet.union (signature_concl ty) (signature_concl t))
| Cic.Appl l -> add l
| Cic.MutCase _
| Cic.Fix _
let rec signature_of = function
| Cic.Cast (t, _) -> signature_of t
| Cic.Prod (_, _, t) -> signature_of t
- | Cic.LetIn (_, _, t) -> signature_of t
+ | Cic.LetIn (_, _, _, t) -> signature_of t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
Some (u, []), add l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
(*assert (not (is_main_pos pos));*)
let set = aux (next_pos pos) set source in
aux (next_pos pos) set target
- | Cic.LetIn (_, term, target) ->
+ | Cic.LetIn (_, term, _, target) ->
if is_main_pos pos then
aux pos set (CicSubstitution.subst term target)
else
| Cic.Lambda (_, source, target) ->
let acc = aux in_hyp acc source in
aux in_hyp acc target
- | Cic.LetIn (_, term, target) ->
+ | Cic.LetIn (_, term, _, target) ->
aux in_hyp acc (CicSubstitution.subst term target)
| Cic.Appl [] -> assert false
| Cic.Appl (hd :: tl) ->
(fun (t,i) -> function
| None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
| Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
- | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1)
+ | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
(t,List.length menv) ctx
;;
match ctxentry with
| Some (_,Cic.Decl t) ->
(Cic.Rel i, CicSubstitution.lift i t)::res,i+1
- | Some (_,Cic.Def (_,Some t)) ->
+ | Some (_,Cic.Def (_,t)) ->
(Cic.Rel i, CicSubstitution.lift i t)::res,i+1
- | Some (_,Cic.Def (_,None)) ->
- let t = Cic.Rel i in
- let ty,_ =
- CicTypeChecker.type_of_aux'
- metasenv context t CicUniv.empty_ugraph
- in
- (t,ty)::res,i+1
- | _ -> res,i+1)
+ | None -> res,i+1)
([],1) context
in l
[] -> []
| Some(name,Cic.Decl(a))::next ->
[Some(name,Cic.Decl(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(a,ty))::next ->
[Some(name,
- Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
+ Cic.Def((CicSubstitution.lift n a),CicSubstitution.lift n ty))
] @ superlift next (n+1)
| _::next -> superlift next (n+1) (*?? ??*)
remove_refl p1
| _ -> Cic.Appl (List.map remove_refl args))
| Cic.Appl l -> Cic.Appl (List.map remove_refl l)
- | Cic.LetIn (name,bo,rest) ->
- Cic.LetIn (name,remove_refl bo,remove_refl rest)
+ | Cic.LetIn (name,bo,ty,rest) ->
+ Cic.LetIn (name,remove_refl bo,remove_refl ty,remove_refl rest)
| _ -> t
in
let rec canonical_trough_lambda context = function
and canonical context t =
match t with
- | Cic.LetIn(name,bo,rest) ->
+ | Cic.LetIn(name,bo,ty,rest) ->
let bo = canonical_trough_lambda context bo in
- let context' = (Some (name,Cic.Def (bo,None)))::context in
- Cic.LetIn(name,bo,canonical context' rest)
+ let ty = canonical_trough_lambda context ty in
+ let context' = (Some (name,Cic.Def (bo,ty)))::context in
+ Cic.LetIn(name,bo,ty,canonical context' rest)
| Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
when LibraryObjects.is_sym_eq_URI uri_sym ->
(match p_of_sym ens tl with
when LibraryObjects.is_sym_eq_URI uri_sym ->
let ty,l,r,p = open_sym ens tl in
mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
- | Cic.LetIn (name,body,rest) ->
- Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest)
+ | Cic.LetIn (name,body,bodyty,rest) ->
+ Cic.LetIn
+ (name,look_ahead (aux uri) body, bodyty,
+ aux uri ty left right ctx_d ctx_ty rest)
| Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
when LibraryObjects.is_eq_ind_URI uri_ind ||
LibraryObjects.is_eq_ind_r_URI uri_ind ->
acc@[id,real_cic],n+1,h)
([],0,[]) lets
in
+ let _,lets =
+ List.fold_left
+ (fun (context,res) (id,cic) ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' [] context cic CicUniv.oblivion_ugraph
+ in
+ Some (Cic.Name ("H" ^ string_of_int id),
+ Cic.Def (cic,ty))::context,res@[id,cic,ty]
+ ) (context,[]) lets
+ in
let proof,se =
let rec aux se current_proof = function
| [] -> current_proof,se
let n,proof =
let initial = proof in
List.fold_right
- (fun (id,cic) (n,p) ->
+ (fun (id,cic,ty) (n,p) ->
n-1,
Cic.LetIn (
Cic.Name ("H"^string_of_int id),
- cic, p))
+ cic,
+ ty,
+ p))
lets (letsno-1,initial)
in
canonical
aux_ens table ens1 ens2
| C.Cast (s1, t1), C.Cast (s2, t2)
| C.Prod (_, s1, t1), C.Prod (_, s2, t2)
- | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
- | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
+ | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) ->
+ let table = aux table s1 s2 in
+ aux table t1 t2
+ | C.LetIn (_, s1, ty1, t1), C.LetIn (_, s2, ty2, t2) ->
let table = aux table s1 s2 in
+ let table = aux table ty1 ty2 in
aux table t1 t2
| C.Appl l1, C.Appl l2 -> (
try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
| _ -> assert false
in
let rec skip_letin ctx = function
- | Cic.LetIn (n,b,t) ->
+ | Cic.LetIn (n,b,_,t) ->
pp_proofterm (Some (rename "Lemma " n)) b ctx::
skip_letin ((Some n)::ctx) t
| t ->
let metasenv,s = aux metasenv n s in
let metasenv,t = aux metasenv (n+1) t in
metasenv,Cic.Prod(name,s,t)
- | Cic.LetIn(name,s,t) ->
+ | Cic.LetIn(name,s,ty,t) ->
let metasenv,s = aux metasenv n s in
+ let metasenv,ty = aux metasenv n ty in
let metasenv,t = aux metasenv (n+1) t in
- metasenv,Cic.LetIn(name,s,t)
+ metasenv,Cic.LetIn(name,s,ty,t)
| Cic.Const(uri,ens) ->
let metasenv,ens =
List.fold_right
| Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
| Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
| Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
- | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+ | Cic.LetIn (n,s,ty,t) -> Cic.LetIn (n, aux k s, aux k ty, aux (k+1) t)
| Cic.Appl [] -> assert false
| Cic.Appl l -> Cic.Appl (List.map (aux k) l)
| Cic.Const (uri,exp_named_subst) ->
TermSet.union (aux s) (aux t)
| C.Prod(n,s,t) ->
TermSet.union (aux s) (aux t)
- | C.LetIn(n,s,t) ->
- TermSet.union (aux s) (aux t)
+ | C.LetIn(n,s,ty,t) ->
+ TermSet.union (aux s) (TermSet.union (aux ty) (aux t))
| t -> TermSet.empty (* TODO: maybe add other cases? *)
in
aux term
| C.Cast (t1, t2)
| C.Lambda (_, t1, t2)
| C.Prod (_, t1, t2)
- | C.LetIn (_, t1, t2) ->
+ | C.LetIn (_, t1, _, t2) ->
let w1 = aux t1 in
let w2 = aux t2 in
w1 + w2 + 1
collect_context ctx (howmany - 1) do_whd t
in
(context',ty,C.Lambda(n',s,bo))
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,sty,t) ->
let (context',ty,bo) =
- collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t
+ collect_context ((Some (n,(C.Def (s,sty))))::context) (howmany - 1) do_whd t
in
- (context',ty,C.LetIn(n,s,bo))
+ (context',ty,C.LetIn(n,s,sty,bo))
| _ as t ->
if howmany <= 0 then
let irl =
| C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
| C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
| C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
- | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
+ | C.LetIn (nn,s,ty,t) -> C.LetIn (nn, aux n s, aux n ty, aux (n+1) t)
| C.Appl l -> C.Appl (List.map (aux n) l)
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
match entry with
Some (n,Cic.Decl s) ->
Some (n,Cic.Decl (subst_in canonical_context' s))
- | Some (n,Cic.Def (s,None)) ->
- Some (n,Cic.Def ((subst_in canonical_context' s),None))
| None -> None
- | Some (n,Cic.Def (bo,Some ty)) ->
+ | Some (n,Cic.Def (bo,ty)) ->
Some
(n,
Cic.Def
(subst_in canonical_context' bo,
- Some (subst_in canonical_context' ty)))
+ subst_in canonical_context' ty))
in
entry'::canonical_context'
) canonical_context []
CicMkImplicit.identity_relocation_list_for_metavariable context
in
let newmeta1ty = CicSubstitution.lift 1 ty in
-(* This is the pre-letin implementation
- let bo' =
- C.Appl
- [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
- C.Meta (newmeta2,irl2)]
- in
-*)
let bo' =
- Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1))
+ Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), term, C.Meta (newmeta1,irl1))
in
let (newproof, _) =
ProofEngineHelpers.subst_meta_in_proof proof metano bo'
let fresh_name =
mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
let context_for_newmeta =
- (Some (fresh_name,C.Def (term,Some tty)))::context in
+ (Some (fresh_name,C.Def (term,tty)))::context in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable
context_for_newmeta
in
let newmetaty = CicSubstitution.lift 1 ty in
- let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
+ let bo' = C.LetIn (fresh_name,term,tty,C.Meta (newmeta,irl)) in
let (newproof, _) =
ProofEngineHelpers.subst_meta_in_proof
proof metano bo'[newmeta,context_for_newmeta,newmetaty]
| C.Lambda (_, s, t) ->
let s, t = gen_term k s, gen_term (succ k) t in
if is_meta [s; t] then meta else C.Lambda (anon, s, t)
- | C.LetIn (_, s, t) ->
- let s, t = gen_term k s, gen_term (succ k) t in
- if is_meta [s; t] then meta else C.LetIn (anon, s, t)
+ | C.LetIn (_, s, ty, t) ->
+ let s,ty,t = gen_term k s, gen_term k ty, gen_term (succ k) t in
+ if is_meta [s; t] then meta else C.LetIn (anon, s, ty, t)
| C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl)
| C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl)
in
[ReductionTactics.simpl_tac
~pattern:(ProofEngineTypes.conclusion_pattern None)])
;;
-
-(* FG: insetrts a "hole" in the context (derived from letin_tac) *)
-
-let letout_tac =
- let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
- let term = C.Sort C.Set in
- let letout_tac (proof, goal) =
- let curi, metasenv, _subst, pbo, pty, attrs = proof in
- let metano, context, ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
- let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
- let context_for_newmeta = None :: context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
- let newmetaty = CicSubstitution.lift 1 ty in
- let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
- let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
- newproof, [newmeta]
- in
- PET.mk_tactic letout_tac
(* FG *)
-(* inserts a hole in the context *)
-val letout_tac:
- ProofEngineTypes.tactic
-
val mk_predicate_for_elim:
context:Cic.context -> metasenv:Cic.metasenv ->
ugraph:CicUniv.universe_graph -> goal:Cic.term ->
List.map
(function
Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None))
| None -> None
- | Some (n,Cic.Def (bo,Some ty)) ->
- Some (n,Cic.Def (subst_in bo,Some (subst_in ty)))
+ | Some (n,Cic.Def (bo,ty)) ->
+ Some (n,Cic.Def (subst_in bo,subst_in ty))
) 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,None)) ->
- Some (i,Cic.Def (subst_in t,None))
- | Some (i,Cic.Def (bo,Some ty)) ->
- Some (i,Cic.Def (subst_in bo,Some (subst_in ty)))
+ | Some (i,Cic.Def (bo,ty)) ->
+ Some (i,Cic.Def (subst_in bo,subst_in ty))
) canonical_context
in
(m,canonical_context',subst_in ty)::i
(CicSubstitution.lift 1 w) t2
in
subst,metasenv,ugraph,rest1 @ rest2
- | Cic.LetIn (name, t1, t2) ->
+ | Cic.LetIn (name, t1, t2, t3) ->
let subst,metasenv,ugraph,rest1 =
find subst metasenv ugraph context w t1 in
let subst,metasenv,ugraph,rest2 =
- find subst metasenv ugraph (Some (name, Cic.Def (t1,None))::context)
- (CicSubstitution.lift 1 w) t2
+ find subst metasenv ugraph context w t2 in
+ let subst,metasenv,ugraph,rest3 =
+ find subst metasenv ugraph (Some (name, Cic.Def (t1,t2))::context)
+ (CicSubstitution.lift 1 w) t3
in
- subst,metasenv,ugraph,rest1 @ rest2
+ subst,metasenv,ugraph,rest1 @ rest2 @ rest3
| Cic.Appl l ->
List.fold_left
(fun (subst,metasenv,ugraph,acc) t ->
aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
| Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
| Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
- | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) ->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (Cic.Name n1, s1, t1),
- Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
+ | Cic.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) ->
+ aux context s1 s2 @
+ aux context ty1 ty2 @
+ aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+ | Cic.LetIn (Cic.Name n1, s1, ty1, t1),
+ Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2->
+ aux context s1 s2 @
+ aux context ty1 ty2 @
+ aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+ | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> []
| Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2
| Cic.Var (_, subst1), Cic.Var (_, subst2)
| Cic.Const (_, subst1), Cic.Const (_, subst2)
true, Cic.Lambda (Cic.Anonymous, s, t)
else
not_found
- | Cic.LetIn (_, s, t) ->
+ | Cic.LetIn (_, s, ty, t) ->
let b1,s = aux s in
- let b2,t = aux t in
- if b1||b2 then
- true, Cic.LetIn (Cic.Anonymous, s, t)
+ let b2,ty = aux ty in
+ let b3,t = aux t in
+ if b1||b2||b3 then
+ true, Cic.LetIn (Cic.Anonymous, s, ty, t)
else
not_found
| Cic.Appl terms ->
| Some (name,Cic.Def (bo, ty)) ->
(match pattern with
| None ->
- let selected_ty=match ty with None -> None | Some _ -> Some [] in
+ let selected_ty = [] in
subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
(entry::context)
| Some pat ->
select_in_term ~metasenv ~context ~ugraph ~term:bo
~pattern:(what, Some pat) in
let subst,metasenv,ugraph,terms_ty =
- match ty with
- None -> subst,metasenv,ugraph,None
- | Some ty ->
- let subst,metasenv,ugraph,res =
- select_in_term ~metasenv ~context ~ugraph ~term:ty
- ~pattern:(what, Some pat)
- in
- subst,metasenv,ugraph,Some res
+ let subst,metasenv,ugraph,res =
+ select_in_term ~metasenv ~context ~ugraph ~term:ty
+ ~pattern:(what, Some pat)
+ in
+ subst,metasenv,ugraph,res
in
subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
(entry::context))
| Cic.Prod (name, s, t)
| Cic.Lambda (name, s, t) ->
aux context s @ aux (add_ctx context name (Cic.Decl s)) t
- | Cic.LetIn (name, s, t) ->
- aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
+ | Cic.LetIn (name, s, ty, t) ->
+ aux context s @
+ aux context ty @
+ aux (add_ctx context name (Cic.Def (s,ty))) t
| Cic.Appl tl -> auxs context tl
| Cic.MutCase (_, _, out, t, pat) ->
aux context out @ aux context t @ auxs context pat
context',res
| Some (_, Cic.Def (bo,ty)) ->
let res = res @ locate_in_term what ~where:bo context in
- let res =
- match ty with
- None -> res
- | Some ty ->
- res @ locate_in_term what ~where:ty context in
+ let res = res @ locate_in_term what ~where:ty context in
let context' = entry::context in
context',res
) context ([],[])
let lookup_type metasenv context hyp =
let rec aux p = function
| Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
- p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+ | Some (Cic.Name name, Cic.Def (_,t)) :: _ when name = hyp -> p, t
| _ :: tail -> aux (succ p) tail
| [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
in
(List.map
(function
| None -> []
- | Some (_,Cic.Decl t)
- | Some (_,Cic.Def (t,None)) ->
+ | Some (_,Cic.Decl t) ->
List.map fst (CicUtil.metas_of_term ty)
- | Some (_,Cic.Def (t,Some ty)) ->
+ | Some (_,Cic.Def (t,ty)) ->
List.map fst (CicUtil.metas_of_term ty) @
List.map fst (CicUtil.metas_of_term t))
ctx)
pattern:ProofEngineTypes.lazy_pattern ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph *
[ `Decl of (Cic.context * Cic.term) list
- | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option
+ | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list
] option list *
(Cic.context * Cic.term) list
| C.Cast (te,ty) -> C.Cast (aux te, aux ty)
| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+ | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t)
| C.Appl l ->
(* Invariant enforced: no application of an application *)
(match List.map aux l with
find_image_aux (what,with_what)
in
let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
- let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+ let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
let rec substaux k ctx what t =
try
S.lift (k-1) (find_image ctx what t)
| C.Lambda (n,s,t) ->
C.Lambda
(n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+ (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k ctx what) tl in
C.Prod (n, substaux k s, substaux (k + 1) t)
| C.Lambda (n,s,t) ->
C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) ->
- C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,ty,t) ->
+ C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k) tl in
C.Prod (n, subst_term k v, subst_term (succ k) t)
| C.Lambda (n, v, t) ->
C.Lambda (n, subst_term k v, subst_term (succ k) t)
- | C.LetIn (n, v, t) ->
- C.LetIn (n, subst_term k v, subst_term (succ k) t)
+ | C.LetIn (n, v, ty, t) ->
+ C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t)
| C.Fix (i, fixes) ->
let fixesno = List.length fixes in
let fixes = List.map (subst_fix fixesno k) fixes in
| he::tl -> reduceaux context tl (S.subst he t)
(* when name is Anonimous the substitution should be superfluous *)
)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
reduceaux context l (S.subst (reduceaux context [] s) t)
| C.Appl (he::tl) ->
let tl' = List.map (reduceaux context []) tl in
(* be superfluous *)
aux (he::rev_constant_args) tl (S.subst he t)
end
- | C.LetIn (_,s,t) ->
+ | C.LetIn (_,s,_,t) ->
aux rev_constant_args l (S.subst s t)
| C.Fix (i,fl) ->
let (_,recindex,_,body) = List.nth fl i in
(* when name is Anonimous the substitution should *)
(* be superfluous *)
aux tl (S.subst he t))
- | C.LetIn (_,s,t) -> aux l (S.subst s t)
+ | C.LetIn (_,s,_,t) -> aux l (S.subst s t)
| Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
let recno =
prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
(fun entry context ->
match entry with
Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
- let cleared_entry =
- let ty =
- match ty with
- Some ty -> ty
- | None ->
- fst
- (CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.empty_ugraph) (* TASSI: FIXME *)
- in
- Some (C.Name hyp, Cic.Decl ty)
- in
+ let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in
cleared_entry::context
| None -> None::context
- | Some (n,C.Decl t)
- | Some (n,C.Def (t,None)) ->
+ | Some (n,C.Decl t) ->
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
))
in
entry::context
- | Some (n,Cic.Def (te,Some ty)) ->
+ | Some (n,Cic.Def (te,ty)) ->
(try
ignore
(CicTypeChecker.type_of_aux' metasenv context te
(true, None::context)
| None -> (b, None::context)
| Some (n,C.Decl t)
- | Some (n,Cic.Def (t,Some _))
- | Some (n,C.Def (t,None)) ->
+ | Some (n,Cic.Def (t,_)) ->
if b then
let _,_ =
try
Some (name,Cic.Decl ty')::context', metasenv, ugraph
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
let bo', metasenv, ugraph =
- change subst bo selected_bo metasenv ugraph
- in
+ change subst bo selected_bo metasenv ugraph in
let ty', metasenv, ugraph =
- match ty,selected_ty with
- None,None -> None, metasenv, ugraph
- | Some ty,Some selected_ty ->
- let ty', metasenv, ugraph =
- change subst ty selected_ty metasenv ugraph
- in
- Some ty', metasenv, ugraph
- | _,_ -> assert false
+ change subst ty selected_ty metasenv ugraph
in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
(Some (name,Cic.Decl ty')::context'), metasenv, ugraph
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
let bo', metasenv, ugraph =
- change subst bo selected_bo metasenv ugraph
- in
+ change subst bo selected_bo metasenv ugraph in
let ty', metasenv, ugraph =
- match ty,selected_ty with
- None,None -> None, metasenv, ugraph
- | Some ty,Some selected_ty ->
- let ty', metasenv, ugraph =
- change subst ty selected_ty metasenv ugraph
- in
- Some ty', metasenv, ugraph
- | _,_ -> assert false
+ change subst ty selected_ty metasenv ugraph
in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
(* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
- Cic.LetIn (Cic.Anonymous,c2,hyp)
+ Cic.LetIn (Cic.Anonymous,c2,assert false,hyp)
in
let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
let oppdir = opposite_direction direction in
let s' = dummies_of_coercions s in
let t' = dummies_of_coercions t in
Cic.Prod (n,s',t')
- | Cic.LetIn(n,s,t) ->
+ | Cic.LetIn(n,s,ty,t) ->
let s' = dummies_of_coercions s in
+ let ty' = dummies_of_coercions ty in
let t' = dummies_of_coercions t in
- Cic.LetIn (n,s',t')
+ Cic.LetIn (n,s',ty',t')
| Cic.MutCase _ -> Cic.Meta (-1,[])
| t -> t
;;
(Some (_, C.Decl t)) when
fst (R.are_convertible context (S.lift n t) ty
CicUniv.empty_ugraph) -> n
- | (Some (_, C.Def (_,Some ty'))) when
+ | (Some (_, C.Def (_,ty'))) when
fst (R.are_convertible context (S.lift n ty') ty
CicUniv.empty_ugraph) -> n
- | (Some (_, C.Def (t,None))) ->
- let ty_t, u = (* TASSI: FIXME *)
- CicTypeChecker.type_of_aux' metasenv context (S.lift n t)
- CicUniv.empty_ugraph in
- let b,_ = R.are_convertible context ty_t ty u in
- if b then n else find (n+1) tl
| _ -> find (n+1) tl
)
| [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
| Cic.Prod (Cic.Name n, s, t) ->
PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
- | Cic.LetIn (Cic.Name n, s, t) ->
+ | Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
- aux (Some (Cic.Name n, Cic.Def (s,None))::c) t)
+ aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
| Cic.Meta _ -> PT.Implicit
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
projects / helm.git / commitdiff