| [] -> goal := None
;;
+let elim_intros term =
+ elim term ;
+ intros ()
+;;
+
let reduction_tactic reduction_function term =
let curi,metasenv,pbo,pty =
match !proof with
| Some (metano,(context,ty)) -> metano,context,ty
in
let term' = reduction_function term in
- let ty' = ProofEngineReduction.replace term term' ty in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+ (*CSC: che si guadagni nulla in fatto di efficienza. *)
+ let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
+ let ty' = replace ty in
+ let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+ let metasenv' =
+ List.map
+ (function
+ (n,_) when n = metano -> (metano,ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some (metano,(context',ty'))
;;
-let whd = reduction_tactic CicReduction.whd;;
-let reduce = reduction_tactic ProofEngineReduction.reduce;;
-(*
-let simpl = reduction_tactic ProofEngineReduction.simpl;;
-*)
-
-let simpl term =
+let reduction_tactic_in_scratch reduction_function ty term =
let curi,metasenv,pbo,pty =
match !proof with
None -> assert false
| Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
in
- let (metano,context,ty) =
+ let (metano,context,_) =
match !goal with
None -> assert false
| Some (metano,(context,ty)) -> metano,context,ty
in
- let term' = ProofEngineReduction.simpl term in
- let ty' = ProofEngineReduction.replace term term' ty in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ let term' = reduction_function term in
+ ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
;;
+let whd = reduction_tactic CicReduction.whd;;
+let reduce = reduction_tactic ProofEngineReduction.reduce;;
+let simpl = reduction_tactic ProofEngineReduction.simpl;;
+
+let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;;
+let reduce_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.reduce;;
+let simpl_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.simpl;;
+
(* It is just the opposite of whd. The code should probably be merged. *)
let fold term =
let curi,metasenv,pbo,pty =
| Some (metano,(context,ty)) -> metano,context,ty
in
let term' = CicReduction.whd term in
- let ty' = ProofEngineReduction.replace term' term ty in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+ (*CSC: che si guadagni nulla in fatto di efficienza. *)
+ let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
+ let ty' = replace ty in
+ let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+ let metasenv' =
+ List.map
+ (function
+ (n,_) when n = metano -> (metano,ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some (metano,(context',ty'))
;;
let cut term =