type binder_type =
- Declaration
- | Definition
+ Declaration of Cic.name * Cic.term
+ | Definition of Cic.name * Cic.term
;;
type metasenv = (int * Cic.term) list;;
-type context = (binder_type * Cic.name * Cic.term) list;;
+type named_context = binder_type list;;
-type sequent = context * Cic.term;;
+type sequent = named_context * Cic.term;;
let proof =
ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
exception NotImplemented
-(*CSC: Funzione che deve sparire!!! *)
-let cic_context_of_context =
+let cic_context_of_named_context =
List.map
(function
- Declaration,_,t -> t
- | Definition,_,_ -> raise NotImplemented
+ Declaration (_,t) -> Cic.Decl t
+ | Definition (_,t) -> Cic.Def t
)
;;
(*CSC: generatore di nomi? Chiedere il nome? *)
| C.Anonimous -> C.Name "fresh_name"
in
- ((Declaration,n',s)::ctx,ty,C.Lambda(n',s,bo))
+ ((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))
+ ((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
(* 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
+ let context = cic_context_of_named_context context in
if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
begin
refine_meta metano bo [] ;
(* Invariant: context is the actual context of the meta in the proof *)
metano,context,ty
in
- (*CSC: deve sparire! *)
- let ciccontext = cic_context_of_context context in
+ let ciccontext = cic_context_of_named_context context in
let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in
let bo' =
(* Invariant: context is the actual context of the meta in the proof *)
metano,context,ty
in
- (*CSC: deve sparire! *)
- let ciccontext = cic_context_of_context context in
+ let ciccontext = cic_context_of_named_context context in
let termty = T.type_of_aux' metasenv ciccontext term in
let uri,cookingno,typeno,args =
match termty with
| [] -> 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' =
+ (* 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
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
+ Definition (n,t) -> Definition (n,replace t)
+ | Declaration (n,t) -> Declaration (n,replace t)
+ ) context
in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ 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 curi,metasenv,pbo,pty =
+let reduction_tactic_in_scratch reduction_function ty term =
+ let metasenv =
match !proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ None -> []
+ | Some (_,metasenv,_,_) -> metasenv
in
- let (metano,context,ty) =
+ let context =
match !goal with
- None -> assert false
- | Some (metano,(context,ty)) -> metano,context,ty
+ None -> []
+ | Some (_,(context,_)) -> context
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' =
+ (* 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
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
+ Declaration (n,t) -> Declaration (n,replace t)
+ | Definition (n,t) -> Definition (n,replace t)
+ ) context
in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ 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 =
refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
goal :=
Some
- (newmeta1,((Declaration, C.Name "dummy_for_cut", term)::context,
+ (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
newmeta1ty))
;;
+let letin term =
+ let module C = Cic in
+ 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) =
+ match !goal with
+ None -> assert false
+ | Some (metano,(context,ty)) -> metano,context,ty
+ in
+ let ciccontext = cic_context_of_named_context context in
+ let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
+ let newmeta = new_meta () in
+ let newmetaty = CicSubstitution.lift 1 ty in
+ let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
+ refine_meta metano bo' [newmeta,newmetaty];
+ goal :=
+ Some
+ (newmeta,
+ ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
+;;
+
exception NotConvertible;;
(*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
None -> assert false
| Some (metano,(context,ty)) -> metano,context,ty
in
- (*CSC: deve sparire! *)
- let ciccontext = cic_context_of_context context in
+ let ciccontext = cic_context_of_named_context context in
(* are_convertible works only on well-typed terms *)
ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
if CicReduction.are_convertible goal_input input then
projects / helm.git / blobdiff