From d1d5f6ee41209f05c072ba20e3cd50bc774ebff4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Apr 2002 09:37:28 +0000 Subject: [PATCH] * Many improvements. * Intros and Exact are now implemented. * Inner sorts are now generated and used. * Perforation of the proof is now implemented. --- helm/gTopLevel/cic2Xml.ml | 198 +++++++++++++-------- helm/gTopLevel/cic2acic.ml | 262 +++++++++++++++++++++------- helm/gTopLevel/gTopLevel.ml | 197 ++++++++++++++------- helm/gTopLevel/logicalOperations.ml | 20 ++- helm/gTopLevel/proofEngine.ml | 250 ++++++++++++++++++++++++++ helm/gTopLevel/sequentPp.ml | 38 ++-- 6 files changed, 755 insertions(+), 210 deletions(-) diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index 692037311..db5fd23c5 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -31,23 +31,27 @@ exception NotImplemented;; let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -let print_term curi = +let print_term curi ids_to_inner_sorts = let rec aux = let module C = Cic in let module X = Xml in let module U = UriManager in function C.ARel (id,n,b) -> - X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "REL" + ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort] | C.AVar (id,uri) -> let vdepth = U.depth_of_uri uri - and cdepth = U.depth_of_uri curi in + and cdepth = U.depth_of_uri curi + and sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "VAR" ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^ (U.name_of_uri uri) ; - "id",id] + "id",id ; "sort",sort] | C.AMeta (id,n) -> - X.xml_empty "META" ["no",(string_of_int n) ; "id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort] | C.ASort (id,s) -> let string_of_sort = function @@ -58,43 +62,52 @@ let print_term curi = X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] | C.AImplicit _ -> raise NotImplemented | C.AProd (id,C.Anonimous,s,t) -> - X.xml_nempty "PROD" ["id",id] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" [] (aux t) - >] + let ty = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "PROD" ["id",id ; "type",ty] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] | C.AProd (xid,C.Name id,s,t) -> - X.xml_nempty "PROD" ["id",xid] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" ["binder",id] (aux t) - >] + let ty = Hashtbl.find ids_to_inner_sorts xid in + X.xml_nempty "PROD" ["id",xid ; "type",ty] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] | C.ACast (id,v,t) -> - X.xml_nempty "CAST" ["id",id] - [< X.xml_nempty "term" [] (aux v) ; - X.xml_nempty "type" [] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "CAST" ["id",id ; "sort",sort] + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] | C.ALambda (id,C.Anonimous,s,t) -> - X.xml_nempty "LAMBDA" ["id",id] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" [] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "LAMBDA" ["id",id ; "sort",sort] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] | C.ALambda (xid,C.Name id,s,t) -> - X.xml_nempty "LAMBDA" ["id",xid] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" ["binder",id] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts xid in + X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort] + [< X.xml_nempty "source" [] (aux s) ; + 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!!!*) | C.ALetIn (xid,C.Name id,s,t) -> - X.xml_nempty "LETIN" ["id",xid] - [< X.xml_nempty "term" [] (aux s) ; - X.xml_nempty "letintarget" ["binder",id] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts xid in + X.xml_nempty "LETIN" ["id",xid ; "sort",sort] + [< X.xml_nempty "term" [] (aux s) ; + X.xml_nempty "letintarget" ["binder",id] (aux t) + >] | C.AAppl (id,li) -> - X.xml_nempty "APPLY" ["id",id] - [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "APPLY" ["id",id ; "sort",sort] + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) + >] | C.AConst (id,uri,_) -> - X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "CONST" + ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort] | C.AAbst (id,uri) -> raise NotImplemented | C.AMutInd (id,uri,_,i) -> X.xml_empty "MUTIND" @@ -102,46 +115,91 @@ let print_term curi = "noType",(string_of_int i) ; "id",id] | C.AMutConstruct (id,uri,_,i,j) -> - X.xml_empty "MUTCONSTRUCT" - ["uri", (U.string_of_uri uri) ; - "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; - "id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "MUTCONSTRUCT" + ["uri", (U.string_of_uri uri) ; + "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; + "id",id ; "sort",sort] | C.AMutCase (id,uri,_,typeno,ty,te,patterns) -> - X.xml_nempty "MUTCASE" - ["uriType",(U.string_of_uri uri) ; - "noType", (string_of_int typeno) ; - "id", id] - [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; - X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; - List.fold_right - (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) - patterns [<>] - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "MUTCASE" + ["uriType",(U.string_of_uri uri) ; + "noType", (string_of_int typeno) ; + "id", id ; "sort",sort] + [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; + X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; + List.fold_right + (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) + patterns [<>] + >] | C.AFix (id, no, funs) -> - X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id] - [< List.fold_right - (fun (fi,ai,ti,bi) i -> - [< X.xml_nempty "FixFunction" - ["name", fi; "recIndex", (string_of_int ai)] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] ; - i - >] - ) funs [<>] - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "FIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_right + (fun (fi,ai,ti,bi) i -> + [< X.xml_nempty "FixFunction" + ["name", fi; "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] | C.ACoFix (id,no,funs) -> - X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id] - [< List.fold_right - (fun (fi,ti,bi) i -> - [< X.xml_nempty "CofixFunction" ["name", fi] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] ; - i - >] - ) funs [<>] - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "COFIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_right + (fun (fi,ti,bi) i -> + [< X.xml_nempty "CofixFunction" ["name", fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + in + aux +;; + +exception NotImplemented;; + +(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +let print_object curi ids_to_inner_sorts = + let rec aux = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + function + C.ACurrentProof (id,n,conjectures,bo,ty) -> + X.xml_nempty "CurrentProof" ["name",n ; "id", id] + [< List.fold_left + (fun i (n,t) -> + [< i ; + X.xml_nempty "Conjecture" ["no",(string_of_int n)] + (print_term curi ids_to_inner_sorts t) + >]) + [<>] conjectures ; + X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ; + X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >] + | C.ADefinition (id,n,bo,ty,C.Actual params) -> + let params' = + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" + in + X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id] + [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ; + X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >] + | C.ADefinition _ -> assert false + | _ -> raise NotImplemented in aux ;; diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 825544afe..8b6a257be 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -25,14 +25,13 @@ exception NotImplemented;; -let fresh_id ids_to_terms ids_to_father_ids = - let id = ref 0 in - fun father t -> - let res = "i" ^ string_of_int !id in - incr id ; - Hashtbl.add ids_to_father_ids res father ; - Hashtbl.add ids_to_terms res t ; - res +let fresh_id seed ids_to_terms ids_to_father_ids = + fun father t -> + let res = "i" ^ string_of_int !seed in + incr seed ; + Hashtbl.add ids_to_father_ids res father ; + Hashtbl.add ids_to_terms res t ; + res ;; exception NotEnoughElements;; @@ -48,61 +47,204 @@ let rec get_nth l n = | (_,_) -> raise NotEnoughElements ;; -let acic_of_cic_env env t = +let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + metasenv env t += + let module T = CicTypeChecker in let module C = Cic in - let ids_to_terms = Hashtbl.create 503 in - let ids_to_father_ids = Hashtbl.create 503 in - let fresh_id' = fresh_id ids_to_terms ids_to_father_ids in + let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in let rec aux father bs tt = let fresh_id'' = fresh_id' father tt in let aux' = aux (Some fresh_id'') in - match tt with - C.Rel n -> - let id = - match get_nth bs n with - C.Name s -> s - | _ -> raise NameExpected - in - C.ARel (fresh_id'', n, id) - | C.Var uri -> C.AVar (fresh_id'', uri) - | C.Meta n -> C.AMeta (fresh_id'', n) - | C.Sort s -> C.ASort (fresh_id'', s) - | C.Implicit -> C.AImplicit (fresh_id'') - | C.Cast (v,t) -> - C.ACast (fresh_id'', aux' bs v, aux' bs t) - | C.Prod (n,s,t) -> - C.AProd (fresh_id'', n, aux' bs s, aux' (n::bs) t) - | C.Lambda (n,s,t) -> - C.ALambda (fresh_id'',n, aux' bs s, aux' (n::bs) t) - | C.LetIn (n,s,t) -> - C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t) - | C.Appl l -> C.AAppl (fresh_id'', List.map (aux' bs) l) - | C.Const (uri,cn) -> C.AConst (fresh_id'', uri, cn) - | C.Abst _ -> raise NotImplemented - | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno) - | C.MutConstruct (uri,cn,tyno,consno) -> - C.AMutConstruct (fresh_id'', uri, cn, tyno, consno) - | C.MutCase (uri, cn, tyno, outty, term, patterns) -> - 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,_,_,_) -> C.Name name) funs in - C.AFix (fresh_id'', funno, - List.map - (fun (name, indidx, ty, bo) -> - (name, indidx, aux' bs ty, aux' (names@bs) bo) - ) funs - ) - | C.CoFix (funno, funs) -> - let names = List.map (fun (name,_,_) -> C.Name name) funs in - C.ACoFix (fresh_id'', funno, - List.map - (fun (name, ty, bo) -> - (name, aux' bs ty, aux' (names@bs) bo) - ) funs - ) - in - aux None env t, ids_to_terms, ids_to_father_ids + (* 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 *) + (*CSC: and inner sorts: very deep terms have their types/sorts *) + (*CSC: computed again and again. *) + let string_of_sort = + function + C.Sort C.Prop -> "Prop" + | C.Sort C.Set -> "Set" + | C.Sort C.Type -> "Type" + | _ -> assert false + in + let 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 + in + match tt with + C.Rel n -> + let id = + match get_nth bs n with + (C.Name s,_) -> s + | _ -> raise NameExpected + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.ARel (fresh_id'', n, id) + | C.Var uri -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AVar (fresh_id'', uri) + | C.Meta n -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AMeta (fresh_id'', n) + | C.Sort s -> C.ASort (fresh_id'', s) + | C.Implicit -> C.AImplicit (fresh_id'') + | C.Cast (v,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.ACast (fresh_id'', aux' bs v, aux' bs t) + | 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.Lambda (n,s,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + 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! ;-( + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t) +*) assert false + | C.Appl l -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AAppl (fresh_id'', List.map (aux' bs) l) + | C.Const (uri,cn) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AConst (fresh_id'', uri, cn) + | C.Abst _ -> raise NotImplemented + | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno) + | C.MutConstruct (uri,cn,tyno,consno) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + 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 ; + 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 ; + C.AFix (fresh_id'', funno, + List.map + (fun (name, indidx, ty, bo) -> + (name, indidx, aux' bs ty, aux' (names@bs) bo) + ) funs + ) + | 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 ; + C.ACoFix (fresh_id'', funno, + List.map + (fun (name, ty, bo) -> + (name, aux' bs ty, aux' (names@bs) bo) + ) funs + ) + in + aux 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 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 +;; + +exception Found of (Cic.name * Cic.term) list;; + +(* get_context_of_meta meta term *) +(* returns the context of the occurrence of [meta] in [term]. *) +(* Warning: if [meta] occurs not linearly in [term], the context *) +(* of one "random" occurrence is returned. *) +let get_context_of_meta meta term = + let module C = Cic in + let rec aux ctx = + function + C.Rel _ + | C.Var _ -> () + | C.Meta i when meta = i -> raise (Found ctx) + | C.Meta _ + | 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.Appl l -> List.iter (aux ctx) l + | C.Const _ -> () + | C.Abst _ -> assert false + | C.MutInd _ + | C.MutConstruct _ -> () + | C.MutCase (_,_,_,outt,t,pl) -> + aux ctx outt ; aux ctx t; List.iter (aux ctx) pl + | C.Fix (_,ifl) -> + let counter = ref 0 in + let ctx' = + List.rev_map + (function (name,_,ty,bo) -> + let res = ((*P.Definition,*) C.Name name, C.Fix (!counter,ifl)) in + incr counter ; + res + ) ifl + @ ctx + in + List.iter (function (_,_,ty,bo) -> aux ctx ty ; aux ctx' bo) ifl + | C.CoFix (_,ifl) -> + let counter = ref 0 in + let ctx' = + List.rev_map + (function (name,ty,bo) -> + let res = ((*P.Definition,*) C.Name name, C.CoFix (!counter,ifl)) in + incr counter ; + res + ) ifl + @ ctx + in + List.iter (function (_,ty,bo) -> aux ctx ty ; aux ctx' bo) ifl + in + try + aux [] term ; + assert false (* No occurrences found. *) + with + Found context -> context ;; -let acic_of_cic = acic_of_cic_env [];; +exception NotImplemented;; + +let acic_object_of_cic_object obj = + let module C = Cic in + 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 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 + let acic_term_of_cic_term' = acic_term_of_cic_term_env' [] [] in + let aobj = + match obj with + C.Definition (id,bo,ty,params) -> + let abo = acic_term_of_cic_term' bo in + let aty = acic_term_of_cic_term' ty + in + C.ADefinition ("mettereaposto",id,abo,aty,(Cic.Actual params)) + | C.Axiom (id,ty,params) -> raise NotImplemented + | C.Variable (id,bo,ty) -> raise NotImplemented + | C.CurrentProof (id,conjectures,bo,ty) -> + let aconjectures = + List.map + (function (i,term) -> + let context = get_context_of_meta i bo in + let aterm = acic_term_of_cic_term_env' conjectures context term in + (i, aterm)) + conjectures in + let abo = acic_term_of_cic_term_env' conjectures [] bo in + let aty = acic_term_of_cic_term_env' conjectures [] ty in + 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 +;; diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7c01b4d75..eeda38e49 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -51,8 +51,6 @@ let htmlfooter = let htmlheader_and_content = ref htmlheader;; -let filename4uwobo = "/public/sacerdot/prova.xml";; - let current_cic_infos = ref None;; @@ -80,12 +78,15 @@ let c1 = parseStyle "rootcontent.xsl";; let g = parseStyle "genmmlid.xsl";; let c2 = parseStyle "annotatedpres.xsl";; + +let getterURL = Configuration.getter_url;; +let processorURL = Configuration.processor_url;; (* let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";; let getterURL = "http://phd.cs.unibo.it:8081/";; -*) let processorURL = "http://localhost:8080/helm/servelt/uwobo/";; let getterURL = "http://localhost:8081/";; +*) let mml_styles = [d_c ; c1 ; g ; c2 ; l];; let mml_args = @@ -140,59 +141,142 @@ let applyStylesheets input styles args = input styles ;; -let mml_of_cic acic = -prerr_endline "BBB CREAZIONE" ; +let mml_of_cic_object annobj ids_to_inner_sorts = let xml = - Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic + Cic2Xml.print_object + (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts annobj in - Xml.pp ~quiet:true xml (Some filename4uwobo) ; -prerr_endline "BBB PARSING" ; - let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in -prerr_endline "BBB STYLESHEETS" ; + let input = + Xml2Gdome.document_of_xml domImpl xml + in let output = applyStylesheets input mml_styles mml_args in -prerr_endline "BBB RESA" ; -ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ; - output + output ;; (* CALLBACKS *) +let refresh_proof (output : GMathView.math_view) = + let currentproof = + match !ProofEngine.proof with + 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) = + Cic2acic.acic_object_of_cic_object currentproof + in + let mml = mml_of_cic_object acic ids_to_inner_sorts 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 +(* +ignore(domImpl#saveDocumentToFile ~doc:sequent_doc + ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; +ignore(domImpl#saveDocumentToFile ~doc:sequent_mml + ~name:"/public/sacerdot/guruguru2" ~indent:true ()) +*) +;; + let exact rendering_window () = + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in let inputt = (rendering_window#inputt : GEdit.text) in (*CSC: Gran cut&paste da sotto... *) let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen ^ "\n" in let lexbuf = Lexing.from_string input in + let context = + List.map + (function (_,n,_) -> n) + (match !ProofEngine.goal with + None -> assert false + | Some (_,(ctx,_)) -> ctx + ) + in try while true do (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with + match + CicTextualParserContext.main context CicTextualLexer.token lexbuf + with None -> () | Some expr -> try -(*??? Ma servira' da qualche parte! - let ty = CicTypeChecker.type_of_aux' [] expr in -*) - let (acic, ids_to_terms, ids_to_father_ids) = - Cic2acic.acic_of_cic expr - in -(*CSC: chiamare la vera tattica exact qui! *) - () + ProofEngine.exact expr ; + proofw#unload ; + refresh_proof output with e -> - print_endline ("? " ^ CicPp.ppterm expr) ; + print_endline ("? " ^ CicPp.ppterm expr) ; flush stdout ; raise e done with CicTextualParser0.Eof -> inputt#delete_text 0 inputlen -(*CSC: fare qualcosa di utile *) | e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout ;; +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 +;; + +exception OpenConjecturesStillThere;; +exception WrongProof;; + +let save rendering_window () = + match !ProofEngine.proof with + None -> assert false + | Some ([],bo,ty) -> + if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then + 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) = + Cic2acic.acic_object_of_cic_object proof + in + let mml = mml_of_cic_object acic ids_to_inner_sorts in + (rendering_window#output : GMathView.math_view)#load_tree mml ; + current_cic_infos := Some (ids_to_terms,ids_to_father_ids) + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere +;; + let proveit rendering_window () = + let module L = LogicalOperations in let module G = Gdome in match rendering_window#output#get_selection with Some node -> @@ -207,26 +291,16 @@ let proveit rendering_window () = if xpath = "" then assert false (* "ERROR: No xref found!!!" *) else begin - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids) -> - let id = xpath in - let sequent = - LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids - in - SequentPp.TextualPp.print_sequent sequent ; - let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args - in - rendering_window#proofw#load_tree ~dom:sequent_mml ; -ignore(domImpl#saveDocumentToFile ~doc:sequent_doc - ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; -ignore(domImpl#saveDocumentToFile ~doc:sequent_mml - ~name:"/public/sacerdot/guruguru2" ~indent:true ()) - | None -> assert false (* "ERROR: No current term!!!" *) + try + match !current_cic_infos with + Some (ids_to_terms, ids_to_father_ids) -> + let id = xpath in + if L.to_sequent id ids_to_terms ids_to_father_ids then + refresh_proof rendering_window#output ; + refresh_sequent rendering_window#proofw + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout end | None -> assert false (* "ERROR: No selection!!!" *) ;; @@ -236,7 +310,7 @@ let output_html outputhtml msg = outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;; -let execute rendering_window () = +let state rendering_window () = let inputt = (rendering_window#inputt : GEdit.text) in let oldinputt = (rendering_window#oldinputt : GEdit.text) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -253,20 +327,11 @@ let execute rendering_window () = None -> () | Some expr -> try - let ty = CicTypeChecker.type_of_aux' [] expr in - let whd = CicReduction.whd expr in - - let (acic, ids_to_terms, ids_to_father_ids) = - Cic2acic.acic_of_cic expr - in - let mml = mml_of_cic acic in - output#load_tree mml ; -prerr_endline "BBB FINE RESA" ; - current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ; -print_endline ("? " ^ CicPp.ppterm expr) ; -print_endline (">> " ^ CicPp.ppterm whd) ; -print_endline (": " ^ CicPp.ppterm ty) ; -flush stdout ; + let _ = CicTypeChecker.type_of_aux' [] [] expr in + ProofEngine.proof := Some ([1,expr], Cic.Meta 1, expr) ; + ProofEngine.goal := Some (1,([],expr)) ; + refresh_sequent proofw ; + refresh_proof output ; with e -> print_endline ("? " ^ CicPp.ppterm expr) ; @@ -447,6 +512,9 @@ class rendering_window output proofw (label : GMisc.label) = let button_export_to_postscript = GButton.button ~label:"export_to_postscript" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let saveb = + GButton.button ~label:"Save" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let closeb = GButton.button ~label:"Close" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in @@ -457,8 +525,8 @@ class rendering_window output proofw (label : GMisc.label) = ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 ~packing:(vbox#pack ~padding:5) () in - let executeb = - GButton.button ~label:"Execute" + let stateb = + GButton.button ~label:"State" ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 ~packing:(vbox#pack ~padding:5) () in @@ -473,6 +541,9 @@ class rendering_window output proofw (label : GMisc.label) = let exactb = GButton.button ~label:"Exact" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let introsb = + GButton.button ~label:"Intros" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -498,10 +569,12 @@ object(self) button_export_to_postscript (choose_selection output) in ignore(settingsb#connect#clicked settings_window#show) ; ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; + ignore(saveb#connect#clicked (save self)) ; ignore(proveitb#connect#clicked (proveit self)) ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(executeb#connect#clicked (execute self)) ; + ignore(stateb#connect#clicked (state self)) ; ignore(exactb#connect#clicked (exact self)) ; + ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;; diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 664425062..b7c1a9bcf 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -57,6 +57,8 @@ let get_context ids_to_terms ids_to_father_ids = exception NotImplemented;; +(* It returns true iff the proof has been perforated, i.e. if a subterm *) +(* has been changed into a meta. *) 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 @@ -68,6 +70,20 @@ let to_sequent id ids_to_terms ids_to_father_ids = | P.Definition,_,_ -> raise NotImplemented ) context in - let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in - ((context,ty) : ProofEngine.sequent) + let metasenv = + match !P.proof with + None -> assert false + | Some (metasenv,_,_) -> metasenv + in + let ty = + CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term + 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 ;; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index fc0df2d02..f9250d3e3 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -3,6 +3,256 @@ type binder_type = | Definition ;; +type metas_context = (int * Cic.term) list;; + type context = (binder_type * Cic.name * Cic.term) list;; type sequent = context * Cic.term;; + +let proof = ref (None : (metas_context * Cic.term * Cic.term) option);; +(*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *) +(* Note: the sequent is redundant: it can be computed from the type of the *) +(* metavariable and its context in the proof. We keep it just for efficiency *) +(* because computing the context of a term may be quite expensive. *) +let goal = ref (None : (int * sequent) option);; + +exception NotImplemented + +(*CSC: Funzione che deve sparire!!! *) +let cic_context_of_context = + List.map + (function + Declaration,_,t -> t + | Definition,_,_ -> raise NotImplemented + ) +;; + +let refine_meta meta term newmetasenv = + let (metasenv,bo,ty) = + match !proof with + None -> assert false + | 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 + in + proof := Some (metasenv',bo',ty) +;; + +let new_meta () = + let metasenv = + match !proof with + None -> assert false + | Some (metasenv,_,_) -> metasenv + in + let rec aux = + function + None,[] -> 1 + | Some n,[] -> n + | None,(n,_)::tl -> aux (Some n,tl) + | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + in + 1 + aux (None,metasenv) +;; + +(* metas_in_term term *) +(* Returns the ordered list of the metas that occur in [term]. *) +(* Duplicates are removed. The implementation is not very efficient. *) +let metas_in_term term = + let module C = Cic in + let rec aux = + function + C.Rel _ + | C.Var _ -> [] + | C.Meta n -> [n] + | C.Sort _ + | C.Implicit -> [] + | C.Cast (te,ty) -> (aux te) @ (aux ty) + | C.Prod (_,s,t) -> (aux s) @ (aux t) + | C.Lambda (_,s,t) -> (aux s) @ (aux t) + | C.LetIn (_,s,t) -> (aux s) @ (aux t) + | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ -> [] + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + (aux outt) @ (aux t) @ + (List.fold_left (fun i t -> i @ (aux t)) [] pl) + | C.Fix (i,fl) -> + List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl + | C.CoFix (i,fl) -> + List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl + in + let metas = aux term in + let rec elim_duplicates = + function + [] -> [] + | he::tl -> + he::(elim_duplicates (List.filter (function el -> he <> el) tl)) + in + elim_duplicates metas +;; + +(* perforate context term ty *) +(* replaces the term [term] in the proof with a new metavariable whose type *) +(* is [ty]. [context] must be the context of [term] in the whole proof. This *) +(* could be easily computed; so the only reasons to have it as an argument *) +(* are efficiency reasons. *) +let perforate context term ty = + let module C = Cic in + let newmeta = new_meta () in + match !proof with + None -> assert false + | Some (metasenv,bo,gty) -> + (* We push the new meta at the end of the list for pretty-printing *) + (* purposes: in this way metas are ordered. *) + let metasenv' = metasenv@[newmeta,ty] in + let rec aux = + function + (* Is == strong enough? *) + t when t == term -> C.Meta newmeta + | C.Rel _ as t -> t + | C.Var _ as t -> t + | 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 + let bo' = aux bo in + (* It may be possible that some metavariables occurred only in *) + (* the term we are perforating and they now occurs no more. We *) + (* get rid of them, collecting the really useful metavariables *) + (* in metasenv''. *) + let newmetas = metas_in_term bo' in + let metasenv'' = + List.filter (function (n,_) -> List.mem n newmetas) metasenv' + in + proof := Some (metasenv'',bo',gty) ; + goal := Some (newmeta,(context,ty)) ; + newmeta +;; + +(************************************************************) +(* Some easy tactics. *) +(************************************************************) + +exception Fail of string;; + +let intros () = + let module C = Cic in + let module R = CicReduction 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)) -> metano,context,ty + in + let newmeta = new_meta () in + let rec collect_context = + function + C.Cast (te,_) -> collect_context te + | C.Prod (n,s,t) -> + let (ctx,ty,bo) = collect_context t in + ((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)) + | _ as t -> [], t, (C.Meta newmeta) + in + let revcontext',ty',bo' = collect_context ty in + let context'' = (List.rev revcontext') @ context in + refine_meta metano bo' [newmeta,ty'] ; + goal := Some (newmeta,(context'',ty')) +;; + +(* The term bo must be closed in the current context *) +let exact bo = + let module T = CicTypeChecker in + let module R = CicReduction 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 context = cic_context_of_context context in + if R.are_convertible (T.type_of_aux' metasenv context bo) ty then + refine_meta metano bo [] + else + raise (Fail "The type of the provided term is not the one expected.") +;; diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index 8fbb78b2a..7bfa6b36a 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -38,30 +38,36 @@ module TextualPp = module XmlPp = struct - let print_sequent (context,goal) = + let print_sequent metasenv (context,goal) = let module X = Xml in X.xml_nempty "Sequent" [] (let final_s,final_env = (List.fold_right (fun (b,n,t) (s,env) -> - [< s ; - X.xml_nempty - (match b with - ProofEngine.Definition -> "Definition" - | ProofEngine.Declaration -> "Declaration" - ) ["name",(match n with Cic.Name n -> n | _ -> assert false)] - (Cic2Xml.print_term - (UriManager.uri_of_string "cic:/dummy.con") - (let (acic,_,_) = Cic2acic.acic_of_cic_env env t in acic)) ; - >],(n::env) + 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" + ) ["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! *) ) context ([<>],[]) ) in - [< final_s ; - Xml.xml_nempty "Goal" [] - (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") - (let (acic,_,_) = Cic2acic.acic_of_cic_env final_env goal in acic)) - >] + let (acic,_,_,ids_to_inner_sorts) = + Cic2acic.acic_of_cic_env metasenv final_env goal + in + [< final_s ; + Xml.xml_nempty "Goal" [] + (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") + ids_to_inner_sorts acic) + >] ) ;; end -- 2.39.2