-let whole_statement_universe =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"]
-;;
-
-let only_conclusion_universe =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"]
-;;
-
-let refine_constraints (constr_obj, constr_rel, constr_sort) =
- function
- "/searchPattern" ->
- whole_statement_universe,
- (constr_obj, constr_rel, constr_sort),
- (Some constr_obj, Some constr_rel, Some constr_sort)
- | "/matchConclusion" ->
- let constr_obj' =
- List.map
- (function (uri,pos,_) -> (uri,pos,None))
- (List.filter
- (function (uri,pos,depth) as constr -> is_concl_pos pos)
- constr_obj)
- in
- only_conclusion_universe,
- (*CSC: we must select the must constraints here!!! *)
- (constr_obj',[],[]),(Some constr_obj', None, None)
- | _ -> assert false
-in
-