X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=e08847c8fd7290b27a5a73eb43432405a5065c45;hb=4020414d9bc31b545e311760045d4ce8f0645916;hp=b1c84ce10a483e414ad2e2ea44957397822f65ee;hpb=ec899ba2461af8c3f0ef253a8879fc1882b8b46f;p=helm.git diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index b1c84ce10..e08847c8f 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -12,15 +12,18 @@ let par () = "

" (* CIC term inspecting functions *) +let env = ref [] (* metasemv *) +let cont = ref [] (* context *) + let ie_out (r, b, v) = let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in - res (pos ^ str_uref r) ^ nl () + res (pos ^ str_uref r) ^ nl () (* FG: si puo' usare xp_str_uref se si vuole xpointer *) let rec il_out = function | [] -> "" | head :: tail -> ie_out head ^ il_out tail -let ie_struri (u, b, v) = str_uref u +let ie_str_uri (u, b, v) = xp_str_uref u let rec il_restrict level = function | [] -> [] @@ -36,61 +39,78 @@ let rec ie_insert ie = function | head :: tail -> head :: if ie_eq head ie then tail else ie_insert ie tail -let inspect_uri main l uri tc v = +let degree t = + let u0 = CicTypeChecker.type_of_aux' !env !cont t in + let u = CicReduction.whd !cont u0 in + let rec deg = function + | Sort _ -> 1 + | Cast (uu, _) -> deg uu + | Prod (_, _, tt) -> deg tt + | _ -> 2 + in deg u + +let inspect_uri main l uri tc v term = + let d = degree term in let fi = match tc with | t0 :: c0 :: _ -> [t0 + 1; c0] | t0 :: _ -> [t0 + 1] | [] -> [] - in ie_insert ((uri, fi), main, v) l + in ie_insert ((uri, fi), main, 2 * v + d - 1) l -let rec inspect_term main l v = function - | Rel i -> l - | Meta (i, _) -> l - | Sort s -> l +let rec inspect_term main l v term = + match term with + | Rel _ -> l + | Meta (_, _) -> l + | Sort _ -> l | Implicit -> l - | Var u -> inspect_uri main l u [] v - | Const (u, i) -> inspect_uri main l u [] v - | MutInd (u, i, t) -> inspect_uri main l u [t] v - | MutConstruct (u, i, t, c) -> inspect_uri main l u [t; c] v + | Var u -> inspect_uri main l u [] v term + | Const (u, _) -> inspect_uri main l u [] v term + | MutInd (u, _, t) -> inspect_uri main l u [t] v term + | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term | Cast (uu, _) -> - (*CSC: Cast modified so that it behaves exactly as if no Cast was there *) inspect_term main l v uu - | Prod (n, uu, tt) -> + | Prod (_, uu, tt) -> let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Lambda (n, uu, tt) -> + inspect_term main luu (v + 1) tt + | Lambda (_, uu, tt) -> let luu = inspect_term false l (v + 1) uu in inspect_term false luu (v + 1) tt - | LetIn (n, uu, tt) -> + | LetIn (_, uu, tt) -> let luu = inspect_term false l (v + 1) uu in inspect_term false luu (v + 1) tt | Appl m -> inspect_list main l true v m - | MutCase (u, i, t, tt, uu, m) -> - let lu = inspect_uri main l u [t] (v + 1) in + | 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 - | Fix (i, m) -> inspect_ind l (v + 1) m - | CoFix (i, m) -> inspect_coind l (v + 1) m + | Fix (_, m) -> inspect_ind l (v + 1) m + | 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 + let ltt = inspect_term main l (if head then v else v + 1) tt in inspect_list false ltt false v m and inspect_ind l v = function | [] -> l - | (n, i, tt, uu) :: m -> + | (_, _, 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 - | (n, tt, uu) :: m -> + | (_, 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 -let inspect t = inspect_term true [] 0 t +let rec inspect_backbone = function + | Cast (uu, _) -> inspect_backbone uu + | Prod (_, _, tt) -> inspect_backbone tt + | LetIn (_, uu, tt) -> inspect_backbone tt + | t -> inspect_term true [] 0 t + +let inspect t = inspect_backbone t (* query building functions *) @@ -104,12 +124,12 @@ let build_select (r, b, v) n = let svar = "str" ^ string_of_int n in let mqs = if b then MQMConclusion else MQConclusion in MQSelect (rvar, - MQUse (MQReference [str_uref r], svar), + MQUse (MQReference [xp_str_uref r], svar), MQIs (MQStringSVar svar, mqs) ) let rec build_inter n = function - | [] -> MQPattern [(None, [MQBSS], [MQFSS])] + | [] -> MQPattern (None, [MQBSS], [MQFSS]) | [ie] -> build_select ie n | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) @@ -118,7 +138,7 @@ let restrict_universe query = [] -> query (* no constraints ===> the universe is the library *) | l -> let universe = - MQReference (List.map ie_struri l) + MQReference (List.map ie_str_uri l) in MQLetIn ( "universe", universe, @@ -149,8 +169,13 @@ let close = Mqint.close let locate s = let query = +(*CSC: next query to be fixed + 1) I am exploiting the bug that does not quote '|' + 2) I am searching only constants and mutual inductive definition blocks + (i.e. no fragment identifier at all) +*) MQList (MQSelect ("ref", - MQPattern [(None, [MQBSS], [MQFSS])], + MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]), MQIs (MQFunc (MQName, "ref"), MQCons s ) @@ -159,7 +184,13 @@ let locate s = in build_result query -let backward t level = +let levels e c t level = + env := e; cont := c; + let il = inspect t in + par () ^ il_out il ^ nl () + +let backward e c t level = + env := e; cont := c; let il = inspect t in let query = build_inter 0 (il_restrict level il) in let query' = restrict_universe query il in