+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-exception WrongUriToConstant;;
-exception WrongUriToInductiveDefinition;;
-exception CircularDependency of string;;
-
-module OrderedUris =
- struct
- type t = UriManager.uri
- let compare (s1 : t) (s2 : t) =
- (* library function for = *)
- compare s1 s2
- (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*)
- end
-;;
-
-let filename_of_uri uri =
- let uri' = UriManager.string_of_uri uri in
- let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in
- fn ^ ".xml"
-;;
-
-(* quite inefficient coding of a set of strings: the only operations *)
-(* performed are mem O(log n), and union O(n * log n?) *)
-(* Perhaps a better implementation would be an array of bits or a map *)
-(* from uri to booleans *)
-module SetOfUris = Set.Make(OrderedUris);;
-
-let (@@) = SetOfUris.union;;
-
-let rec parameters_of te ty pparams=
- let module S = SetOfUris in
- let module C = Cic in
- let rec aux =
- function
- C.Rel _ -> S.empty
- | C.Var uri -> S.singleton uri
- | C.Meta _ -> S.empty
- | C.Sort _ -> S.empty
- | C.Implicit -> S.empty
- | 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_right (fun x i -> aux x @@ i) l S.empty
- | C.Const (uri,_) ->
- (* the parameters could be not exact but only possible *)
- fix_params uri (Some (filename_of_uri uri)) ;
- (* now the parameters are surely possible *)
- (match CicCache.get_obj uri with
- C.Definition (_, _, _, params) ->
- List.fold_right
- (fun (_,l) i ->
- List.fold_right
- (fun x i -> S.singleton x @@ i) l i
- ) params S.empty
- | C.Axiom (_, _, params) ->
- List.fold_right
- (fun (_,l) i ->
- List.fold_right
- (fun x i -> S.singleton x @@ i) l i
- ) params S.empty
- | C.CurrentProof _ -> S.empty (*CSC wrong *)
- | _ -> raise WrongUriToConstant
- )
- | C.MutInd (uri,_,_) ->
- (match CicCache.get_obj uri with
- C.InductiveDefinition (_, params, _) ->
- List.fold_right
- (fun (_,l) i ->
- List.fold_right
- (fun x i -> S.singleton x @@ i) l i
- ) params S.empty
- | _ -> raise WrongUriToInductiveDefinition
- )
- | C.MutConstruct (uri,_,_,_) ->
- (match CicCache.get_obj uri with
- C.InductiveDefinition (_, params, _) ->
- List.fold_right
- (fun (_,l) i ->
- List.fold_right
- (fun x i -> S.singleton x @@ i) l i
- ) params S.empty
- | _ -> raise WrongUriToInductiveDefinition
- )
- | C.MutCase (uri,_,_,outtype,term,patterns) ->
- (*CSC cosa basta? Ci vuole anche uri? *)
- (match CicCache.get_obj uri with
- C.InductiveDefinition (_, params, _) ->
- List.fold_right
- (fun (_,l) i ->
- List.fold_right
- (fun x i -> S.singleton x @@ i) l i
- ) params S.empty
- | _ -> raise WrongUriToInductiveDefinition
- ) @@ aux outtype @@ aux term @@
- List.fold_right (fun x i -> aux x @@ i) patterns S.empty
- | C.Fix (_,fl) ->
- List.fold_right
- (fun (_,_,ty,bo) i -> aux ty @@ aux bo @@ i)
- fl S.empty
- | C.CoFix (_,fl) ->
- List.fold_right
- (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
- fl S.empty
- in
- let actual_params = aux te @@ aux ty in
- (* sort_actual_params wants in input the ordered list of possible params *)
- let rec sort_actual_params2 =
- function
- [] -> []
- | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
- | _::tl -> sort_actual_params2 tl
- in
- let rec sort_actual_params =
- function
- [] -> []
- | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
- in
- sort_actual_params pparams
-
-and fix_params uri filename =
- let module C = Cic in
- let ann = CicCache.get_annobj uri in
- match ann with
- C.ADefinition (xid, id, te, ty, C.Possible pparams) ->
- let te' = Deannotate.deannotate_term te in
- let ty' = Deannotate.deannotate_term ty in
- let real_params = parameters_of te' ty' pparams in
- let fixed =
- C.ADefinition (xid,id,te,ty,C.Actual real_params)
- in
- Xml.pp (Cic2Xml.pp fixed uri) filename ;
- | _ -> ()
-;;
projects / helm.git / blobdiff