let unopt = function Some x -> x | None -> assert false
let incr_depth = function
- | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
- | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
+ | `MainConclusion (Some (Eq depth)) -> `MainConclusion (Some (Eq (depth + 1)))
+ | `MainHypothesis (Some (Eq depth)) -> `MainHypothesis (Some (Eq (depth + 1)))
| _ -> assert false
let var_has_body uri =
| Cic.Prod (_, source, target) ->
(match pos with
| `MainConclusion _ ->
- let set = aux (`MainHypothesis (Some 0)) set source in
+ let set = aux (`MainHypothesis (Some (Eq 0))) set source in
aux (incr_depth pos) set target
| `MainHypothesis _ ->
let set = aux `InHypothesis set source in
List.flatten
(List.map (compute_var (next_pos pos)) params) in
(match pos with
- | `MainHypothesis (Some 0) ->
- let pos = `MainHypothesis (Some (depth_offset params)) in
+ | `MainHypothesis (Some (Eq 0)) ->
+ let pos = `MainHypothesis (Some (Eq (depth_offset params))) in
(compute pos ~body:None ~ty)@metadata_of_vars
| `InHypothesis ->
(compute pos ~body:None ~ty)@metadata_of_vars
match o with
| Cic.Variable (_, body, ty, params, _)
| Cic.Constant (_, body, ty, params, _) ->
- let pos = `MainConclusion (Some (depth_offset params)) in
+ let pos = `MainConclusion (Some (Eq (depth_offset params))) in
let metadata = compute pos ~body ~ty
in
let metadata_of_vars =
List.flatten
- (List.map (compute_var (`MainHypothesis (Some 0))) params)
+ (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params)
in
[UriManager.string_of_uri uri,
UriManager.name_of_uri uri,metadata @ metadata_of_vars]
| Cic.InductiveDefinition (types, params, _, _) ->
- let pos = `MainConclusion(Some (depth_offset params)) in
+ let pos = `MainConclusion(Some (Eq (depth_offset params))) in
let metadata_of_vars =
List.flatten
- (List.map (compute_var (`MainHypothesis (Some 0))) params) in
+ (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) in
let metadata = compute_ind pos ~uri ~types in
List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
| Cic.CurrentProof _ -> assert false
-let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty
+let compute ~body ~ty = compute (`MainConclusion (Some (Eq 0))) ~body ~ty
open MetadataTypes
+let pp_relation r =
+ match r with
+ | Eq i -> sprintf "= %d" i
+ | Ge i -> sprintf ">= %d" i
+ | Gt i -> sprintf "> %d" i
+ | Le i -> sprintf "<= %d" i
+ | Lt i -> sprintf "< %d" i
+
let pp_position = function
- | `MainConclusion (Some d) -> sprintf "MainConclusion(%d)" d
+ | `MainConclusion (Some d) -> sprintf "MainConclusion(%s)" (pp_relation d)
| `MainConclusion None -> sprintf "MainConclusion"
- | `MainHypothesis (Some d) -> sprintf "MainHypothesis(%d)" d
+ | `MainHypothesis (Some d) -> sprintf "MainHypothesis(%s)" (pp_relation d)
| `MainHypothesis None -> "MainHypothesis"
| `InConclusion -> "InConclusion"
| `InHypothesis -> "InHypothesis"
| `InHypothesis -> inhyp_pos
| `InBody -> inbody_pos
-let columns_of_position = function
- | `MainConclusion (Some d) -> `String mainconcl_pos, `Int d
+let columns_of_position pos =
+ match pos with
+ | `MainConclusion (Some (Eq d)) -> `String mainconcl_pos, `Int d
| `MainConclusion None -> `String mainconcl_pos, `Null
- | `MainHypothesis (Some d) -> `String mainhyp_pos, `Int d
+ | `MainHypothesis (Some (Eq d)) -> `String mainhyp_pos, `Int d
| `MainHypothesis None -> `String mainhyp_pos, `Null
| `InConclusion -> `String inconcl_pos, `Null
| `InHypothesis -> `String inhyp_pos, `Null
| `InBody -> `String inbody_pos, `Null
+ | _ -> assert false
(*
let metadata_ns = "http://www.cs.unibo.it/helm/schemas/schema-helm"
(fun (sort_cols, rel_cols, obj_cols) metadata ->
match metadata with
| `Sort (s, p) ->
- let (p, d) = columns_of_position p in
+ let (p, d) = columns_of_position (p :> position) in
[source; p; d; sort s] :: sort_cols, rel_cols, obj_cols
| `Rel p ->
- let (p, d) = columns_of_position p in
+ let (p, d) = columns_of_position (p :> position) in
sort_cols, [source; p; d] :: rel_cols, obj_cols
| `Obj (o, p) ->
let (p, d) = columns_of_position p in
[ "Obj" ] @ List.map Dbi.sdebug (obj_cols :> Dbi.sql_t list list))
*)
+
let elim ~dbd uri =
let constraints =
[`Rel [`MainConclusion None];
- `Sort (Cic.Prop,[`MainHypothesis (Some 1)]);
- `Obj (uri,[`MainHypothesis (Some 0)]);
+ `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Gt 1))]);
+ `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
`Obj (uri,[`InHypothesis]);
]
in
let no_concl = MetadataDb.count_distinct `Conclusion metadata in
let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
let no_full = MetadataDb.count_distinct `Statement metadata in
- let is_dummy =
- function
- `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy"
- | _ -> true in
- let rec look_for_dummy_main =
- function
- [] -> None
- | `Obj(s,`MainConclusion (Some d))::_
- when ((String.sub s 0 10) = "cic:/dummy") ->
- let len = String.length s in
- let dummy_index = int_of_string (String.sub s 11 (len-11)) in
- let dummy_type = List.nth types dummy_index in
- Some (d,dummy_type)
- | _::l -> look_for_dummy_main l in
+ let is_dummy = function
+ | `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy"
+ | _ -> true
+ in
+ let rec look_for_dummy_main = function
+ | [] -> None
+ | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
+ when ((String.sub s 0 10) = "cic:/dummy") ->
+ let len = String.length s in
+ let dummy_index = int_of_string (String.sub s 11 (len-11)) in
+ let dummy_type = List.nth types dummy_index in
+ Some (d,dummy_type)
+ | _::l -> look_for_dummy_main l
+ in
match (look_for_dummy_main metadata) with
- None->
- prerr_endline "Caso None";
- (* no dummy in main position *)
- let metadata = List.filter is_dummy metadata in
- let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- let concl_card = Some (MetadataConstraints.Eq no_concl) in
- let full_card = Some (MetadataConstraints.Eq no_full) in
- let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
- Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
+ | None->
+ prerr_endline "Caso None";
+ (* no dummy in main position *)
+ let metadata = List.filter is_dummy metadata in
+ let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+ let concl_card = Some (MetadataConstraints.Eq no_concl) in
+ let full_card = Some (MetadataConstraints.Eq no_full) in
+ let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
+ Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
| Some (depth, dummy_type) ->
prerr_endline
- (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type));
- (* a dummy in main position *)
- let metadata_for_dummy_type =
- MetadataExtractor.compute ~body:None ~ty:dummy_type in
- (* Let us skip this for the moment
- let main_of_dummy_type =
- look_for_dummy_main metadata_for_dummy_type in *)
- let metadata = List.filter is_dummy metadata in
- let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- let metadata_for_dummy_type =
- List.filter is_dummy metadata_for_dummy_type in
- let constraints_for_dummy_type =
- List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
- (* start with the dummy constant in main conlusion *)
- let from = ["refObj as table0"] in
- let where =
- [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
- sprintf "table0.h_depth = %d" depth] in
- let (n,from,where) =
- List.fold_left
- (MetadataConstraints.add_constraint ~start:2)
- (2,from,where) constraints in
- let concl_card = Some (MetadataConstraints.Eq no_concl) in
- let full_card = Some (MetadataConstraints.Eq no_full) in
- let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
- let (n,from,where) =
- MetadataConstraints.add_all_constr
- (n,from,where) concl_card full_card diff in
- (* join with the constraints over the type of the constant *)
- let where =
- (sprintf "table0.h_occurrence = table%d.source" n)::where in
- let (m,from,where) =
- List.fold_left
- (MetadataConstraints.add_constraint ~start:n)
- (n,from,where) constraints_for_dummy_type in
- Constr.exec ~dbd (m,from,where)
+ (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type));
+ (* a dummy in main position *)
+ let metadata_for_dummy_type =
+ MetadataExtractor.compute ~body:None ~ty:dummy_type in
+ (* Let us skip this for the moment
+ let main_of_dummy_type =
+ look_for_dummy_main metadata_for_dummy_type in *)
+ let metadata = List.filter is_dummy metadata in
+ let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+ let metadata_for_dummy_type =
+ List.filter is_dummy metadata_for_dummy_type in
+ let metadata_for_dummy_type, depth' =
+ (* depth' = the depth of the A -> A -> Prop *)
+ List.fold_left (fun (acc,dep) c ->
+ match c with
+ | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
+ (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
+ | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
+ (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
+ | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) ->
+ (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
+ | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
+ in
+ let constraints_for_dummy_type =
+ List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
+ (* start with the dummy constant in main conlusion *)
+ let from = ["refObj as table0"] in
+ let where =
+ [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
+ sprintf "table0.h_depth >= %d" depth] in
+ let (n,from,where) =
+ List.fold_left
+ (MetadataConstraints.add_constraint ~start:2)
+ (2,from,where) constraints in
+ let concl_card = Some (MetadataConstraints.Eq no_concl) in
+ let full_card = Some (MetadataConstraints.Eq no_full) in
+ let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
+ let (n,from,where) =
+ MetadataConstraints.add_all_constr
+ (n,from,where) concl_card full_card diff in
+ (* join with the constraints over the type of the constant *)
+ let where =
+ (sprintf "table0.h_occurrence = table%d.source" n)::where in
+ let where =
+ sprintf "table0.h_depth - table%d.h_depth = %d"
+ n (depth - depth')::where
+ in
+ let (m,from,where) =
+ List.fold_left
+ (MetadataConstraints.add_constraint ~start:n)
+ (n,from,where) constraints_for_dummy_type in
+ Constr.exec ~dbd (m,from,where)
projects / helm.git / commitdiff