* Intros and Exact are now implemented.
* Inner sorts are now generated and used.
* Perforation of the proof is now implemented.
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
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"
"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
;;
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;;
| (_,_) -> 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
+;;
let htmlheader_and_content = ref htmlheader;;
-let filename4uwobo = "/public/sacerdot/prova.xml";;
-
let current_cic_infos = ref None;;
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 =
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 ->
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!!!" *)
;;
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
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) ;
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
~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
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:"<html><body bgColor=\"white\"></body></html>"
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;;
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
| 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
;;
| 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.")
+;;
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
projects / helm.git / commitdiff