contexts.
* Let...In tactic implemented (but not tested!)
X.xml_nempty "target" ["binder",id] (aux t)
>]
| C.ALetIn (xid,C.Anonimous,s,t) ->
- assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+ assert false
| C.ALetIn (xid,C.Name id,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts xid in
X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
| C.Prod (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id''
(string_of_sort innertype) ;
- C.AProd (fresh_id'', n, aux' bs s, aux' ((n,s)::bs) t)
+ C.AProd (fresh_id'', n, aux' bs s, aux' ((n, C.Decl s)::bs) t)
| C.Lambda (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
if not father_is_lambda then
add_inner_type fresh_id''
end ;
- C.ALambda (fresh_id'',n, aux' bs s, aux' ((n,s)::bs) t)
+ C.ALambda (fresh_id'',n, aux' bs s, aux' ((n, C.Decl s)::bs) t)
| C.LetIn (n,s,t) ->
-(*CSC: Nell'environment debbo poter avere anche dichiarazioni! ;-(
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
- C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t)
-*) assert false
+ C.ALetIn (fresh_id'', n, aux' bs s, aux' ((n, C.Def s)::bs) t)
| C.Appl l ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
aux' bs term, List.map (aux' bs) patterns)
| C.Fix (funno, funs) ->
- let names = List.map (fun (name,_,ty,_) -> C.Name name,ty) funs in
+ let names =
+ List.map (fun (name,_,ty,_) -> C.Name name, C.Decl ty) funs
+ in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
) funs
)
| C.CoFix (funno, funs) ->
- let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in
+ let names =
+ List.map (fun (name,ty,_) -> C.Name name, C.Decl ty) funs in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;
-exception Found of (Cic.name * Cic.term) list;;
+exception Found of (Cic.name * Cic.context_entry) list;;
(* get_context_of_meta meta term *)
(* returns the context of the occurrence of [meta] in [term]. *)
| C.Sort _
| C.Implicit -> ()
| C.Cast (te,ty) -> aux ctx te ; aux ctx ty
- | C.Prod (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
- | C.Lambda (n,s,t) -> aux ctx s ; aux (((*P.Declaration,*)n,s)::ctx) t
- | C.LetIn (n,s,t) ->
- aux ctx s ; assert false (* aux ([P.Definition,n,s]::ctx) t *)
+ | C.Prod (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+ | C.Lambda (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
+ | C.LetIn (n,s,t) -> aux ctx s ; aux ((n, C.Def s)::ctx) t
| C.Appl l -> List.iter (aux ctx) l
| C.Const _ -> ()
| C.Abst _ -> assert false
let ctx' =
List.rev_map
(function (name,_,ty,bo) ->
- let res = ((*P.Definition,*) C.Name name, C.Fix (!counter,ifl)) in
+ let res = (C.Name name, C.Def (C.Fix (!counter,ifl))) in
incr counter ;
res
) ifl
let ctx' =
List.rev_map
(function (name,ty,bo) ->
- let res = ((*P.Definition,*) C.Name name, C.CoFix (!counter,ifl)) in
+ let res = (C.Name name, C.Def (C.CoFix (!counter,ifl))) in
incr counter ;
res
) ifl
in
let context =
List.map
- (function (_,n,_) -> n)
+ (function
+ ProofEngine.Definition (n,_)
+ | ProofEngine.Declaration (n,_) -> n)
(match !ProofEngine.goal with
None -> assert false
| Some (_,(ctx,_)) -> ctx
in
let context =
List.map
- (function (_,n,_) -> n)
+ (function
+ ProofEngine.Definition (n,_)
+ | ProofEngine.Declaration (n,_) -> n)
(match !ProofEngine.goal with
None -> assert false
| Some (_,(ctx,_)) -> ctx
let change rendering_window =
call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
;;
+let letin rendering_window =
+ call_tactic_with_input ProofEngine.letin rendering_window
+;;
let whd_in_scratch scratch_window =
None -> []
| Some (_,(ctx,_)) -> ctx
in
- ProofEngine.cic_context_of_context context,
- List.map (function (_,n,_) -> n) context
+ ProofEngine.cic_context_of_named_context context,
+ List.map
+ (function
+ ProofEngine.Declaration (n,_)
+ | ProofEngine.Definition (n,_) -> n
+ ) context
in
(* Do something interesting *)
let lexbuf = Lexing.from_string input in
let changeb =
GButton.button ~label:"Change"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let letinb =
+ GButton.button ~label:"Let ... In"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:"<html><body bgColor=\"white\"></body></html>"
ignore(foldb#connect#clicked (fold self)) ;
ignore(cutb#connect#clicked (cut self)) ;
ignore(changeb#connect#clicked (change self)) ;
+ ignore(letinb#connect#clicked (letin self)) ;
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
| C.Sort _
| C.Implicit
| C.Cast _ -> []
- | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s]
+ | C.Prod (n,s,t) when t == term -> [P.Declaration (n,s)]
| C.Prod _ -> []
- | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s]
+ | C.Lambda (n,s,t) when t == term -> [P.Declaration (n,s)]
| C.Lambda _ -> []
- | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s]
+ | C.LetIn (n,s,t) when t == term -> [P.Definition (n,s)]
| C.LetIn _ -> []
| C.Appl _
| C.Const _ -> []
let counter = ref 0 in
List.rev_map
(function (name,_,ty,bo) ->
- let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in
+ let res = (P.Definition (C.Name name, C.Fix (!counter,ifl))) in
incr counter ;
res
) ifl
let counter = ref 0 in
List.rev_map
(function (name,ty,bo) ->
- let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in
+ let res = (P.Definition (C.Name name, C.CoFix (!counter,ifl))) in
incr counter ;
res
) ifl
let module P = ProofEngine in
let term = Hashtbl.find ids_to_terms id in
let context = get_context ids_to_terms ids_to_father_ids id in
- let type_checker_env_of_context =
- List.map
- (function
- P.Declaration,_,t -> t
- | P.Definition,_,_ -> raise NotImplemented
- ) context
+ let metasenv =
+ match !P.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
in
- let metasenv =
- match !P.proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
+ let ty =
+ CicTypeChecker.type_of_aux' metasenv
+ (P.cic_context_of_named_context context) term
in
- let ty =
- CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term
+ let (meta,perforated) =
+ (* If the selected term is already a meta, we return it. *)
+ (* Otherwise, we are trying to refine a non-meta term... *)
+ match term with
+ Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
+ | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
in
- let (meta,perforated) =
- (* If the selected term is already a meta, we return it. *)
- (* Otherwise, we are trying to refine a non-meta term... *)
- match term with
- Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
- | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
- in
- perforated
+ perforated
;;
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
(*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 context' =
+ List.map
+ (function
+ Definition (n,t) -> Definition (n,replace t)
+ | Declaration (n,t) -> Declaration (n,replace t)
+ ) context
+ in
let metasenv' =
List.map
(function
(*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 context' =
+ List.map
+ (function
+ Declaration (n,t) -> Declaration (n,replace t)
+ | Definition (n,t) -> Definition (n,replace t)
+ ) context
+ in
let metasenv' =
List.map
(function
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
List.fold_right
(fun i env ->
match i with
- (P.Declaration,n,t) ->
+ P.Declaration (n,t) ->
print_endline (print_name n ^ ":" ^ CicPp.pp t env) ;
flush stdout ;
n::env
- | (P.Definition,n,t) ->
+ | P.Definition (n,t) ->
print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ;
flush stdout ;
n::env
in
let final_s,final_env =
(List.fold_right
- (fun (b,n,t) (s,env) ->
- let acic = acic_of_cic_env env t in
- [< s ;
- X.xml_nempty
- (match b with
- ProofEngine.Definition -> "Def"
- | ProofEngine.Declaration -> "Decl"
- ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
- (Cic2Xml.print_term
- (UriManager.uri_of_string "cic:/dummy.con")
- ids_to_inner_sorts acic)
- >],((n,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *)
+ (fun binding (s,env) ->
+ let b,n,t,cicbinding =
+ match binding with
+ ProofEngine.Definition (n,t) -> "Def", n, t,Cic.Def t
+ | ProofEngine.Declaration (n,t) -> "Decl", n, t, Cic.Decl t
+ in
+ let acic = acic_of_cic_env env t in
+ [< s ;
+ X.xml_nempty b
+ ["name",(match n with Cic.Name n -> n | _ -> assert false)]
+ (Cic2Xml.print_term
+ (UriManager.uri_of_string "cic:/dummy.con")
+ ids_to_inner_sorts acic)
+ >],((n,cicbinding)::env)
) context ([<>],[])
)
in
projects / helm.git / commitdiff