From: Claudio Sacerdoti Coen Date: Mon, 8 Apr 2002 12:57:42 +0000 (+0000) Subject: * Many improvements X-Git-Tag: V_0_3_0_debian_8~173 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cba2bdcb2944a5d2a4f2e1560262430fd45e61e6;p=helm.git * Many improvements * Proofs are now rendered in natural language. The inner-types file is store in /public/sacerdot/innertypes and directly retrieved from there. We must find a better solution. * Apply tactic now implemented. It is based on the unification stuff of Andrea. --- diff --git a/helm/gTopLevel/.cvsignore b/helm/gTopLevel/.cvsignore new file mode 100644 index 000000000..59d39c9af --- /dev/null +++ b/helm/gTopLevel/.cvsignore @@ -0,0 +1 @@ +*.cm[iox] gTopLevel.opt diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 08a8acd17..c0d7aabd0 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,6 +1,6 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ - helm-xml gdome_xslt + helm-xml gdome_xslt helm-cic_unification PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index db5fd23c5..115d1ee66 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -203,3 +203,16 @@ let print_object curi ids_to_inner_sorts = in aux ;; + +let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = + let module X = Xml in + X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi] + (Hashtbl.fold + (fun id ty x -> + [< x ; + X.xml_nempty "TYPE" ["of",id] + (print_term curi ids_to_inner_sorts ty) + >] + ) ids_to_inner_types [<>] + ) +;; diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 8b6a257be..789a72b91 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -48,14 +48,14 @@ let rec get_nth l n = ;; let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - metasenv env t + ids_to_inner_types metasenv env t = let module T = CicTypeChecker in let module C = Cic in let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in - let rec aux father bs tt = + let rec aux computeinnertypes father bs tt = let fresh_id'' = fresh_id' father tt in - let aux' = aux (Some fresh_id'') in + let aux' = aux true (Some fresh_id'') in (* First of all we compute the inner type and the inner sort *) (* of the term. They may be useful in what follows. *) (*CSC: This is a very inefficient way of computing inner types *) @@ -68,11 +68,22 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts | C.Sort C.Type -> "Type" | _ -> assert false in - let innertype,innersort = + let ainnertype,innertype,innersort = let cicenv = List.map (function (_,ty) -> ty) bs in let innertype = T.type_of_aux' metasenv cicenv tt in let innersort = T.type_of_aux' metasenv cicenv innertype in - innertype, string_of_sort innersort + let ainnertype = + if computeinnertypes then + Some (aux false (Some fresh_id'') bs innertype) + else + None + in + ainnertype, innertype, string_of_sort innersort + in + let add_inner_type id = + match ainnertype with + None -> () + | Some ainnertype -> Hashtbl.add ids_to_inner_types id ainnertype in match tt with C.Rel n -> @@ -93,6 +104,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts | C.Implicit -> C.AImplicit (fresh_id'') | C.Cast (v,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; C.ACast (fresh_id'', aux' bs v, aux' bs t) | C.Prod (n,s,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' @@ -100,6 +113,22 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts C.AProd (fresh_id'', n, aux' bs s, aux' ((n,s)::bs) t) | C.Lambda (n,s,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + begin + let father_is_lambda = + match father with + None -> false + | Some father' -> + match Hashtbl.find ids_to_father_ids father' with + None -> assert false + | Some fatherid -> + match Hashtbl.find ids_to_terms fatherid with + C.Lambda _ -> true + | _ -> false + in + 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.LetIn (n,s,t) -> (*CSC: Nell'environment debbo poter avere anche dichiarazioni! ;-( @@ -108,6 +137,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts *) assert false | C.Appl l -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; C.AAppl (fresh_id'', List.map (aux' bs) l) | C.Const (uri,cn) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; @@ -119,11 +150,15 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts C.AMutConstruct (fresh_id'', uri, cn, tyno, consno) | C.MutCase (uri, cn, tyno, outty, term, patterns) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; 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 Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; C.AFix (fresh_id'', funno, List.map (fun (name, indidx, ty, bo) -> @@ -133,6 +168,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts | C.CoFix (funno, funs) -> let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; C.ACoFix (fresh_id'', funno, List.map (fun (name, ty, bo) -> @@ -140,17 +177,18 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ) funs ) in - aux None env t + aux true None env t ;; let acic_of_cic_env metasenv env t = let ids_to_terms = Hashtbl.create 503 in let ids_to_father_ids = Hashtbl.create 503 in let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in let seed = ref 0 in acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - metasenv env t, - ids_to_terms, ids_to_father_ids, ids_to_inner_sorts + ids_to_inner_types 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;; @@ -220,9 +258,11 @@ let acic_object_of_cic_object obj = let ids_to_terms = Hashtbl.create 503 in let ids_to_father_ids = Hashtbl.create 503 in let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in let seed = ref 0 in let acic_term_of_cic_term_env' = - acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts in + acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + ids_to_inner_types in let acic_term_of_cic_term' = acic_term_of_cic_term_env' [] [] in let aobj = match obj with @@ -246,5 +286,5 @@ let acic_object_of_cic_object obj = C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty) | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented in - aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts + aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types ;; diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index eeda38e49..4f8a29d76 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -100,8 +100,9 @@ let mml_args = "media-type", "'text/html'" ; "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'no'" ; + "naturalLanguage", "'yes'" ; "annotations", "'no'" ; + "explodeall", "'true()'" ; "topurl", "'http://phd.cs.unibo.it/helm'" ; "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] ;; @@ -120,6 +121,7 @@ let sequent_args = "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; "naturalLanguage", "'no'" ; "annotations", "'no'" ; + "explodeall", "'true()'" ; "topurl", "'http://phd.cs.unibo.it/helm'" ; "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] ;; @@ -141,14 +143,21 @@ let applyStylesheets input styles args = input styles ;; -let mml_of_cic_object annobj ids_to_inner_sorts = +let mml_of_cic_object annobj ids_to_inner_sorts ids_to_inner_types = let xml = Cic2Xml.print_object (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts annobj in - let input = - Xml2Gdome.document_of_xml domImpl xml - in + let xmlinnertypes = + Cic2Xml.print_inner_types + (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts + ids_to_inner_types + in + let input = Xml2Gdome.document_of_xml domImpl xml in +(*CSC: We save the innertypes to disk so that we can retrieve them in the *) +(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) +(*CSC: local. *) + Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ; let output = applyStylesheets input mml_styles mml_args in output ;; @@ -162,33 +171,35 @@ let refresh_proof (output : GMathView.math_view) = None -> assert false | Some (metasenv,bo,ty) -> Cic.CurrentProof ("unnamed", metasenv, bo, ty) in - let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) = + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types) + = Cic2acic.acic_object_of_cic_object currentproof in - let mml = mml_of_cic_object acic ids_to_inner_sorts in + let mml = mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types in output#load_tree mml ; current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ;; let refresh_sequent (proofw : GMathView.math_view) = - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (metasenv,_,_) -> metasenv - in - let currentsequent = - match !ProofEngine.goal with - None -> assert false - | Some (_,sequent) -> sequent - in - let sequent_gdome = SequentPp.XmlPp.print_sequent metasenv currentsequent in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args - in - proofw#load_tree ~dom:sequent_mml + match !ProofEngine.goal with + None -> proofw#unload + | Some (_,currentsequent) -> + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (metasenv,_,_) -> metasenv + in + let sequent_gdome = + SequentPp.XmlPp.print_sequent metasenv currentsequent + in + let sequent_doc = + Xml2Gdome.document_of_xml domImpl sequent_gdome + in + let sequent_mml = + applyStylesheets sequent_doc sequent_styles sequent_args + in + proofw#load_tree ~dom:sequent_mml (* ignore(domImpl#saveDocumentToFile ~doc:sequent_doc ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; @@ -197,10 +208,44 @@ ignore(domImpl#saveDocumentToFile ~doc:sequent_mml *) ;; -let exact rendering_window () = +let output_html outputhtml msg = + htmlheader_and_content := !htmlheader_and_content ^ msg ; + outputhtml#source (!htmlheader_and_content ^ htmlfooter) +;; + +(***********************) +(* TACTICS *) +(***********************) + +let call_tactic tactic rendering_window () = + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + begin + try + tactic () ; + refresh_sequent proofw ; + refresh_proof output + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end +;; + +let call_tactic_with_input tactic rendering_window () = let proofw = (rendering_window#proofw : GMathView.math_view) in let output = (rendering_window#output : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let inputt = (rendering_window#inputt : GEdit.text) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in (*CSC: Gran cut&paste da sotto... *) let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen ^ "\n" in @@ -215,43 +260,38 @@ let exact rendering_window () = in try while true do - (* Execute the actions *) match CicTextualParserContext.main context CicTextualLexer.token lexbuf with None -> () | Some expr -> - try - ProofEngine.exact expr ; - proofw#unload ; - refresh_proof output - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; flush stdout ; - raise e + tactic expr ; + refresh_sequent proofw ; + refresh_proof output done with CicTextualParser0.Eof -> inputt#delete_text 0 inputlen | e -> - print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout +prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ; + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

"); + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ;; -let intros rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - begin - try - ProofEngine.intros () ; - with - e -> - print_endline "? Intros " ; - raise e - end ; - refresh_sequent proofw ; - refresh_proof output +let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; +let exact rendering_window = + call_tactic_with_input ProofEngine.exact rendering_window +;; +let apply rendering_window = + call_tactic_with_input ProofEngine.apply rendering_window ;; +(**********************) +(* END OF TACTICS *) +(**********************) + exception OpenConjecturesStillThere;; exception WrongProof;; @@ -263,10 +303,15 @@ let save rendering_window () = begin (*CSC: Wrong: [] is just plainly wrong *) let proof = Cic.Definition ("unnamed",bo,ty,[]) in - let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) = + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types) + = Cic2acic.acic_object_of_cic_object proof in - let mml = mml_of_cic_object acic ids_to_inner_sorts in + let mml = + mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types + in (rendering_window#output : GMathView.math_view)#load_tree mml ; current_cic_infos := Some (ids_to_terms,ids_to_father_ids) end @@ -305,11 +350,6 @@ let proveit rendering_window () = | None -> assert false (* "ERROR: No selection!!!" *) ;; -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) -;; - let state rendering_window () = let inputt = (rendering_window#inputt : GEdit.text) in let oldinputt = (rendering_window#oldinputt : GEdit.text) in @@ -544,6 +584,9 @@ class rendering_window output proofw (label : GMisc.label) = let introsb = GButton.button ~label:"Intros" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let applyb = + GButton.button ~label:"Apply" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -574,6 +617,7 @@ object(self) ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; ignore(stateb#connect#clicked (state self)) ; ignore(exactb#connect#clicked (exact self)) ; + ignore(applyb#connect#clicked (apply 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/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index f9250d3e3..b676832c1 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -34,48 +34,48 @@ let refine_meta meta term newmetasenv = | 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 + 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 - proof := Some (metasenv',bo',ty) + let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in + let bo' = aux bo in + proof := Some (metasenv'',bo',ty) ;; +(* Returns the first meta whose number is above the number of the higher meta. *) let new_meta () = let metasenv = match !proof with @@ -252,7 +252,108 @@ let exact bo = (*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 [] + begin + refine_meta metano bo [] ; + goal := None + end else raise (Fail "The type of the provided term is not the one expected.") ;; + +(* The term bo must be closed in the current context *) +let apply term = + let module T = CicTypeChecker in + let module R = CicReduction in + let module C = Cic 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 ciccontext = cic_context_of_context context in + let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in + let mgul = Array.to_list mgu in + let mgutl = Array.to_list mgut in + let applymetas_to_metas = + let newmeta = new_meta () in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + Array.init (List.length mgul) (function i -> newmeta + i) in + (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) + (* Here we assume that either a META has been instantiated with *) + (* a close term or with itself. *) + let uninstantiatedmetas = + List.fold_right2 + (fun bo ty newmetas -> + match bo with + Cic.Meta i -> + let newmeta = applymetas_to_metas.(i) in + (*CSC: se ty contiene metas, queste hanno il numero errato!!! *) + let ty_with_newmetas = + (* Substitues (META n) with (META (applymetas_to_metas.(n))) *) + let rec aux = + function + C.Rel _ + | C.Var _ as t -> t + | C.Meta n -> C.Meta (applymetas_to_metas.(n)) + | C.Sort _ + | 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 _ -> assert false + | C.MutInd _ + | 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 ty + in + (newmeta,ty_with_newmetas)::newmetas + | _ -> newmetas + ) mgul mgutl [] + in + let mgul' = + List.map + (function + Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i)) + | _ as t -> t + ) mgul in + let bo' = + if List.length mgul' = 0 then + term + else + Cic.Appl (term::mgul') + in + refine_meta metano bo' uninstantiatedmetas ; + match uninstantiatedmetas with + (n,ty)::tl -> goal := Some (n,(context,ty)) + | [] -> goal := None +;; diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index 7bfa6b36a..ba2d5140f 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -44,14 +44,14 @@ module XmlPp = (let final_s,final_env = (List.fold_right (fun (b,n,t) (s,env) -> - let (acic,_,_,ids_to_inner_sorts) = + let (acic,_,_,ids_to_inner_sorts,_) = Cic2acic.acic_of_cic_env metasenv env t in [< s ; X.xml_nempty (match b with - ProofEngine.Definition -> "Definition" - | ProofEngine.Declaration -> "Declaration" + 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") @@ -60,7 +60,7 @@ module XmlPp = ) context ([<>],[]) ) in - let (acic,_,_,ids_to_inner_sorts) = + let (acic,_,_,ids_to_inner_sorts,_) = Cic2acic.acic_of_cic_env metasenv final_env goal in [< final_s ;