METADIR = ../meta
-REQUIRES = threads hbugs-common helm-cic_proof_checking helm-tactics helm-getter
+REQUIRES = threads hbugs-common helm-cic_proof_checking helm-getter \
+ helm-cic_textual_parser \
+ helm-mathql helm-mathql_interpreter helm-tactics
COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
OCAMLFIND = ocamlfind
OCAMLC = $(OCAMLFIND) ocamlc $(COMMONOPTS)
--- /dev/null
+requires="helm-urimanager helm-mathql helm-cic helm-cic_proof_checking"
+version="1.2"
+archive(byte)="mathql_generator.cma"
+archive(native)="mathql_generator.cmxa"
+linkopts=""
--- /dev/null
+*.cmi
+*.cmo
+*.cma
+*.cmx
+*.cmxa
--- /dev/null
+mQueryLevels2.cmi: mQueryGenerator.cmi
+mQueryLevels.cmo: mQueryLevels.cmi
+mQueryLevels.cmx: mQueryLevels.cmi
+mQueryLevels2.cmo: mQueryLevels2.cmi
+mQueryLevels2.cmx: mQueryLevels2.cmi
+mQueryGenerator.cmo: mQueryGenerator.cmi
+mQueryGenerator.cmx: mQueryGenerator.cmi
--- /dev/null
+PACKAGE = mathql_generator
+REQUIRES = helm-urimanager helm-mathql helm-cic helm-cic_proof_checking
+PREDICATES =
+
+INTERFACE_FILES = mQueryLevels.mli mQueryLevels2.mli mQueryGenerator.mli
+
+IMPLEMENTATION_FILES = mQueryLevels.ml mQueryLevels2.ml mQueryGenerator.ml
+
+EXTRA_OBJECTS_TO_INSTALL =
+
+EXTRA_OBJECTS_TO_CLEAN =
+
+include ../Makefile.common
--- /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/.
+ *)
+
+(* Query issuing functions **************************************************)
+
+type uri = string
+type position = string
+type depth = int option
+type sort = string
+
+type r_obj = (uri * position * depth)
+type r_rel = (position* depth)
+type r_sort = (position* depth * sort)
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type only_restrictions =
+ (r_obj list option * r_rel list option * r_sort list option)
+type universe = position list option
+
+let builtin s =
+ let ns = "h:" in
+ match s with
+ | "MH" -> ns ^ "MainHypothesis"
+ | "IH" -> ns ^ "InHypothesis"
+ | "MC" -> ns ^ "MainConclusion"
+ | "IC" -> ns ^ "InConclusion"
+ | "IB" -> ns ^ "InBody"
+ | "SET" -> ns ^ "Set"
+ | "PROP" -> ns ^ "Prop"
+ | "TYPE" -> ns ^ "Type"
+ | _ -> raise (Failure "MQueryGenerator.builtin")
+
+(* Query building functions ************************************************)
+
+module M = MathQL
+
+let locate s =
+ M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
+
+let query_of_constraints univ must_use can_use =
+(* FG : The (univ : universe) is not used in this implementation *)
+ let in_path s = (s, []) in
+ let assign v p = (in_path v, in_path p) in
+
+(* can restrictions *)
+
+ let (cr_o,cr_r,cr_s) = can_use in
+
+ let uri_of_entry (r, p, d) = r in
+
+ let universe =
+ match cr_o with
+ None -> []
+ | Some cr_o -> List.map uri_of_entry cr_o
+ in
+
+ let tfst (a,b,c) = a in
+ let tsnd (a,b,c) = b in
+ let trd (a,b,c) = c in
+
+ let to_int_list l d =
+ match d with
+ None -> l
+ | Some d -> l@[d]
+ in
+
+ let opos =
+ match cr_o with
+ None -> []
+ | Some cr_o -> (List.map tsnd cr_o) in
+
+ let odep =
+ match cr_o with
+ None -> []
+ | Some cr_o -> List.map trd cr_o
+ (* let odep_option_list = List.map trd cr_o in
+ let lo_dep_int = List.fold_left to_int_list [] odep_option_list in
+ List.map string_of_int lo_dep_int*)
+ in
+ print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout;
+ print_endline"";
+ let rpos =
+ match cr_r with
+ None -> []
+ | Some cr_r -> (List.map fst cr_r) in
+
+ let rdep =
+ match cr_r with
+ None -> []
+ | Some cr_r -> List.map snd cr_r
+ (* let rdep_option_list = List.map snd cr_r in
+ let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in
+ List.map string_of_int lr_dep_int *)
+ in
+
+
+ let spos =
+ match cr_s with
+ None -> []
+ | Some cr_s -> (List.map tfst cr_s) in
+
+
+ let sdep =
+ match cr_s with
+ None -> []
+ | Some cr_s -> List.map tsnd cr_s
+ (* let sdep_option_list = List.map tsnd cr_s in
+ let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in
+ List.map string_of_int ls_dep_int*)
+ in
+
+
+ let sor =
+ match cr_s with
+ None -> []
+ | Some cr_s -> List.map trd cr_s in
+
+ (* let q_where_obj = function
+ Some l ->
+ if odep = [] then
+ M.Sub
+ (M.RefOf
+ (M.Select
+ ("uri",
+ M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]),
+ M.Ex ["uri"]
+ (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))),
+ M.VVar "universe")
+ else
+ M.Sub
+ (M.RefOf
+ (M.Select
+ ("uri",
+ M.Relation
+ (false, M.RefineExact, in_path "refObj",
+ M.Ref (M.RefOf (M.RVar "uri0")),
+ [assign "p" "position"; assign "d" "depth"]
+ ),
+ M.Ex ["uri"]
+ (M.And
+ ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))),
+ (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d")))))
+ )
+ ),
+ M.VVar "universe"
+ )
+
+ | None -> M.True
+ in*)
+
+
+
+ let q_where_obj n = function
+ Some l ->
+ let rec q_ex n = function
+ [] -> M.True
+ | [(u,p,None)] ->
+ M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p"))
+
+ | [(u,p,d)] ->
+ print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
+ print_endline"";
+ M.And
+ (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")),
+ M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d")))
+ | (u,p,None)::tl ->
+ M.Or
+ (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")),
+ q_ex (n+1) tl)
+ | (u,p,d)::tl ->
+ print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
+ print_endline"";
+ M.Or
+ ((M.And
+ ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))),
+ (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))),
+ q_ex (n+1) tl)
+ in
+ M.Sub
+ (M.RefOf
+ (M.Select
+ ("uri",
+ M.Relation
+ (false, M.RefineExact, in_path "refObj",
+ M.Ref (M.RefOf (M.RVar "uri0")),
+ [assign "p" "position"; assign "d" "depth"]
+ ),
+ M.Ex ["uri"]
+ (q_ex 1 l))),
+ M.VVar "universe")
+ | None -> M.True
+ in
+
+
+
+
+ let rec q_where_rel n cr_r= (*function*)
+ (* Some l ->*)
+ let q0 =
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refRel", ["position"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar ("rel_position" ^ string_of_int n))
+ in
+ match cr_r with
+ Some [] -> M.True
+ | Some [(p,None)] -> q0
+ | Some [(p,d)] ->
+ M.And
+ (q0,
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refRel", ["depth"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar ("rel_depth" ^ string_of_int n)))
+ | Some ((p,None)::tl) ->
+ M.Or
+ (q0,
+ q_where_rel (n+1) (Some tl))
+ | Some ((p,d)::tl) ->
+ M.Or
+ (M.And
+ (q0,
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refRel", ["depth"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar ("rel_depth" ^ string_of_int n))),
+ q_where_rel (n+1) (Some tl))
+ | None -> M.True
+ in
+
+ let rec q_where_sort n cr_s = (*function *)
+ (* Some l ->*)
+ let q0 =
+ M.And
+ (M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refSort", ["position"]),
+ M.RefOf(M.RVar "uri0")
+ ),
+ M.VVar ("sort_position" ^ string_of_int n)),
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refSort", ["sort"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar ("sort" ^ string_of_int n)))
+ in
+ match cr_s with
+ Some [] -> M.True
+ | Some [(p,None,s)] -> q0
+
+ | Some [(p,d,s)] ->
+ M.And
+ (q0,
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refSort", ["depth"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar ("sort_depth" ^ string_of_int n)))
+
+ | Some ((p,None,s)::tl) ->
+ M.Or
+ (q0,
+ q_where_sort (n+1) (Some tl))
+
+ | Some((p,d,s)::tl) ->
+ M.Or
+ (M.And
+ (q0,
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refSort", ["depth"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar ("sort_depth" ^ string_of_int n))),
+ q_where_sort (n+1) (Some tl))
+ | None -> M.True
+ in
+
+
+
+
+ let q_where cr =
+ let (cr_o,cr_r,cr_s) = cr in
+ M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s))
+
+ in
+
+(* must restrictions *)
+
+ let build_select_obj (r, pos, dep) =
+ match dep with
+ None -> M.Select
+ ("uri",
+ M.Relation (false, M.RefineExact, ("backPointer", []),
+ M.Ref (M.Const [r]), [assign "p" "position"]),
+ M.Ex ["uri"]
+ ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))))
+ | Some dep -> let string_dep = string_of_int dep in
+ M.Select
+ ("uri",
+ M.Relation (false, M.RefineExact, ("backPointer", []),
+ M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
+ M.Ex ["uri"]
+ (M.And
+ ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+ (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
+ in
+
+ let build_select_rel (pos, dep) =
+ match dep with
+ None -> M.Select
+ ("uri",
+ M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
+ M.Ex ["uri"]
+ (M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))
+ | Some dep -> let string_dep = string_of_int dep in
+ M.Select
+ ("uri",
+ M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
+ M.Ex ["uri"]
+ (M.And
+ ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+ (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
+ in
+
+ let build_select_sort (pos, dep, sor) =
+ match dep with
+ None -> M.Select
+ ("uri",
+ M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
+ M.Ex ["uri"]
+ (M.And
+ ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+ (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
+
+ | Some dep -> let string_dep = string_of_int dep in
+ M.Select
+ ("uri",
+ M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
+ M.Ex ["uri"]
+ (M.And
+ ((M.And
+ ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+ (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))),
+ (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
+ in
+
+ let rec build_intersect_obj = function
+ [] -> M.Pattern (M.Const ["[.]*"])
+ | [hd] -> build_select_obj hd
+ | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
+ in
+
+ let rec build_intersect_rel = function
+ [] -> M.Ref(M.Const [])
+ | [hd] -> build_select_rel hd
+ | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
+ in
+
+ let rec build_intersect_sort = function
+ [] -> M.Ref(M.Const [])
+ | [hd] -> build_select_sort hd
+ | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
+ in
+
+ let build_intersect = function
+(* let tostring_sort (a,b,c) =
+ let b1 = string_of_int b in
+ (a,b1,c)
+ in
+ let tostring_rel (a,b) =
+ let b1 = string_of_int b in
+ (a,b1)
+ in*)
+
+(* let (l1,l2,l3) = must in
+ match (l1,l2,l3) with *)
+ l1,[],[] -> build_intersect_obj l1
+ | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
+ build_intersect_rel l2
+ | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*)
+ build_intersect_sort l3
+ | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
+ M.Intersect (build_intersect_obj l1, build_intersect_rel l2)
+ | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in *)
+ M.Intersect (build_intersect_obj l1, build_intersect_sort l3)
+ | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in
+ let lsort = List.map tostring_sort l3 in*)
+ M.Intersect (build_intersect_rel l2, build_intersect_sort l3)
+ | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in
+ let lsort = List.map tostring_sort l3 in *)
+ M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3)
+ in
+
+ let q_in = build_intersect must_use in
+ let q_select = M.Select ("uri0", q_in, q_where can_use) in
+
+(* variables for can restrictions *)
+
+ let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in
+
+ let rec q_let_s sor n =
+ match sor with
+ [] -> q_let_u
+ | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u)
+ | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1))
+ in
+
+(* let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *)
+
+ let rec q_let_ds sdep n =
+ match sdep with
+ []
+ | [None] -> q_let_s sor 1
+ | (None)::tl -> q_let_ds tl (n+1)
+ | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1)
+ | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1))
+ in
+
+(* let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in *)
+
+ let rec q_let_dr rdep n =
+ match rdep with
+ []
+ | [None] -> q_let_ds sdep 1
+ | (None)::tl -> q_let_dr tl (n+1)
+ | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1)
+ | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1))
+ in
+
+
+ (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*)
+
+ let rec q_let_do odep n =
+ match odep with
+ []
+ | [None] -> q_let_dr rdep 1
+ | (None)::tl -> q_let_do tl (n+1)
+ | [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1)
+ | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1))
+ in
+
+
+(* let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in *)
+
+
+ let rec q_let_ps spos n =
+ match spos with
+ [] -> q_let_do odep 1
+ | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1)
+ | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1))
+ in
+
+
+(* let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *)
+
+
+ let rec q_let_pr rpos n =
+ match rpos with
+ [] -> q_let_ps spos 1
+ | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1)
+ | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1))
+ in
+
+
+
+(* let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *)
+
+ let rec q_let_po opos n =
+ match opos with
+ [] -> q_let_pr rpos 1
+ | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1)
+ | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1))
+ in
+
+ (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
+
+ let query = (M.Ref (M.RefOf (q_let_po opos 1))) in
+
+print_endline "### "; MQueryUtil.text_of_query print_string query "\n"; flush stdout;
+ query
--- /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/.
+ *)
+
+type uri = string
+type position = string
+type depth = int option
+type sort = string
+
+type r_obj = (uri * position * depth)
+type r_rel = (position * depth)
+type r_sort = (position * depth * sort)
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type only_restrictions =
+ (r_obj list option * r_rel list option * r_sort list option)
+type universe = position list option
+
+val locate : string -> MathQL.query
+
+val query_of_constraints : universe -> must_restrictions -> only_restrictions -> MathQL.query
+
+val builtin : MathQL.vvar -> string
--- /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 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+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/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
+(* 30/04/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+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 *)
+(* *)
+(******************************************************************************)
+
+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',Some 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#Prop"
+ | 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',Some 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
+ 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
+ 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 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
+ ) rels ;
+ prerr_endline "Constraints on Sorts:" ;
+ List.iter
+ (function (s1,n,s2) ->
+ prerr_endline
+ (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
+ " " ^ 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
-mqgtop.cmo: mQGTopParser.cmo
+mqgtop.cmo: mQGTopParser.cmi
mqgtop.cmx: mQGTopParser.cmx
+mQGTopParser.cmo: mQGTopParser.cmi
+mQGTopParser.cmx: mQGTopParser.cmi
+mQGTopLexer.cmo: mQGTopParser.cmi
+mQGTopLexer.cmx: mQGTopParser.cmx
BIN_DIR = /usr/local/bin
-REQUIRES = unix helm-cic helm-cic_textual_parser helm-mathql helm-mathql_interpreter helm-mquery_generator
+REQUIRES = unix helm-cic helm-cic_textual_parser helm-mathql \
+ helm-mathql_interpreter helm-mathql_generator
PREDICATES =
OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
MQGTOP = mqgtop.ml
DEPOBJS = $(MQTOP) $(MQITOP) $(MQGTOP)
-AUXOBJS = mQGTopParser.ml mQGTopLexer.ml
+AUXOBJS = mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
all: $(DEPOBJS:.ml=)
opt: $(DEPOBJS:.ml=.opt)
depend: $(AUXOBJS)
- $(OCAMLDEP) $(DEPOBJS) > .depend
+ $(OCAMLDEP) $(DEPOBJS) $(AUXOBJS) > .depend
mqtop: $(MQTOP:.ml=.cmo) $(LIBRARIES)
$(OCAMLC) -linkpkg -o mqtop $(MQTOP:.ml=.cmo)
let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
- let q = MQG.searchPattern (om,rm,sm) (oo,ro,so) in
+ let q = MQG.query_of_constraints None (om,rm,sm) (oo,ro,so) in
if not (List.mem q ! queries) then
begin
issue handle q;
prerr_endline "-x -execute issues a query given in the input file";
prerr_endline "-i -interp FILE sets the CIC short names interpretation file";
prerr_endline "-d -disply outputs the CIC terms given in the input file";
- prerr_endline "-C -compose issues the \"Compose\" query reading its specifications";
- prerr_endline " from the input file";
prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
+(* prerr_endline "-C -compose issues the \"Compose\" query reading its specifications";
+ prerr_endline " from the input file";
prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all";
prerr_endline " CIC terms in the input file";
prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
prerr_endline " on all CIC terms in the input file";
- prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all";
+*) 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";
| ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
| ("-c"|"-check") :: rem -> check (); parse rem
| ("-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 ->
let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem