gTopLevel.ml
TOPLEVELOBJS = \
- doubleTypeInference.cmo eta_fixing.cmo content2cic.cmo \
+ eta_fixing.cmo content2cic.cmo \
proofEngine.cmo logicalOperations.cmo \
disambiguate.cmo termEditor.cmo texTermEditor.cmo termViewer.cmo \
invokeTactics.cmo hbugs.cmo gTopLevel.cmo
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
- let must = MQueryLevels2.get_constraints expr in
+ let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:false n
) must
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:true n
) only
module P = MQGTopParser
module TL = CicTextualLexer
module TP = CicTextualParser
-module C2 = MQueryLevels2
-module C1 = MQueryLevels
+module C2 = CGSearchPattern
+module C1 = CGMatchConclusion
module GU = MQGUtil
let get_handle () =
issue handle (G.locate name);
C.close handle
+let unreferred target source =
+ let handle = get_handle () in
+ issue handle (G.unreferred target source);
+ C.close handle
+
let mpattern n m l =
let queries = ref [] in
let univ = Some GU.universe_for_search_pattern in
let mbackward n m l =
let queries = ref [] in
- let torigth_restriction (u, b) =
- let p = if b then `MainConclusion None else `InConclusion in (p, u)
- in
let univ = Some GU.universe_for_match_conclusion in
let handle = get_handle () in
let rec backward level = function
backward level tail;
print_string ("? " ^ CicPp.ppterm term ^ nl);
let t = U.start_time () in
- let list_of_must, only = C1.out_restr [] [] term in
+ let list_of_must, only = C1.get_constraints [] [] term in
let max_level = pred (List.length list_of_must) in
let must = List.nth list_of_must (min level max_level) in
- let rigth_must = List.map torigth_restriction must in
- let rigth_only = Some (List.map torigth_restriction only) in
- let q = G.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in
+ let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in
if not (List.mem q ! queries) then
begin
issue handle q;
prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all";
prerr_endline " CIC terms in the input file";
prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0";
- prerr_endline " on all CIC terms in the input file\n";
+ prerr_endline " on all CIC terms in the input file";
+ prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns\n";
prerr_endline "NOTES: * current interpreter options are:";
prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)";
prerr_endline " * CIC terms are read with the HELM CIC Textual Parser";
| ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
| ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
| ("-C"|"-compose") :: rem -> compose (); parse rem
- | ("-M"|"-backward") :: arg :: rem ->
+ | ("-B"|"-backward") :: arg :: rem ->
let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
| ("-MB"|"-multi-backward") :: arg :: rem ->
let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
| ("-P"|"-pattern") :: arg :: rem ->
let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
| ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
+ | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem ->
+ unreferred arg1 arg2; parse rem
| _ :: rem -> parse rem
let _ =
mQGUtil.cmi: mQGTypes.cmo
mQueryGenerator.cmi: mQGTypes.cmo
-mQueryLevels2.cmi: mQGTypes.cmo
+cGMatchConclusion.cmi: mQGTypes.cmo
+cGSearchPattern.cmi: mQGTypes.cmo
mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi
mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi
mQueryGenerator.cmo: mQGTypes.cmo mQGUtil.cmi mQueryGenerator.cmi
mQueryGenerator.cmx: mQGTypes.cmx mQGUtil.cmx mQueryGenerator.cmi
-mQueryLevels.cmo: mQueryLevels.cmi
-mQueryLevels.cmx: mQueryLevels.cmi
-mQueryLevels2.cmo: mQGTypes.cmo mQGUtil.cmi mQueryLevels2.cmi
-mQueryLevels2.cmx: mQGTypes.cmx mQGUtil.cmx mQueryLevels2.cmi
+cGMatchConclusion.cmo: cGMatchConclusion.cmi
+cGMatchConclusion.cmx: cGMatchConclusion.cmi
+cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi
+cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi
PREDICATES =
INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \
- mQueryLevels.mli mQueryLevels2.mli
+ cGMatchConclusion.mli cGSearchPattern.mli
IMPLEMENTATION_FILES = mQGTypes.ml $(INTERFACE_FILES:%.mli=%.ml)
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+let text_of_entries out entries =
+ out "(** MatchConclusion: results of the term inspection **)\n";
+ let text_of_entry (u, b, v) =
+ out (string_of_int v ^ " ");
+ out (if b then "$MC " else "$IC ");
+ out (u ^ "\n")
+ in List.iter text_of_entry entries
+
+let sort_entries entries =
+ let comparator (_, _, v1) (_, _, v2) = compare v1 v2 in
+ List.fast_sort comparator entries
+
+let levels_of_term metasenv context term =
+ let module TC = CicTypeChecker in
+ let module Red = CicReduction in
+ let module Util = MQueryUtil in
+ let degree t =
+ let rec degree_aux = function
+ | Cic.Sort _ -> 1
+ | Cic.Cast (u, _) -> degree_aux u
+ | Cic.Prod (_, _, t) -> degree_aux t
+ | _ -> 2
+ in
+ let u = TC.type_of_aux' metasenv context t in
+ degree_aux (Red.whd context u)
+ in
+ let entry_eq (s1, b1, v1) (s2, b2, v2) =
+ s1 = s2 && b1 = b2
+ in
+ let rec entry_in e = function
+ | [] -> [e]
+ | head :: tail ->
+ head :: if entry_eq head e then tail else entry_in e tail
+ in
+ let inspect_uri main l uri tc v term =
+ let d = degree term in
+ entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
+ in
+ let rec inspect_term main l v term = match term with
+ Cic.Rel _ -> l
+ | Cic.Meta _ -> l
+ | Cic.Sort _ -> l
+ | Cic.Implicit -> l
+ | Cic.Var (u,exp_named_subst) ->
+ let l' = inspect_uri main l u [] v term in
+ inspect_exp_named_subst l' (succ v) exp_named_subst
+ | Cic.Const (u,exp_named_subst) ->
+ let l' = inspect_uri main l u [] v term in
+ inspect_exp_named_subst l' (succ v) exp_named_subst
+ | Cic.MutInd (u, t, exp_named_subst) ->
+ let l' = inspect_uri main l u [t] v term in
+ inspect_exp_named_subst l' (succ v) exp_named_subst
+ | Cic.MutConstruct (u, t, c, exp_named_subst) ->
+ let l' = inspect_uri main l u [t; c] v term in
+ inspect_exp_named_subst l' (succ v) exp_named_subst
+ | Cic.Cast (uu, _) ->
+ inspect_term main l v uu
+ | Cic.Prod (_, uu, tt) ->
+ let luu = inspect_term false l (succ v) uu in
+ inspect_term main luu (succ v) tt
+ | Cic.Lambda (_, uu, tt) ->
+ let luu = inspect_term false l (succ v) uu in
+ inspect_term false luu (succ v) tt
+ | Cic.LetIn (_, uu, tt) ->
+ let luu = inspect_term false l (succ v) uu in
+ inspect_term false luu (succ v) tt
+ | Cic.Appl m -> inspect_list main l true v m
+ | Cic.MutCase (u, t, tt, uu, m) ->
+ let lu = inspect_uri main l u [t] (succ v) term in
+ let ltt = inspect_term false lu (succ v) tt in
+ let luu = inspect_term false ltt (succ v) uu in
+ inspect_list main luu false (succ v) m
+ | Cic.Fix (_, m) -> inspect_ind l (succ v) m
+ | Cic.CoFix (_, m) -> inspect_coind l (succ v) m
+ and inspect_list main l head v = function
+ | [] -> l
+ | tt :: m ->
+ let ltt = inspect_term main l (if head then v else v + 1) tt in
+ inspect_list false ltt false v m
+ and inspect_exp_named_subst l v = function
+ [] -> l
+ | (_,t) :: tl ->
+ let l' = inspect_term false l v t in
+ inspect_exp_named_subst l' v tl
+ and inspect_ind l v = function
+ | [] -> l
+ | (_, _, tt, uu) :: m ->
+ let ltt = inspect_term false l v tt in
+ let luu = inspect_term false ltt v uu in
+ inspect_ind luu v m
+ and inspect_coind l v = function
+ | [] -> l
+ | (_, tt, uu) :: m ->
+ let ltt = inspect_term false l v tt in
+ let luu = inspect_term false ltt v uu in
+ inspect_coind luu v m
+ in
+ let rec inspect_backbone = function
+ | Cic.Cast (uu, _) -> inspect_backbone uu
+ | Cic.Prod (_, _, tt) -> inspect_backbone tt
+ | Cic.LetIn (_, uu, tt) -> inspect_backbone tt
+ | t -> inspect_term true [] 0 t
+ in
+ inspect_backbone term
+
+let get_constraints e c t =
+ let can = sort_entries (levels_of_term e c t) in (* can restrictions *)
+ text_of_entries prerr_string can; flush stderr; (* logging *)
+ let rest_of (u, b, _) =
+ let p = if b then `MainConclusion None else `InConclusion in (p, u)
+ in
+ let rec split vp = function
+ | [], ((_, _, v) as hd) :: tl -> split v ([rest_of hd], tl)
+ | prev, ((_, _, ve) as hd) :: tl when vp = ve ->
+ split vp (rest_of hd :: prev, tl)
+ | p, l -> p, l
+ in
+ let rec mk_musts prev acc = function
+ | [] -> prev, acc
+ | l ->
+ let slice, next = split 0 ([], l) in
+ let acc = acc @ slice in
+ mk_musts (prev @ [acc]) acc next
+ in
+ mk_musts [] [] can
+(*
+ let uri_pos (u,b,v) = (u,b) in
+ let can_use = List.map uri_pos can in
+ let lofl (u,b,v) = [(u,b)] in
+ let rec organize_restr rlist prev_r=
+ match rlist with
+ [] -> []
+ | r::tl ->let curr_r = r@prev_r in
+ curr_r::(organize_restr tl curr_r)
+ in
+ let mrest = List.map lofl can in
+ let must_use = organize_restr mrest [] in (* must restrictions *)
+ (must_use,can_use)
+*)
--- /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/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+val get_constraints: Cic.metasenv -> Cic.context -> Cic.term ->
+ MQGTypes.r_obj list list *
+ MQGTypes.r_obj list
--- /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
+;;
--- /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 *)
+(* *)
+(******************************************************************************)
+
+val get_constraints: Cic.term -> MQGTypes.must_restrictions
false (M.Const s)
in M.StatQuery query
+let unreferred target_pattern source_pattern =
+ let query =
+ M.Bin M.BinFDiff
+ (
+ M.Property false M.RefineExact [] [] [] [] []
+ true (M.Const target_pattern)
+ ) (
+ M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
+ true (M.Const source_pattern)
+
+ )
+ in M.StatQuery query
+
let compose cl =
let letin = ref [] in
let must = ref [] in
| [head] -> (f head)
| head :: tail -> let t = (iter f g tail) in g (f head) t
in
- U.mathql_of_specs prerr_string cl;
+ prerr_endline "(** Compose: received constraints **)";
+ U.mathql_of_specs prerr_string cl; flush stderr;
aux cl;
let must_query =
if ! must = [] then
(* interface for the low-level constraints *********************************)
-val locate : string -> MathQL.query
+val locate : string -> MathQL.query
-val compose : MQGTypes.spec list -> MathQL.query
+val unreferred : string -> string -> MathQL.query
+
+val compose : MQGTypes.spec list -> MathQL.query
(* interface for the high-level constraints ********************************)
+++ /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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-let levels_of_term metasenv context term =
- let module TC = CicTypeChecker in
- let module Red = CicReduction in
- let module Util = MQueryUtil in
- let degree t =
- let rec degree_aux = function
- | Cic.Sort _ -> 1
- | Cic.Cast (u, _) -> degree_aux u
- | Cic.Prod (_, _, t) -> degree_aux t
- | _ -> 2
- in
- let u = TC.type_of_aux' metasenv context t in
- degree_aux (Red.whd context u)
- in
- let entry_eq (s1, b1, v1) (s2, b2, v2) =
- s1 = s2 && b1 = b2
- in
- let rec entry_in e = function
- | [] -> [e]
- | head :: tail ->
- head :: if entry_eq head e then tail else entry_in e tail
- in
- let inspect_uri main l uri tc v term =
- let d = degree term in
- entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
- in
- let rec inspect_term main l v term = match term with
- Cic.Rel _ -> l
- | Cic.Meta _ -> l
- | Cic.Sort _ -> l
- | Cic.Implicit -> l
- | Cic.Var (u,exp_named_subst) ->
- let l' = inspect_uri main l u [] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.Const (u,exp_named_subst) ->
- let l' = inspect_uri main l u [] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.MutInd (u, t, exp_named_subst) ->
- let l' = inspect_uri main l u [t] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.MutConstruct (u, t, c, exp_named_subst) ->
- let l' = inspect_uri main l u [t; c] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.Cast (uu, _) ->
- inspect_term main l v uu
- | Cic.Prod (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term main luu (v + 1) tt
- | Cic.Lambda (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Cic.LetIn (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Cic.Appl m -> inspect_list main l true v m
- | Cic.MutCase (u, t, tt, uu, m) ->
- let lu = inspect_uri main l u [t] (v + 1) term in
- let ltt = inspect_term false lu (v + 1) tt in
- let luu = inspect_term false ltt (v + 1) uu in
- inspect_list main luu false (v + 1) m
- | Cic.Fix (_, m) -> inspect_ind l (v + 1) m
- | Cic.CoFix (_, m) -> inspect_coind l (v + 1) m
- and inspect_list main l head v = function
- | [] -> l
- | tt :: m ->
- let ltt = inspect_term main l (if head then v else v + 1) tt in
- inspect_list false ltt false v m
- and inspect_exp_named_subst l v = function
- [] -> l
- | (_,t) :: tl ->
- let l' = inspect_term false l v t in
- inspect_exp_named_subst l' v tl
- and inspect_ind l v = function
- | [] -> l
- | (_, _, tt, uu) :: m ->
- let ltt = inspect_term false l v tt in
- let luu = inspect_term false ltt v uu in
- inspect_ind luu v m
- and inspect_coind l v = function
- | [] -> l
- | (_, tt, uu) :: m ->
- let ltt = inspect_term false l v tt in
- let luu = inspect_term false ltt v uu in
- inspect_coind luu v m
- in
- let rec inspect_backbone = function
- | Cic.Cast (uu, _) -> inspect_backbone uu
- | Cic.Prod (_, _, tt) -> inspect_backbone tt
- | Cic.LetIn (_, uu, tt) -> inspect_backbone tt
- | t -> inspect_term true [] 0 t
- in
- inspect_backbone term
-
-let out_restr e c t =
- let can = levels_of_term e c t in (* can restrictions *)
-prerr_endline "";
-prerr_endline
- ("#### IN LEVELS @@@@ lunghezza can: " ^ string_of_int (List.length can));
-prerr_endline "";
-(* let rest = restrict level levels in *)
- let uri_pos (u,b,v) = (u,b) in
- let can_use = List.map uri_pos can in
- let lofl (u,b,v) = [(u,b)] in
- let rec organize_restr rlist prev_r=
- match rlist with
- [] -> []
- | r::tl ->let curr_r = r@prev_r in
- curr_r::(organize_restr tl curr_r)
- in
- let mrest = List.map lofl can in
- let must_use = organize_restr mrest [] in (* must restrictions *)
- (must_use,can_use)
-;;
+++ /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/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list)
+++ /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
-;;
+++ /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 *)
-(* *)
-(******************************************************************************)
-
-val get_constraints: Cic.term -> MQGTypes.must_restrictions
let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
- let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
+ let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
let must = choose_must list_of_must only in
- let torigth_restriction (u,b) =
- (if b then `MainConclusion None else `InConclusion), u
- in
- let rigth_must = List.map torigth_restriction must in
- let rigth_only = Some (List.map torigth_restriction only) in
let result =
I.execute mqi_handle
(G.query_of_constraints
(Some U.universe_for_match_conclusion)
- (rigth_must,[],[]) (rigth_only,None,None)) in
+ (must,[],[]) (Some only,None,None)) in
let uris =
List.map
(function uri,_ ->
val matchConclusion : MQIConn.handle ->
?output_html:(string -> unit) ->
- (* boolean value: true = in main position *)
- choose_must:((MQGTypes.uri * bool) list list ->
- (MQGTypes.uri * bool) list ->
- (MQGTypes.uri * bool) list) ->
+ choose_must:(MQGTypes.r_obj list list ->
+ MQGTypes.r_obj list ->
+ MQGTypes.r_obj list) ->
unit -> status: ProofEngineTypes.status -> string list
U.universe_for_search_pattern,
(constr_obj, constr_rel, constr_sort), (None,None,None)
| req_path ->
- let must = MQueryLevels2.get_constraints term in
+ let must = CGSearchPattern.get_constraints term in
refine_constraints must req_path
;;
let result = MQueryInterpreter.execute mqi_handle query in
C.close mqi_handle;
Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
+ | "/unreferred" ->
+ let mqi_handle = C.init mqi_flags debug_print in
+ let target = req#param "target" in
+ let source = req#param "source" in
+ let query = G.unreferred target source in
+ let result = MQueryInterpreter.execute mqi_handle query in
+ C.close mqi_handle;
+ Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
| "/getpage" ->
(* TODO implement "is_permitted" *)
(let is_permitted _ = true in
projects / helm.git / commitdiff