exception Fail of string;;
+(* lambda_abstract newmeta ty *)
+(* returns a triple [bo],[context],[ty'] where *)
+(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
+(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *)
+(* So, lambda_abstract is the core of the implementation of *)
+(* the Intros tactic. *)
+let lambda_abstract newmeta ty =
+ let module C = Cic in
+ let rec collect_context =
+ function
+ C.Cast (te,_) -> collect_context te
+ | C.Prod (n,s,t) ->
+ let (ctx,ty,bo) = collect_context t in
+ let n' =
+ match n with
+ C.Name _ -> n
+(*CSC: generatore di nomi? Chiedere il nome? *)
+ | C.Anonimous -> C.Name "fresh_name"
+ in
+ ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
+ | C.LetIn (n,s,t) ->
+ let (ctx,ty,bo) = collect_context t in
+ ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
+ | _ as t -> [], t, (C.Meta newmeta)
+ in
+ let revcontext,ty',bo = collect_context ty in
+ bo,(List.rev revcontext),ty'
+;;
+
let intros () =
let module C = Cic in
let module R = CicReduction in
| Some (metano,(context,ty)) -> metano,context,ty
in
let newmeta = new_meta () in
- let rec collect_context =
- function
- C.Cast (te,_) -> collect_context te
- | C.Prod (n,s,t) ->
- let (ctx,ty,bo) = collect_context t in
- let n' =
- match n with
- C.Name _ -> n
-(*CSC: generatore di nomi? Chiedere il nome? *)
- | C.Anonimous -> C.Name "fresh_name"
- in
- ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
- | C.LetIn (n,s,t) ->
- let (ctx,ty,bo) = collect_context t in
- ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
- | _ as t -> [], t, (C.Meta newmeta)
- in
- let revcontext',ty',bo' = collect_context ty in
- let context'' = (List.rev revcontext') @ context in
+ let (bo',newcontext,ty') = lambda_abstract newmeta ty in
+ let context'' = newcontext @ context in
refine_meta metano bo' [newmeta,ty'] ;
goal := Some (newmeta,(context'',ty'))
;;
raise (Fail "The type of the provided term is not the one expected.")
;;
+(*CSC: The call to the Intros tactic is embedded inside the code of the *)
+(*CSC: Elim tactic. Do we already need tacticals? *)
(* Auxiliary function for apply: given a type (a backbone), it returns its *)
-(* head, a META environment in which there is a META for each hypothesis and *)
-(* the indexes of the first and last new METAs introduced. *)
+(* head, a META environment in which there is new a META for each hypothesis,*)
+(* a list of arguments for the new applications and the indexes of the first *)
+(* and last new METAs introduced. The nth argument in the list of arguments *)
+(* is the nth new META lambda-abstracted as much as possible. Hence, this *)
+(* functions already provides the behaviour of Intros on the new goals. *)
+let new_metasenv_for_apply_intros ty =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let rec aux newmeta =
+ function
+ C.Cast (he,_) -> aux newmeta he
+ | C.Prod (_,s,t) ->
+ let newargument,newcontext,ty' = lambda_abstract newmeta s in
+ let (res,newmetasenv,arguments,lastmeta) =
+ aux (newmeta + 1) (S.subst newargument t)
+ in
+ res,(newmeta,ty')::newmetasenv,newargument::arguments,lastmeta
+ | t -> t,[],[],newmeta
+ in
+ let newmeta = new_meta () in
+ (* WARNING: here we are using the invariant that above the most *)
+ (* recente new_meta() there are no used metas. *)
+ let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
+ res,newmetasenv,arguments,newmeta,lastmeta
+;;
+
+(* Auxiliary function for apply: given a type (a backbone), it returns its *)
+(* head, a META environment in which there is new a META for each hypothesis,*)
+(* a list of arguments for the new applications and the indexes of the first *)
+(* and last new METAs introduced. The nth argument in the list of arguments *)
+(* is just the nth new META. *)
let new_metasenv_for_apply ty =
let module C = Cic in
let module S = CicSubstitution in
function
C.Cast (he,_) -> aux newmeta he
| C.Prod (_,s,t) ->
- let (res,newmetasenv,lastmeta) =
- aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
- in
- res,(newmeta,s)::newmetasenv,lastmeta
- | t -> t,[],newmeta
+ let newargument = C.Meta newmeta in
+ let (res,newmetasenv,arguments,lastmeta) =
+ aux (newmeta + 1) (S.subst newargument t)
+ in
+ res,(newmeta,s)::newmetasenv,newargument::arguments,lastmeta
+ | t -> t,[],[],newmeta
in
let newmeta = new_meta () in
(* WARNING: here we are using the invariant that above the most *)
(* recente new_meta() there are no used metas. *)
- let (res,newmetasenv,lastmeta) = aux newmeta ty in
- res,newmetasenv,newmeta,lastmeta
+ let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
+ res,newmetasenv,arguments,newmeta,lastmeta
;;
+
(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
let classify_metas newmeta in_subst_domain apply_subst metasenv =
List.fold_right
let ciccontext = cic_context_of_named_context context in
let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
(* newmeta is the lowest index of the new metas introduced *)
- let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in
+ let (consthead,newmetas,arguments,newmeta,_) =
+ new_metasenv_for_apply termty
+ in
let newmetasenv = newmetas@metasenv in
let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
if List.length newmetas = 0 then
term
else
- let arguments =
- List.map apply_subst
- (List.map (function (i,_) -> C.Meta i) newmetas)
- in
- Cic.Appl (term::arguments)
+ let arguments' = List.map apply_subst arguments in
+ Cic.Appl (term::arguments')
in
refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
(new_uninstantiatedmetas@old_uninstantiatedmetas) ;
-prerr_endline "QUI4" ; flush stderr ; (
match new_uninstantiatedmetas with
[] -> goal := None
| (i,ty)::_ -> goal := Some (i,(context,ty))
-) ;
-List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas)
-; prerr_endline "FATTO" ; flush stderr ;
-List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ;
-prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b))
-; prerr_endline "FATTO2" ; flush stderr
;;
let eta_expand metasenv ciccontext t arg =
exception NotTheRightEliminatorShape;;
exception NoHypothesesFound;;
-let elim term =
+let elim_intros term =
let module T = CicTypeChecker in
let module U = UriManager in
let module R = CicReduction in
let ety =
T.type_of_aux' [] [] eliminator_ref
in
- let (econclusion,newmetas,newmeta,lastmeta) =
+ let (econclusion,newmetas,arguments,newmeta,lastmeta) =
new_metasenv_for_apply ety
in
(* Here we assume that we have only one inductive hypothesis to *)
(* to refine the term. *)
let emeta, fargs =
match ueconclusion with
+(*CSC: Code to be used for Apply *)
C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
+ | C.Meta emeta -> emeta,[]
+(*CSC: Code to be used for ApplyIntros
+ C.Appl (he::fargs) ->
+ let rec find_head =
+ function
+ C.Meta emeta -> emeta
+ | C.Lambda (_,_,t) -> find_head t
+ | C.LetIn (_,_,t) -> find_head t
+ | _ ->raise NotTheRightEliminatorShape
+ in
+ find_head he,fargs
+*)
| _ -> raise NotTheRightEliminatorShape
in
let ty' = CicUnification.apply_subst subst1 ty in
let old_uninstantiatedmetas,new_uninstantiatedmetas =
classify_metas newmeta in_subst_domain apply_subst newmetasenv
in
- let arguments =
- List.map apply_subst
- (List.map (function (i,_) -> C.Meta i) newmetas)
- in
- let bo' = Cic.Appl (eliminator_ref::arguments) in
+ let arguments' = List.map apply_subst arguments in
+ let bo' = Cic.Appl (eliminator_ref::arguments') in
prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
refine_meta_with_brand_new_metasenv metano bo'
| (i,ty)::_ -> goal := Some (i,(context,ty))
;;
-let elim_intros term =
- elim term ;
- intros ()
-;;
-
let reduction_tactic reduction_function term =
let curi,metasenv,pbo,pty =
match !proof with
projects / helm.git / commitdiff