--- /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/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 02/12/2002 *)
+(* *)
+(* Missing description *)
+(* *)
+(******************************************************************************)
+
+type classification =
+ Backbone of int
+ | Branch of int
+ | InConclusion
+ | InHypothesis
+;;
+
+let soften_classification =
+ function
+ Backbone _ -> InConclusion
+ | Branch _ -> InHypothesis
+ | k -> k
+;;
+
+let (!!) =
+ function
+ Backbone n ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
+ | Branch n ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
+ | InConclusion ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
+ | InHypothesis ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
+;;
+
+let (@@) (l1,l2,l3) (l1',l2',l3') =
+ let merge l1 l2 =
+ List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
+ in
+ merge l1 l1', merge l2 l2', merge l3 l3'
+;;
+
+let get_constraints term =
+ let module U = UriManager in
+ let module C = Cic in
+ let rec process_type_aux kind =
+ function
+ C.Var (uri,expl_named_subst) ->
+ let kind',depth = !!kind in
+ ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
+ (process_type_aux_expl_named_subst kind expl_named_subst)
+ | C.Rel _ ->
+ let kind',depth = !!kind in
+ (match depth with
+ None -> [],[],[]
+ | Some d -> [],[kind',d],[])
+ | C.Sort s ->
+ (match kind with
+ Backbone _
+ | Branch _ ->
+ let s' =
+ match s with
+ Cic.Prop ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#Prod"
+ | Cic.Set ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
+ | Cic.Type ->
+ "http://www.cs.unibo.it/helm/schemas/schema-helm#Type"
+ in
+ let kind',depth = !!kind in
+ (match depth with
+ None -> assert false
+ | Some d -> [],[],[kind',d,s'])
+ | _ -> [],[],[])
+ | C.Meta _
+ | C.Implicit -> assert false
+ | C.Cast (te,_) ->
+ (* type ignored *)
+ process_type_aux kind te
+ | C.Prod (_,sou,ta) ->
+ let (source_kind,target_kind) =
+ match kind with
+ Backbone n -> (Branch 0, Backbone (n+1))
+ | Branch n -> (InHypothesis, Branch (n+1))
+ | k -> (k,k)
+ in
+ process_type_aux source_kind sou @@
+ process_type_aux target_kind ta
+ | C.Lambda (_,sou,ta) ->
+ let kind' = soften_classification kind in
+ process_type_aux kind' sou @@
+ process_type_aux kind' ta
+ | C.LetIn (_,te,ta)->
+ let kind' = soften_classification kind in
+ process_type_aux kind' te @@
+ process_type_aux kind ta
+ | C.Appl (he::tl) ->
+ let kind' = soften_classification kind in
+ process_type_aux kind he @@
+ List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
+ | C.Appl _ -> assert false
+ | C.Const (uri,_) ->
+ let kind',depth = !!kind in
+ [UriManager.string_of_uri uri,kind',depth],[],[]
+ | C.MutInd (uri,typeno,expl_named_subst) ->
+ let kind',depth = !!kind in
+ ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
+ ")", kind', depth],[],[]) @@
+ (process_type_aux_expl_named_subst kind expl_named_subst)
+ | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
+ let kind',depth = !!kind in
+ ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
+ "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
+ (process_type_aux_expl_named_subst kind expl_named_subst)
+ | C.MutCase (_,_,_,term,patterns) ->
+ (* outtype ignored *)
+ let kind' = soften_classification kind in
+ process_type_aux kind' term @@
+ List.fold_left (fun i t -> i @@ process_type_aux kind' t)
+ ([],[],[]) patterns
+ | C.Fix (_,funs) ->
+ let kind' = soften_classification kind in
+ List.fold_left
+ (fun i (_,_,bo,ty) ->
+ i @@
+ process_type_aux kind' bo @@
+ process_type_aux kind' ty
+ ) ([],[],[]) funs
+ | C.CoFix (_,funs) ->
+ let kind' = soften_classification kind in
+ List.fold_left
+ (fun i (_,bo,ty) ->
+ i @@
+ process_type_aux kind' bo @@
+ process_type_aux kind' ty
+ ) ([],[],[]) funs
+ and process_type_aux_expl_named_subst kind =
+ List.fold_left
+ (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
+ ([],[],[])
+in
+ process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term),
+ (None,None,None)
+;;
+
+(*CSC: Debugging only *)
+let get_constraints term =
+ let res = get_constraints term in
+ let ((objs,rels,sorts),can) = res in
+ prerr_endline "Constraints on objs:" ;
+ List.iter
+ (function (s1,s2,n) ->
+ prerr_endline
+ (s1 ^ " " ^ s2 ^ " " ^
+ match n with None -> "NULL" | Some n -> string_of_int n)
+ ) objs ;
+ prerr_endline "Constraints on Rels:" ;
+ List.iter
+ (function (s,n) ->
+ prerr_endline (s ^ " " ^ string_of_int n)) rels ;
+ prerr_endline "Constraints on Sorts:" ;
+ List.iter
+ (function (s1,n,s2) ->
+ prerr_endline (s1 ^ " " ^ string_of_int n ^ " " ^ s2)) sorts ;
+ res
+;;
--- /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/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 30/04/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+val get_constraints:
+ Cic.term ->
+(*
+ MQueryGenerator.must_restrictions * MQueryGenerator.can_restrictions
+*)
+ ((string * string * int option) list * (string * int) list *
+ (string * int * string) list) *
+ ((string * string * int option) list option * (string * int) list option *
+ (string * int * string) list option)
projects / helm.git / commitdiff