+++ /dev/null
-(*CSC codice cut & paste da cicPp e xmlcommand *)
-
-exception ImpossiblePossible;;
-exception NotImplemented;;
-exception BinderNotSpecified;;
-
-let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
-
-(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi =
- let rec aux =
- let module C = Cic in
- let module X = Xml in
- let module U = UriManager in
- function
- C.ARel (id,_,n,Some b) ->
- X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
- | C.ARel _ -> raise BinderNotSpecified
- | C.AVar (id,_,uri) ->
- let vdepth = U.depth_of_uri uri
- and cdepth = U.depth_of_uri curi in
- X.xml_empty "VAR"
- ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
- (U.name_of_uri uri) ;
- "id",id]
- | C.AMeta (id,_,n) ->
- X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
- | C.ASort (id,_,s) ->
- let string_of_sort =
- function
- C.Prop -> "Prop"
- | C.Set -> "Set"
- | C.Type -> "Type"
- in
- 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)
- >]
- | 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)
- >]
- | C.ACast (id,_,v,t) ->
- X.xml_nempty "CAST" ["id",id]
- [< 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)
- >]
- | 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)
- >]
- | C.AAppl (id,_,li) ->
- X.xml_nempty "APPLY" ["id",id]
- [< (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]
- | C.AAbst (id,_,uri) -> raise NotImplemented
- | C.AMutInd (id,_,uri,_,i) ->
- X.xml_empty "MUTIND"
- ["uri", (U.string_of_uri uri) ;
- "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]
- | 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 [<>]
- >]
- | 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 [<>]
- >]
- | 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 [<>]
- >]
- in
- aux
-;;
-
-let encode params =
- List.fold_right
- (fun (n,l) i ->
- match l with
- [] -> i
- | _ ->
- string_of_int n ^ ": " ^
- String.concat " " (List.map UriManager.name_of_uri l) ^
- i
- ) params ""
-;;
-
-let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
- let module C = Cic in
- let module X = Xml in
- [< X.xml_nempty "InductiveType"
- ["name",typename ;
- "inductive",(string_of_bool inductive)
- ]
- [< X.xml_nempty "arity" [] (print_term curi arity) ;
- (List.fold_right
- (fun (name,ty,_) i ->
- [< X.xml_nempty "Constructor" ["name",name]
- (print_term curi ty) ;
- i
- >])
- constructors
- [<>]
- )
- >]
- >]
-;;
-
-let pp obj curi =
- let module C = Cic in
- let module X = Xml in
- match obj with
- C.ADefinition (xid, _, id, te, ty, params) ->
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
- X.xml_nempty "Definition"
- (["name", id ; "id",xid] @
- match params with
- C.Possible _ -> raise ImpossiblePossible
- (*CSC params are kept in inverted order in the internal *)
- (* representation (the order of application) *)
- | C.Actual fv' -> ["params",(encode (List.rev fv'))])
- [< X.xml_nempty "body" [] (print_term curi te) ;
- X.xml_nempty "type" [] (print_term curi ty) >]
- >]
- | C.AAxiom (xid, _, id, ty, params) ->
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
- X.xml_nempty "Axiom"
- (*CSC params are kept in inverted order in the internal *)
- (* representation (the order of application) *)
- ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
- [< X.xml_nempty "type" [] (print_term curi ty) >]
- >]
- | C.AVariable (xid, _, name, ty) ->
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
- X.xml_nempty "Variable" ["name",name ; "id",xid]
- [< X.xml_nempty "type" [] (print_term curi ty) >]
- >]
- | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
- X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
- [< List.fold_right
- (fun (j,t) i ->
- [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
- [< print_term curi t >] ; i >])
- conjs [<>] ;
- X.xml_nempty "body" [] [< print_term curi bo >] ;
- X.xml_nempty "type" [] [< print_term curi ty >]
- >]
- >]
- | C.AInductiveDefinition (xid, _, tys, params, paramsno) ->
- let names =
- List.map
- (fun (typename,_,_,_) -> typename)
- tys
- in
- [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
- dtdname ^ "\">\n\n") ;
- X.xml_nempty "InductiveDefinition"
- (*CSC params are kept in inverted order in the internal *)
- (* representation (the order of application) *)
- ["noParams",string_of_int paramsno ;
- "params",(encode (List.rev params)) ;
- "id",xid]
- [< List.fold_right
- (fun x i -> [< print_mutual_inductive_type curi x ; i >])
- tys [< >]
- >]
- >]
-;;