substaux 1 what where
;;
-(* replaces in a term a term with another one. *)
-(* Lifting are performed as usual. *)
+(* replaces in a term a list of terms with other ones. *)
+(* Lifting are performed as usual. *)
let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let rec substaux k =
- let module C = Cic in
- let module S = CicSubstitution in
- function
- t when (equality t what) -> S.lift (k-1) with_what
- | C.Rel n as t ->
- if n < k then C.Rel n else C.Rel (n + nnn)
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
- in
- C.Var (uri,exp_named_subst')
- | C.Meta (i, l) as t ->
- let l' =
- List.map
- (function
- None -> None
- | Some t -> Some (substaux k t)
- ) l
- in
- C.Meta(i,l')
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | 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.Appl (he::tl) ->
- (* Invariant: no Appl applied to another Appl *)
- let tl' = List.map (substaux k) tl in
- begin
- match substaux k he with
- C.Appl l -> C.Appl (l@tl')
- | _ as he' -> C.Appl (he'::tl')
- end
- | C.Appl _ -> assert false
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
- in
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,i,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
- in
- C.MutInd (uri,i,exp_named_subst')
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let exp_named_subst' =
- List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
- in
- C.MutConstruct (uri,i,j,exp_named_subst')
- | C.MutCase (sp,i,outt,t,pl) ->
- C.MutCase (sp,i,substaux k outt, substaux k t,
- List.map (substaux k) pl)
- | C.Fix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) ->
- (name, i, substaux k ty, substaux (k+len) bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,ty,bo) ->
- (name, substaux k ty, substaux (k+len) bo))
- fl
- in
- C.CoFix (i, substitutedfl)
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let find_image t =
+ let rec find_image_aux =
+ function
+ [],[] -> raise Not_found
+ | what::tl1,with_what::tl2 ->
+ if equality t what then with_what else find_image_aux (tl1,tl2)
+ | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
+ in
+ find_image_aux (what,with_what)
+ in
+ let rec substaux k t =
+ try
+ S.lift (k-1) (find_image t)
+ with Not_found ->
+ match t with
+ C.Rel n as t ->
+ if n < k then C.Rel n else C.Rel (n + nnn)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
+ | C.Meta (i, l) as t ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (substaux k t)
+ ) l
+ in
+ C.Meta(i,l')
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | 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.Appl (he::tl) ->
+ (* Invariant: no Appl applied to another Appl *)
+ let tl' = List.map (substaux k) tl in
+ begin
+ match substaux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,substaux k outt, substaux k t,
+ List.map (substaux k) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) ->
+ (name, i, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) ->
+ (name, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
in
-let res =
substaux 1 where
-in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
;;
(* Takes a well-typed term and fully reduces it. *)
(* ANCORA DA DEBUGGARE *)
+exception AllSelectedTermsMustBeConvertible;;
+
(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
-let generalize_tac ~term ~status:((proof,goal) as status) =
+let generalize_tac ~terms ~status:((proof,goal) as status) =
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-(*
- let found = false in
- let rec new_context context ty =
- if ty == term then let found = true in context
- else match ty with
- C.Rel _
- | C.Var _
- | C.Meta _ (* ???? *)
- | C.Sort s
- | C.Implicit -> context
- | C.Cast (val,typ) ->
- let tmp_context = new_context context val in
- tmp_context @ (new_context tmp_context typ)
- | C.Prod (binder, source, target) ->
- | C.Lambda (binder, source, target) ->
- let tmp_context = new_context context source in
- tmp_context @ (new_context tmp_context binder)
- | C.LetIn (binder, term, target) ->
- | C.Appl applist ->
- let rec aux context =
- match applist with
- [] -> context
- | hd::tl ->
- let tmp_context = (new_context context hd)
- in aux tmp_context tl
- in aux context applist
- | C.Const (uri, exp_named_subst)
- | C.MutInd (uri, typeno, exp_named_subst)
- | C.MutConstruct (uri, typeno, consno, exp_named_subst) ->
- match exp_named_subst with
- [] -> context
- | (uri,t)::_ -> new_context context (type_of_aux' context t)
- | _ -> assert false
- | C.MutCase (uri, typeno, outtype, iterm, patterns)
- | C.Fix (funno, funlist)
- | C.CoFix (funno, funlist) ->
- match funlist with
- [] -> context (* caso possibile? *)
- | (name, index, type, body)::_ ->
- let tmp_context = ~
- in
-*)
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let typ =
+ match terms with
+ [] -> assert false
+ | he::tl ->
+ (* We need to check that all the convertibility of all the terms *)
+ List.iter
+ (function t ->
+ if not (CicReduction.are_convertible context he t) then
+ raise AllSelectedTermsMustBeConvertible
+ ) tl ;
+ (CicTypeChecker.type_of_aux' metasenv context he)
+ in
T.thens
~start:
(P.cut_tac
(C.Prod(
(C.Name "dummy_for_gen"),
- (CicTypeChecker.type_of_aux' metasenv context term),
+ typ,
(ProofEngineReduction.replace_lifting_csc 1
~equality:(==)
- ~what:term
- ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
+ ~what:terms
+ ~with_what:(List.map (function _ -> C.Rel 1) terms)
~where:ty)
)))
~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
projects / helm.git / commitdiff