+++ /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 *)
-(* *)
-(******************************************************************************)
-
-module T = MQGTypes
-module U = MQGUtil
-
-type classification =
- Backbone of int
- | Branch of int
- | InConclusion
- | InHypothesis
-;;
-
-let soften_classification =
- function
- Backbone _ -> InConclusion
- | Branch _ -> InHypothesis
- | k -> k
-;;
-
-let (!!) =
- function
- Backbone n -> `MainConclusion (Some n)
- | Branch n -> `MainHypothesis (Some n)
- | _ -> assert false
-;;
-
-let (!!!) =
- function
- Backbone n -> `MainConclusion (Some n)
- | Branch n -> `MainHypothesis (Some n)
- | InConclusion -> `InConclusion
- | InHypothesis -> `InHypothesis
-;;
-
-
-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) ->
- ([!!!kind, UriManager.string_of_uri uri],[],[]) @@
- (process_type_aux_expl_named_subst kind expl_named_subst)
- | C.Rel _ ->
- (match kind with
- | InConclusion
- | InHypothesis -> [],[],[]
- | _ -> [],[!!kind],[])
- | C.Sort s ->
- (match kind with
- Backbone _
- | Branch _ ->
- let s' =
- match s with
- Cic.Prop -> T.Prop
- | Cic.Set -> T.Set
- | Cic.Type -> T.Type
- in
- [],[],[!!kind,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,_) ->
- [!!!kind, UriManager.string_of_uri uri],[],[]
- | C.MutInd (uri,typeno,expl_named_subst) ->
- ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
- string_of_int (typeno + 1) ^ ")"],[],[]) @@
- (process_type_aux_expl_named_subst kind expl_named_subst)
- | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
- ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
- string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[])
- @@ (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
- let obj_constraints,rel_constraints,sort_constraints =
- process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
- in
- (obj_constraints,rel_constraints,sort_constraints)
-;;
-
-(*CSC: Debugging only *)
-let get_constraints term =
- let res = get_constraints term in
- let (objs,rels,sorts) = res in
- let text_of_pos p =
- U.text_of_position p ^ " " ^ U.text_of_depth p "NULL"
- in
- prerr_endline "Constraints on objs:" ;
- List.iter
- (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ;
- prerr_endline "Constraints on Rels:" ;
- List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ;
- prerr_endline "Constraints on Sorts:" ;
- List.iter
- (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s)
- ) sorts ;
- res
-;;
projects / helm.git / blobdiff