From: Enrico Tassi Date: Tue, 1 Jun 2004 13:44:34 +0000 (+0000) Subject: new universes implementation X-Git-Tag: pre_subst_in_kernel~43 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git new universes implementation --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index bda4c4b82..eeb6053aa 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -469,6 +469,11 @@ let qed () = None -> assert false | Some (uri,[],bo,ty) -> let uri = match uri with Some uri -> uri | _ -> assert false in + (* we want to typecheck in the ENV *) + (*let old_working = CicUniv.get_working () in + CicUniv.set_working (CicUniv.get_global ());*) + CicUniv.directly_to_env_begin () ; + prerr_endline "-------------> QED"; if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty @@ -484,7 +489,16 @@ let qed () = let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in make_dirs pathname ; save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types - pathname + pathname; + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri ( + Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[])); + (* FIXME: the variable list!! *) + (* + CicUniv.qed (); (* now the env has the right constraints *)*) + CicUniv.directly_to_env_end(); + CicUniv.reset_working (); + prerr_endline "-------------> FINE"; end else raise WrongProof @@ -1593,7 +1607,8 @@ let open_ () = let notebook = (rendering_window ())#notebook in try let uri = input_or_locate_uri ~title:"Open" in - CicTypeChecker.typecheck uri ; + ignore(CicTypeChecker.typecheck uri); + (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = match CicEnvironment.get_cooked_obj uri with Cic.Constant (_,Some bo,ty,_) -> [],bo,ty diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index d9b6219b2..ab8d4327a 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -58,11 +58,12 @@ let get_current_status_as_xml () = ;; let apply_tactic ~tactic = + let module PET = ProofEngineTypes in match get_proof (),!goal with | None,_ | _,None -> assert false | Some proof', Some goal' -> - let (newproof, newgoals) = tactic (proof', goal') in + let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in set_proof (Some newproof); goal := (match newgoals, newproof with diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index ee1b982c4..fccdc19c6 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -112,10 +112,12 @@ let test_uri uri = (* We do this to clear the alarm set by the signal handler *) ignore (Unix.alarm 0) ; `TimeOut + (* | exn -> prerr_endline (sprintf "Top Level Uncaught Exception: %s" (Printexc.to_string exn)); - `Nok + `Nok*) + | exn -> raise exn let report (ok,nok,maybe,timeout) = print_newline (); diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index d76fde47a..05e0a99a1 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -34,312 +34,508 @@ (* *) (******************************************************************************) -(* +open Printf - todo: - - in add_eq there is probably no need of add_gt, simple @ the gt lists - - the problem of duplicates in the 1steg gt/ge list if two of them are - add_eq may be "fixed" in some ways: - - lazy, do nothing on add_eq and eventually update the ge list - on closure - - add a check_duplicates_after_eq function called by add_eq - - do something like rmap, add a list of canonical that point to us - so when we collapse we have the list of the canonical we may update - - don't use failure but another exception - -*) +(******************************************************************************) +(** Types and default values **) +(******************************************************************************) -(* ************************************************************************** *) -(* TYPES *) -(* ************************************************************************** *) -type universe = int - -type canonical_repr = { - mutable ge:universe list; - mutable gt:universe list; - (* since we collapse we may need the reverse map *) - mutable eq:universe list; - (* the canonical representer *) - u:universe -} +type universe = int module UniverseType = struct type t = universe let compare = Pervasives.compare end -module MapUC = Map.Make(UniverseType) +module SOF = Set.Make(UniverseType) -(* ************************************************************************** *) -(* Globals *) -(* ************************************************************************** *) +type entry = { + eq_closure : SOF.t; + ge_closure : SOF.t; + gt_closure : SOF.t; + in_eq_of : SOF.t; + in_ge_of : SOF.t; + in_gt_of : SOF.t; + one_s_eq : SOF.t; + one_s_ge : SOF.t; + one_s_gt : SOF.t; +} -let map = ref MapUC.empty -let used = ref (-1) +module MAL = Map.Make(UniverseType) -(* ************************************************************************** *) -(* Helpers *) -(* ************************************************************************** *) +type arc_type = GE | GT | EQ -(* create a canonical for [u] *) -let mk_canonical u = - {u = u ; gt = [] ; ge = [] ; eq = [u] } +type arc = arc_type * universe * universe -(* give a new universe *) -let fresh () = - used := !used + 1; - map := MapUC.add !used (mk_canonical !used) !map; - !used - -let reset () = - map := MapUC.empty; - used := -1 +type bag = entry MAL.t * (arc list) + +let empty_entry = { + eq_closure=SOF.empty; + ge_closure=SOF.empty; + gt_closure=SOF.empty; + in_eq_of=SOF.empty; + in_ge_of=SOF.empty; + in_gt_of=SOF.empty; + one_s_eq=SOF.empty; + one_s_ge=SOF.empty; + one_s_gt=SOF.empty; +} + +let empty_bag = (MAL.empty, []) + +let env_bag = ref empty_bag + +(******************************************************************************) +(** Pretty printings **) +(******************************************************************************) + +let string_of_universe u = string_of_int u + +let string_of_arc_type u = + match u with + EQ -> "EQ" + | GT -> "GT" + | GE -> "EQ" + +let string_of_arc u = + let atype,a,b = u in + (string_of_arc_type atype) ^ " " ^ + (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; " +;; + +let string_of_universe_set l = + SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l "" + +let string_of_arc_list l = + List.fold_left (fun s x -> s ^ (string_of_arc x) ^ " ") "" l + +let string_of_node n = + "{"^ + "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^ + "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^ + "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^ + "i_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^ + "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^ + "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n" -(* ************************************************************************** *) -(* Pretty printing *) -(* ************************************************************************** *) -(* pp *) -let string_of_universe = string_of_int - -(* pp *) -let canonical_to_string c = - let s_gt = - List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.gt in - let s_ge = - List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.ge in - let s_eq = - List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.eq in - let s_u = (string_of_universe c.u) in - "{ u:" ^ s_u ^ " ; gt:" ^ s_gt ^ " ; ge:" ^ s_ge ^ " ; eq: " ^ s_eq ^ "}" - -(* print the content of map *) -let print_map () = - MapUC.iter (fun u c -> - prerr_endline - (" " ^ (string_of_universe u) ^ " -> " ^ (canonical_to_string c))) - !map; - prerr_endline "" - -(* ************************************************************************** *) -(* The way we fail *) -(* ************************************************************************** *) -(* we are doing bad *) -let error s = - (*prerr_endline " ======= Universe Inconsistency ========="; - print_map ();*) - prerr_endline (" " ^ s ^ "\n"); - failwith s - -(* ************************************************************************** *) -(* The real code *) -(* ************************************************************************** *) -(* <--------> *) - -(* the canonical representer of the [u] equaliti class *) -let repr u = +let string_of_mal m = + let rc = ref "" in + MAL.iter (fun k v -> rc := !rc ^ sprintf "%d --> %s" k (string_of_node v)) m; + !rc + +let string_of_bag b = + let (m,l) = b in + let s_m = string_of_mal m in + let s_l = string_of_arc_list l in + s_m ^"["^s_l^"]" + +(******************************************************************************) +(** Helpers **) +(******************************************************************************) + +(* + we need to merge the 2 graphs... here the code +*) +let repr u m = try - MapUC.find u !map + MAL.find u m with - Not_found -> error ("map inconsistency, unbound " ^ (string_of_universe u)) - -(* all the nodes we can ifer in the ge list of u *) -let close_ge u = - let repr_u = repr u in - let rec close_ge_aux tofollow bag = - match tofollow with - [] -> bag - | v::tl -> let repr_v = repr v in - if List.mem repr_v bag then (* avoid loops *) - (close_ge_aux tl bag ) - else - (close_ge_aux (tl @ repr_v.ge) (repr_v::bag)) - (* we assume that v==u -> v \notin (repr u).ge *) - in - close_ge_aux repr_u.ge [] + Not_found -> + try + let m',_ = !env_bag in + MAL.find u m' + with + Not_found -> empty_entry + +(* + FIXME: May be faster if we make it by hand +*) +let merge_closures f nodes m = + SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty -(* all the nodes we can ifer in the gt list of u, - we must follow bot gt and ge arcs, but we must put in bag only - the nodes that have a gt in theys path +(******************************************************************************) +(** Real stuff GT **) +(******************************************************************************) + +(* + todo is the SOF of nodes that needs to be recomputed, + m is the MAL map, s is the already touched nodes *) -let close_gt u = - let repr_u = repr u in - let rec close_gt_aux bag todo inspected = - (*print_all bag todo;Unix.sleep 1;*) - match todo with - [],[] -> bag - | [],p::may -> let repr_p = repr p in - if List.mem repr_p.u inspected then (* avoid loops *) - close_gt_aux bag ([],may) inspected - else - close_gt_aux bag (repr_p.gt,repr_p.ge @ may) - (repr_p.u::inspected) - | s::secure,may -> let repr_s = repr s in - if List.mem repr_s.u inspected then (* avoid loops *) - if List.mem repr_s bag then - close_gt_aux bag (secure,may) inspected - else - (* even if we ave already inspected the node, now - it is in the secure list so we want it in the bag - *) - close_gt_aux (repr_s::bag) (secure,may) inspected - else - close_gt_aux ((repr_s)::bag) - (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected) - in - close_gt_aux [] (repr_u.gt,repr_u.ge) [] - -(* when we add an eq we have to change the mapping of u to c*) -let remap u c = - let repr_u = repr u in - List.iter (fun u' -> if u <> u' then map := MapUC.remove u' !map) repr_u.eq; - List.iter (fun u' -> map := MapUC.add u' c !map) repr_u.eq - -(* we suspect that u and v are connected by a == implyed by two >= *) -let rec collapse u v = - let repr_u = repr u in - let repr_v = repr v in - let ge_v = close_ge v in - let ge_u = close_ge u in - if List.mem repr_u ge_v && List.mem repr_v ge_u then - add_eq u v - -(* we have to add u == v *) -and add_eq u v = - let repr_u = repr u in - let repr_v = repr v in - (* if we already have u == v then do nothing *) - if repr_u = repr_v then - () +let rec redo_gt_closure todo m s = + if SOF.is_empty todo then m else - (* if we already have v > u then fail *) - let gt_v = close_gt v in - if List.mem repr_u gt_v then - error ("Asking for " ^ (string_of_universe u) ^ " == " ^ - (string_of_universe v) ^ " but " ^ - (string_of_universe v) ^ " > " ^ (string_of_universe u)) - else - (* if we already have u > v then fail *) - let gt_u = close_gt u in - if List.mem repr_v gt_u then - error ("Asking for " ^ (string_of_universe u) ^ " == " ^ - (string_of_universe v) ^ " but " ^ - (string_of_universe u) ^ " > " ^ (string_of_universe v)) - else - (* add the inherited > constraints *) - List.iter (fun v -> add_gt u v ) (*gt_v*) repr_v.gt; - (* add the inherited >= constraints *) - (* close_ge assumes that v==u -> v \notin (repr u).ge *) - repr_u.ge <- List.filter (fun x -> x <> u && x <> v) - (repr_v.ge @ repr_u.ge); - (* mege the eq list, we assume they are disjuncted *) - repr_u.eq <- repr_u.eq @ repr_v.eq; - (* we have to remap all node represented by repr_v to repr_u *) - remap v repr_u; - (* FIXME: not sure this is what we have to do - think more to the list of suspected cicles - *) - List.iter (fun x -> collapse u x) repr_u.ge - -(* we have to add u >= v *) -and add_ge u v = - let repr_u = repr u in - let repr_v = repr v in - (* if we already have u == v then do nothing *) - if repr_u = repr_v then - () - else - (* if we already have v > u then fail *) - let gt = close_gt v in - if List.memq repr_u gt then - error ("Asking for " ^ (string_of_universe u) ^ " >= " ^ - (string_of_universe v) ^ " but " ^ - (string_of_universe v) ^ " > " ^ (string_of_universe u)) + begin + (* we choose the node to recompute *) + let u = SOF.choose todo in + if not (SOF.mem u s) then + let ru = repr u m in + let ru' = {ru with gt_closure = + (* the new gt closure is the gt-closures + ge-closures + eq-closures + of the one step gt-connected nodes *) + SOF.union ru.one_s_gt (merge_closures + (fun x -> SOF.union x.eq_closure + (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in + let m' = MAL.add u ru' m in + let s' = SOF.add u s in + redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s' else - (* it is now safe to add u >= v *) - repr_u.ge <- v::repr_u.ge; - (* but we may have introduced a cicle *) - collapse u v (* FIXME: not sure it is from u to v, think more. *) - -(* we have to add u > v *) -and add_gt u v = - let repr_u = repr u in - let repr_v = repr v in - (* if we already have u == v then fail *) - if repr_u = repr_v then - error ("Asking for " ^ (string_of_universe u) ^ " > " ^ - (string_of_universe v) ^ " but " ^ - (string_of_universe u) ^ " == " ^ (string_of_universe v)) - else - (* if we already have u > v do nothing *) - let gt_u = close_gt u in - if List.memq repr_v gt_u then - () + (* if already done go next. FIXME: think if it is right + maybe we should check if we changed something or not *) + redo_gt_closure (SOF.remove u todo) m s + end + +(* + calculates the closures of u and adjusts the in_*_of of v, then + starts redo_*_closure to adjust the colure of nodew thet have + (clusure u) in theyr closures +*) +let add_gt_arc u v m = + let ru = repr u m in + let rv = repr v m in + let ru' = { + (* new node: we add the v gt-closure and v to our gt-closure *) + eq_closure = ru.eq_closure; + ge_closure = ru.ge_closure; + gt_closure = SOF.add v + (SOF.union ru.gt_closure + (SOF.union rv.ge_closure + (SOF.union rv.eq_closure rv.gt_closure))); + in_eq_of = ru.in_eq_of; + in_ge_of = ru.in_ge_of; + in_gt_of = ru.in_gt_of; + one_s_eq = ru.one_s_eq; + one_s_ge = ru.one_s_ge; + one_s_gt = SOF.add v ru.one_s_gt; + } in + (* may add the sanity check *) + let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } in + let m' = MAL.add u ru' m in + let m'' = MAL.add v rv' m' in + redo_gt_closure ru'.in_gt_of m'' SOF.empty + +(* + given the 2 nodes plus the current bag, adds the arc, recomputes the + closures and returns the new map +*) +let add_gt u v b = + let m,l = b in + let m' = add_gt_arc u v m in + let l' = (GT,u,v)::l in + (m',l') + +(******************************************************************************) +(** Real stuff GE **) +(******************************************************************************) + +(* + todo is the SOF of nodes that needs to be recomputed, + m is the MAL map, s is the already touched nodes +*) +let rec redo_ge_closure todo m s = + if SOF.is_empty todo then m,s + else + begin + let u = SOF.choose todo in + if not (SOF.mem u s) then + begin + let ru = repr u m in + (* the ge-closure is recomputed as the ge-closures of + ge connected nodes plus theys eq-closure *) + let ru' = {ru with ge_closure = merge_closures + (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in + let m' = MAL.add u ru' m in + let s' = SOF.add u s in + redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s' + end else - (* if we already have v > u then fail *) - let gt = close_gt v in - if List.memq repr_u gt then - error ("Asking for " ^ (string_of_universe u) ^ " > " ^ - (string_of_universe v) ^ " but " ^ - (string_of_universe v) ^ " > " ^ (string_of_universe u)) + redo_ge_closure (SOF.remove u todo) m s + end + +(* + calculates the closures of u and adjusts the in_*_of of v, then + starts redo_*_closure to adjust the colure of nodew thet have + (clusure u) in theyr closures +*) +let add_ge_arc u v m = + let ru = repr u m in + let rv = repr v m in + let ru' = { + eq_closure = ru.eq_closure; + ge_closure = SOF.add v + (SOF.union ru.ge_closure + (SOF.union rv.eq_closure rv.ge_closure)); + gt_closure = ru.gt_closure; + in_eq_of = ru.in_eq_of; + in_ge_of = ru.in_ge_of; + in_gt_of = ru.in_gt_of; + one_s_eq = ru.one_s_eq; + one_s_ge = SOF.add v ru.one_s_ge; + one_s_gt = ru.one_s_gt; + } in + let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in + let m' = MAL.add u ru' m in + let m'' = MAL.add v rv' m' in + let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in + (* closing ge may provoke aome changes in gt-closures *) + redo_gt_closure (SOF.union ru'.in_gt_of + (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of)) + td SOF.empty )) m''' SOF.empty + +(* + given the 2 nodes plus the current bag, adds the arc, recomputes the + closures and returns the new map +*) +let add_ge u v b = + let m,l = b in + let m' = add_ge_arc u v m in + let l' = (GE,u,v)::l in + (m',l') + +(******************************************************************************) +(** Real stuff EQ **) +(******************************************************************************) + +let rec redo_eq_closure todo m s = + if SOF.is_empty todo then m,s + else begin + let u = SOF.choose todo in + if not (SOF.mem u s) then + begin + let ru = repr u m in + let eq_closure = merge_closures + (fun x -> x.eq_closure) ru.one_s_eq m in + let ru' = {ru with eq_closure = eq_closure + ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in + let m' = MAL.add u ru' m in + let s' = SOF.add u s in + redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s' + end + else + redo_eq_closure (SOF.remove u todo) m s + end + +(* + calculates the closures of u and adjusts the in_*_of of v, then + starts redo_*_closure to adjust the colure of nodew thet have + (clusure u) in theyr closures +*) +let add_eq_arc u v m = + let ru = repr u m in + let rv = repr v m in + (* since eq is symmetric we have to chage more *) + let eq_closure = SOF.add u (SOF.add v + (SOF.union ru.eq_closure rv.eq_closure)) in + let ru' = { + eq_closure = eq_closure; + ge_closure = SOF.union ru.ge_closure rv.ge_closure; + gt_closure = SOF.union ru.gt_closure rv.gt_closure; + in_eq_of = eq_closure; + in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of; + in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of; + one_s_eq = eq_closure; + one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge; + one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt; + } in + (* this is a collapse *) + let rv' = ru' in + let m' = MAL.add u ru' m in + let m'' = MAL.add v rv' m' in + let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in + (* redoing a eq may change some ge and some gt *) + let m'''',td' = redo_ge_closure + (SOF.union ru'.in_ge_of + (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of)) + td SOF.empty)) m''' SOF.empty in + redo_gt_closure (SOF.union ru'.in_gt_of + (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of)) + td' SOF.empty)) m'''' SOF.empty + +(* + given the 2 nodes plus the current bag, adds the arc, recomputes the + closures and returns the new map +*) +let add_eq u v b = + let m,l = b in + let m' = add_eq_arc u v m in + let l' = (EQ,u,v)::l in + (m',l') + +(******************************************************************************) +(** Oyther real code **) +(******************************************************************************) + +exception UniverseInconsistency of string + +let error arc node1 closure_type node2 closure = + let s = " ===== Universe Inconsistency detected =====\n\n" ^ + "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^ + (string_of_universe node1) ^ " is in the " ^ + (string_of_arc_type closure_type) ^ " closure {" ^ + (string_of_universe_set closure) ^ "} of " ^ + (string_of_universe node2) ^ "\n\n" ^ + " ===== Universe Inconsistency detected =====\n" in + prerr_endline s; + raise (UniverseInconsistency s) + +(* + we merge the env_bag with b +*) +let qed b = + let m,l = b in + let m',l' = !env_bag in + let m'' = ref m' in + MAL.iter (fun k v -> m'':= MAL.add k v !m'') m; + let l'' = l @ l' in + env_bag := (!m'',l'') + +let add_eq u v b = + (* should we check to no add twice the same?? *) + let m,_ = b in + let ru = repr u m in + if SOF.mem v ru.gt_closure then + error (EQ,u,v) v GT u ru.gt_closure + else + begin + let rv = repr v m in + if SOF.mem u rv.gt_closure then + error (EQ,u,v) u GT v rv.gt_closure + else + add_eq u v b + end + +let add_ge u v b = + (* should we check to no add twice the same?? *) + let m,_ = b in + let rv = repr v m in + if SOF.mem u rv.gt_closure then + error (GE,u,v) u GT v rv.gt_closure + else + add_ge u v b + +let add_gt u v b = + (* should we check to no add twice the same?? *) + let m,_ = b in + let rv = repr v m in + if SOF.mem u rv.gt_closure then + error (GT,u,v) u GT v rv.gt_closure + else + begin + if SOF.mem u rv.ge_closure then + error (GT,u,v) u GE v rv.ge_closure else - (* if we already have v >= u then fail *) - let ge = close_ge v in - if List.memq repr_u ge then - error ("Asking for " ^ (string_of_universe u) ^ " > " ^ - (string_of_universe v) ^ " but " ^ - (string_of_universe v) ^ " >= " ^ (string_of_universe u)) - else - (* it is safe to add u > v *) - repr_u.gt <- v::repr_u.gt + begin + if SOF.mem u rv.eq_closure then + error (GT,u,v) u EQ v rv.eq_closure + else + add_gt u v b + end + end + + + +(******************************************************************************) +(** World interface **) +(******************************************************************************) + +type universe_graph = bag + +let work_bag = ref empty_bag +let current_index = ref (-1) + +let get_working () = !work_bag +let get_global () = !env_bag +let set_working b = work_bag := b + +let fresh () = + current_index := !current_index + 1; + !current_index + +let qed () = + qed !work_bag + +let print_global_graph () = + let s = string_of_bag !env_bag in + prerr_endline s + +let print_working_graph () = + let s = string_of_bag !work_bag in + prerr_endline s + +type history_ticket = int + +let get_history_ticket b = + let m,l = b in + List.length l + +let redo_history t b b'= + let rec get_history l n = + if n == 0 then + [] + else + begin + match l with + [] -> failwith "erroer, lista piu' corta della history" + | h::tl -> h::(get_history tl (n - 1)) + end + in + let rec redo_commands l b = + match l with + [] -> b + | (GE,u,v)::tl -> redo_commands tl (add_ge u v b) + | (GT,u,v)::tl -> redo_commands tl (add_gt u v b) + | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b) + in + let (m,l) = b in + let todo = List.rev (get_history l ((List.length l) - t)) in + try + redo_commands todo b' + with + UniverseInconsistency s -> failwith s + (*| _ -> failwith "Unexpected exception"*) let add_gt u v = try - add_gt u v; true + work_bag := add_gt u v !work_bag; true with - exn -> false + UniverseInconsistency s -> false + (*| _ -> failwith "Unexpected exception"*) -let add_ge u v = +let add_ge u v = try - add_ge u v; true + work_bag := add_ge u v !work_bag;true with - exn -> false + UniverseInconsistency s -> false + (*| _ -> failwith "Unexpected exception"*) let add_eq u v = try - add_eq u v; true + work_bag := add_eq u v !work_bag;true with - exn -> false - -(* <--------> *) + UniverseInconsistency s -> false + (*| _ -> failwith "Unexpected exception"*) -(* ************************************************************************** *) -(* To make tests *) -(* ************************************************************************** *) +let saved_data = ref (empty_bag,0) -(* -let check_status_eq l = - let s = List.fold_left (fun s u -> s^(string_of_universe u) ^ ";") "" l in - let repr_u = repr (List.hd l) in - let rec check_status_eq_aux c = - match c with - [] -> print_endline (" Result check_status_eq["^s^"] = OK");true - | u::tl -> if repr u != repr_u then - (print_endline (" Result check_status_eq["^s^"] = FAILED"); - print_endline ((string_of_universe u) ^ " != " ^ - (string_of_universe repr_u.u)); - print_map ();false) - else - check_status_eq_aux tl - in - check_status_eq_aux (List.tl l) -*) +let directly_to_env_begin () = + saved_data := (!work_bag, get_history_ticket !env_bag); + work_bag := empty_bag + +let directly_to_env_end () = + qed (); + let (b,t) = !saved_data in + work_bag := redo_history t !env_bag b + +let reset_working () = work_bag := empty_bag -(* ************************************************************************** *) -(* Fake implementation *) -(* ************************************************************************** *) +(******************************************************************************) +(** Fake implementatoin **) +(******************************************************************************) -(* <--------> * -let add_ge u v = true -let add_gt u v = true -let add_eq u v = true -* <--------> *) +let reset_working = function _ -> () +let directly_to_env_end = function _ -> () +let directly_to_env_begin = function _ -> () +let add_eq = fun _ _ -> true +let add_ge = fun _ _ -> true +let add_gt = fun _ _ -> true +let get_working = function a -> empty_bag +let set_working = function a -> () diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index d7eb7dc41..f98ea84c6 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -23,17 +23,27 @@ * http://helm.cs.unibo.it/ *) +(* Cic.Type of universe *) type universe + +(* returns a fresh universe and puts it in the working graph *) val fresh: unit -> universe + +(* add eq/ge/gt constraints to the woring graph *) val add_eq: universe -> universe -> bool val add_ge: universe -> universe -> bool val add_gt: universe -> universe -> bool -(* -val string_of_universe: universe -> string -val print_map: unit -> unit -*) +(* prints the graphs *) +val print_global_graph: unit -> unit +val print_working_graph: unit -> unit + +type universe_graph +val get_working: unit -> universe_graph +val set_working: universe_graph -> unit + +val directly_to_env_begin: unit -> unit +val directly_to_env_end: unit -> unit -val reset: unit -> unit +val reset_working: unit -> unit -(* val check_status_eq: universe list -> bool *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index f7cfce144..637636e0b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -204,48 +204,56 @@ let interpretate ~context ~env ast = subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in - (match cic with - | Cic.Const (uri, []) -> - let uris = - match CicEnvironment.get_obj uri with - | Cic.Constant (_, _, _, uris) -> uris - | _ -> assert false - in - Cic.Const (uri, mk_subst uris) - | Cic.Var (uri, []) -> - let uris = - match CicEnvironment.get_obj uri with - | Cic.Variable (_, _, _, uris) -> uris - | _ -> assert false - in - Cic.Var (uri, mk_subst uris) - | Cic.MutInd (uri, i, []) -> - let uris = - match CicEnvironment.get_obj uri with - | Cic.InductiveDefinition (_, uris, _) -> uris - | _ -> assert false - in - Cic.MutInd (uri, i, mk_subst uris) - | Cic.MutConstruct (uri, i, j, []) -> - let uris = - match CicEnvironment.get_obj uri with - | Cic.InductiveDefinition (_, uris, _) -> uris - | _ -> assert false - in - Cic.MutConstruct (uri, i, j, mk_subst uris) - | Cic.Meta _ | Cic.Implicit _ as t -> + (try + match cic with + | Cic.Const (uri, []) -> + let uris = + (*match CicEnvironment.get_obj uri with*) + match CicTypeChecker.typecheck uri with + | Cic.Constant (_, _, _, uris) -> uris + | _ -> assert false + in + Cic.Const (uri, mk_subst uris) + | Cic.Var (uri, []) -> + let uris = + (*match CicEnvironment.get_obj uri with*) + match CicTypeChecker.typecheck uri with + | Cic.Variable (_, _, _, uris) -> uris + | _ -> assert false + in + Cic.Var (uri, mk_subst uris) + | Cic.MutInd (uri, i, []) -> + let uris = + (*match CicEnvironment.get_obj uri with*) + match CicTypeChecker.typecheck uri with + | Cic.InductiveDefinition (_, uris, _) -> uris + | _ -> assert false + in + Cic.MutInd (uri, i, mk_subst uris) + | Cic.MutConstruct (uri, i, j, []) -> + let uris = + (*match CicEnvironment.get_obj uri with*) + match CicTypeChecker.typecheck uri with + | Cic.InductiveDefinition (_, uris, _) -> uris + | _ -> assert false + in + Cic.MutConstruct (uri, i, j, mk_subst uris) + | Cic.Meta _ | Cic.Implicit _ as t -> (* - prerr_endline (sprintf - "Warning: %s must be instantiated with _[%s] but we do not enforce it" - (CicPp.ppterm t) - (String.concat "; " - (List.map - (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term) - subst))); + prerr_endline (sprintf + "Warning: %s must be instantiated with _[%s] but we do not enforce it" + (CicPp.ppterm t) + (String.concat "; " + (List.map + (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term) + subst))); *) - t - | _ -> - raise DisambiguateChoices.Invalid_choice)) + t + | _ -> + raise DisambiguateChoices.Invalid_choice + with + CicEnvironment.CircularDependency _ -> + raise DisambiguateChoices.Invalid_choice)) | CicAst.Implicit -> Cic.Implicit None | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> @@ -464,7 +472,7 @@ module Make (C: Callbacks) = in (* (3) test an interpretation filling with meta uninterpreted identifiers *) - let test_env current_env todo_dom = + let test_env current_env todo_dom univ = let filled_env = List.fold_left (fun env item -> @@ -476,55 +484,64 @@ module Make (C: Callbacks) = current_env todo_dom in try + CicUniv.set_working univ; let cic_term = interpretate ~context:disambiguate_context ~env:filled_env term in - refine metasenv context cic_term + let k = refine metasenv context cic_term in + let new_univ = CicUniv.get_working () in + (k , new_univ ) with - | Try_again -> Uncertain - | DisambiguateChoices.Invalid_choice -> Ko + | Try_again -> Uncertain,univ + | DisambiguateChoices.Invalid_choice -> Ko,univ in (* (4) build all possible interpretations *) - let rec aux current_env todo_dom = + let rec aux current_env todo_dom base_univ = match todo_dom with | [] -> - (match test_env current_env [] with - | Ok (term, metasenv) -> [ current_env, metasenv, term ] - | Ko | Uncertain -> []) + (match test_env current_env [] base_univ with + | Ok (term, metasenv),new_univ -> + [ current_env, metasenv, term, new_univ ] + | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item)); + (string_of_domain_item item)); let choices = lookup_choices item in - let rec filter = function + let rec filter univ = function | [] -> [] | codomain_item :: tl -> debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ; let new_env = Environment.add item codomain_item current_env in - (match test_env new_env remaining_dom with - | Ok (term, metasenv) -> + (match test_env new_env remaining_dom univ with + | Ok (term, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, metasenv, term ] - | _ -> aux new_env remaining_dom) @ filter tl - | Uncertain -> + | [] -> [ new_env, metasenv, term, new_univ ] + | _ -> aux new_env remaining_dom new_univ )@ + filter univ tl + | Uncertain,new_univ -> (match remaining_dom with | [] -> [] - | _ -> aux new_env remaining_dom) @ filter tl - | Ko -> filter tl) + | _ -> aux new_env remaining_dom new_univ )@ + filter univ tl + | Ko,_ -> filter univ tl) in - filter choices + filter base_univ choices in - match aux current_env todo_dom with + let base_univ = CicUniv.get_working () in + try + match aux current_env todo_dom base_univ with | [] -> raise NoWellTypedInterpretation - | [ _ ] as l -> + | [ e,me,t,u ] as l -> debug_print "UNA SOLA SCELTA"; - l + CicUniv.set_working u; + [ e,me,t ] | l -> debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); let choices = List.map - (fun (env, _, _) -> + (fun (env, _, _, _) -> List.map (fun domain_item -> let description = @@ -535,7 +552,17 @@ module Make (C: Callbacks) = l in let choosed = C.interactive_interpretation_choice choices in - List.map (List.nth l) choosed - + let l' = List.map (List.nth l) choosed in + match l' with + [] -> assert false + | [e,me,t,u] -> + CicUniv.set_working u; + (*CicUniv.print_working_graph ();*) + [e,me,t] + | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *) + List.map (fun (e,me,t,u) -> (e,me,t)) l' + with + CicEnvironment.CircularDependency s -> + raise (Failure "e chi la becca sta CircularDependency?"); end diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 8014a1940..e15186fde 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -38,6 +38,7 @@ let cleanup_tmp = true;; let trust_obj = function uri -> true;; +(*let trust_obj = function uri -> false;;*) type type_checked_obj = CheckedObj of Cic.obj (* cooked obj *) @@ -317,7 +318,9 @@ let find_or_add_unchecked_to_cache uri = (* The body does not exist ==> we consider it an axiom *) None in + CicUniv.directly_to_env_begin (); let obj = CicParser.obj_of_xml filename bodyfilename in + CicUniv.directly_to_env_end (); if cleanup_tmp then begin Unix.unlink filename ; @@ -405,3 +408,11 @@ let in_cache uri = ignore (Cache.find_cooked uri);true with Not_found -> false ;; + +let add_type_checked_term uri obj = + match obj with + Cic.Constant (s,(Some bo),ty,ul) -> + Cache.add_cooked ~key:uri obj + | _ -> assert false + Cache.add_cooked +;; diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 615cdf9be..e3def568e 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -61,6 +61,9 @@ val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj (* again in the future (is_type_checked will return true) *) val set_type_checking_info : UriManager.uri -> unit +(* We need this in the Qed. *) +val add_type_checked_term : UriManager.uri -> Cic.obj -> unit + (* get_cooked_obj ~trust uri *) (* returns the object if it is already type-checked or if it can be *) (* trusted (if [trust] = true and the trusting function accepts it) *) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 36bfb28b1..140e41712 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -127,6 +127,7 @@ let rec type_of_constant uri = CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> CicLogger.log (`Start_type_checking uri) ; + CicUniv.directly_to_env_begin (); (* let's typecheck the uncooked obj *) (match uobj with C.Constant (_,Some te,ty,_) -> @@ -160,6 +161,7 @@ let rec type_of_constant uri = ("Unknown constant:" ^ U.string_of_uri uri)) ); CicEnvironment.set_type_checking_info uri ; + CicUniv.directly_to_env_end (); CicLogger.log (`Type_checking_completed uri) ; match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj @@ -180,6 +182,7 @@ and type_of_variable uri = CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> CicLogger.log (`Start_type_checking uri) ; + CicUniv.directly_to_env_begin (); (* only to check that ty is well-typed *) let _ = type_of ty in (match bo with @@ -190,6 +193,7 @@ and type_of_variable uri = ("Unknown variable:" ^ U.string_of_uri uri)) ) ; CicEnvironment.set_type_checking_info uri ; + CicUniv.directly_to_env_end (); CicLogger.log (`Type_checking_completed uri) ; ty | _ -> @@ -518,8 +522,10 @@ and type_of_mutual_inductive_defs uri i = CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> CicLogger.log (`Start_type_checking uri) ; + CicUniv.directly_to_env_begin (); check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; + CicUniv.directly_to_env_end (); CicLogger.log (`Type_checking_completed uri) ; (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj @@ -543,8 +549,10 @@ and type_of_mutual_inductive_constr uri i j = CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> CicLogger.log (`Start_type_checking uri) ; + (*CicUniv.directly_to_env_begin ();*) check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; + (*CicUniv.directly_to_env_end ();*) CicLogger.log (`Type_checking_completed uri) ; (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj @@ -799,7 +807,7 @@ and guarded_by_destructors context n nn kl x safes = | Some (_,C.Def (bo,_)) -> guarded_by_destructors context m nn kl x safes (CicSubstitution.lift m bo) - | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") + | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") ) | C.Meta _ | C.Sort _ @@ -1236,9 +1244,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop | C.Sort C.Set -> true - | C.Sort C.CProp -> true + | C.Sort C.CProp -> true | C.Sort (C.Type _) -> - (* TASSI: da verificare *) + (* TASSI: da verificare *) (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> let (_,_,_,cl) = List.nth itl i in @@ -1345,7 +1353,7 @@ and type_of_aux' metasenv context t = | Some (_,C.Def (bo,None)) -> debug_print "##### CASO DA INVESTIGARE E CAPIRE" ; type_of_aux context (S.lift n bo) - | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") + | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") with _ -> raise (TypeCheckerFailure "unbound variable") @@ -1366,8 +1374,8 @@ and type_of_aux' metasenv context t = | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in if not (CicUniv.add_gt t' t ) then - assert false (* t' is fresh! an error in CicUniv *) - else + assert false (* t' is fresh! an error in CicUniv *) + else C.Sort (C.Type t') (* TASSI: CONSTRAINTS *) | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ())) @@ -1587,7 +1595,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ List.rev (List.map (fun (n,ty,_) -> - let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl) + let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl) in let len = List.length types in List.iter @@ -1660,7 +1668,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ match (t1', t2') with (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> - (* different from Coq manual!!! *) + (* different from Coq manual!!! *) C.Sort s2 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) @@ -1670,7 +1678,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ C.Sort (C.Type t') | (C.Sort _,C.Sort (C.Type t1)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) - C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *) + C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *) | (C.Meta _, C.Sort _) -> t2' | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> @@ -1771,15 +1779,18 @@ in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res *) ;; +(* tassi FIXME: not sure where is this called... no history here... *) let typecheck uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.is_type_checked ~trust:false uri with - CicEnvironment.CheckedObj _ -> () + (*match CicEnvironment.is_type_checked ~trust:false uri with*) + match CicEnvironment.is_type_checked ~trust:true uri with + CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) CicLogger.log (`Start_type_checking uri) ; + CicUniv.directly_to_env_begin (); (match uobj with C.Constant (_,Some te,ty,_) -> let _ = type_of ty in @@ -1819,5 +1830,7 @@ let typecheck uri = check_mutual_inductive_defs uri uobj ) ; CicEnvironment.set_type_checking_info uri ; - CicLogger.log (`Type_checking_completed uri) + CicUniv.directly_to_env_end (); + CicLogger.log (`Type_checking_completed uri); + uobj ;; diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 95ee658c7..3973c16c1 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -27,7 +27,7 @@ exception TypeCheckerFailure of string exception AssertFailure of string -val typecheck : UriManager.uri -> unit +val typecheck : UriManager.uri -> Cic.obj (* FUNCTIONS USED ONLY IN THE TOPLEVEL *) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index b3525d318..e8ea0769d 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -162,8 +162,8 @@ and type_of_aux' metasenv context t = in CicSubstitution.lift_meta l ty, subst', metasenv' (* TASSI: CONSTRAINT *) - | C.Sort (C.Type t) -> - let t' = CicUniv.fresh() in + | C.Sort (C.Type t) -> + let t' = CicUniv.fresh() in if not (CicUniv.add_gt t' t ) then assert false (* t' is fresh! an error in CicUniv *) else @@ -487,7 +487,7 @@ and type_of_aux' metasenv context t = C.Sort s2,subst,metasenv | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) - let t' = CicUniv.fresh() in + let t' = CicUniv.fresh() in if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then assert false ; (* not possible, error in CicUniv *) C.Sort (C.Type t'),subst,metasenv diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index 295c638b9..9b4237811 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -14,10 +14,10 @@ http_getter_env.cmo: http_getter_const.cmi http_getter_logger.cmi \ http_getter_misc.cmi http_getter_types.cmo http_getter_env.cmi http_getter_env.cmx: http_getter_const.cmx http_getter_logger.cmx \ http_getter_misc.cmx http_getter_types.cmx http_getter_env.cmi -http_getter_common.cmo: http_getter_env.cmi http_getter_misc.cmi \ - http_getter_types.cmo http_getter_common.cmi -http_getter_common.cmx: http_getter_env.cmx http_getter_misc.cmx \ - http_getter_types.cmx http_getter_common.cmi +http_getter_common.cmo: http_getter_env.cmi http_getter_logger.cmi \ + http_getter_misc.cmi http_getter_types.cmo http_getter_common.cmi +http_getter_common.cmx: http_getter_env.cmx http_getter_logger.cmx \ + http_getter_misc.cmx http_getter_types.cmx http_getter_common.cmi http_getter_map.cmo: http_getter_map.cmi http_getter_map.cmx: http_getter_map.cmi http_getter_cache.cmo: http_getter_common.cmi http_getter_env.cmi \ diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 3a60f60ac..242671197 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -1,19 +1,23 @@ filter_auto.cmi: newConstraints.cmi -proofEngineHelpers.cmi: proofEngineTypes.cmo -tacticals.cmi: proofEngineTypes.cmo -reductionTactics.cmi: proofEngineTypes.cmo -proofEngineStructuralRules.cmi: proofEngineTypes.cmo -primitiveTactics.cmi: proofEngineTypes.cmo -tacticChaser.cmi: proofEngineTypes.cmo -variousTactics.cmi: proofEngineTypes.cmo -introductionTactics.cmi: proofEngineTypes.cmo -eliminationTactics.cmi: proofEngineTypes.cmo -negationTactics.cmi: proofEngineTypes.cmo -equalityTactics.cmi: proofEngineTypes.cmo -discriminationTactics.cmi: proofEngineTypes.cmo -ring.cmi: proofEngineTypes.cmo -fourierR.cmi: proofEngineTypes.cmo -statefulProofEngine.cmi: proofEngineTypes.cmo +proofEngineHelpers.cmi: proofEngineTypes.cmi +tacticals.cmi: proofEngineTypes.cmi +reductionTactics.cmi: proofEngineTypes.cmi +proofEngineStructuralRules.cmi: proofEngineTypes.cmi +primitiveTactics.cmi: proofEngineTypes.cmi +tacticChaser.cmi: proofEngineTypes.cmi +variousTactics.cmi: proofEngineTypes.cmi +introductionTactics.cmi: proofEngineTypes.cmi +eliminationTactics.cmi: proofEngineTypes.cmi +negationTactics.cmi: proofEngineTypes.cmi +equalityTactics.cmi: proofEngineTypes.cmi +discriminationTactics.cmi: proofEngineTypes.cmi +ring.cmi: proofEngineTypes.cmi +fourierR.cmi: proofEngineTypes.cmi +statefulProofEngine.cmi: proofEngineTypes.cmi +proofEngineTypes.cmo: proofEngineTypes.cmi +proofEngineTypes.cmx: proofEngineTypes.cmi +proofEngineTypes.cmo: proofEngineTypes.cmi +proofEngineTypes.cmx: proofEngineTypes.cmi newConstraints.cmo: newConstraints.cmi newConstraints.cmx: newConstraints.cmi match_concl.cmo: newConstraints.cmi match_concl.cmi @@ -24,60 +28,58 @@ proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi proofEngineHelpers.cmx: proofEngineHelpers.cmi -newConstraints.cmo: newConstraints.cmi -newConstraints.cmx: newConstraints.cmi -match_concl.cmo: newConstraints.cmi match_concl.cmi -match_concl.cmx: newConstraints.cmx match_concl.cmi -tacticals.cmo: proofEngineTypes.cmo tacticals.cmi +tacticals.cmo: proofEngineTypes.cmi tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi -reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi -reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi -proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ +reductionTactics.cmo: proofEngineReduction.cmi proofEngineTypes.cmi \ + reductionTactics.cmi +reductionTactics.cmx: proofEngineReduction.cmx proofEngineTypes.cmx \ + reductionTactics.cmi +proofEngineStructuralRules.cmo: proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ proofEngineStructuralRules.cmi primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \ + proofEngineTypes.cmi reductionTactics.cmi tacticals.cmi \ primitiveTactics.cmi primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \ - primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi + primitiveTactics.cmi proofEngineTypes.cmi tacticChaser.cmi tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \ primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmo tacticChaser.cmi tacticals.cmi variousTactics.cmi + proofEngineTypes.cmi tacticChaser.cmi tacticals.cmi variousTactics.cmi variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx tacticChaser.cmx tacticals.cmx variousTactics.cmi -introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \ +introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmi \ introductionTactics.cmi introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ introductionTactics.cmi eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ - tacticals.cmi eliminationTactics.cmi + proofEngineTypes.cmi tacticals.cmi eliminationTactics.cmi eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ - tacticals.cmx eliminationTactics.cmi + proofEngineTypes.cmx tacticals.cmx eliminationTactics.cmi negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \ - proofEngineTypes.cmo tacticals.cmi variousTactics.cmi negationTactics.cmi + proofEngineTypes.cmi tacticals.cmi variousTactics.cmi negationTactics.cmi negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \ proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \ proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \ + proofEngineStructuralRules.cmi proofEngineTypes.cmi reductionTactics.cmi \ tacticals.cmi equalityTactics.cmi equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \ proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \ tacticals.cmx equalityTactics.cmi discriminationTactics.cmo: eliminationTactics.cmi equalityTactics.cmi \ - introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmo \ + introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmi \ tacticals.cmi discriminationTactics.cmi discriminationTactics.cmx: eliminationTactics.cmx equalityTactics.cmx \ introductionTactics.cmx primitiveTactics.cmx proofEngineTypes.cmx \ tacticals.cmx discriminationTactics.cmi ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmo tacticals.cmi \ + proofEngineStructuralRules.cmi proofEngineTypes.cmi tacticals.cmi \ ring.cmi ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \ @@ -85,10 +87,10 @@ ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ fourier.cmo: fourier.cmi fourier.cmx: fourier.cmi fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ - proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \ + proofEngineHelpers.cmi proofEngineTypes.cmi reductionTactics.cmi ring.cmi \ tacticals.cmi fourierR.cmi fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ tacticals.cmx fourierR.cmi -statefulProofEngine.cmo: proofEngineTypes.cmo statefulProofEngine.cmi +statefulProofEngine.cmo: proofEngineTypes.cmi statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx statefulProofEngine.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 0cf06c578..c837f2df8 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -4,7 +4,7 @@ REQUIRES = \ helm-cic_unification helm-mathql_interpreter helm-mathql_generator INTERFACE_FILES = \ - newConstraints.mli match_concl.mli filter_auto.mli\ + proofEngineTypes.mli newConstraints.mli match_concl.mli filter_auto.mli\ proofEngineReduction.mli proofEngineHelpers.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli tacticChaser.mli variousTactics.mli \ diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index dd2e68d09..ceaccdcef 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -25,7 +25,8 @@ open HelmLibraryObjects -let rec injection_tac ~term status = +let rec injection_tac ~term = + let injection_tac ~term status = let (proof, goal) = status in let module C = Cic in let module U = UriManager in @@ -34,6 +35,7 @@ let rec injection_tac ~term status = let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in + ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) when (U.eq equri Logic.eq_URI) -> ( @@ -43,7 +45,8 @@ let rec injection_tac ~term status = match t1,t2 with ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) - when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> + when (uri1 = uri2) && (typeno1 = typeno2) && + (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)), (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) @@ -73,126 +76,132 @@ let rec injection_tac ~term status = ) | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation") ) status + in + ProofEngineTypes.mk_tactic (injection_tac ~term) - -and injection1_tac ~term ~i status = -let (proof, goal) = status in -(* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *) - let module C = Cic in - let module S = CicSubstitution in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let termty = (CicTypeChecker.type_of_aux' metasenv context term) in - match termty with (* an equality *) - (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( - match tty with (* some inductive type *) - (C.MutInd (turi,typeno,exp_named_subst)) - | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> -prerr_endline ("XXXX term " ^ CicPp.ppterm term) ; -prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ; -prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; -prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; -prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; - let t1',t2',consno = (* sono i due sottotermini che differiscono *) - match t1,t2 with - ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)), - (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) - when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *) - (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2 - | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai") - in - let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in -prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ; -prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ; -prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; -prerr_endline ("XXXX consno " ^ string_of_int consno) ; - let pattern = - match (CicEnvironment.get_obj turi) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx) -> - let _,_,_,constructor_list = (List.nth ind_type_list typeno) in - let i_constr_id,_ = List.nth constructor_list (consno - 1) in - List.map - (function (id,cty) -> - let reduced_cty = CicReduction.whd context cty in - let rec aux t k = - match t with - C.Prod (_,_,target) when (k <= nr_ind_params_dx) -> - aux target (k+1) - | C.Prod (binder,source,target) when (k > nr_ind_params_dx) -> - let binder' = - match binder with - C.Name b -> C.Name b - | C.Anonymous -> C.Name "y" - in - C.Lambda (binder',source,(aux target (k+1))) - | _ -> - let nr_param_constr = k - 1 - nr_ind_params_dx in - if (id = i_constr_id) - then C.Rel (nr_param_constr - i + 1) - else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *) - in aux reduced_cty 1 - ) - constructor_list - | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible") +and injection1_tac ~term ~i = + let injection1_tac ~term ~i status = + let (proof, goal) = status in + (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *) + let module C = Cic in + let module S = CicSubstitution in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let termty = (CicTypeChecker.type_of_aux' metasenv context term) in + match termty with (* an equality *) + (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) + when (U.eq equri Logic.eq_URI) -> ( + match tty with (* some inductive type *) + (C.MutInd (turi,typeno,exp_named_subst)) + | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> + prerr_endline ("XXXX term " ^ CicPp.ppterm term) ; + prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ; + prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; + prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; + prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; + let t1',t2',consno = (* sono i due sottotermini che differiscono *) + match t1,t2 with + ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)), + (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) + when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *) + (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2 + | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai") in -prerr_endline ("XXXX cominciamo!") ; - T.thens - ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) - ~continuations:[ - T.then_ - ~start:(injection_tac ~term:(C.Rel 1)) - ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) - ; - T.then_ - ~start: - (fun status -> - let (proof, goal) = status in - let _,metasenv,_,_ = proof in - let _,context,gty = CicUtil.lookup_meta goal metasenv in -prerr_endline ("XXXX goal " ^ string_of_int goal) ; -prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ; -prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ; -prerr_endline ("XXXX change " ^ CicPp.ppterm (C.Appl [ C.Lambda (C.Name "x", tty, C.MutCase (turi, typeno, (C.Lambda ((C.Name "x"),(S.lift 1 tty),(S.lift 2 tty'))), (C.Rel 1), pattern)); t1])) ; - let new_t1' = - match gty with - (C.Appl (C.MutInd (_,_,_)::arglist)) -> - List.nth arglist 1 - | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") - in -prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; - P.change_tac - ~what:new_t1' - ~with_what: - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ( - (C.Name "x"), - (S.lift 1 tty), - (S.lift 2 tty'))), - (C.Rel 1), pattern - ) - ); - t1] - ) - status - ) - ~continuation: - (T.then_ - ~start:(EqualityTactics.rewrite_simpl_tac ~term) - ~continuation:EqualityTactics.reflexivity_tac - ) - ] - status - | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") - ) - | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality") + let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in + prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ; + prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ; + prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; + prerr_endline ("XXXX consno " ^ string_of_int consno) ; + let pattern = + match (CicEnvironment.get_obj turi) with + C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx) -> + let _,_,_,constructor_list = (List.nth ind_type_list typeno) in + let i_constr_id,_ = List.nth constructor_list (consno - 1) in + List.map + (function (id,cty) -> + let reduced_cty = CicReduction.whd context cty in + let rec aux t k = + match t with + C.Prod (_,_,target) when (k <= nr_ind_params_dx) -> + aux target (k+1) + | C.Prod (binder,source,target) when (k > nr_ind_params_dx) -> + let binder' = + match binder with + C.Name b -> C.Name b + | C.Anonymous -> C.Name "y" + in + C.Lambda (binder',source,(aux target (k+1))) + | _ -> + let nr_param_constr = k - 1 - nr_ind_params_dx in + if (id = i_constr_id) + then C.Rel (nr_param_constr - i + 1) + else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *) + in aux reduced_cty 1 + ) + constructor_list + | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible") + in + prerr_endline ("XXXX cominciamo!") ; + ProofEngineTypes.apply_tactic + (T.thens + ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) + ~continuations:[ + T.then_ + ~start:(injection_tac ~term:(C.Rel 1)) + ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) + ; + T.then_ + ~start:(ProofEngineTypes.mk_tactic + (fun status -> + let (proof, goal) = status in + let _,metasenv,_,_ = proof in + let _,context,gty = CicUtil.lookup_meta goal metasenv in + prerr_endline ("XXXX goal " ^ string_of_int goal) ; + prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ; + prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ; + prerr_endline ("XXXX change " ^ CicPp.ppterm (C.Appl [ C.Lambda (C.Name "x", tty, C.MutCase (turi, typeno, (C.Lambda ((C.Name "x"),(S.lift 1 tty),(S.lift 2 tty'))), (C.Rel 1), pattern)); t1])) ; + let new_t1' = + match gty with + (C.Appl (C.MutInd (_,_,_)::arglist)) -> + List.nth arglist 1 + | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") + in + prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; + ProofEngineTypes.apply_tactic + (P.change_tac + ~what:new_t1' + ~with_what: + (C.Appl [ + C.Lambda ( + C.Name "x", tty, + C.MutCase ( + turi, typeno, + (C.Lambda ( + (C.Name "x"), + (S.lift 1 tty), + (S.lift 2 tty'))), + (C.Rel 1), pattern + ) + ); + t1] + )) + status + )) + ~continuation: + (T.then_ + ~start:(EqualityTactics.rewrite_simpl_tac ~term) + ~continuation:EqualityTactics.reflexivity_tac + ) + ]) + status + | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") + ) + | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality") + in + ProofEngineTypes.mk_tactic (injection1_tac ~term ~i) ;; @@ -202,7 +211,8 @@ exception TwoDifferentSubtermsFound of int (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) -let discriminate'_tac ~term status = +let discriminate'_tac ~term = + let discriminate'_tac ~term status = let (proof, goal) = status in let module C = Cic in let module U = UriManager in @@ -286,8 +296,9 @@ prerr_endline ("XXXX nth funzionano ") ; in let (proof',goals') = - EliminationTactics.elim_type_tac - ~term:(C.MutInd(Logic.false_URI,0,[])) + ProofEngineTypes.apply_tactic + (EliminationTactics.elim_type_tac + ~term:(C.MutInd(Logic.false_URI,0,[]))) status in (match goals' with @@ -296,7 +307,8 @@ prerr_endline ("XXXX nth funzionano ") ; let _,context',gty' = CicUtil.lookup_meta goal' metasenv' in - T.then_ + ProofEngineTypes.apply_tactic + (T.then_ ~start: (P.change_tac ~what:gty' @@ -329,21 +341,26 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic T.then_ ~start:(EqualityTactics.rewrite_back_simpl_tac ~term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) - ) + )) (proof',goal') | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal") ) | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") ) | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality") + in + ProofEngineTypes.mk_tactic (discriminate'_tac ~term) ;; - -let discriminate_tac ~term status = - Tacticals.then_ - ~start:(* (injection_tac ~term) *) Tacticals.id_tac - ~continuation:(discriminate'_tac ~term) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *) +let discriminate_tac ~term = + let discriminate_tac ~term status = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(* (injection_tac ~term) *) Tacticals.id_tac + ~continuation:(discriminate'_tac ~term)) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *) status + in + ProofEngineTypes.mk_tactic (discriminate_tac ~term) ;; @@ -356,8 +373,8 @@ e' vera o no e lo risolve *) -let compare_tac ~term status = Tacticals.id_tac status -(* +let compare_tac ~term = Tacticals.id_tac + (* (* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *) (* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *) let module C = Cic in diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 29aa1c4f1..1db11951f 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -56,15 +56,18 @@ let induction_tac ~term status = ;; *) - -let elim_type_tac ~term status = - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - T.thens - ~start: (P.cut_tac term) - ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] - status +let elim_type_tac ~term = + let elim_type_tac ~term status = + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + ProofEngineTypes.apply_tactic + (T.thens + ~start: (P.cut_tac term) + ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]) + status + in + ProofEngineTypes.mk_tactic (elim_type_tac ~term) ;; @@ -131,7 +134,8 @@ let call_back uris = ;; *) -let decompose_tac ?(uris_choice_callback=(function l -> l)) term status = +let decompose_tac ?(uris_choice_callback=(function l -> l)) term = + let decompose_tac uris_choice_callback term status = let (proof, goal) = status in let module C = Cic in let module R = CicReduction in @@ -190,35 +194,39 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term status = | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) when (List.mem (uri,typeno,exp_named_subst) urilist) -> warn ("elim " ^ CicPp.ppterm termty); - T.then_ + ProofEngineTypes.apply_tactic + (T.then_ ~start:(P.elim_intros_simpl_tac ~term:term') ~continuation:( (* clear the hyp that has just been eliminated *) - (fun status -> + ProofEngineTypes.mk_tactic (fun status -> let (proof, goal) = status in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let new_context_len = List.length context in warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in - T.then_ + ProofEngineTypes.apply_tactic + (T.then_ ~start:( if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end) - ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim) + ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim))) status - )) + ))) status | _ -> let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)); elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status else (* no hyp to elim left in this goal *) - T.id_tac status + ProofEngineTypes.apply_tactic T.id_tac status in elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status + in + ProofEngineTypes.mk_tactic (decompose_tac uris_choice_callback term) ;; diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 0e9f72b0f..a649d4a23 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -23,119 +23,132 @@ * http://cs.unibo.it/helm/. *) - -let rewrite_tac ~term:equality (proof,goal) = - let module C = Cic in - let module U = UriManager in - let curi,metasenv,pbo,pty = proof in - let metano,context,gty = CicUtil.lookup_meta goal metasenv in - let eq_ind_r,ty,t1,t2 = - match CicTypeChecker.type_of_aux' metasenv context equality with - C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] - when U.eq uri HelmLibraryObjects.Logic.eq_URI -> - let eq_ind_r = - C.Const - (HelmLibraryObjects.Logic.eq_ind_r_URI,[]) - in - eq_ind_r,ty,t1,t2 - | _ -> - raise - (ProofEngineTypes.Fail - "Rewrite: the argument is not a proof of an equality") - in - let pred = - let gty' = CicSubstitution.lift 1 gty in - let t1' = CicSubstitution.lift 1 t1 in - let gty'' = - ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.alpha_equivalence - ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' - in - C.Lambda - (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty, - ty, gty'') +let rewrite_tac ~term:equality = + let rewrite_tac ~term:equality (proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = CicUtil.lookup_meta goal metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri HelmLibraryObjects.Logic.eq_URI -> + let eq_ind_r = + C.Const + (HelmLibraryObjects.Logic.eq_ind_r_URI,[]) + in + eq_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") in - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in - - let (proof',goals) = - PrimitiveTactics.exact_tac - ~term:(C.Appl - [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) - ((curi,metasenv',pbo,pty),goal) + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' + in + C.Lambda + (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty, + ty, gty'') in - assert (List.length goals = 0) ; - (proof',[fresh_meta]) + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in + let irl =CicMkImplicit.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])) ((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) + in + ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality) ;; -let rewrite_simpl_tac ~term status = - Tacticals.then_ - ~start:(rewrite_tac ~term) - ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None) - status +let rewrite_simpl_tac ~term = + let rewrite_simpl_tac ~term status = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(rewrite_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)) + status + in + ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term) ;; -let rewrite_back_tac ~term:equality (proof,goal) = - let module C = Cic in - let module U = UriManager in - let curi,metasenv,pbo,pty = proof in - let metano,context,gty = CicUtil.lookup_meta goal metasenv in - let eq_ind_r,ty,t1,t2 = - match CicTypeChecker.type_of_aux' metasenv context equality with - C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] - when U.eq uri HelmLibraryObjects.Logic.eq_URI -> - let eq_ind_r = - C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[]) - in - eq_ind_r,ty,t2,t1 - | _ -> - raise - (ProofEngineTypes.Fail - "Rewrite: the argument is not a proof of an equality") - in - let pred = - let gty' = CicSubstitution.lift 1 gty in - let t1' = CicSubstitution.lift 1 t1 in - let gty'' = - ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.alpha_equivalence - ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' - in - C.Lambda - (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty, - ty, gty'') +let rewrite_back_tac ~term:equality = + let rewrite_back_tac equality (proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = CicUtil.lookup_meta goal metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri HelmLibraryObjects.Logic.eq_URI -> + let eq_ind_r = + C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[]) + in + eq_ind_r,ty,t2,t1 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") in - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in - - let (proof',goals) = - PrimitiveTactics.exact_tac - ~term:(C.Appl - [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) - ((curi,metasenv',pbo,pty),goal) + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' + in + C.Lambda + (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty, + ty, gty'') in - assert (List.length goals = 0) ; - (proof',[fresh_meta]) - + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])) + ((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) + in + ProofEngineTypes.mk_tactic (rewrite_back_tac equality) ;; -let rewrite_back_simpl_tac ~term status = - Tacticals.then_ - ~start:(rewrite_back_tac ~term) - ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None) - status +let rewrite_back_simpl_tac ~term = + let rewrite_back_simpl_tac ~term status = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(rewrite_back_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)) + status + in + ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term) ;; - -let replace_tac ~what ~with_what status = +let replace_tac ~what ~with_what = + let replace_tac ~what ~with_what status = let (proof, goal) = status in let module C = Cic in let module U = UriManager in @@ -147,7 +160,8 @@ let replace_tac ~what ~with_what status = try if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) then - T.thens + ProofEngineTypes.apply_tactic + (T.thens ~start:( P.cut_tac (C.Appl [ @@ -161,10 +175,13 @@ let replace_tac ~what ~with_what status = ~continuation:( ProofEngineStructuralRules.clear ~hyp:(List.hd context)) ; - T.id_tac] + T.id_tac]) status else raise (ProofEngineTypes.Fail "Replace: terms not replaceable") - with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context") + with (Failure "hd") -> + raise (ProofEngineTypes.Fail "Replace: empty context") + in + ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what) ;; @@ -174,23 +191,28 @@ let reflexivity_tac = IntroductionTactics.constructor_tac ~n:1 ;; - -let symmetry_tac (proof, goal) = +let symmetry_tac = + let symmetry_tac (proof, goal) = let module C = Cic in let module R = CicReduction in let module U = UriManager in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) -> - PrimitiveTactics.apply_tac (proof,goal) - ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, [])) + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) + when (U.eq uri HelmLibraryObjects.Logic.eq_URI) -> + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac + ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))) + (proof,goal) | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") + in + ProofEngineTypes.mk_tactic symmetry_tac ;; - -let transitivity_tac ~term status = +let transitivity_tac ~term = + let transitivity_tac ~term status = let (proof, goal) = status in let module C = Cic in let module R = CicReduction in @@ -199,15 +221,19 @@ let transitivity_tac ~term status = let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = HelmLibraryObjects.Logic.eq_URI) -> - T.thens + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) + when (uri = HelmLibraryObjects.Logic.eq_URI) -> + ProofEngineTypes.apply_tactic + (T.thens ~start:(PrimitiveTactics.apply_tac ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, []))) ~continuations: - [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac] + [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]) status | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") + in + ProofEngineTypes.mk_tactic (transitivity_tac ~term) ;; diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index f5cc890aa..3556a85f2 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -31,6 +31,7 @@ des in *) open Fourier +open ProofEngineTypes let debug x = print_string ("____ "^x) ; flush stdout;; @@ -569,7 +570,8 @@ let rational_to_real x = (* preuve que 0 pall "n0" status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in - let tacd=ref - (fun status -> pall "d0" status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in + let tacn=ref (mk_tactic (fun status -> + pall "n0" status _Rlt_zero_1 ; + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in + let tacd=ref (mk_tactic (fun status -> + pall "d0" status _Rlt_zero_1 ; + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in for i=1 to n-1 do - tacn:=(Tacticals.then_ ~start:(fun status -> pall ("n"^string_of_int i) - status _Rlt_zero_pos_plus1; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 status) - ~continuation:!tacn); + tacn:=(Tacticals.then_ + ~start:(mk_tactic (fun status -> + pall ("n"^string_of_int i) status _Rlt_zero_pos_plus1; + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) + status)) + ~continuation:!tacn); done; for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(fun status -> pall "d" - status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacd); + tacd:=(Tacticals.then_ + ~start:(mk_tactic (fun status -> + pall "d" status _Rlt_zero_pos_plus1 ; + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status)) + ~continuation:!tacd); done; - - debug("TAC ZERO INF POS\n"); - -(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) - ~continuations:[ - !tacn ; - !tacd ] - status) + apply_tactic + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[!tacn ;!tacd ] ) + status + in + mk_tactic (tac_zero_inf_pos (n,d)) ;; @@ -614,30 +621,32 @@ debug("TAC ZERO INF POS\n"); (* preuve que 0<=n*1/d *) -let tac_zero_infeq_pos gl (n,d) status = - (*let cste = pf_parse_constr gl in*) - debug("inizio tac_zero_infeq_pos\n"); - let tacn = ref - (*(if n=0 then - (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) - else*) - (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) - (* ) *) - in - let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in - for i=1 to n-1 do - tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); - done; - for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); - done; - let r = - (Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in - debug("fine tac_zero_infeq_pos\n"); - r +let tac_zero_infeq_pos gl (n,d) = + let tac_zero_infeq_pos gl (n,d) status = + (*let cste = pf_parse_constr gl in*) + debug("inizio tac_zero_infeq_pos\n"); + let tacn = ref + (*(if n=0 then + (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) + else*) + (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) + (* ) *) + in + let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); + done; + apply_tactic + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) + ~continuations:[!tacn;!tacd]) status + in + mk_tactic (tac_zero_infeq_pos gl (n,d)) ;; @@ -645,75 +654,68 @@ let tac_zero_infeq_pos gl (n,d) status = (* preuve que 0<(-n)*(1/d) => False *) -let tac_zero_inf_false gl (n,d) status= - debug("inizio tac_zero_inf_false\n"); - if n=0 then - (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 status) in - debug("fine\n"); - r) - else - (debug "2\n";let r = (Tacticals.then_ ~start:( - fun status -> +let tac_zero_inf_false gl (n,d) = + let tac_zero_inf_false gl (n,d) status = + if n=0 then + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status + else + apply_tactic (Tacticals.then_ + ~start:( mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " - ^ CicPp.ppterm ty ^"\n"); - let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt status in - debug("!!!!!!!!!2\n"); - r - ) - ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in - debug("fine\n"); - r - ) + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status)) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) + status + in + mk_tactic (tac_zero_inf_false gl (n,d)) ;; (* preuve que 0<=n*(1/d) => False ; n est negatif *) -let tac_zero_infeq_false gl (n,d) status= -let (proof, goal) = status in -debug("stat tac_zero_infeq_false\n"); -let r = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - - debug("faccio fold di " ^ CicPp.ppterm - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) ^ "\n") ; - debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); - (*CSC: Patch to undo the over-simplification of RewriteSimpl *) - Tacticals.then_ - ~start: - (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~also_in_hypotheses:false - ~term: - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) - ) - ~continuation: - (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d))) status in - debug("end tac_zero_infeq_false\n"); - r -(*PORTING - Tacticals.id_tac status -*) +let tac_zero_infeq_false gl (n,d) = + let tac_zero_infeq_false gl (n,d) status = + let (proof, goal) = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + + debug("faccio fold di " ^ CicPp.ppterm + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] + ] + ) ^ "\n") ; + debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); + (*CSC: Patch to undo the over-simplification of RewriteSimpl *) + apply_tactic + (Tacticals.then_ + ~start: + (ReductionTactics.fold_tac ~reduction:CicReduction.whd + ~also_in_hypotheses:false + ~term: + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] + ] + ) + ) + ~continuation: + (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) + ~continuation:(tac_zero_inf_pos (-n,d)))) + status + in + mk_tactic (tac_zero_infeq_false gl (n,d)) ;; (* *********** ********** ******** ??????????????? *********** **************) -let apply_type_tac ~cast:t ~applist:al (proof,goal) = +let apply_type_tac ~cast:t ~applist:al = + let apply_type_tac ~cast:t ~applist:al (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in @@ -722,76 +724,73 @@ let apply_type_tac ~cast:t ~applist:al (proof,goal) = let metasenv' = (fresh_meta,context,t)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = - PrimitiveTactics.apply_tac - (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*) - ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) - (proof',goal) + apply_tactic + (PrimitiveTactics.apply_tac + (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) *) + ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al))) (* ??? *) + (proof',goal) in proof'',fresh_meta::goals + in + mk_tactic (apply_type_tac ~cast:t ~applist:al) ;; - - - - -let my_cut ~term:c (proof,goal)= +let my_cut ~term:c = + let my_cut ~term:c (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - -debug("my_cut di "^CicPp.ppterm c^"\n"); - - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,c)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = - apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, - CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] - (proof',goal) + apply_tactic + (apply_type_tac + ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) + ~applist:[Cic.Meta(fresh_meta,irl)]) + (proof',goal) in (* We permute the generated goals to be consistent with Coq *) match goals with [] -> assert false | he::tl -> proof'',he::fresh_meta::tl + in + mk_tactic (my_cut ~term:c) ;; - let exact = PrimitiveTactics.exact_tac;; -let tac_use h status = -let (proof, goal) = status in -debug("Inizio TC_USE\n"); -let curi,metasenv,pbo,pty = proof in -let metano,context,ty = CicUtil.lookup_meta goal metasenv in -debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); -debug ("ty = "^ CicPp.ppterm ty^"\n"); - -let res = -match h.htype with - "Rlt" -> exact ~term:h.hname status - |"Rle" -> exact ~term:h.hname status - |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) status - |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) status - |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) status - |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) status - |_->assert false -in -debug("Fine TAC_USE\n"); -res +let tac_use h = + let tac_use h status = + let (proof, goal) = status in + debug("Inizio TC_USE\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + apply_tactic + (match h.htype with + "Rlt" -> exact ~term:h.hname + | "Rle" -> exact ~term:h.hname + | "Rgt" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) + ~continuation:(exact ~term:h.hname)) + | "Rge" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) + ~continuation:(exact ~term:h.hname)) + | "eqTLR" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) + ~continuation:(exact ~term:h.hname)) + | "eqTRL" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) + ~continuation:(exact ~term:h.hname)) + | _->assert false) + status + in + mk_tactic (tac_use h) ;; - - let is_ineq (h,t) = match t with Cic.Appl ( Cic.Const(u,boh)::next) -> @@ -843,62 +842,64 @@ let rec filter_real_hyp context cont = [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont ;;*) + let filter_real_hyp context _ = let rec filter_aux context num = match context with - [] -> [] - | Some(Cic.Name(h),Cic.Decl(t))::next -> - ( - (*let n = find_in_context h cont in*) - debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); - [(Cic.Rel(num),t)] @ filter_aux next (num+1) - ) - | a::next -> filter_aux next (num+1) + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> + [(Cic.Rel(num),t)] @ filter_aux next (num+1) + | a::next -> filter_aux next (num+1) in - filter_aux context 1 + filter_aux context 1 ;; (* lifts everithing at the conclusion level *) let rec superlift c n= match c with - [] -> [] - | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl( - CicSubstitution.lift n a))] @ superlift next (n+1) - | Some(name,Cic.Def(a,None))::next -> [Some(name,Cic.Def(( - CicSubstitution.lift n a),None))] @ superlift next (n+1) - | Some(name,Cic.Def(a,Some ty))::next -> [Some(name,Cic.Def(( - CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1) + [] -> [] + | Some(name,Cic.Decl(a))::next -> + [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1) + | Some(name,Cic.Def(a,None))::next -> + [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1) + | Some(name,Cic.Def(a,Some ty))::next -> + [Some(name, + Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty))) + ] @ superlift next (n+1) | _::next -> superlift next (n+1) (*?? ??*) ;; -let equality_replace a b status = -debug("inizio EQ\n"); - let module C = Cic in - let proof,goal = status in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in -debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); - let (proof,goals) = - EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) +let equality_replace a b = + let equality_replace a b status = + debug("inizio EQ\n"); + let module C = Cic in + let proof,goal = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in + debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); + let (proof,goals) = apply_tactic + (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))) ((curi,metasenv',pbo,pty),goal) - in - let new_goals = fresh_meta::goals in -debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " - ^string_of_int( List.length goals)^"+ meta\n"); - (proof,new_goals) + in + let new_goals = fresh_meta::goals in + debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " + ^string_of_int( List.length goals)^"+ meta\n"); + (proof,new_goals) + in + mk_tactic (equality_replace a b) ;; let tcl_fail a (proof,goal) = - match a with - 1 -> raise (ProofEngineTypes.Fail "fail-tactical") - |_-> (proof,[goal]) + match a with + 1 -> raise (ProofEngineTypes.Fail "fail-tactical") + | _ -> (proof,[goal]) ;; (* Galla: moved in variousTactics.ml @@ -935,13 +936,13 @@ let contradiction_tac (proof,goal)= let rec fourier (s_proof,s_goal)= let s_curi,s_metasenv,s_pbo,s_pty = s_proof in let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in - debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); + debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n"); debug_pcontext s_context; let fhyp = String.copy "new_hyp_for_fourier" in -(* here we need to negate the thesis, but to do this we need to apply the right -theoreme,so let's parse our thesis *) +(* here we need to negate the thesis, but to do this we need to apply the + right theoreme,so let's parse our thesis *) let th_to_appl = ref _Rfourier_not_le_gt in (match s_ty with @@ -961,11 +962,12 @@ theoreme,so let's parse our thesis *) (* now let's change our thesis applying the th and put it with hp *) - let proof,gl = - Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation:(PrimitiveTactics.intros_tac ()) - (s_proof,s_goal) in + let proof,gl = apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:(PrimitiveTactics.intros_tac ())) + (s_proof,s_goal) + in let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in @@ -977,7 +979,6 @@ theoreme,so let's parse our thesis *) let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* now we want to convert hp to inequations, but first we must lift everyting to thesis level, so that a variable has the save Rel(n) in each hp ( needed by ineq1_of_term ) *) @@ -997,7 +998,6 @@ theoreme,so let's parse our thesis *) List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) with _-> ()) hyps; - debug ("applico fourier a "^ string_of_int (List.length !lineq)^ " disequazioni\n"); @@ -1057,28 +1057,26 @@ theoreme,so let's parse our thesis *) debug "inizio a costruire tac1\n"; Fourier.print_rational(c1); - let tac1=ref ( fun status -> - if h1.hstrict then + let tac1=ref ( mk_tactic (fun status -> + apply_tactic + (if h1.hstrict then (Tacticals.thens - ~start:( - fun status -> + ~start:(mk_tactic (fun status -> debug ("inizio t1 strict\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt status) - ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] - status - ) - else + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status)) + ~continuations:[tac_use h1; + tac_zero_inf_pos (rational_to_fraction c1)]) + else (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] status - ) - ) + (rational_to_fraction c1)])) + status)) in s:=h1.hstrict; @@ -1087,45 +1085,39 @@ theoreme,so let's parse our thesis *) (if h.hstrict then (debug("tac1 1\n"); tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_lt_lt) + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_lt) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else + (rational_to_fraction c)])) + else (debug("tac1 2\n"); Fourier.print_rational(c1); tac1:=(Tacticals.thens - ~start:( - fun status -> + ~start:(mk_tactic (fun status -> debug("INIZIO TAC 1 2\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le status) + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le) + status)) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - ) - else + (rational_to_fraction c)]))) + else (if h.hstrict then (debug("tac1 3\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else + (rational_to_fraction c)])) + else (debug("tac1 4\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - ) - ); - s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + (rational_to_fraction c)])))); + s:=(!s)||(h.hstrict)) (* end fun -> *) + lutil;(*end List.iter*) let tac2 = if sres then @@ -1135,48 +1127,46 @@ theoreme,so let's parse our thesis *) in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) - ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ - ~start:(fun status -> + ~continuations:[Tacticals.then_ + ~start:( mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - PrimitiveTactics.change_tac ~what:ty - ~with_what:(Cic.Appl [ _not; ineq]) status) + apply_tactic + (PrimitiveTactics.change_tac ~what:ty + ~with_what:(Cic.Appl [ _not; ineq])) + status)) ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term: (if sres then _Rnot_lt_lt else _Rnot_le_le)) ~continuation:(Tacticals.thens - ~start:( - fun status -> - debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); - let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~start:(mk_tactic (fun status -> + debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^ + CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); + let r = apply_tactic + (equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc) status in (match r with (p,gl) -> debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); - r) + r)) ~continuations:[(Tacticals.thens - ~start:( - fun status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 status in + ~start:(mk_tactic (fun status -> + let r = apply_tactic + (equality_replace (Cic.Appl[_Rinv;_R1]) _R1) + status + in (match r with (p,gl) -> debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); - r) + r)) ~continuations: - [PrimitiveTactics.apply_tac ~term:_Rinv_R1 - ;Tacticals.try_tactics - ~tactics:[ "ring", (fun status -> - debug("begin RING\n"); - let r = Ring.ring_tac status in - debug ("end RING\n"); - r) - ; "id", Tacticals.id_tac] - ]) + [PrimitiveTactics.apply_tac ~term:_Rinv_R1; + Tacticals.try_tactics + ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] + ]) ;(*Tacticals.id_tac*) Tacticals.then_ - ~start: - ( - fun status -> + ~start:(mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -1187,11 +1177,11 @@ theoreme,so let's parse our thesis *) Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) |_ -> assert false) in - let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 status in + let r = apply_tactic + (PrimitiveTactics.change_tac ~what:ty ~with_what:w1) + status in debug("fine MY_CHNGE\n"); - r - - ) + r)) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) @@ -1199,12 +1189,12 @@ theoreme,so let's parse our thesis *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); ( - let r = !tac (proof,goal) in + let r = apply_tactic !tac (proof,goal) in debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r ) ;; -let fourier_tac (proof,goal) = fourier (proof,goal);; +let fourier_tac = mk_tactic fourier diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml index 9751b2b74..f6283cf68 100644 --- a/helm/ocaml/tactics/introductionTactics.ml +++ b/helm/ocaml/tactics/introductionTactics.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let constructor_tac ~n (proof, goal) = +let fake_constructor_tac ~n (proof, goal) = let module C = Cic in let module R = CicReduction in let (_,metasenv,_,_) = proof in @@ -31,14 +31,17 @@ let constructor_tac ~n (proof, goal) = match (R.whd context ty) with (C.MutInd (uri, typeno, exp_named_subst)) | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> - PrimitiveTactics.apply_tac - ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) - (proof, goal) + ProofEngineTypes.apply_tactic ( + PrimitiveTactics.apply_tac + ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))) + (proof, goal) | _ -> raise (ProofEngineTypes.Fail "Constructor: failed") ;; -let exists_tac status = constructor_tac ~n:1 status ;; -let split_tac status = constructor_tac ~n:1 status ;; -let left_tac status = constructor_tac ~n:1 status ;; -let right_tac status = constructor_tac ~n:2 status ;; +let constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n) + +let exists_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;; +let split_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;; +let left_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;; +let right_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:2) ;; diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index 65fe892fa..a4b7d9ba8 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -23,8 +23,8 @@ * http://cs.unibo.it/helm/. *) - -let absurd_tac ~term status = +let absurd_tac ~term = + let absurd_tac ~term status = let (proof, goal) = status in let module C = Cic in let module U = UriManager in @@ -32,31 +32,41 @@ let absurd_tac ~term status = let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *) - then P.apply_tac - ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) status + then ProofEngineTypes.apply_tactic + (P.apply_tac + ~term:( + C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; + term ; ty]) + ) + status else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") + in + ProofEngineTypes.mk_tactic (absurd_tac ~term) ;; - -let contradiction_tac status = +let contradiction_tac = + let contradiction_tac status = let module C = Cic in let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in try - T.then_ + ProofEngineTypes.apply_tactic ( + T.then_ ~start:(P.intros_tac ()) ~continuation:( - T.then_ + T.then_ ~start: (EliminationTactics.elim_type_tac ~term: (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []))) - ~continuation: VariousTactics.assumption_tac) + ~continuation: VariousTactics.assumption_tac)) status with (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption") (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *) + in + ProofEngineTypes.mk_tactic contradiction_tac ;; (* Questa era in fourierR.ml diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 388ac2056..d26de4447 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -334,231 +334,247 @@ let apply_tac ~term (proof, goal) = (* TODO per implementare i tatticali e' necessario che tutte le tattiche sollevino _solamente_ Fail *) -let apply_tac ~term status = +let apply_tac ~term = + let apply_tac ~term status = try apply_tac ~term status (* TODO cacciare anche altre eccezioni? *) with CicUnification.UnificationFailure _ as e -> raise (Fail (Printexc.to_string e)) + in + mk_tactic (apply_tac ~term) -let intros_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) () - (proof, goal) -= - let module C = Cic in - let module R = CicReduction in - let (_,metasenv,_,_) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = new_meta_of_proof ~proof in - let (context',ty',bo') = - lambda_abstract metasenv context newmeta ty mk_fresh_name_callback - in - let (newproof, _) = - subst_meta_in_proof proof metano bo' [newmeta,context',ty'] - in - (newproof, [newmeta]) - -let cut_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) - term (proof, goal) -= - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta1 = new_meta_of_proof ~proof in - let newmeta2 = newmeta1 + 1 in - let fresh_name = - mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in - let context_for_newmeta1 = - (Some (fresh_name,C.Decl term))::context in - let irl1 = - CicMkImplicit.identity_relocation_list_for_metavariable - context_for_newmeta1 - in - let irl2 = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newmeta1ty = CicSubstitution.lift 1 ty in - let bo' = - C.Appl - [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; - C.Meta (newmeta2,irl2)] - in - let (newproof, _) = - subst_meta_in_proof proof metano bo' - [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; - in - (newproof, [newmeta1 ; newmeta2]) - -let letin_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) - term (proof, goal) -= - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let _ = CicTypeChecker.type_of_aux' metasenv context term in +let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()= + let intros_tac + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) () + (proof, goal) + = + let module C = Cic in + let module R = CicReduction in + let (_,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = new_meta_of_proof ~proof in + let (context',ty',bo') = + lambda_abstract metasenv context newmeta ty mk_fresh_name_callback + in + let (newproof, _) = + subst_meta_in_proof proof metano bo' [newmeta,context',ty'] + in + (newproof, [newmeta]) + in + mk_tactic (intros_tac ~mk_fresh_name_callback ()) + +let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term= + let cut_tac + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) + term (proof, goal) + = + let module C = Cic in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let newmeta1 = new_meta_of_proof ~proof in + let newmeta2 = newmeta1 + 1 in let fresh_name = - mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in - let context_for_newmeta = - (Some (fresh_name,C.Def (term,None)))::context in - let irl = + mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in + let context_for_newmeta1 = + (Some (fresh_name,C.Decl term))::context in + let irl1 = CicMkImplicit.identity_relocation_list_for_metavariable - context_for_newmeta + context_for_newmeta1 + in + let irl2 = + CicMkImplicit.identity_relocation_list_for_metavariable context in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in + let newmeta1ty = CicSubstitution.lift 1 ty in + let bo' = + C.Appl + [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; + C.Meta (newmeta2,irl2)] + in let (newproof, _) = - subst_meta_in_proof - proof metano bo'[newmeta,context_for_newmeta,newmetaty] + subst_meta_in_proof proof metano bo' + [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; in - (newproof, [newmeta]) + (newproof, [newmeta1 ; newmeta2]) + in + mk_tactic (cut_tac ~mk_fresh_name_callback term) - (** functional part of the "exact" tactic *) -let exact_tac ~term (proof, goal) = - (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_,_) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let module T = CicTypeChecker in - let module R = CicReduction in - if R.are_convertible context (T.type_of_aux' metasenv context term) ty then - begin - let (newproof, metasenv') = - subst_meta_in_proof proof metano term [] in - (newproof, []) - end - else - raise (Fail "The type of the provided term is not the one expected.") +let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) term= + let letin_tac + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) + term (proof, goal) + = + let module C = Cic in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let _ = CicTypeChecker.type_of_aux' metasenv context term in + let newmeta = new_meta_of_proof ~proof in + let fresh_name = + mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in + let context_for_newmeta = + (Some (fresh_name,C.Def (term,None)))::context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable + context_for_newmeta + in + let newmetaty = CicSubstitution.lift 1 ty in + let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in + let (newproof, _) = + subst_meta_in_proof + proof metano bo'[newmeta,context_for_newmeta,newmetaty] + in + (newproof, [newmeta]) + in + mk_tactic (letin_tac ~mk_fresh_name_callback term) + (** functional part of the "exact" tactic *) +let exact_tac ~term = + let exact_tac ~term (proof, goal) = + (* Assumption: the term bo must be closed in the current context *) + let (_,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let module T = CicTypeChecker in + let module R = CicReduction in + if R.are_convertible context (T.type_of_aux' metasenv context term) ty then + begin + let (newproof, metasenv') = + subst_meta_in_proof proof metano term [] in + (newproof, []) + end + else + raise (Fail "The type of the provided term is not the one expected.") + in + mk_tactic (exact_tac ~term) (* not really "primitive" tactics .... *) - -let elim_tac ~term (proof, goal) = - let module T = CicTypeChecker in - let module U = UriManager in - let module R = CicReduction in - let module C = Cic in - let (curi,metasenv,_,_) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let termty = T.type_of_aux' metasenv context term in - let uri,exp_named_subst,typeno,args = - match termty with - C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) - | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> - (uri,exp_named_subst,typeno,args) - | _ -> raise NotAnInductiveTypeToEliminate - in - let eliminator_uri = - let buri = U.buri_of_uri uri in - let name = - match CicEnvironment.get_obj uri with - C.InductiveDefinition (tys,_,_) -> - let (name,_,_,_) = List.nth tys typeno in - name - | _ -> assert false - in - let ext = - match T.type_of_aux' metasenv context ty with - C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort C.CProp -> "_rec" - | C.Sort (C.Type _)-> "_rect" (* TASSI *) - | _ -> assert false - in - U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") +let elim_tac ~term = + let elim_tac ~term (proof, goal) = + let module T = CicTypeChecker in + let module U = UriManager in + let module R = CicReduction in + let module C = Cic in + let (curi,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let termty = T.type_of_aux' metasenv context term in + let uri,exp_named_subst,typeno,args = + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> + (uri,exp_named_subst,typeno,args) + | _ -> raise NotAnInductiveTypeToEliminate in - let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in - let ety = T.type_of_aux' metasenv context eliminator_ref in - let newmeta = new_meta_of_proof ~proof in - let (econclusion,newmetas,arguments,lastmeta) = - new_metasenv_for_apply newmeta proof context ety - in - (* Here we assume that we have only one inductive hypothesis to *) - (* eliminate and that it is the last hypothesis of the theorem. *) - (* A better approach would be fingering the hypotheses in some *) - (* way. *) - let meta_of_corpse = - let (_,canonical_context,_) = - CicUtil.lookup_meta (lastmeta - 1) newmetas - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable - canonical_context - in - Cic.Meta (lastmeta - 1, irl) - in - let newmetasenv = newmetas @ metasenv in - let subst1,newmetasenv' = - CicUnification.fo_unif newmetasenv context term meta_of_corpse + let eliminator_uri = + let buri = U.buri_of_uri uri in + let name = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tys,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + | _ -> assert false + in + let ext = + match T.type_of_aux' metasenv context ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.CProp -> "_rec" + | C.Sort (C.Type _)-> "_rect" (* TASSI *) + | _ -> assert false + in + U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") + in + let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in + let ety = T.type_of_aux' metasenv context eliminator_ref in + let newmeta = new_meta_of_proof ~proof in + let (econclusion,newmetas,arguments,lastmeta) = + new_metasenv_for_apply newmeta proof context ety in - let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in - (* The conclusion of our elimination principle is *) - (* (?i farg1 ... fargn) *) - (* The conclusion of our goal is ty. So, we can *) - (* eta-expand ty w.r.t. farg1 .... fargn to get *) - (* a new ty equal to (P farg1 ... fargn). Now *) - (* ?i can be instantiated with P and we are ready *) - (* to refine the term. *) - let emeta, fargs = - match ueconclusion with - C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs - | C.Meta (emeta,_) -> emeta,[] - | _ -> raise NotTheRightEliminatorShape + (* Here we assume that we have only one inductive hypothesis to *) + (* eliminate and that it is the last hypothesis of the theorem. *) + (* A better approach would be fingering the hypotheses in some *) + (* way. *) + let meta_of_corpse = + let (_,canonical_context,_) = + CicUtil.lookup_meta (lastmeta - 1) newmetas in - let ty' = CicMetaSubst.apply_subst subst1 ty in - let eta_expanded_ty = -(*CSC: newmetasenv' era metasenv ??????????? *) - List.fold_left (eta_expand newmetasenv' context) ty' fargs + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable + canonical_context in - let subst2,newmetasenv'' = -(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite -da subst1!!!! Dovrei rimuoverle o sono innocue?*) - CicUnification.fo_unif - newmetasenv' context ueconclusion eta_expanded_ty + Cic.Meta (lastmeta - 1, irl) + in + let newmetasenv = newmetas @ metasenv in + let subst1,newmetasenv' = + CicUnification.fo_unif newmetasenv context term meta_of_corpse + in + let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in + (* The conclusion of our elimination principle is *) + (* (?i farg1 ... fargn) *) + (* The conclusion of our goal is ty. So, we can *) + (* eta-expand ty w.r.t. farg1 .... fargn to get *) + (* a new ty equal to (P farg1 ... fargn). Now *) + (* ?i can be instantiated with P and we are ready *) + (* to refine the term. *) + let emeta, fargs = + match ueconclusion with + C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs + | C.Meta (emeta,_) -> emeta,[] + | _ -> raise NotTheRightEliminatorShape + in + let ty' = CicMetaSubst.apply_subst subst1 ty in + let eta_expanded_ty = + (*CSC: newmetasenv' era metasenv ??????????? *) + List.fold_left (eta_expand newmetasenv' context) ty' fargs in - let in_subst_domain i = - let eq_to_i = function (j,_) -> i=j in - List.exists eq_to_i subst1 || - List.exists eq_to_i subst2 + let subst2,newmetasenv'' = + (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite + da subst1!!!! Dovrei rimuoverle o sono innocue?*) + CicUnification.fo_unif + newmetasenv' context ueconclusion eta_expanded_ty in - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. apply_subst doesn't need the context. Hence *) - (* the underscore. *) - let apply_subst _ t = - let t' = CicMetaSubst.apply_subst subst1 t in - CicMetaSubst.apply_subst_reducing - (Some (emeta,List.length fargs)) subst2 t' + let in_subst_domain i = + let eq_to_i = function (j,_) -> i=j in + List.exists eq_to_i subst1 || + List.exists eq_to_i subst2 in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - classify_metas newmeta in_subst_domain apply_subst - newmetasenv'' - in - let arguments' = List.map (apply_subst context) arguments in - let bo' = Cic.Appl (eliminator_ref::arguments') in - let newmetasenv''' = - new_uninstantiatedmetas@old_uninstantiatedmetas - in - let (newproof, newmetasenv'''') = - (* When unwinding the META that corresponds to the *) - (* elimination predicate (which is emeta), we must *) - (* also perform one-step beta-reduction. *) - (* The only difference w.r.t. apply_subst is that *) - (* we also substitute metano with bo'. *) - (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) - (*CSC: no? *) - let apply_subst' t = - let t' = CicMetaSubst.apply_subst subst1 t in - CicMetaSubst.apply_subst_reducing - (Some (emeta,List.length fargs)) - ((metano,bo')::subst2) t' - in - subst_meta_and_metasenv_in_proof - proof metano apply_subst' newmetasenv''' + (* When unwinding the META that corresponds to the elimination *) + (* predicate (which is emeta), we must also perform one-step *) + (* beta-reduction. apply_subst doesn't need the context. Hence *) + (* the underscore. *) + let apply_subst _ t = + let t' = CicMetaSubst.apply_subst subst1 t in + CicMetaSubst.apply_subst_reducing + (Some (emeta,List.length fargs)) subst2 t' + in + let old_uninstantiatedmetas,new_uninstantiatedmetas = + classify_metas newmeta in_subst_domain apply_subst + newmetasenv'' + in + let arguments' = List.map (apply_subst context) arguments in + let bo' = Cic.Appl (eliminator_ref::arguments') in + let newmetasenv''' = + new_uninstantiatedmetas@old_uninstantiatedmetas in - (newproof, - List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + let (newproof, newmetasenv'''') = + (* When unwinding the META that corresponds to the *) + (* elimination predicate (which is emeta), we must *) + (* also perform one-step beta-reduction. *) + (* The only difference w.r.t. apply_subst is that *) + (* we also substitute metano with bo'. *) + (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) + (*CSC: no? *) + let apply_subst' t = + let t' = CicMetaSubst.apply_subst subst1 t in + CicMetaSubst.apply_subst_reducing + (Some (emeta,List.length fargs)) + ((metano,bo')::subst2) t' + in + subst_meta_and_metasenv_in_proof + proof metano apply_subst' newmetasenv''' + in + (newproof, + List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + in + mk_tactic (elim_tac ~term) ;; (* The simplification is performed only on the conclusion *) @@ -577,35 +593,38 @@ exception NotConvertible (*CSC: while [what] can have a richer context (because of binders) *) (*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *) (*CSC: Is that evident? Is that right? Or should it be changed? *) -let change_tac ~what ~with_what (proof, goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* are_convertible works only on well-typed terms *) - ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; - if CicReduction.are_convertible context what with_what then - begin - let replace = - ProofEngineReduction.replace - ~equality:(==) ~what:[what] ~with_what:[with_what] - in - let ty' = replace ty in - let context' = - List.map - (function - Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None)) - | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) - | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context - in - let metasenv' = +let change_tac ~what ~with_what = + let change_tac ~what ~with_what (proof, goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + (* are_convertible works only on well-typed terms *) + ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; + if CicReduction.are_convertible context what with_what then + begin + let replace = + ProofEngineReduction.replace + ~equality:(==) ~what:[what] ~with_what:[with_what] + in + let ty' = replace ty in + let context' = List.map (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv + Some (name,Cic.Def (t,None))->Some (name,Cic.Def ((replace t),None)) + | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) + | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false + ) context in - (curi,metasenv',pbo,pty), [metano] - end - else - raise (ProofEngineTypes.Fail "Not convertible") + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] + end + else + raise (ProofEngineTypes.Fail "Not convertible") + in + mk_tactic (change_tac ~what ~with_what) diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 20b0f21c9..e89569445 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -25,128 +25,133 @@ open ProofEngineTypes -let clearbody ~hyp (proof, goal) = - let module C = Cic in - match hyp with - None -> assert false - | Some (_, C.Def (_, Some _)) -> assert false - | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") - | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body -> - let curi,metasenv,pbo,pty = proof in - let metano,_,_ = CicUtil.lookup_meta goal metasenv in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear_body -> - let cleared_entry = - let ty = - CicTypeChecker.type_of_aux' metasenv context term +let clearbody ~hyp = + let clearbody ~hyp (proof, goal) = + let module C = Cic in + match hyp with + None -> assert false + | Some (_, C.Def (_, Some _)) -> assert false + | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") + | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body -> + let curi,metasenv,pbo,pty = proof in + let metano,_,_ = CicUtil.lookup_meta goal metasenv in + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + t when t == hyp_to_clear_body -> + let cleared_entry = + let ty = + CicTypeChecker.type_of_aux' metasenv context term + in + Some (n_to_clear_body, Cic.Decl ty) + in + cleared_entry::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def (t,None)) -> + let _ = + try + CicTypeChecker.type_of_aux' metasenv context t + with + _ -> + raise + (Fail + ("The correctness of hypothesis " ^ + string_of_name n ^ + " relies on the body of " ^ + string_of_name n_to_clear_body) + ) in - Some (n_to_clear_body, Cic.Decl ty) - in - cleared_entry::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("The correctness of hypothesis " ^ - string_of_name n ^ - " relies on the body of " ^ - string_of_name n_to_clear_body) - ) - in - entry::context - | Some (_,Cic.Def (_,Some _)) -> assert false - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("The correctness of the goal relies on the body of " ^ - string_of_name n_to_clear_body)) + entry::context + | Some (_,Cic.Def (_,Some _)) -> assert false + ) canonical_context [] in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] + let _ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + with + _ -> + raise + (Fail + ("The correctness of the goal relies on the body of " ^ + string_of_name n_to_clear_body)) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] + in + mk_tactic (clearbody ~hyp) -let clear ~hyp:hyp_to_clear (proof, goal) = - let module C = Cic in - match hyp_to_clear with - None -> assert false - | Some (n_to_clear, _) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = - CicUtil.lookup_meta goal metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" +let clear ~hyp = + let clear ~hyp:hyp_to_clear (proof, goal) = + let module C = Cic in + match hyp_to_clear with + None -> assert false + | Some (n_to_clear, _) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = + CicUtil.lookup_meta goal metasenv in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear -> None::context - | None -> None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("Hypothesis " ^ - string_of_name n ^ - " uses hypothesis " ^ - string_of_name n_to_clear) - ) - in - entry::context - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("Hypothesis " ^ string_of_name n_to_clear ^ - " occurs in the goal")) + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + t when t == hyp_to_clear -> None::context + | None -> None::context + | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,C.Decl t) + | Some (n,C.Def (t,None)) -> + let _ = + try + CicTypeChecker.type_of_aux' metasenv context t + with + _ -> + raise + (Fail + ("Hypothesis " ^ + string_of_name n ^ + " uses hypothesis " ^ + string_of_name n_to_clear) + ) + in + entry::context + ) canonical_context [] in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] - + let _ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + with + _ -> + raise + (Fail + ("Hypothesis " ^ string_of_name n_to_clear ^ + " occurs in the goal")) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] + in + mk_tactic (clear ~hyp) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 3e0a12e4e..ac0713bd0 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -38,9 +38,22 @@ type status = proof * goal (** an unfinished proof with the optional current goal *) type tactic = status -> proof * goal list + (** creates an opaque tactic from a status->proof*goal list function *) +let mk_tactic t = t + (** tactic failure *) exception Fail of string + (** + calls the opaque tactic on the status, restoring the original + universe graph if the tactic Fails + *) +let apply_tactic t status = + let saved_univ = CicUniv.get_working() in + try + t status + with Fail s -> CicUniv.set_working saved_univ; raise (Fail s) + (** constraint: the returned value will always be constructed by Cic.Name **) type mk_fresh_name_type = Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli new file mode 100644 index 000000000..c58b729b5 --- /dev/null +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -0,0 +1,49 @@ +(* Copyright (C) 2002, 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/. + *) + + (** + current proof (proof uri * metas * (in)complete proof * term to be prooved) + *) +type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term + (** current goal, integer index *) +type goal = int +type status = proof * goal + + (** + a tactic: make a transition from one status to another one or, usually, + raise a "Fail" (@see Fail) exception in case of failure + *) + (** an unfinished proof with the optional current goal *) +type tactic +val mk_tactic: (status -> proof * goal list) -> tactic + + (** tactic failure *) +exception Fail of string + +val apply_tactic: tactic -> status -> proof * goal list + + (** constraint: the returned value will always be constructed by Cic.Name **) +type mk_fresh_name_type = + Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 80cb3306a..d356499a1 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +open ProofEngineTypes + (* let reduction_tac ~reduction (proof,goal) = let curi,metasenv,pbo,pty = proof in @@ -89,41 +91,52 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) = (curi,metasenv',pbo,pty), [metano] ;; -let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;; -let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;; -let whd_tac = reduction_tac ~reduction:CicReduction.whd ;; +let simpl_tac ~also_in_hypotheses ~terms = + mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl + ~also_in_hypotheses ~terms);; -let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let term' = reduction context term in - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) - (*CSC: che si guadagni nulla in fatto di efficienza. *) - let replace = - ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term] - in - let ty' = replace ty in - let metasenv' = - let context' = - if also_in_hypotheses then +let reduce_tac ~also_in_hypotheses ~terms = + mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce + ~also_in_hypotheses ~terms);; + +let whd_tac ~also_in_hypotheses ~terms = + mk_tactic ( reduction_tac ~reduction:CicReduction.whd + ~also_in_hypotheses ~terms);; + +let fold_tac ~reduction ~also_in_hypotheses ~term = + let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let term' = reduction context term in + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) + (*CSC: che si guadagni nulla in fatto di efficienza. *) + let replace = + ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term] + in + let ty' = replace ty in + let metasenv' = + let context' = + if also_in_hypotheses then + List.map + (function + Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) + | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None)) + | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false + ) context + else + context + in List.map (function - Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) - | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None)) - | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context - else - context + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - - in - (curi,metasenv',pbo,pty), [metano] + (curi,metasenv',pbo,pty), [metano] + in + mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term) ;; diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index e2de04591..cf6950c4b 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -389,11 +389,15 @@ let elim_type_tac ~term status = @param term term to cut @param proof term used to prove second subgoal generated by elim_type *) -let elim_type2_tac ~term ~proof status = +let elim_type2_tac ~term ~proof = + let elim_type2_tac ~term ~proof status = let module E = EliminationTactics in warn "in Ring.elim_type2"; - Tacticals.thens ~start:(E.elim_type_tac ~term) - ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status + ProofEngineTypes.apply_tactic + (Tacticals.thens ~start:(E.elim_type_tac ~term) + ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status + in + ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof) (* Galla: spostata in variousTactics.ml (** @@ -423,7 +427,8 @@ let lift ~n (a,b,c,d,e,f,g,h) = @param count number of hypotheses to remove @param status current proof engine status *) -let purge_hyps_tac ~count status = +let purge_hyps_tac ~count = + let purge_hyps_tac ~count status = let module S = ProofEngineStructuralRules in let (proof, goal) = status in let rec aux n context status = @@ -432,7 +437,8 @@ let purge_hyps_tac ~count status = | (0, _) -> status | (n, hd::tl) -> aux (n-1) tl - (status_of_single_goal_tactic_result (S.clear ~hyp:hd status)) + (status_of_single_goal_tactic_result + (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status)) | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in let (_, metasenv, _, _) = proof in @@ -440,6 +446,8 @@ let purge_hyps_tac ~count status = let proof',goal' = aux count context status in assert (goal = goal') ; proof',[goal'] + in + ProofEngineTypes.mk_tactic (purge_hyps_tac ~count) (** THE TACTIC! *) @@ -447,6 +455,7 @@ let purge_hyps_tac ~count status = Ring tactic, does associative and commutative rewritings in Reals ring @param status current proof engine status *) + let ring_tac status = let (proof, goal) = status in warn "in Ring tactic"; @@ -467,8 +476,8 @@ let ring_tac status = t2; t2'; t2''; t2'_eq_t2'']); try let new_hyps = ref 0 in (* number of new hypotheses created *) - Tacticals.try_tactics - status + ProofEngineTypes.apply_tactic + (Tacticals.try_tactics ~tactics:[ "reflexivity", EqualityTactics.reflexivity_tac ; "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; @@ -483,15 +492,17 @@ let ring_tac status = ] ; t1'_eq_t1'' ]) ; - "elim_type eqt su t1 ...", (fun status -> + "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status -> let status' = (* status after 1st elim_type use *) let context = context_of_status status in if not (are_convertible context t1'' t1) then begin warn "t1'' and t1 are NOT CONVERTIBLE"; let newstatus = - elim_type2_tac (* 1st elim_type use *) - status ~proof:t1'_eq_t1'' - ~term:(Cic.Appl [eqt; r; t1''; t1]) + ProofEngineTypes.apply_tactic + (elim_type2_tac (* 1st elim_type use *) + ~proof:t1'_eq_t1'' + ~term:(Cic.Appl [eqt; r; t1''; t1])) + status in incr new_hyps; (* elim_type add an hyp *) match newstatus with @@ -506,8 +517,8 @@ let ring_tac status = lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') in let status'' = - Tacticals.try_tactics (* try to solve 1st subgoal *) - status' + ProofEngineTypes.apply_tactic + (Tacticals.try_tactics (* try to solve 1st subgoal *) ~tactics:[ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; "exact sym_eqt su t2 ...", @@ -521,15 +532,18 @@ let ring_tac status = ] ; t2'_eq_t2'' ]) ; - "elim_type eqt su t2 ...", (fun status -> + "elim_type eqt su t2 ...", + ProofEngineTypes.mk_tactic (fun status -> let status' = let context = context_of_status status in if not (are_convertible context t2'' t2) then begin warn "t2'' and t2 are NOT CONVERTIBLE"; let newstatus = - elim_type2_tac (* 2nd elim_type use *) - status ~proof:t2'_eq_t2'' - ~term:(Cic.Appl [eqt; r; t2''; t2]) + ProofEngineTypes.apply_tactic + (elim_type2_tac (* 2nd elim_type use *) + ~proof:t2'_eq_t2'' + ~term:(Cic.Appl [eqt; r; t2''; t2])) + status in incr new_hyps; (* elim_type add an hyp *) match newstatus with @@ -542,12 +556,16 @@ let ring_tac status = in try (* try to solve main goal *) warn "trying reflexivity ...."; - EqualityTactics.reflexivity_tac status' + ProofEngineTypes.apply_tactic + EqualityTactics.reflexivity_tac status' with (Fail _) -> (* leave conclusion to the user *) warn "reflexivity failed, solution's left as an ex :-)"; - purge_hyps_tac ~count:!new_hyps status')] + ProofEngineTypes.apply_tactic + (purge_hyps_tac ~count:!new_hyps) status')]) + status' in - status'')] + status'')]) + status with (Fail s) -> raise (Fail ("Ring failure: " ^ s)) end @@ -555,9 +573,12 @@ let ring_tac status = assert false (* wrap ring_tac catching GoalUnringable and raising Fail *) + let ring_tac status = try ring_tac status with GoalUnringable -> raise (Fail "goal unringable") +let ring_tac = ProofEngineTypes.mk_tactic ring_tac + diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml index 1c970249c..94710c412 100644 --- a/helm/ocaml/tactics/statefulProofEngine.ml +++ b/helm/ocaml/tactics/statefulProofEngine.ml @@ -183,7 +183,7 @@ class ['a] status let old_internal_status = self#internal_status in let (new_proof, new_goals) = try - tactic (_proof, self#active_goal) + ProofEngineTypes.apply_tactic tactic (_proof, self#active_goal) with exn -> raise (Tactic_failure exn) in _proof <- new_proof; diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index f9c7feae7..c8217e786 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -75,10 +75,10 @@ match list_of_must with if let time = Unix.gettimeofday() in (try - ignore + ignore(ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac ~term:(MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri)) + (MQueryMisc.cic_textual_parser_uri_of_string uri))) status); let time1 = Unix.gettimeofday() in prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) ); @@ -179,9 +179,9 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st try (m, (prerr_endline ("STO APPLICANDO " ^ uri); - (PrimitiveTactics.apply_tac + (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac ~term:(MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri)) + (MQueryMisc.cic_textual_parser_uri_of_string uri))) status)))::tl' (* with ProofEngineTypes.Fail _ -> tl' *) (* patch to cover CSC's exportation bug *) diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 8d4eb891e..5ea64913d 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -42,7 +42,10 @@ let warn s = (* not a tactical, but it's used only here (?) *) -let id_tac (proof,goal) = (proof,[goal]) +let id_tac = + let tac (proof,goal) = (proof,[goal]) + in + mk_tactic tac (** @@ -54,13 +57,14 @@ let id_tac (proof,goal) = (proof,[goal]) Galla: is this exactly Coq's "First"? *) -let rec try_tactics ~(tactics: (string * tactic) list) status = +let try_tactics ~tactics = + let rec try_tactics ~(tactics: (string * tactic) list) status = warn "in Tacticals.try_tactics"; match tactics with | (descr, tac)::tactics -> warn ("Tacticals.try_tactics IS TRYING " ^ descr); (try - let res = tac status in + let res = apply_tactic tac status in warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!"); res with @@ -76,30 +80,35 @@ let rec try_tactics ~(tactics: (string * tactic) list) status = | _ -> raise e (* [e] must not be caught ; let's re-raise it *) ) | [] -> raise (Fail "try_tactics: no tactics left") + in + mk_tactic (try_tactics ~tactics) - -let thens ~start ~continuations status = - let (proof,new_goals) = start status in +let thens ~start ~continuations = + let thens ~start ~continuations status = + let (proof,new_goals) = apply_tactic start status in try List.fold_left2 (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic (proof,goal) in + let (proof',new_goals') = apply_tactic tactic (proof,goal) in (proof',goals@new_goals') ) (proof,[]) new_goals continuations with Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + in + mk_tactic (thens ~start ~continuations ) - -let then_ ~start ~continuation status = - let (proof,new_goals) = start status in +let then_ ~start ~continuation = + let then_ ~start ~continuation status = + let (proof,new_goals) = apply_tactic start status in List.fold_left (fun (proof,goals) goal -> - let (proof',new_goals') = continuation (proof,goal) in + let (proof',new_goals') = apply_tactic continuation (proof,goal) in (proof',goals@new_goals') ) (proof,[]) new_goals - + in + mk_tactic (then_ ~start ~continuation) (* Galla *) (* si suppone che tutte le tattiche sollevino solamente Fail? *) @@ -111,9 +120,10 @@ let then_ ~start ~continuation status = (* When generates more than one goal, you have a tree of application on the tactic, repeat_tactic works in depth on this tree *) -let rec repeat_tactic ~tactic status = +let repeat_tactic ~tactic = + let rec repeat_tactic ~tactic status = warn "in repeat_tactic"; - try let (proof, goallist) = tactic status in + try let (proof, goallist) = apply_tactic tactic status in let rec step proof goallist = match goallist with [] -> (proof, []) @@ -126,25 +136,29 @@ let rec repeat_tactic ~tactic status = with (Fail _) as e -> warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - id_tac status + apply_tactic id_tac status + in + mk_tactic (repeat_tactic ~tactic) ;; (* This tries to apply tactic n times *) - -let rec do_tactic ~n ~tactic status = +let do_tactic ~n ~tactic = + let rec do_tactic ~n ~tactic status = warn "in do_tactic"; try let (proof, goallist) = - if (n>0) then tactic status - else id_tac status in -(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *) + if (n>0) then apply_tactic tactic status + else apply_tactic id_tac status in +(* else (proof, []) in *) +(* perche' non va bene questo? stessa questione di ##### ? *) let rec step proof goallist = match goallist with [] -> (proof, []) | head::tail -> - let (proof', goallist') = do_tactic ~n:(n-1) ~tactic (proof, head) in + let (proof', goallist') = + do_tactic ~n:(n-1) ~tactic (proof, head) in let (proof'', goallist'') = step proof' tail in proof'', goallist'@goallist'' in @@ -152,48 +166,57 @@ let rec do_tactic ~n ~tactic status = with (Fail _) as e -> warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - id_tac status + apply_tactic id_tac status + in + mk_tactic (do_tactic ~n ~tactic) ;; (* This applies tactic and catches its possible failure *) - -let rec try_tactic ~tactic status = +let try_tactic ~tactic = + let rec try_tactic ~tactic status = warn "in Tacticals.try_tactic"; try - tactic status + apply_tactic tactic status with (Fail _) as e -> warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); - id_tac status + apply_tactic id_tac status + in + mk_tactic (try_tactic ~tactic) ;; (* This tries tactics until one of them doesn't _solve_ the goal *) (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) - -let rec solve_tactics ~(tactics: (string * tactic) list) status = +let solve_tactics ~tactics = + let rec solve_tactics ~(tactics: (string * tactic) list) status = warn "in Tacticals.solve_tactics"; match tactics with | (descr, currenttactic)::moretactics -> warn ("Tacticals.solve_tactics is trying " ^ descr); (try - let (proof, goallist) = currenttactic status in + let (proof, goallist) = apply_tactic currenttactic status in match goallist with - [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!"); -(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *) -(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) + [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ + " solved the goal!!!"); +(* questo significa che non ci sono piu' goal, o che current_tactic non ne + ha aperti di nuovi? (la 2a!) ##### + nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) (proof, goallist) | _ -> warn ("Tacticals.solve_tactics: try the next tactic"); solve_tactics ~tactics:(moretactics) status with (Fail _) as e -> - warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e); + warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ + Printexc.to_string e); solve_tactics ~tactics status ) | [] -> raise (Fail "solve_tactics cannot solve the goal"); - id_tac status + apply_tactic id_tac status + in + mk_tactic (solve_tactics ~tactics) ;; diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index daf461c5b..0566564dc 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -56,6 +56,8 @@ let search_theorems_in_context status = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in + let module PET = ProofEngineTypes in + let module PT = PrimitiveTactics in prerr_endline "Entro in search_context"; let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in @@ -64,9 +66,9 @@ let search_theorems_in_context status = | hd::tl -> let res = try - Some (PrimitiveTactics.apply_tac status ~term:(C.Rel n)) + Some (PET.apply_tactic (PT.apply_tac ~term:(C.Rel n)) status ) with - ProofEngineTypes.Fail _ -> None in + PET.Fail _ -> None in (match res with Some res -> res::(find (n+1) tl) | None -> find (n+1) tl) @@ -147,17 +149,23 @@ prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist)); | None -> proof ;; -let auto_tac mqi_handle (proof,goal) = +let auto_tac mqi_handle = + let module PET = ProofEngineTypes in + let auto_tac mqi_handle (proof,goal) = prerr_endline "Entro in Auto"; try let proof = auto_tac_aux mqi_handle depth proof goal in -prerr_endline "AUTO_TAC HA FINITO"; - (proof,[]) + prerr_endline "AUTO_TAC HA FINITO"; + (proof,[]) with | MaxDepth -> assert false (* this should happens only if depth is 0 above *) | NotApplicableTheorem -> prerr_endline("No applicable theorem"); - raise (ProofEngineTypes.Fail "No Applicable theorem");; + raise (ProofEngineTypes.Fail "No Applicable theorem") + in + PET.mk_tactic (auto_tac mqi_handle) +;; + *) (**** ESPERIMENTO ************************) @@ -211,7 +219,8 @@ let rec auto_new mqi_handle = function ;; -let auto_tac mqi_handle (proof,goal) = +let auto_tac mqi_handle = + let auto_tac mqi_handle (proof,goal) = prerr_endline "Entro in Auto"; try let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in @@ -220,17 +229,23 @@ prerr_endline "AUTO_TAC HA FINITO"; with | NoOtherChoices -> prerr_endline("Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem");; + raise (ProofEngineTypes.Fail "No Applicable theorem") + in + ProofEngineTypes.mk_tactic (auto_tac mqi_handle) +;; (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una funzione di callback che restituisce la (sola) hyp da applicare *) -let assumption_tac status = +let assumption_tac = + let module PET = ProofEngineTypes in + let assumption_tac status = let (proof, goal) = status in let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in + let module PT = PrimitiveTactics in let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function @@ -245,8 +260,10 @@ let assumption_tac status = (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n | _ -> find (n+1) tl ) - | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption") - in PrimitiveTactics.apply_tac status ~term:(C.Rel (find 1 context)) + | [] -> raise (PET.Fail "Assumption: No such assumption") + in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status + in + PET.mk_tactic assumption_tac ;; (* ANCORA DA DEBUGGARE *) @@ -257,42 +274,46 @@ exception AllSelectedTermsMustBeConvertible;; e li aggiunga nel context, poi si conta la lunghezza di questo nuovo contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) -let generalize_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) - terms status -= - let (proof, goal) = status in - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let typ = - match terms with - [] -> assert false - | he::tl -> - (* We need to check that all the convertibility of all the terms *) - List.iter - (function t -> - if not (CicReduction.are_convertible context he t) then - raise AllSelectedTermsMustBeConvertible - ) tl ; - (CicTypeChecker.type_of_aux' metasenv context he) - in - T.thens - ~start: - (P.cut_tac - (C.Prod( - (mk_fresh_name_callback metasenv context C.Anonymous typ), - typ, - (ProofEngineReduction.replace_lifting_csc 1 - ~equality:(==) - ~what:terms - ~with_what:(List.map (function _ -> C.Rel 1) terms) - ~where:ty) - ))) - ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] - status +let generalize_tac + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms + = + let module PET = ProofEngineTypes in + let generalize_tac mk_fresh_name_callback terms status = + let (proof, goal) = status in + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let typ = + match terms with + [] -> assert false + | he::tl -> + (* We need to check that all the convertibility of all the terms *) + List.iter + (function t -> + if not (CicReduction.are_convertible context he t) then + raise AllSelectedTermsMustBeConvertible + ) tl ; + (CicTypeChecker.type_of_aux' metasenv context he) + in + PET.apply_tactic + (T.thens + ~start: + (P.cut_tac + (C.Prod( + (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), + typ, + (ProofEngineReduction.replace_lifting_csc 1 + ~equality:(==) + ~what:terms + ~with_what:(List.map (function _ -> C.Rel 1) terms) + ~where:ty) + ))) + ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]) + status + in + PET.mk_tactic (generalize_tac mk_fresh_name_callback terms) ;; diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index c27e542ff..a4d471e3b 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -32,7 +32,5 @@ val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list -> ProofEngineTypes.tactic -val auto_tac : - MQIConn.handle -> ProofEngineTypes.status -> - ProofEngineTypes.proof * ProofEngineTypes.goal list +val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic