From 3e0de84a7ef35919fc3c4722c525fcc6cbf68bb5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Apr 2002 16:54:59 +0000 Subject: [PATCH] * The interface of CicTypeChecker now allows the usage of definitions in contexts. * Let...In tactic implemented (but not tested!) --- helm/gTopLevel/cic2Xml.ml | 2 +- helm/gTopLevel/cic2acic.ml | 28 +++++------ helm/gTopLevel/gTopLevel.ml | 23 +++++++-- helm/gTopLevel/logicalOperations.ml | 44 ++++++++--------- helm/gTopLevel/proofEngine.ml | 73 ++++++++++++++++++++--------- helm/gTopLevel/sequentPp.ml | 30 ++++++------ 6 files changed, 121 insertions(+), 79 deletions(-) diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index 115d1ee66..a25d7f670 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -92,7 +92,7 @@ let print_term curi ids_to_inner_sorts = 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] diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 677d633e5..ec9dc680e 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -110,7 +110,7 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts | 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 @@ -126,12 +126,10 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -152,7 +150,9 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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'' ; @@ -163,7 +163,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ) 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'' ; @@ -188,7 +189,7 @@ let acic_of_cic_env metasenv env t = 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]. *) @@ -205,10 +206,9 @@ let get_context_of_meta meta 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 @@ -221,7 +221,7 @@ let get_context_of_meta meta term = 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 @@ -233,7 +233,7 @@ let get_context_of_meta meta term = 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 diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 3774ed0d7..268d2846e 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -282,7 +282,9 @@ let call_tactic_with_input tactic rendering_window () = 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 @@ -379,7 +381,9 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = 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 @@ -479,6 +483,9 @@ let cut rendering_window = 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 = @@ -652,8 +659,12 @@ let check rendering_window 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 @@ -952,6 +963,9 @@ class rendering_window output proofw (label : GMisc.label) = 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:"" @@ -993,6 +1007,7 @@ object(self) 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)) diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 277451bf4..80f7d04cb 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -20,11 +20,11 @@ let get_context ids_to_terms ids_to_father_ids = | 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 _ -> [] @@ -37,7 +37,7 @@ let get_context ids_to_terms ids_to_father_ids = 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 @@ -45,7 +45,7 @@ let get_context ids_to_terms ids_to_father_ids = 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 @@ -63,27 +63,21 @@ let to_sequent id ids_to_terms ids_to_father_ids = 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 ;; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 8f5d0c96e..29a23a191 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -1,13 +1,13 @@ 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) @@ -20,12 +20,11 @@ let goal = ref (None : (int * sequent) 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 ) ;; @@ -192,10 +191,10 @@ let intros () = (*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 @@ -221,8 +220,7 @@ let exact bo = (* 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 [] ; @@ -321,8 +319,7 @@ let apply term = (* 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' = @@ -407,8 +404,7 @@ let elim term = (* 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 @@ -562,7 +558,13 @@ let reduction_tactic reduction_function term = (*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 @@ -618,7 +620,13 @@ let fold term = (*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 @@ -654,10 +662,34 @@ prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ; 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, *) @@ -675,8 +707,7 @@ let change ~goal_input ~input = 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 diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index 7bdfeb5c3..fb040dfd8 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -11,11 +11,11 @@ module TextualPp = 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 @@ -51,18 +51,20 @@ module XmlPp = 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 -- 2.39.2