| Definition
;;
+type metas_context = (int * Cic.term) list;;
+
type context = (binder_type * Cic.name * Cic.term) list;;
type sequent = context * Cic.term;;
+
+let proof = ref (None : (metas_context * Cic.term * Cic.term) option);;
+(*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
+(* Note: the sequent is redundant: it can be computed from the type of the *)
+(* metavariable and its context in the proof. We keep it just for efficiency *)
+(* because computing the context of a term may be quite expensive. *)
+let goal = ref (None : (int * sequent) option);;
+
+exception NotImplemented
+
+(*CSC: Funzione che deve sparire!!! *)
+let cic_context_of_context =
+ List.map
+ (function
+ Declaration,_,t -> t
+ | Definition,_,_ -> raise NotImplemented
+ )
+;;
+
+let refine_meta meta term newmetasenv =
+ let (metasenv,bo,ty) =
+ match !proof with
+ None -> assert false
+ | Some (metasenv,bo,ty) -> metasenv,bo,ty
+ in
+ let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
+ let bo' =
+ let rec aux =
+ let module C = Cic in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta meta' when meta=meta' -> term
+ | C.Meta _ as t -> t
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | 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.Appl l -> C.Appl (List.map aux l)
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ C.MutCase (sp,cookingsno,i,aux outt, aux t,
+ List.map aux pl)
+ | C.Fix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+ aux bo
+ in
+ proof := Some (metasenv',bo',ty)
+;;
+
+let new_meta () =
+ let metasenv =
+ match !proof with
+ None -> assert false
+ | Some (metasenv,_,_) -> metasenv
+ in
+ let rec aux =
+ function
+ None,[] -> 1
+ | Some n,[] -> n
+ | None,(n,_)::tl -> aux (Some n,tl)
+ | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+ in
+ 1 + aux (None,metasenv)
+;;
+
+(* metas_in_term term *)
+(* Returns the ordered list of the metas that occur in [term]. *)
+(* Duplicates are removed. The implementation is not very efficient. *)
+let metas_in_term term =
+ let module C = Cic in
+ let rec aux =
+ function
+ C.Rel _
+ | C.Var _ -> []
+ | C.Meta n -> [n]
+ | C.Sort _
+ | C.Implicit -> []
+ | C.Cast (te,ty) -> (aux te) @ (aux ty)
+ | C.Prod (_,s,t) -> (aux s) @ (aux t)
+ | C.Lambda (_,s,t) -> (aux s) @ (aux t)
+ | C.LetIn (_,s,t) -> (aux s) @ (aux t)
+ | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
+ | C.Const _
+ | C.Abst _
+ | C.MutInd _
+ | C.MutConstruct _ -> []
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ (aux outt) @ (aux t) @
+ (List.fold_left (fun i t -> i @ (aux t)) [] pl)
+ | C.Fix (i,fl) ->
+ List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
+ | C.CoFix (i,fl) ->
+ List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
+ in
+ let metas = aux term in
+ let rec elim_duplicates =
+ function
+ [] -> []
+ | he::tl ->
+ he::(elim_duplicates (List.filter (function el -> he <> el) tl))
+ in
+ elim_duplicates metas
+;;
+
+(* perforate context term ty *)
+(* replaces the term [term] in the proof with a new metavariable whose type *)
+(* is [ty]. [context] must be the context of [term] in the whole proof. This *)
+(* could be easily computed; so the only reasons to have it as an argument *)
+(* are efficiency reasons. *)
+let perforate context term ty =
+ let module C = Cic in
+ let newmeta = new_meta () in
+ match !proof with
+ None -> assert false
+ | Some (metasenv,bo,gty) ->
+ (* We push the new meta at the end of the list for pretty-printing *)
+ (* purposes: in this way metas are ordered. *)
+ let metasenv' = metasenv@[newmeta,ty] in
+ let rec aux =
+ function
+ (* Is == strong enough? *)
+ t when t == term -> C.Meta newmeta
+ | C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta _ as t -> t
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | 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.Appl l -> C.Appl (List.map aux l)
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ C.MutCase (sp,cookingsno,i,aux outt, aux t,
+ List.map aux pl)
+ | C.Fix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+ let bo' = aux bo in
+ (* It may be possible that some metavariables occurred only in *)
+ (* the term we are perforating and they now occurs no more. We *)
+ (* get rid of them, collecting the really useful metavariables *)
+ (* in metasenv''. *)
+ let newmetas = metas_in_term bo' in
+ let metasenv'' =
+ List.filter (function (n,_) -> List.mem n newmetas) metasenv'
+ in
+ proof := Some (metasenv'',bo',gty) ;
+ goal := Some (newmeta,(context,ty)) ;
+ newmeta
+;;
+
+(************************************************************)
+(* Some easy tactics. *)
+(************************************************************)
+
+exception Fail of string;;
+
+let intros () =
+ let module C = Cic in
+ let module R = CicReduction in
+ let metasenv =
+ match !proof with
+ None -> assert false
+ | Some (metasenv,_,_) -> metasenv
+ in
+ let (metano,context,ty) =
+ match !goal with
+ None -> assert false
+ | 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
+ ((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
+ refine_meta metano bo' [newmeta,ty'] ;
+ goal := Some (newmeta,(context'',ty'))
+;;
+
+(* The term bo must be closed in the current context *)
+let exact bo =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let metasenv =
+ match !proof with
+ None -> assert false
+ | Some (metasenv,_,_) -> metasenv
+ in
+ let (metano,context,ty) =
+ match !goal with
+ None -> assert false
+ | Some (metano,(context,ty)) ->
+ assert (ty = List.assoc metano metasenv) ;
+ (* Invariant: context is the actual context of the meta in the proof *)
+ metano,context,ty
+ in
+ (*CSC: deve sparire! *)
+ let context = cic_context_of_context context in
+ if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
+ refine_meta metano bo []
+ else
+ raise (Fail "The type of the provided term is not the one expected.")
+;;
projects / helm.git / blobdiff