summaryrefslogtreecommitdiff
path: root/plugins/xml/acic2Xml.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/acic2Xml.ml4')
-rw-r--r--plugins/xml/acic2Xml.ml4363
1 files changed, 363 insertions, 0 deletions
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
new file mode 100644
index 00000000..fb40ed86
--- /dev/null
+++ b/plugins/xml/acic2Xml.ml4
@@ -0,0 +1,363 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * The HELM Project / The EU MoWGLI Project *)
+(* * University of Bologna *)
+(************************************************************************)
+(* This file is distributed under the terms of the *)
+(* GNU Lesser General Public License Version 2.1 *)
+(* *)
+(* Copyright (C) 2000-2004, HELM Team. *)
+(* http://helm.cs.unibo.it *)
+(************************************************************************)
+
+(*CSC codice cut & paste da cicPp e xmlcommand *)
+
+exception ImpossiblePossible;;
+exception NotImplemented;;
+let dtdname = "http://mowgli.cs.unibo.it/dtd/cic.dtd";;
+let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";;
+
+let rec find_last_id =
+ function
+ [] -> Util.anomaly "find_last_id: empty list"
+ | [id,_,_] -> id
+ | _::tl -> find_last_id tl
+;;
+
+let export_existential = string_of_int
+
+let print_term ids_to_inner_sorts =
+ let rec aux =
+ let module A = Acic in
+ let module N = Names in
+ let module X = Xml in
+ function
+ A.ARel (id,n,idref,b) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ X.xml_empty "REL"
+ ["value",(string_of_int n) ; "binder",(N.string_of_id b) ;
+ "id",id ; "idref",idref; "sort",sort]
+ | A.AVar (id,uri) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort]
+ | A.AEvar (id,n,l) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ X.xml_nempty "META"
+ ["no",(export_existential n) ; "id",id ; "sort",sort]
+ (List.fold_left
+ (fun i t ->
+ [< i ; X.xml_nempty "substitution" [] (aux t) >]
+ ) [< >] (List.rev l))
+ | A.ASort (id,s) ->
+ let string_of_sort =
+ match Term.family_of_sort s with
+ Term.InProp -> "Prop"
+ | Term.InSet -> "Set"
+ | Term.InType -> "Type"
+ in
+ X.xml_empty "SORT" ["value",string_of_sort ; "id",id]
+ | A.AProds (prods,t) ->
+ let last_id = find_last_id prods in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "PROD" ["type",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort =
+ Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+ in
+ let attrs =
+ ("id",id)::("type",sort)::
+ match binder with
+ Names.Anonymous -> []
+ | Names.Name b -> ["binder",Names.string_of_id b]
+ in
+ [< X.xml_nempty "decl" attrs (aux s) ; i >]
+ ) [< >] prods ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | A.ACast (id,v,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)
+ >]
+ | A.ALambdas (lambdas,t) ->
+ let last_id = find_last_id lambdas in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "LAMBDA" ["sort",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort =
+ Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+ in
+ let attrs =
+ ("id",id)::("type",sort)::
+ match binder with
+ Names.Anonymous -> []
+ | Names.Name b -> ["binder",Names.string_of_id b]
+ in
+ [< X.xml_nempty "decl" attrs (aux s) ; i >]
+ ) [< >] lambdas ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | A.ALetIns (letins,t) ->
+ let last_id = find_last_id letins in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "LETIN" ["sort",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort =
+ Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+ in
+ let attrs =
+ ("id",id)::("sort",sort)::
+ match binder with
+ Names.Anonymous -> assert false
+ | Names.Name b -> ["binder",Names.string_of_id b]
+ in
+ [< X.xml_nempty "def" attrs (aux s) ; i >]
+ ) [< >] letins ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | A.AApp (id,li) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ X.xml_nempty "APPLY" ["id",id ; "sort",sort]
+ [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li)
+ >]
+ | A.AConst (id,subst,uri) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs = ["uri", uri ; "id",id ; "sort",sort] in
+ aux_subst (X.xml_empty "CONST" attrs) subst
+ | A.AInd (id,subst,uri,i) ->
+ let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in
+ aux_subst (X.xml_empty "MUTIND" attrs) subst
+ | A.AConstruct (id,subst,uri,i,j) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ["uri", uri ;
+ "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
+ "id",id ; "sort",sort]
+ in
+ aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst
+ | A.ACase (id,uri,typeno,ty,te,patterns) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ X.xml_nempty "MUTCASE"
+ ["uriType", uri ;
+ "noType", (string_of_int typeno) ;
+ "id", id ; "sort",sort]
+ [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
+ X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
+ List.fold_left
+ (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >])
+ [<>] patterns
+ >]
+ | A.AFix (id, no, 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_left
+ (fun i (id,fi,ai,ti,bi) ->
+ [< i ;
+ X.xml_nempty "FixFunction"
+ ["id",id ; "name", (Names.string_of_id fi) ;
+ "recIndex", (string_of_int ai)]
+ [< X.xml_nempty "type" [] [< aux ti >] ;
+ X.xml_nempty "body" [] [< aux bi >]
+ >]
+ >]
+ ) [<>] funs
+ >]
+ | A.ACoFix (id,no,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_left
+ (fun i (id,fi,ti,bi) ->
+ [< i ;
+ X.xml_nempty "CofixFunction"
+ ["id",id ; "name", Names.string_of_id fi]
+ [< X.xml_nempty "type" [] [< aux ti >] ;
+ X.xml_nempty "body" [] [< aux bi >]
+ >]
+ >]
+ ) [<>] funs
+ >]
+ and aux_subst target (id,subst) =
+ if subst = [] then
+ target
+ else
+ Xml.xml_nempty "instantiate"
+ (match id with None -> [] | Some id -> ["id",id])
+ [< target ;
+ List.fold_left
+ (fun i (uri,arg) ->
+ [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >]
+ ) [<>] subst
+ >]
+ in
+ aux
+;;
+
+let param_attribute_of_params params =
+ List.fold_right
+ (fun (path,l) i ->
+ List.fold_right
+ (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i'
+ ) l "" ^ match i with "" -> "" | i' -> " " ^ i'
+ ) params ""
+;;
+
+let print_object uri ids_to_inner_sorts =
+ let rec aux =
+ let module A = Acic in
+ let module X = Xml in
+ function
+ A.ACurrentProof (id,n,conjectures,bo,ty) ->
+ let xml_for_current_proof_body =
+(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
+(*CSC: I think so. Not implemented yet. *)
+ X.xml_nempty "CurrentProof" ["of",uri ; "id", id]
+ [< List.fold_left
+ (fun i (cid,n,canonical_context,t) ->
+ [< i ;
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",export_existential n]
+ [< List.fold_left
+ (fun i (hid,t) ->
+ [< (match t with
+ n,A.Decl t ->
+ X.xml_nempty "Decl"
+ ["id",hid;"name",Names.string_of_id n]
+ (print_term ids_to_inner_sorts t)
+ | n,A.Def (t,_) ->
+ X.xml_nempty "Def"
+ ["id",hid;"name",Names.string_of_id n]
+ (print_term ids_to_inner_sorts t)
+ ) ;
+ i
+ >]
+ ) [< >] canonical_context ;
+ X.xml_nempty "Goal" []
+ (print_term ids_to_inner_sorts t)
+ >]
+ >])
+ [<>] (List.rev conjectures) ;
+ X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
+ in
+ let xml_for_current_proof_type =
+ X.xml_nempty "ConstantType" ["name",n ; "id", id]
+ (print_term ids_to_inner_sorts ty)
+ in
+ let xmlbo =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
+ xml_for_current_proof_body
+ >] in
+ let xmlty =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
+ xml_for_current_proof_type
+ >]
+ in
+ xmlty, Some xmlbo
+ | A.AConstant (id,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xmlbo =
+ match bo with
+ None -> None
+ | Some bo ->
+ Some
+ [< X.xml_cdata
+ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
+ X.xml_nempty "ConstantBody"
+ ["for",uri ; "params",params' ; "id", id]
+ [< print_term ids_to_inner_sorts bo >]
+ >]
+ in
+ let xmlty =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
+ X.xml_nempty "ConstantType"
+ ["name",n ; "params",params' ; "id", id]
+ [< print_term ids_to_inner_sorts ty >]
+ >]
+ in
+ xmlty, xmlbo
+ | A.AVariable (id,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n") ;
+ X.xml_nempty "Variable" ["name",n ; "params",params' ; "id", id]
+ [< (match bo with
+ None -> [<>]
+ | Some bo ->
+ X.xml_nempty "body" []
+ (print_term ids_to_inner_sorts bo)
+ ) ;
+ X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+ >]
+ >], None
+ | A.AInductiveDefinition (id,tys,params,nparams) ->
+ let params' = param_attribute_of_params params in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+ dtdname ^ "\">\n") ;
+ X.xml_nempty "InductiveDefinition"
+ ["noParams",string_of_int nparams ;
+ "id",id ;
+ "params",params']
+ [< (List.fold_left
+ (fun i (id,typename,finite,arity,cons) ->
+ [< i ;
+ X.xml_nempty "InductiveType"
+ ["id",id ; "name",Names.string_of_id typename ;
+ "inductive",(string_of_bool finite)
+ ]
+ [< X.xml_nempty "arity" []
+ (print_term ids_to_inner_sorts arity) ;
+ (List.fold_left
+ (fun i (name,lc) ->
+ [< i ;
+ X.xml_nempty "Constructor"
+ ["name",Names.string_of_id name]
+ (print_term ids_to_inner_sorts lc)
+ >]) [<>] cons
+ )
+ >]
+ >]
+ ) [< >] tys
+ )
+ >]
+ >], None
+ in
+ aux
+;;
+
+let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+ let module C2A = Cic2acic in
+ let module X = Xml in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^"\">\n");
+ X.xml_nempty "InnerTypes" ["of",curi]
+ (Hashtbl.fold
+ (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
+ [< x ;
+ X.xml_nempty "TYPE" ["of",id]
+ [< X.xml_nempty "synthesized" []
+ (print_term ids_to_inner_sorts synty) ;
+ match expty with
+ None -> [<>]
+ | Some expty' ->
+ X.xml_nempty "expected" []
+ (print_term ids_to_inner_sorts expty')
+ >]
+ >]
+ ) ids_to_inner_types [<>]
+ )
+ >]
+;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 18:23:40 +0000