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'
raise
(ProofEngineTypes.Fail (lazy
"You can't letin a term containing the current goal"));
- let _,_ =
+ let tty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
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,None)))::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]
| _ -> assert false
in
(* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *)
- let rec mk_pred metasenv context' pred arg' = function
+ let rec mk_pred metasenv context' pred arg' cpattern' = function
| [] -> metasenv, pred, arg'
| arg :: tail ->
(* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
- let argty, _ugraph = TC.type_of_aux' metasenv context' arg ugraph in
- let argty = CicReduction.whd context' argty in
+ let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in
+ let argty = CicReduction.whd context argty in
let fresh_name =
FreshNamesGenerator.mk_fresh_name
~subst:[] metasenv context' C.Anonymous ~typ:argty
let distance = List.length c - List.length context in
S.lift distance arg, m, u
in
- let pattern = Some lazy_term, [], Some cpattern in
+ let pattern = Some lazy_term, [], Some cpattern' in
let subst, metasenv, _ugraph, _conjecture, selected_terms =
ProofEngineHelpers.select
~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern
let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in
let pred = MS.apply_subst subst pred in
let pred = C.Lambda (fresh_name, argty, pred) in
- mk_pred metasenv (hyp :: context') pred arg' tail
+ let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
+ mk_pred metasenv (hyp :: context') pred arg' cpattern' tail
in
- let metasenv, pred, arg = mk_pred metasenv context goal arg actual_args in
- HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
+ let metasenv, pred, arg =
+ mk_pred metasenv context goal arg cpattern (List.rev actual_args)
+ in
+ HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
metasenv, pred, arg, actual_args
let beta_after_elim_tac upto predicate =
| 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
projects / helm.git / blobdiff